meta-theorems-of-predicate-logic.wiki (1490B)
1 %template math 2 == Meta-Theorems of Predicate Logic == 3 Entailment syntactically (⊢) and semantically (⊨) 4 * Γ ⊢ ψ: there is natural deduction derivation of ψ that only uses premises in Γ 5 * Γ ⊨ ψ: for all M and l, if M ⊨l Φ for every Φ ∈ Γ, then M ⊨ ψ 6 7 Soundness and completeness: 8 * Γ ⊢ Φ ⇔ Γ ⊨ Φ 9 * for all formulas Φ, every set Γ of formulas 10 * soundness (correctness): left-to-right (⇒) 11 * completeness: right-to-left (⇐) 12 13 soundness theorem: 14 * Γ ⊢ Φ ⇒ Γ ⊨ Φ 15 * if there is natural deduction derivation of Φ from Γ, then there's no model M in which all formulas of Γ are true, but Φ is false 16 * "correct" means not possible to derive false conclusion Φ from true premises Γ 17 * prove by induction on derivation lengths 18 19 completeness theorem: 20 * Γ ⊨ Φ ⇒ Γ ⊢ Φ 21 * derivations are strong enough to derive all valid semantic entailment statements 22 * "complete" means more derivation rules are not necessary 23 * proof is non-trivial 24 25 consistency and syntactical consistency 26 * Γ is consistent ⇔ Γ is syntactically consistent 27 * Γ has a model ⇔ there is no derivation of ⊥ from Γ 28 29 semantical consistency: 30 * set Γ of formulas is consistent if there is model M and environment l such that M ⊨ Φ for all Φ ∈ Γ 31 32 syntactical consistency: 33 * set Γ of formulas is syntactically consistent if Γ ⊬ ⊥ 34 35 compactness theorem: 36 * Γ is consistent ⇔ every finite subset Γ₀ ⊆ Γ si consistent 37