Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 3 Propositional Calculus(Cont’d) Logic in Computer Science { p.1/17 Completeness Theorem Logic in Computer Science { p.2/17 Completeness of is complete i for any w A A 2 or A 2 Logic in Computer Science { p.3/17 Let be a consistent set of w s. De ne a sequence as follows. 0 = n+1 = 8 < : n [fA n g if n ‘ A n n [f A n g otherwise = S 1 n=0 n Logic in Computer Science { p.4/17 Some Properties 1. n is consistent. 2. n n+1 3. is complete. 4. If ‘ A then there exists n 2 N such that n ‘ A. 5. A 2 i ‘ A 6. is consistent. Logic in Computer Science { p.5/17 is an assignment (A) = 8 < : T if A 2 F otherwise is an assignment. Logic in Computer Science { p.6/17 Completeness Theorem If j= A then ‘ A (G odel 1930) ‘ A i j= A ‘ A i j= A Logic in Computer Science { p.7/17 A For any w A, let A = 8 < : A if (A) = T A if (A) = F Lemma: Let all variables in A be among p 1 ; ;p n . Then p 1 ; ;p n ‘ A Logic in Computer Science { p.8/17 Another Proof of Completeness Theorem? Every tautology is a theorem of P. Proof Sketch: By using the above lemma. Let A be a w and let n be the number of variables which occurred in A. Prove that for any assignment , p 1 ; ;p j ‘ A by induction on n j(0 j n). Logic in Computer Science { p.9/17 Compactness Satis ability and consistency are coextensive. Let be any set of w s, is satis able i is consistent. Compactness Theorem is satis able i every nite subset of is satis able. Logic in Computer Science { p.10/17 Independence in Formal Systems Logic in Computer Science { p.11/17 Independence An axiom is independent i it can’t be derived from the other axioms by the rules of inference. An axiom schema is independent i not every instance of it is a theorem of the system obtained by deleting from the set of axioms all instances of the schema in question. A rule of inference is independent if there is a theorem which can’t be derived without using that rule of inference. Logic in Computer Science { p.12/17 Independence of P The axiom schemata and the rule of inference of P are all independent. Proof Sketch: It is trivial to see that MP is independent. For the rest, using Arithmetic Interpretation. It su ces to nd some property which the axiom does not have but which all the other axioms of the sys- tem do have, and which is preserved by the rules of inference. Logic in Computer Science { p.13/17 Propositional Connectives Logic in Computer Science { p.14/17 Substitutivity of Equivalence Let A,M and N be w s and let A M N be the result of replacing M by N at zero or more occurrences (henceforth called designate occurrences) of M in A. 1. A M N is a w . 2. If j= M N then j= A A M N . ( sub) If ‘ M N then ‘ A A M N Logic in Computer Science { p.15/17 Propositional Connectives vs truth functions An n-ary truth function is a function from n-tuples of truth values to truth values. A propositional connective is a symbol of a formalized language which, in the intend interpretation, denotes a truth function. How to lift a w to be a truth function? Logic in Computer Science { p.16/17 Abstraction If p 1 ; ;p n are distinct propositional variables including all variables in A, let [ p 1 p n ]A : fT; Fg n ! fT; Fg where [ p 1 p n ]A(x 1 ; ;x n ) = (A) and (p i ) = x i for all 0 i n. Obviously, [ p 1 p n ]A = [ p 1 p n ]B i A B Logic in Computer Science { p.17/17