CS205: Building with Artificial Intelligence

The crucial properties of this set of rules are that they are sound and complete. Informally this means that the rules are correct and that no other rules are required. These claims can be made more formal as follows. The proofs for the soundness and completeness of the propositional logic are not themselves proofs in propositional logic ; these are theorems in ZFC used as a metatheory to prove properties of propositional logic.

We define a truth assignment as a function that maps propositional variables to true or false. Informally such a truth assignment can be understood as the description of a possible state of affairs (or possible world) where certain statements are true and others are not. The semantics of formulas can then be formalized by defining for which "state of affairs" they are considered to be true, which is what is done by the following definition.

• A satisfies the propositional variable P if and only if A(P) = true
• A satisfies ¬φ if and only if A does not satisfy φ
• A satisfies (φ ∧ ψ) if and only if A satisfies both φ and ψ
• A satisfies (φ ∨ ψ) if and only if A satisfies at least one of either φ or ψ
• A satisfies (φ → ψ) if and only if it is not the case that A satisfies φ but not ψ
• A satisfies (φ ↔ ψ) if and only if A satisfies both φ and ψ or satisfies neither one of them

With this definition we can now formalize what it means for a formula φ to be implied by a certain set S of formulas. Informally this is true if in all worlds that are possible given the set of formulas S the formula φ also holds. This leads to the following formal definition: We say that a set S of well-formed formulas semantically entails (or implies) a certain well-formed formula φ if all truth assignments that satisfy all the formulas in S also satisfy φ.

Finally we define syntactical entailment such that φ is syntactically entailed by S if and only if we can derive it with the inference rules that were presented above in a finite number of steps. This allows us to formulate exactly what it means for the set of inference rules to be sound and complete:

Soundness: If the set of well-formed formulas S syntactically entails the well-formed formula φ then S semantically entails φ.

Completeness: If the set of well-formed formulas S semantically entails the well-formed formula φ then S syntactically entails φ.

For the above set of rules this is indeed the case.

Sketch of a soundness proof

Notational conventions: Let G be a variable ranging over sets of sentences. Let A, B and C range over sentences. For "G syntactically entails A" we write "G proves A". For "G semantically entails A" we write "G implies A".

We want to show: (A)(G) (if G proves A, then G implies A).

We note that "G proves A" has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form "If G proves A, then ...". So our proof proceeds by induction.

Notice that Basis Step II can be omitted for natural deduction systems because they have no axioms. When used, Step II involves showing that each of the axioms is a (semantic) logical truth.

The Basis steps demonstrate that the simplest provable sentences from G are also implied by G, for any G. (The proof is simple, since the semantic fact that a set implies any of its members, is also trivial.) The Inductive step will systematically cover all the further sentences that might be provable - by considering each case where we might reach a logical conclusion using an inference rule - and shows that if a new sentence is provable, it is also logically implied. (For example, we might have a rule telling us that from "A" we can derive "A or B". In III.a We assume that if A is provable it is implied. We also know that if A is provable then "A or B" is provable. We have to show that then "A or B" too is implied. We do so by appeal to the semantic definition and the assumption we just made. A is provable from G, we assume. So it is also implied by G. So any semantic valuation making all of G true makes A true. But any valuation making A true makes "A or B" true, by the defined semantics for "or". So any valuation which makes all of G true makes "A or B" true. So "A or B" is implied.) Generally, the Inductive step will consist of a lengthy but simple case-by-case analysis of all the rules of inference, showing that each "preserves" semantic implication.

By the definition of provability, there are no sentences provable other than by being a member of G, an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.

Sketch of completeness proof

(This is usually the much harder direction of proof)

We adopt the same notational conventions as above.

We want to show: If G implies A, then G proves A. We proceed by contraposition: We show instead that if G does not prove A then G does not imply A. If we show that there is a model where A does not hold despite G being true, then obviously G does not imply A. The idea is to build such a model out of our very assumption that G does not prove A.

1. G does not prove A. (Assumption)
2. If G does not prove A, then we can construct an (infinite) maximal set, G^∗, which is a superset of G and which also does not prove A.
   1. Place an ordering (with order type ω) on all the sentences in the language (e.g., shortest first, and equally long ones in extended alphabetical ordering), and number them (E₁, E₂, ...)
   2. Define a series G_n of sets (G₀, G₁, ...) inductively:
      1. $G_{0}=G$
      2. If $G_{k}\cup \{E_{k+1}\}$ proves A, then $G_{k+1}=G_{k}$
      3. If $G_{k}\cup \{E_{k+1}\}$ does not prove A, then $G_{k+1}=G_{k}\cup \{E_{k+1}\}$
   3. Define G^∗ as the union of all the G_n. (That is, G^∗ is the set of all the sentences that are in any G_n).
   4. It can be easily shown that
      1. G^∗ contains (is a superset of) G (by (b.i));
      2. G^∗ does not prove A (because the proof would contain only finitely many sentences and when the last of them is introduced in some G_n, that G_n would prove A contrary to the definition of G_n); and
      3. G^∗ is a maximal set with respect to A: If any more sentences whatever were added to G∗, it would prove A. (Because if it were possible to add any more sentences, they should have been added when they were encountered during the construction of the G_n, again by definition)
3. If G^∗ is a maximal set with respect to A, then it is truth-like. This means that it contains C if and only if it does not contain ¬C; If it contains C and contains "If C then B" then it also contains B; and so forth. In order to show this, one has to show the axiomatic system is strong enough for the following:
   • For any formulas C and D, if it proves both C and ¬C, then it proves D. From this it follows, that a maximal set with respect to A cannot prove both C and ¬C, as otherwise it would prove A.
   • For any formulas C and D, if it proves both C→D and ¬C→D, then it proves D. This is used, together with the deduction theorem, to show that for any formula, either it or its negation is in G^∗: Let B be a formula not in G^∗; then G^∗ with the addition of B proves A. Thus from the deduction theorem it follows that G^∗ proves B→A. But suppose ¬B were also not in G^∗, then by the same logic G^∗ also proves ¬B→A; but then G^∗ proves A, which we have already shown to be false.
   • For any formulas C and D, if it proves C and D, then it proves C→D.
   • For any formulas C and D, if it proves C and ¬D, then it proves ¬(C→D).
   • For any formulas C and D, if it proves ¬C, then it proves C→D.
     If additional logical operation (such as conjunction and/or disjunction) are part of the vocabulary as well, then there are additional requirement on the axiomatic system (e.g. that if it proves C and D, it would also prove their conjunction).
4. G^∗ is truth-like there is a G^∗-Canonical valuation of the language: one that makes every sentence in G^∗ true and everything outside G^∗ false while still obeying the laws of semantic composition in the language. The requirement that it is truth-like is needed to guarantee that the laws of semantic composition in the language will be satisfied by this truth assignment.
5. A G^∗-canonical valuation will make our original set G all true, and make A false.
6. If there is a valuation on which G are true and A is false, then G does not (semantically) imply A.

Thus every system that has modus ponens as an inference rule, and proves the following theorems (including substitutions thereof) is complete:

• $p\to (\neg p\to q)$
• $(p\to q)\to ((\neg p\to q)\to q)$
• $p\to (q\to (p\to q))$
• $p\to (\neg q\to \neg (p\to q))$
• $\neg p\to (p\to q)$
• $p\to p$
• $p\to (q\to p)$
• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$

Example

As an example, it can be shown that as any other tautology, the three axioms of the classical propositional calculus system described earlier can be proven in any system that satisfies the above, namely that has modus ponens as an inference rule, and proves the above eight theorems (including substitutions thereof). Out of the eight theorems, the last two are two of the three axioms; the third axiom, $(\neg q\to \neg p)\to (p\to q)$, can be proven as well, as we now show.

For the proof we may use the hypothetical syllogism theorem (in the form relevant for this axiomatic system), since it only relies on the two axioms that are already in the above set of eight theorems. The proof then is as follows:

1. $q\to (p\to q)$       (instance of the 7th theorem)
2. $(q\to (p\to q))\to ((\neg q\to \neg p)\to (q\to (p\to q)))$       (instance of the 7th theorem)
3. $(\neg q\to \neg p)\to (q\to (p\to q))$       (from (1) and (2) by modus ponens)
4. $(\neg p\to (p\to q))\to ((\neg q\to \neg p)\to (\neg q\to (p\to q)))$       (instance of the hypothetical syllogism theorem)
5. $(\neg p\to (p\to q))$      (instance of the 5th theorem)
6. $(\neg q\to \neg p)\to (\neg q\to (p\to q))$      (from (5) and (4) by modus ponens)
7. $(q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))$      (instance of the 2nd theorem)
8. $((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))\to ((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))$     (instance of the 7th theorem)
9. $(\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))$       (from (7) and (8) by modus ponens)
10.  $((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))\to$
    $(((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))))$       (instance of the 8th theorem)
    
11. $((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))$       (from (9) and (10) by modus ponens)
12. $(\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))$       (from (3) and (11) by modus ponens)
13. $((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))\to (((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q)))$       (instance of the 8th theorem)
14. $((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q))$      (from (12) and (13) by modus ponens)
15. $(\neg q\to \neg p)\to (p\to q)$      (from (6) and (14) by modus ponens)

Verifying completeness for the classical propositional calculus system

We now verify that the classical propositional calculus system described earlier can indeed prove the required eight theorems mentioned above. We use several lemmas proven here:

• $p\to (\neg p\to q)$ - proof:

1. $p\to (\neg q\to p)$       (instance of (A1))
2. $(\neg q\to p)\to (\neg p\to \neg \neg q)$       (instance of (TR1))
3. $p\to (\neg p\to \neg \neg q)$      (from (1) and (2) using the hypothetical syllogism metatheorem)
4. $\neg \neg q\to q$       (instance of (DN1))
5. $(\neg \neg q\to q)\to ((\neg p\to \neg \neg q)\to (\neg p\to q))$      (instance of (HS1))
6. $(\neg p\to \neg \neg q)\to (\neg p\to q)$       (from (4) and (5) using modus ponens)
7. $p\to (\neg p\to q)$      (from (3) and (6) using the hypothetical syllogism metatheorem)

• $(p\to q)\to ((\neg p\to q)\to q)$ - proof:

1. $(p\to q)\to ((\neg q\to p)\to (\neg q\to q))$       (instance of (HS1))
2. $(\neg q\to q)\to q$       (instance of (L3))
3. $((\neg q\to q)\to q)\to (((\neg q\to p)\to (\neg q\to q))\to ((\neg q\to p)\to q))$       (instance of (HS1))
4. $((\neg q\to p)\to (\neg q\to q))\to ((\neg q\to p)\to q)$      (from (2) and (3) by modus ponens)
5. $(p\to q)\to ((\neg q\to p)\to q)$      (from (1) and (4) using the hypothetical syllogism metatheorem)
6. $(\neg p\to q)\to (\neg q\to p)$     (instance of (TR2))
7. $((\neg p\to q)\to (\neg q\to p))\to (((\neg q\to p)\to q)\to ((\neg p\to q)\to q))$       (instance of (HS2))
8.  $((\neg q\to p)\to q)\to ((\neg p\to q)\to q)$       (from (6) and (7) using modus ponens)
9. $(p\to q)\to ((\neg p\to q)\to q)$       (from (5) and (8) using the hypothetical syllogism metatheorem)

• $p\to (q\to (p\to q))$ - proof:

1. $q\to (p\to q)$      (instance of (A1))
2. $(q\to (p\to q))\to (p\to (q\to (p\to q)))$       (instance of (A1))
3. $p\to (q\to (p\to q))$      (from (1) and (2) using modus ponens)

• $p\to (\neg q\to \neg (p\to q))$ - proof:

1. $p\to ((p\to q)\to q)$       (instance of (L1))
2. $((p\to q)\to q)\to (\neg q\to \neg (p\to q))$       (instance of (TR1))
3. $p\to (\neg q\to \neg (p\to q))$      (from (1) and (2) using the hypothetical syllogism metatheorem)

• $\neg p\to (p\to q)$ - proof:

1. $\neg p\to (\neg q\to \neg p)$       (instance of (A1))
2. $(\neg q\to \neg p)\to (p\to q)$       (instance of (A3))
3. $\neg p\to (p\to q)$       (from (1) and (2) using the hypothetical syllogism metatheorem)

• $p\to p$ - proof given in the proof example above
• $p\to (q\to p)$ - axiom (A1)
• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$ - axiom (A2)

Another outline for a completeness proof