MAT 02. Formální systém predikátové logiky

Card Set Information

Author:
hrbi
ID:
222362
Filename:
MAT 02. Formální systém predikátové logiky
Updated:
2013-06-08 08:00:30
Tags:
mat
Folders:

Description:
mszz 2013
Show Answers:

Home > Flashcards > Print Preview

The flashcards below were created by user hrbi on FreezingBlue Flashcards. What would you like to do?


  1. Axiomy predikátové logiky
    • výrokové axiomy:
    • φ → (φ → ψ)
    • (φ → (ψ → η)) → ((φ → ψ) → (φ → η))
    • (¬ψ → ¬φ) → (φ → ψ)
    • axiom kvantifikátoru:
    • (∀x(φ → ψ)) → (φ → (∀xψ)), x nemá volný výskyt ve φ
    • axiom substituce:
    • (∀xφ) → φx[t], t je substituovatelný za x do φ
    • ⊢ (∀zφ) → φ, pokud t = x
    • axiomy rovnosti:
    • x = x
    • (x1 = y1 → (...(xn = yn → f(x1, ..., xn) = f(y1, ..., yn))...))
    • (x1 = y1 → (...(xn = yn → (p(x1, ..., xn) → p(y1, ..., yn)))...))
  2. Pravidlo odloučení
    modus ponens, z formulí φ, φ → ψ se odvodí ψ
  3. Pravidlo zobecnění
    generalizace, pro libovolnou proměnnou x z formule φ se odvodí formule (∀xφ)
  4. Důkaz
    posloupnost formulí, které jsou buď axiomy nebo jsou odvozeny z předchozích formulí
  5. Dokazatelná formule
    ⊢ φ, existuje důkaz, jehož poslední formule je dokazovaná formule
  6. Dokazatelná formule z předpokladů
    T ⊢ φ, existuje důkaz z předpokladů
  7. Prenexní tvar formule
    • Q1 x1 ... Qn xn B, kde
    • 1. n ≥ 0, Qi je ∃ nebo ∀
    • 2. xi jsou navzájem různé proměnné
    • 3. B je otevřená formule (neobsahuje kvantifikátory)
  8. Převod na prenexní tvar
    • 1. vyloučení zbytečných kvantifikátorů
    • 2. přejmenování proměnných
    • 3. eliminace spojky ⇔
    • 4. přesun negace dovnitř
    • 5. přesun kvantifikátorů doleva
  9. Vyloučení zbytečných kvantifikátorů
    Qxφ, vynechání Qx, pokud se x nevyskytuje v φ
  10. Přejmenování proměnných
    najdu QxA nejvíce vlevo takovou, že A obsahuje volné x, pokud je x ještě jinde ve výchozí formuli, nahradím za Qx'A'
  11. Eliminace spojky ⇔
    převedení na (A → B) ∧ (B → A)
  12. Přesun negace dovnitř
    přesunu negace tak, aby byly těsně před atomickými formulemi (proměnnými, funkčními symboly nebo predikáty)
  13. Přesun kvantifikátorů doleva
    • pro podformuli B, ve které není x nahrazujeme:
    • (QxA) ∨ B ... Qx(A ∨ B)
    • (QxA) ∧ B ... Qx(A ∧ B)
    • (QxA) → B ... Q'x(A → B)
    • B → (QxA) ... Qx(B → A)
    • (QxA) ∨ (QxB) ... Qx(A ∨ By[x])
  14. Teorie
    množina formulí T jazyka L
  15. Spornost
    T je sporná, pokud pro každou formuli φ jazyka L platí T ⊢ φ (T dokazuje φ), jinak je bezesporná
  16. Model teorie
    • model M teorie T je realizace jazyka L taková, že M ⊨ φ pro každou formuli φ ∈ T
    • M ⊨ T
    • ∃M: M ⊨ T ⇔ T je bezesporná
  17. Důsledek teorie
    formule φ je důsledek teorie T, pokud pro každý model M teorie T platí M ⊨ T, pak T ⊨ φ
  18. Úplnost teorie
    teorie T je úplná, pokud pro každou formuli φ jazyka L platí T ⊨ φ nebo T ⊨ ¬φ (ale ne zároveň)
  19. Kompaktnost
    teorie T má nějaký model, právě když každá její konečná podmnožina Q ⊆ T má model

What would you like to do?

Home > Flashcards > Print Preview