Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 2 Propositional Calculus Logic in Computer Science { p.1/39 Syntax Formation Rules for P The The Axiomatic Structure of P Theorems and Derived Rules Logic in Computer Science { p.2/39 Primitive Symbols The primitive symbols of P are the following: Improper symbols: (; ); ;_ Proper symbols: denumerably many propositional variable, p;q;r;p 1 ;q 1 ;r 1 ; :The set of Primitive Symbols Logic in Computer Science { p.3/39 Well-Formed Formulas The set of w s is the intersection of all sets S of formulas such that: 1. p 2 S for each propositional variable p 2. For each formula A, if A 2 S, then ( A) 2 S 3. For all formulas A and B, if A 2 S and B 2 S, then (A _ B) 2 S A w is a member of the set of w s. Logic in Computer Science { p.4/39 Principle of Induction on W Let < be a property of formulas, and let <(A) mean that A has property <. Suppose 1. <(q) for each propositional variable q. 2. Whenever <(A), then <( A). 3. Whenever <(A) and <(B), then <((A _ B)). Then every w has property <. Logic in Computer Science { p.5/39 Abbreviations (A ^ B) stands for ( A_ B) (A B) stands for ( A _ B) (A B) stands for ((A B) ^ (B A)) Logic in Computer Science { p.6/39 Substitution A function : ! is a substitution i 1. If x 2 , then (x) 6= 2. If x;y 2 , then (xy) = (x) (y) If 1 and 2 are substitutions such that 1 (x) = 2 (x) for every primitive symbol x, then 1 = 2 Logic in Computer Science { p.7/39 Substitution(Continued) A substitution is nite i fx 2 j (x) 6= xg is nite. A substitution is a substitution for variables i the only primitive symbols x such that (x) 6= x are variables. Let x 1 ; ;x n be distinct primitive symbols and let Y 1 ; ;Y n be formulas. S x 1 ; ;x n Y 1 ; ;Y n is a substitution such that (x) = 8 < : Y i if x = x i ; 1 i n x if x 62 fx 1 ; ;x n g Logic in Computer Science { p.8/39 The Axiomatic Structure of P Axiom Schema 1 A _ A A Axiom Schema 2 A (B _ A) Axiom Schema 3 A B (C _A (B _C)) Modus Ponens (MP) A; A B B Logic in Computer Science { p.9/39 The Axiomatic Structure of P Axiom Schema 1 A _ A A Axiom Schema 2 A (B _ A) Axiom Schema 3 A B (C _A (B _C)) Modus Ponens (MP) A; A B B Logic in Computer Science { p.9/39 The Axiomatic Structure of P Axiom Schema 1 A _ A A Axiom Schema 2 A (B _ A) Axiom Schema 3 A B (C _A (B _C)) Modus Ponens (MP) A; A B B Logic in Computer Science { p.9/39 The Axiomatic Structure of P Axiom Schema 1 A _ A A Axiom Schema 2 A (B _ A) Axiom Schema 3 A B (C _A (B _C)) Modus Ponens (MP) A; A B B Logic in Computer Science { p.9/39 The Axiomatic Structure of P Axiom Schema 1 A _ A A Axiom Schema 2 A (B _ A) Axiom Schema 3 A B (C _A (B _C)) Modus Ponens (MP) A; A B B Logic in Computer Science { p.9/39 What is a Proof A proof of a w B from the set of hypotheses is a nite sequence B 1 ;B 2 ; ;B m of w s such that B m is B, and for each j(1 j m) at least one the following conditions is satis ed. 1. B j is an axiom; 2. B j 2 ; 3. B j is inferred by MP from w s B i and B k , where i < j and k < j. Logic in Computer Science { p.10/39 ‘ ‘ B There is a proof of B from . ‘ B A proof of a w B is a proof of B from the empty set of hypotheses. A theorem is a w which has a proof. Logic in Computer Science { p.11/39 Formal System formal system = + Formation Rules + Axioms + Rules Logic in Computer Science { p.12/39 2 and 2 + 2 If A 2 , then ‘ A. 2 + If 1 ‘ A and 1 2 , then 2 ‘ A. Logic in Computer Science { p.13/39 MP If 1 ‘ A and 2 ‘ A B and 1 and 2 , then ‘ B Logic in Computer Science { p.14/39 Rule of Substitution(Sub) If ‘ A, and if p 1 ; ;p n are distinct variables which do not occur in any w in , then ‘ S p 1 ; ;p n B 1 ; ;B n A Proof Sketch. Let be the substitution S p 1 ; ;p n B 1 ; ;B n . It is easy to see that if C 1 ; ;C m is a proof of A from , then (C 1 ); ; (C m ) is a proof of (A) from . Logic in Computer Science { p.15/39 Derived Rules DR 1 If ‘ A B and ‘ C _ A then ‘ B _ C. ‘ A_ A ‘ A A ‘ A A ‘ A A ‘ A A Logic in Computer Science { p.16/39 Derived Rules Commut If ‘ A _ B then ‘ B _ A. Trans If 1 ‘ A B, 2 ‘ B C, 1 and 2 , then ‘ A C. DR 2 If 1 ‘ A C, 2 ‘ B C, 1 and 2 , then ‘ A _ B C. DR 3 If 1 ‘ A C, 2 ‘ A C, 1 and 2 , then ‘ C. DR 4 If ‘ A B, then ‘ A (C _ B) and ‘ A (B _ C) Assoc ‘ (A _ B) _ C i ‘ A _ (B _ C) DR 5 If 1 ‘ A B, 2 ‘ A (B C), 1 and 2 , then ‘ A C Logic in Computer Science { p.17/39 Deduction Theorem If ;A ‘ B then ‘ A B Proof Sketch: Let C 1 ; ;C m be a proof from B from . We Prove ‘ A C i for all i(1 i m) by induction on i. Logic in Computer Science { p.18/39 Theorems ‘ A ( B (A _ B)) ‘ A ( A B) Logic in Computer Science { p.19/39 Frequently Used Rules (2 ) If 1 ;A ‘ B, 2 ; A ‘ B, 1 and 2 , then ‘ B (:: + ) If ‘ A, then ‘ A (:: ) If ‘ A, then ‘ A (: + ) If ;A ‘ B, ;A ‘ B, then ‘ A (DR) If ‘ A, ‘ A, then ‘ B Logic in Computer Science { p.20/39 Proof Systems Hilbert-style proof system Gentzen’s National Deduction Systems The Sequent Calculus Logic in Computer Science { p.21/39 A Hilbert-style proof system Axiom K A (B A) Axiom S (A (B C)) ((A B) (A C)) Axiom DN A A Modus Ponens A B A B Logic in Computer Science { p.22/39 Gentzen’s National Deduction Systems National Deduction is based upon three principles. 1. Proof takes place within a varying context of assumptions. 2. Each logical connective is de ned independently of the others. 3. Each connective is de ned by introduction and elimination rules. Logic in Computer Science { p.23/39 The sequent calculus A sequent has the form ) where and are nite set of formulas. The sequent A 1 ;A 2 ; ;A m ) B 1 ;B 2 ; ;B n is true if A 1 ^ A 2 ^ ^ A m B 1 _ B 2 _ _ B n : Logic in Computer Science { p.24/39 Sequent Rules basis sequent A; ) A; Negation rules ) ;A A; ) (:l) A; ) ) ; A (:r) Conjunction rules A;B; ) A ^ B; ) (^l) ) ;A ) ;B ) ;A ^ B (^r) Logic in Computer Science { p.25/39 Sequent Rules Disjunction rules A; ) B; ) A _ B; ) (_l) ) ;A;B ) ;A _ B (_r) Implication rules ) ;A B; ) A B; ) (! l) A; ) ;B ) ;A B (! r) Logic in Computer Science { p.26/39 Structural Rules Weakening rules ) A; ) (w : l) ) ) ;A (w : r) Exchange rules Contract rules A;A; ) A; ) (c : l) ) ;A;A ) ;A (c : r) Cut rule ) ;A A; ) ) (cut) Logic in Computer Science { p.27/39 Semantics Logic in Computer Science { p.28/39 Operations over Truth Values Truth Values T; F Operations :;_;^; ; 8 < : :T = F :F = T 8 < : F _ F = F F _ T = T _ F = T _ T = T Logic in Computer Science { p.29/39 Assignment An assignment of truth values to propositional variables is a function from the set of variables to the set of fT, Fg of truth values. An assignment of w A : V ar(A) ! fT; Fg An assignment of : V ar( ) ! fT; Fg Logic in Computer Science { p.30/39 The Semantic Function V V : L(P) ! fT; Fg The value V (A) of a w A with respect to the assignment is de ned as follows by induction on the construction of A: 1. V (p) = (p) 2. V ( B) = :V (B) 3. V (B _ C) = V (B)_V (C) Logic in Computer Science { p.31/39 Related Concepts 1. A is true with respect to if V (A) = T, and false with respect to if V (A) = F. 2. A is a tautology(j= A). A is a contradiction. 3. satis es A(j= A). 4. satis es . Note that every assignment satis es the empty set of w s. 5. is satis able. is unsatis able or contradictory. Logic in Computer Science { p.32/39 Unique Readability To prove that we have used enough parentheses to eliminate any ambiguity in analyzing w s. 1. Every w has the same number of left as right parentheses. 2. Any proper initial segment of a w contains an excess of left parentheses. 3. No proper initial segment of a w can itself be a w . Logic in Computer Science { p.33/39 Unique Readability Theorem and _, when restricted to the set of w s, have ranges which are disjoint from each other and from the set of propositional variables, and are one to one. Logic in Computer Science { p.34/39 Validity and Soundness A w of a logistic system is valid w.r.t an interpretation i the value of that w is truth(under that interpretation) for all assignments of values to its (free) variables. An interpretation of a logistic system is emphasissound i , under that interpretation, the axioms are all valid and the rules of inference preserve validity. Logic in Computer Science { p.35/39 Soundness Theorem A w of P is a tautology if it is valid under the interpretation which is implicit in the de nition of the valuation function V . Every theorem of P is a tautology. If ‘ A then j= A. Logic in Computer Science { p.36/39 Consistency A logistic system is absolutely consistent i there is a w which is not a theorem. A logistic system is consistent w.r.t negation i there is no w A such that both A and A are theorems. is consistent i there is a w A such that 6‘ A. Logic in Computer Science { p.37/39 Consistency Let S be any logistic system in which A ( A B) is a theorem schema and in which MP is a primitive or derived rule. Then S is absolutely consistent i S is consistent w.r.t negation. Logic in Computer Science { p.38/39 Consistency Theorem P is absolutely consistent and consistent w.r.t negation. Lemma: If is consistent and A 62 Th( ) then [f Ag is consistent. Logic in Computer Science { p.39/39