Prop Logic Wrap-up Notes

There is a close connection between provability and logical entailment. In fact, they are equivalent. A set of sentences Δ logically entails a sentence φ if and only if φ is provable from Δ.

Soundness Theorem: If φ is provable from Δ, then Δ logically entails φ.

Completeness Theorem: If Δ logically entails φ, then φ is provable from Δ.

The concept of provability is important because it suggests how we can automate the determination of logical entailment. Starting from a set of premises Δ, we enumerate conclusions from this set. If a sentence φ appears, then it is provable from Δ and is, therefore, a logical consequence. If the negation of φ appears, then ¬φ is a logical consequence of Δ and φ is not logically entailed (unless Δ is inconsistent). Note that it is possible that neither φ nor ¬φ will appear.

Standard Axiom Schemata for Propositional Logic

Standard Axiom Schemata for Propositional Logic

(II): φ ⇒ (ψ ⇒ φ)

(ID): (φ ⇒ (ψ ⇒ χ)) ⇒ ((φ ⇒ ψ) ⇒ (φ ⇒ χ))

(CR): (¬φ ⇒ ψ) ⇒ ((¬φ ⇒ ¬ψ) ⇒ φ)

(EQ):

(φ ⇔ ψ) ⇒ (φ ⇒ ψ)

(φ ⇔ ψ) ⇒ (ψ ⇒ φ)

(φ ⇒ ψ) ⇒ ((ψ ⇒ φ) ⇒ (φ ⇔ ψ))

(OQ):

(φ ⇐ ψ) ⇔ (ψ ⇒ φ)

(φ ∨ ψ) ⇔ (¬φ ⇒ ψ)

(φ ∧ ψ) ⇔ ¬(¬φ ∨ ¬ψ)

(II), (ID), and (CR) form the Mendelson Axiom Schemata for Propositional Logic