MAT 02. Formální systém 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
• (x₁ = y₁ → (...(x_n = y_n → f(x₁, ..., x_n) = f(y₁, ..., y_n))...))
• (x₁ = y₁ → (...(x_n = y_n → (p(x₁, ..., x_n) → p(y₁, ..., y_n)))...))

modus ponens, z formulí φ, φ → ψ se odvodí ψ

generalizace, pro libovolnou proměnnou x z formule φ se odvodí formule (∀xφ)

posloupnost formulí, které jsou buď axiomy nebo jsou odvozeny z předchozích formulí

⊢ φ, existuje důkaz, jehož poslední formule je dokazovaná formule

T ⊢ φ, existuje důkaz z předpokladů

• Q₁ x₁ ... Q_n x_n B, kde
• 1. n ≥ 0, Q_i je ∃ nebo ∀
• 2. x_i jsou navzájem různé proměnné
• 3. B je otevřená formule (neobsahuje kvantifikátory)

• 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

Qxφ, vynechání Qx, pokud se x nevyskytuje v φ

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'

převedení na (A → B) ∧ (B → A)

přesunu negace tak, aby byly těsně před atomickými formulemi (proměnnými, funkčními symboly nebo predikáty)

• 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 ∨ B_y[x])

množina formulí T jazyka L

T je sporná, pokud pro každou formuli φ jazyka L platí T ⊢ φ (T dokazuje φ), jinak je bezesporná

• model M teorie T je realizace jazyka L taková, že M ⊨ φ pro každou formuli φ ∈ T
• M ⊨ T
• ∃M: M ⊨ T ⇔ T je bezesporná

formule φ je důsledek teorie T, pokud pro každý model M teorie T platí M ⊨ T, pak T ⊨ φ

teorie T je úplná, pokud pro každou formuli φ jazyka L platí T ⊨ φ nebo T ⊨ ¬φ (ale ne zároveň)

teorie T má nějaký model, právě když každá její konečná podmnožina Q ⊆ T má model