Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 6 Reasoning in Predicate Calculus Logic in Computer Science { p.1/27 Axiom Schemata for F Axiom Schema 1 A _ A A Axiom Schema 2 A (B _ A) Axiom Schema 3 A B (C _ A (B _ C)) Axiom Schema 4 8xA S x t A where t is a term free for the individual variable x in A Axiom Schema 5 8x(A _ B) (A _8xB) provided that x is not free in A Logic in Computer Science { p.2/27 Derived Rules Trans If ‘ A 1 A 2 ; ;‘ A n A n+1 , then ‘ A 1 A n+1 . _ _ If ‘ A (A 1 A 2 ) and ‘ A (B 1 B 2 ), then ‘ A (A 1 _ B 1 A 2 _ B 2 ) ^ ‘ A ^ B C i ‘ A (B C) Theorem ‘ 8x 1 8x n A A Logic in Computer Science { p.3/27 8 If ‘ A B and x is not free in A, then ‘ A 8xB. (1) ‘ A _ B given (2) ‘ 8x( A _ B) (1)Gen (3) ‘ 8x( A _ B) A _8xB AS5 (4) ‘ A 8xB Theorem ‘ 8x(A B) (8xA 8xB) Theorem ‘ A B ( B A) Theorem ‘ A B (B A) Logic in Computer Science { p.4/27 Positive / Negative Occurrence Let M be a wf part of A. An occurrence of M in A is positive / negative in A i that occurrence is in the scope of an even / odd number of occurrences of in A. M is positive / negative in A i the designated occurrences of M are all positive / negative in A. Let ( 1 ; ; n+1 ) be a designated occurrence of M in A, A M N = 1 N 2 n N n+1 Logic in Computer Science { p.5/27 Substitutivity of Implication Sub Let y 1 ; ;y k be a list including all distinct individual variables which occur free in M or N. 1. If M is positive in A, then ‘ 8y 1 y k (M N) (A A M N ) 2. If M is negative in A, then ‘ 8y 1 y k (M N) (A M N A) 3. If M is positive in A and ‘ M N, then ‘ A A M N 4. If M is negative in A and ‘ M N, then ‘ A M N A Logic in Computer Science { p.6/27 Substitutivity of Equivalence Sub 1. ‘ 8y 1 y k (M N) (A A M N ) 2. If ‘ M N, then ‘ A A M N 3. If ‘ M N and ‘ A, then ‘ A M N Theorems 1. ‘ 8x(A B) (8xA 8xB) 2. ‘ 8x(A B) (9xA 9xB) Logic in Computer Science { p.7/27 ‘ 8xC 8yS x y C? Theorem ‘ 8xC 8yS x y C, provided that y is not free in C and y is free for x in C. (1) ‘ 8xC S x y C AS4 (2) ‘ 8xC 8yS x y C (1) 8 (3) ‘ 8yS x y C S y x S x y C AS4 (4) ‘ 8yS x y C 8xC (3) 8 (5) j= P (p q) ^ (q p) (p q) (6) ‘ 8xC 8yS x y C Logic in Computer Science { p.8/27 Rule Let A;C be w s and x;y be individual variables. If 1. y is not free in C 2. y is free for x in C 3. ‘ A Then ‘ A 8xC 8yS x y C Logic in Computer Science { p.9/27 Proof from Hypotheses Let be a nite set of w s. A proof of a w A from is a nite sequence A 0 ; ;A m such that Logic in Computer Science { p.10/27 1. A m = A and 2. for each i one of the following is satis ed (a) (Ax) A i is an axiom; (b) (Hyp) A i 2 ; (c) (MP) there exist j;k(0 j;k < i) such that A k = A j A i ; (d) (Gen) there exists j(0 j < i) such that A i = 8xA j , and x is not free in ; (e) ( ) there exists j(0 j < i) such that A i = A j 8xC 8yS x y C , and C;x;y satisfy condition. Logic in Computer Science { p.11/27 In general ‘ A means there is a proof of A from some nite subset of . Logic in Computer Science { p.12/27 Universal Instantiation 8I If ‘ 8xA, then ‘ S x t A provided that t is a term free for x in A Logic in Computer Science { p.13/27 A Lemma Lemma Suppose ‘ A where is nite, and let U be a nite set of individual variables which are not free in A or in . Then, there is a proof of A from such that no member of U is generalized upon or occurs free in any w of the proof. Logic in Computer Science { p.14/27 2 + Theorem(2 + ) If 1 ‘ A and 1 2 then 2 ‘ A Corollary If ‘ A then ‘ A Logic in Computer Science { p.15/27 Derived Rules [P] If ‘ A 1 ; ; ‘ A n and if A 1 ^ ^ A n B is tautologous, then ‘ B. Also, if B is tautologous, ‘ B. [ ] If ‘ A B and if x is not free in or in A, then ‘ A 8xB. Deduction Theorem If ;A ‘ B then ‘ A B. Logic in Computer Science { p.16/27 Extended Substitutivity [ sub] If ‘ A and M is positive in A and ‘ M N, then ‘ A M N . [ sub] If ‘ A and M is negative in A and ‘ N M, then ‘ A M N . [ sub] If ‘ A and M N then ‘ A M N . Logic in Computer Science { p.17/27 Rule of Substitution [Sub x ] If ‘ A, then ‘ S x t A, provided that x does not occur free in and t is free for x in A. [Sub p ] If ‘ A, then ‘ S p D A, provided that p does not occur in and D is free for p in A. Logic in Computer Science { p.18/27 8 + If ‘ S x a A and the individual constant a does not occur free in [fAg, then ‘ 8xA. Logic in Computer Science { p.19/27 Theorems 1. ‘ 8x A 9xA 2. ‘ 9x A 8xA 3. ‘ 8x8yA 8y8xA 4. ‘ 9x9yA 9y9xA 5. ‘ S x t A 9xA provided that t is free for x in A. 6. ‘ A 9xA 7. ‘ 8xA 9xA Logic in Computer Science { p.20/27 Derived Rules 9Gen=9 + If ‘ S x t A, where t is a term free for x in A, then ‘ 9xA. 9Rule=9 If ;A ‘ B and if x is not free in [fBg, then ;9xA ‘ B. Rule C If ‘ 9xA and ;S x y A ‘ B where y is an individual variable which is free for x in A and which is not free in [f9xA;Bg, then ‘ B. Rule of Cases If ‘ A _ B and ;A ‘ C and ;B ‘ C, then ‘ C. IP If ; A ‘ B, and ; A ‘ B, then ‘ A. Logic in Computer Science { p.21/27 Theorems 1. ‘ 8xA A if x is not free in A. 2. ‘ 9xA A if x is not free in A. 3. ‘ 8x(A ^ B) 8xA ^8xB 4. ‘ 9x(A _ B) 9xA _9xB 5. ‘ 9x(A _ B) A _9xB if x is not free in A. 6. ‘ 8xA _8xB 8x(A _ B). 7. ‘ 8x(A _ B) (A _8xB) if x is not free in A. 8. ‘ 8x(B _ A) (8xB _ A) if x is not free in A. 9. ‘ 8x(B A) (9xB A) x is not free in A. 10. ‘ 9x8yA 8y9xA 11. ‘ 9x(A ^ B) 9xA ^9xB Logic in Computer Science { p.22/27 Summary To Prove Do A B Assume A, prove B and use Deduction Theorem A B Assume B, prove A A B Assume A and B, prove C^ C. A _ B write this as A B. A ^ B Prove A and B separately. 8xA Prove A and use Gen. If x is free in a hypothesis, prove S x y A, then use Gen and . 9xA Prove S x t A then use 9Gen. 9xA Write this as 8x A. Logic in Computer Science { p.23/27 Summary If one has inferred Do A ^ B Infer A and B by Rule P A _ B Try to use Rule of Cases. A B Write this as A _ B. Or, use MP if A has been inferred. 8xA Try to use 8I. 9xA Try to use Rule C. Logic in Computer Science { p.24/27 Sequent Calculus Logic in Computer Science { p.25/27 Rules for 8 S x t ; ) 8xA; ) (8l) ) ;A ) ;8xA (8r) (8r) holds provided x is not free in the conclusion. Logic in Computer Science { p.26/27 Rules for 9 A; ) 9xA; ) (9l) (9l) holds provided x is not free in the conclusion. ) ;S x t A ) ;9xA (9r) Logic in Computer Science { p.27/27