Propositional Calculus Notes PDF

Propositional Calculus Declaration This note was prepared based on the book Logic for Computer Science by A. Singha. To keep the matter simple, we plan to work with a subset of connectives. We choose the subset {¬, →}. We may introduce other connectives by way o...

Propositional Calculus Declaration This note was prepared based on the book Logic for Computer Science by A. Singha. To keep the matter simple, we plan to work with a subset of connectives. We choose the subset {¬, →}. We may introduce other connectives by way of definitions later. We thus choose our language for propositional calculus (PC, for short) as the fragment of PROP having all propositional variables and the connectives ¬ and →. In PC, right now, we do not have the propositional constants ⊤ and ⊥; and we do not have the connectives ∧, ∨, and ↔. Again, we use the grammar of PROP appropriate for this fragment. We also use the precedence rules to abbreviate our PC-propositions with the usual conventions of omitting brackets and subscripts in the propositional variables. Moreover, we use capital letters A, B, C,... as generic symbols for propositions. The axiom schemes of PC are: (A1) A → (B → A) (A2) (A → (B → C)) → ((A → B) → (A → C)) (A3) (¬A → ¬B) → ((¬A → B) → A) An axiom is any instance of an axiom scheme, obtained by replacing throughout the letters A, B, C by propositions. For example, p → (q → p) is an axiom as it is obtained from A1 by replacing A by p and B by q throughout. We thus refer to p → (q → p) as A1. Similarly, (p → q) → ((q → p) → (p → q)) is also A1. In addition to the axioms, PC has a rule of inference; it is as follows: Modus Ponens (MP): If A and A → B are both propositions (assumptions), then B can be inferred. Formally: A, A → B B The inference rule Modus Ponens (MP) is an incarnation of the valid consequence Modus Ponens: {A, A → B} ⊢ B. 1 Since in an axiomatic system there is no concept of truth or falsity, we simply write the consequence as a fraction: A, A → B. B You may read the rule MP as: From A and A → B, derive B. This is again a rule scheme in the sense that any instance of this scheme is a rule. That is, if you have already derived the propositions p and p → q, then the rule allows you to derive q. The rule allows you to derive q. Deriving q → r from p → q and (p → q) → (q → r) is an application of the rule MP. Informally, the word ‘derive’ signals deductions; formally, it just allows us to write the propositions one after another. The axiomatic system PC has all the propositions having only the connectives ¬ and →. PC has the axiom schemes A1, A2, A3, and the inference rule MP. A proof in PC is defined to be a finite sequence of propositions, where each one is either an axiom or is obtained (derived) from two earlier propositions by an application of MP. The last proposition of a proof is called a theorem of PC; the proof is said to prove the theorem. The fact that “A is a theorem in PC” is written as ⊢PC A. We also read ⊢PC A as “A is provable in PC.” If no other axiomatic system is in sight, we may abbreviate ⊢PC to ⊢ without the subscript PC. In that case, the phrases ‘proof in PC’, ‘PC-proof’, and ‘proof’ mean the same thing. The symbol ⊢ will have the least precedence. For example, ⊢ p → p is a shorthand for writing ⊢ (p → p); and ⊢ ¬p → (p → q) abbreviates ⊢ (¬p → (p → q)). Example 0.1. The following is a proof of ⊢PC r → (p → (q → p)): 1. (p → (q → p)) → (r → (p → (q → p))) A1, A := p → (q → p), B := r 2. p → (q → p) A1, A := p, B := q 3. r → (p → (q → p)) 1, 2, MP Example 0.2. Show that p → p. 1. p → ((q → p) → p) A1 2. (p → ((q → p) → p)) → ((p → (q → p)) → (p → p)) A2 3. (p → (q → p)) → (p → p) 1, 2, MP 4. p → (q → p) A1 5. p → p 3, 4, MP In an axiomatic system such as PC, the notion of a proof is effective, i.e., if it is claimed that some object is a proof of a theorem, then it can be checked whether the claim is 2 correct or not in an algorithmic manner. However, construction of a proof may not be effective; there may or may not be an algorithm to construct a proof of a given theorem. Of course, proofs can be generated mechanically by following the specified rules. The problem comes when a proof is targeted towards proving a given theorem. We will see by way of examples how to do it. We may have to rely on our intuition in constructing proofs. Example 0.3. Show that q → (p → p). Here is the proof: 1. p → ((q → p) → p) 2.... 3.... 4.... 5. p → p (Example 0.2) 6. (p → p) → (q → (p → p)) (A1) 7. q → (p → p) (5, 6, MP) Remark: Just like axiom schemes and inference rules, theorems are theorem schemes. Once you have a proof of p → p, you can have a proof of (p → q) → (p → q). It is simple; just replace p by p → q throughout the proof. Thus, known theorems can be used in proving new theorems. We will mention ‘Th’ in the rightmost column of a proof, when we use an already proved theorem. The proof in Example 0.3 can be rewritten as: 1. p → p (Th) 2. (p → p) → (q → (p → p)) (Axiom A1) 3. q → (p → p) (1, 2, MP) Exercise 0.1. Show that (¬q → q) → q. Let Σ be a set of propositions, and let w be any proposition. A proof of the consequence Σ! ⊢ w in PC is defined to be a finite sequence of propositions where: Each proposition is either an axiom, a proposition in Σ, or is obtained from earlier two propositions by an application of MP (Modus Ponens); and The last proposition in the sequence is w. 3 In the consequence Σ ⊢ w, each proposition from Σ is called a premise, and w is called the conclusion. We write Σ ⊢P C w to say that there exists a proof of the consequence Σ ⊢ w in PC. This fact is also expressed as “the consequence Σ! ⊢ w is provable in PC.” Informally, a proof of Σ! ⊢ w is also called a proof of Σ ⊢P C w. When Σ = {w1 ,... , wn }, a finite set, we write Σ ⊢P C w as: w1 ,... , wn ⊢P C w. As earlier, we will write Σ ⊢ w if no confusion arises. We observe that when Σ = ∅, Σ ⊢ w boils down to ⊢ w. Moreover, it is not mandatory that a proof uses all axioms; similarly, a proof of a consequence need not use all given premises. Proofs of consequences are written in three columns, like proofs of theorems. We mention the letter ‘P’ in the documentation to indicate that the proposition used in that line of the proof is a premise. Example 0.4. Construct a proof to show that ¬p, p ⊢ q. Here is the proof: 1. p (P) 2. p → (¬q → p) (A1) 3. ¬q → p (1, 2, MP) 4. ¬p (P) 5. ¬p → (¬q → ¬p) (A1) 6. ¬q → ¬p (4, 5, MP) 7. (¬q → ¬p) → ((¬q → p) → q) (A3) 8. (¬q → p) → q (6, 7, MP) 9. q (3, 8, MP) Example 0.5. Show that p → q, q → r ⊢ p → r. Here is the proof: 1. q → r (P) 2. p → (q → r) (1, A1) 3. (p → (q → r)) → ((p → q) → (p → r)) (A2) 4. (p → q) → (p → r) (2, 3, MP) 4  5. p → q (P) 6. p → r (4, 5, MP) Derived Rules of Inference: Theorems can be used as new axioms. In the same way, already derived consequences can be used as new inference rules. The reason: proof of such a consequence can be duplicated with necessary replacements. Such new inference rules are referred to as derived rules of inference. The consequence {p → q, q → r} ⊢ p → r in the above example is rewritten as the derived rule of Hypothetical Syllogism: A→B B→C (HS) A→C Example 0.6. Show that ¬q → ¬p ⊢ p → q. We use the derived rule HS in the following proof: 1. ¬q → ¬p (P) 2. (¬q → ¬p) → ((¬q → p) → q) (A3) 3. (¬q → p) → q (1, 2, MP) 4. p → (¬q → p) (A1) 5. p → q (4, 3, HS) Example 0.7. Show that ⊢ ¬¬p → p. 1. ¬¬p → (¬p → ¬¬p) (A1) 2. (¬p → ¬¬p) → ((¬p → ¬p) → p) (A3) 3. ¬¬p → ((¬p → ¬p) → p) (1, 2, HS) 4. (¬¬p → ((¬p → ¬p) → p)) → ((¬¬p → (¬p → ¬p)) → (¬¬p → p)) (A3) 5. (¬¬p → (¬p → ¬p)) → (¬¬p → p) (3, 4, MP) 6. ¬p → ¬p (Th) 7. (¬p → ¬p) → (¬¬p → (¬p → ¬p)) (A1) 8. ¬¬p → (¬p → ¬p) (6, 7, MP) 9. ¬¬p → p (8, 5, MP) 5 0.1 Exercises Try to construct PC-proofs of the following consequences: 1. p → q, q → r, p ⊢ r 2. ¬q → ¬p, p ⊢ q 3. p → q, ¬q ⊢ ¬p 4. p ⊢ ¬¬p 5. p → (q → r), q ⊢ p → r 6. ⊢ (p → q) → (¬q → ¬p) 1 Metatheorems To prove “if x then y” we assume x and derive y. It is accepted in each branch of mathematics. Since we are questioning the process of reasoning itself, can we accept it in PC? We should rather prove this principle. Theorem 1.1 (DT: Deduction Theorem). Let Σ be a set of propositions, and let p, q be propositions. Then, Σ ⊢ p → q iff Σ ∪ {p} ⊢ q. Proof. Suppose that Σ ⊢ p → q. To show Σ ∪ {p} ⊢ q, take the proof of Σ ⊢ p → q, adjoin to it the lines (propositions) p, q. It looks like: 1. · · · 2. · · · 3. p → q (Proof of Σ ⊢ p → q) 4. p (P) 5. q (3, 4, MP) This is a proof of Σ ∪ {p} ⊢ q. Conversely, suppose that Σ ∪ {p} ⊢ q; we have a proof of it. We construct a proof of Σ ⊢ p → q by induction on the number of propositions (number of lines) used in the proof of Σ ∪ {p} ⊢ q. 6 Basis step: Suppose that the proof of Σ ∪ {p} ⊢ q has only one proposition. Then this proposition has to be q. Now, why is this a proof of Σ ∪ {p} ⊢ q? There are three possibilities: (a) q is an axiom. (b) q ∈ Σ. (c) q = p. In each case, we show how to get a proof of Σ ⊢ p → q: (a) In this case, our proof is: (a) q (An axiom) (b) q → (p → q) (A1) (c) p → q (1, 2, MP) It is a proof of Σ ⊢ p → q since it uses no proposition other than axioms. (b) In this case, the above proof still works, only the first line would be documented as ‘P’, a premise in Σ, rather than an axiom. (c) Here, q = p. We just repeat the proof given in Example 0.2: (a) · · · (b) · · · (c) p → p (MP) Induction step: Lay out the induction hypothesis: If there exists a proof of Σ ∪ {p} ⊢ q having less than n propositions in it (in the proof), then there exists a proof of Σ ⊢ p → q. Suppose now that we have a proof P of Σ ∪ {p} ⊢ q having n propositions in it. Observe that we have four cases to consider based on what q is. They are: (i) q is an axiom, (ii) q ∈ Σ, (iii) q = p The cases (i)–(iii) are similar to the basis case. 7 (iv) q has been derived by an application of MP in the proof P. In this case, the proof P looks like: 1. · · ·... m. r · · · P :... m + k. r → q... n. q (m, m + k, MP) where m < n, m + k < n, and r is some proposition. The proof segment P1 (lines 1 through m) proves Σ ∪ {p} ⊢ r. The proof segment P2 (lines 1 through m + k) proves Σ ∪ {p} ⊢ r → q. The proofs P1 , P2 have less than n propositions. By the induction hypothesis, correspond- ing to P1 and P2 , there exist proofs P3 and P4 such that: P3 proves Σ ⊢ p → r. P4 proves Σ ⊢ p → (r → q). Suppose that P3 has i propositions and P4 has j propositions. We use P3 and P4 to construct a proof P5 of Σ ⊢ p → q. The proof P5 is constructed by adjoining P4 to P3 , and then adding some more propositions: 1. · · · (P3 begins)... i. p → r (P3 ends) i + 1. · · · (P4 begins) P5 :... i + j. p → (r → q) (P4 ends) i + j + 1. (p → (r → q)) → ((p → r) → (p → q)) (A2) i + j + 2. (p → r) → (p → q) (i + j, i + j + 1, MP) i + j + 3. p → q (i, i + j + 2, MP) Now, P5 is a proof of Σ ⊢ p → q since the premises used in it are either axioms or propositions from Σ. Let Σ be a set of propositions. 8 We say that Σ is inconsistent iff there exists a proposition w such that Σ ⊢ w and Σ ⊢ ¬w. That is, Σ is inconsistent iff there exists a proof, possibly using premises from Σ, where some proposition and its negation both occur. We say that Σ is consistent iff Σ is not inconsistent. In case of consequences, each premise is also a conclusion since it has a one line proof, with the justification that it is a premise. Similarly, any conclusion that has been derived from a set of premises can still be derived if some more premises are added. This is monotonicity. Theorem 1.2 (M: Monotonicity). Let Σ and Γ be sets of propositions, Σ ⊆ Γ, and let w be a proposition. 1. If Σ ⊢ w, then Γ ⊢ w. 2. If Σ is inconsistent, then Γ is inconsistent. Proof. (1) Let Σ ⊢ w. We then have a proof where some (or all) of the premises from Σ are used to have its last line as w. The same proof shows that Γ ⊢ w. (2) If Σ is inconsistent, then there exists a proposition p such that Σ ⊢ p and Σ ⊢ ¬p. By (1), Γ ⊢ p and Γ ⊢ ¬p. Therefore, Γ is inconsistent. Theorem 1.3 (RA: Reductio ad Absurdum). Let Σ be a set of propositions, and let w be a proposition. 1. Σ ⊢ w iff Σ ∪ {¬w} is inconsistent. 2. Σ ⊢ ¬w iff Σ ∪ {w} is inconsistent. Proof. (1) Suppose that Σ ⊢ w. By monotonicity, Σ ∪ {¬w} ⊢ w. With a one-line proof, Σ ∪ {¬w} ⊢ ¬w. Therefore, Σ ∪ {¬w} is inconsistent. Conversely, suppose that Σ ∪ {¬w} is inconsistent. Then there is a proposition, say p, such that Σ ∪ {¬w} ⊢ p and Σ ∪ {¬w} ⊢ ¬p. By the deduction theorem, Σ ⊢ ¬w → p and Σ ⊢ ¬w → ¬p. Suppose P1 is a proof of Σ ⊢ ¬w → ¬p containing m propositions and P2 is a proof of Σ ⊢ ¬w → p containing n propositions. Construct a proof P of Σ ⊢ w as follows: 1. ··· P1 begins... m. ¬w → ¬p P1 ends m + 1. · · · P2 begins P :... m + n. ¬w → p P2 ends m + n + 1. (¬w → ¬p) → ((¬w → p) → w) A3 m + n + 2. (¬w → p) → w m, m + n + 1, MP m + n + 3. w m + n, m + n + 2, MP 9  (2) If Σ ⊢ ¬w, then by monotonicity, Σ ∪ {w} ⊢ ¬w. Also, Σ ∪ {w} ⊢ w, trivially. Hence, Σ ∪ {w} is inconsistent. Conversely, suppose that Σ ∪ {w} is inconsistent. We show that Σ ∪ {¬¬w} is also inconsistent. Now, inconsistency of Σ ∪ {w} implies that there exists a proposition p such that Σ ∪ {w} ⊢ p and Σ ∪ {w} ⊢ ¬p. So, there exist proofs P1 and P2 such that: P1 proves Σ ∪ {w} ⊢ p P2 proves Σ ∪ {w} ⊢ ¬p Observe that Σ ∪ {¬¬w, ¬w} ⊢ ¬¬w and Σ ∪ {¬¬w, ¬w} ⊢ ¬w. That is, Σ ∪ {¬¬w, ¬w} is inconsistent. By (1), we obtain Σ ∪ {¬¬w} ⊢ w. Then there exists a proof P3 such that P3 proves Σ ∪ {¬¬w} ⊢ w. Now, construct a proof P4 by taking P3 followed by P1. If w is actually used in P1 , then it is mentioned as ‘P’ in it. In P4 , mention it as ‘Th’. This is justified since in the P3 portion, w has already been proved. The proof P4 is a proof of Σ ∪ {¬¬w} ⊢ p. If w is not used in P1 , then as it is, P4 is a proof of Σ ∪ {¬¬w} ⊢ p. Similarly, construct the proof P5 by taking P3 followed by P2 , and change the justification corresponding to the line ¬w in the P2 portion to ‘Th’, if necessary. Now, P5 is a proof of Σ ∪ {¬¬w} ⊢ ¬p. Therefore, Σ ∪ {¬¬w} is inconsistent. By (1), we conclude that Σ ⊢ ¬w. Theorem 1.4 (Finiteness). Let Σ be a set of propositions, and let w be a proposition. Then the following are true: 1. If Σ ⊢ w, then there exists a finite subset Γ ⊆ Σ such that Γ ⊢ w. 2. If Σ is inconsistent, then there exists a finite inconsistent subset of Σ. Proof. Left as an exercise. Theorem 1.5 (Paradox of Material Implication). Let Σ be a set of propositions. Then, Σ is inconsistent if and only if Σ ⊢ x for every proposition x. Proof. Left as an exercise. 1.1 Exercises 1. Assume that ⊢ ¬x → (x → y). Prove Deduction Theorem by using Reductio ad Absurdum (RAA). 2. Let Σ be a set of propositions. Show that Σ is consistent if and only if there exists a proposition w such that Σ ̸⊢ w and Σ ̸⊢ ¬w. 10 3. Transitivity: Let Σ be a set of propositions, and let x, y be propositions. Show that if Σ ⊢ x and x ⊢ y, then Σ ⊢ y. 4. Let Σ and Γ be sets of propositions, and let w be a proposition. Let Σ ⊢ x for each x ∈ Γ. Show that if Σ ∪ Γ ⊢ w, then Σ ⊢ w. 11