Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 9 Logic in Computer Science { p.1/19 Independence Logic in Computer Science { p.2/19 Interpretation over a singleton Let I be < fag;I 0 >, and 2 I . 1. I(A)( ) = I(8xA)( ). 2. I(t)( ) = a. 3. I(S x 1 ; ;x n t 1 ; ;t n A)( ) = I(A)( ). 4. I 0 (P); (P) 2 fI (n) ; (n) g for every n-ary predicate constant (variable), where I (n) (a 1 ; ;a n ) = T and (n) (a 1 ; ;a n ) = F If ‘ A, then _ occurs in A. If ‘ A, then occurs in A. Logic in Computer Science { p.3/19 Independence Theorem The rules of inference and axiom schemata of F are independent. Proof Sketch: Step 1 MP is independent. Step 2 Gen is independent. Step 3 AS 1 ;AS 2 and AS 3 are independent. Step 4 AS 4 is independent. \De ne"8 as 9. Step 5 AS 5 is independent. Do a transformation. In a proof from hypothesis, rule is independent. Logic in Computer Science { p.4/19 Consistency Logic in Computer Science { p.5/19 Consistency absolutely consistency there is a w which is not a theorem. consistency w.r.t negation there is no w A such that both A and A are theorems. consistency there is a w A such that 6‘ A. F is absolutely consistent and consistent with respect to negation. Logic in Computer Science { p.6/19 is consistent The following parts are equivalent. If A 2 L(F), then A 62 Th( ) or A 62 Th( ) There is A 2 L(F) such that A 62 Th( ) or A 62 Th( ) is consistent. Logic in Computer Science { p.7/19 is consistent with 0 is consistent with 0 i [ 0 is consistent. A 1 ; ;A n is consistent with i [fA 1 ; ;A n g is consistent. 1. A 1 ; ;A n is inconsistent with i ‘ A 1 _ A n . 2. A is inconsistent with i ‘ A. 3. If is consistent and ‘ A, then A is consistent with . Logic in Computer Science { p.8/19 Maximal Consistent Set 1. is complete i for any w A A 2 or A 2 2. If satis es (a) is consistent, and (b) For any w A 62 , A is inconsistent with , then we say that is consistent and maximal. Logic in Computer Science { p.9/19 Maximal Consistent Set Let be a consistent and maximal set. 1. A 2 i ‘ A 2. A 2 i A 62 Let be a set of w s. The following parts are equivalent. is consistent and maximal. is consistent and complete. Logic in Computer Science { p.10/19 Completenss Logic in Computer Science { p.11/19 Two forms of Completeness Theorem Let be a set of w s. The following parts are equivalent. If j= A then ‘ A If is consistent, then is satis able. Logic in Computer Science { p.12/19 Sequence of consistent sets of w s Partially Ordered Set A relation on a set S is called partial ordering or partial order if it is re exive, antisymmetric and transitive. A set S together with a partial ordering R is called a partially ordered set, or poset. Totally Ordered Set If < S;R > is a poset and every two elements of S are comparable, S is called a totally ordered set or linearly ordered set. A totally ordered set is also called a chain. Lemma Let S 2 L(F) . If < S; > is a totally ordered set, and for any 2 S, is consistent, then S S is consistent. Logic in Computer Science { p.13/19 Existence of consistent and maximal set Theorem Let L(F) be consistent. There exists 0 2 L(F) such that 1. 0 , and 2. 0 is consistent and maximal. Zorn’s Lemma Let S be a nonempty set such that for any chain Z S, the set S Z 2 S. Then there is a m 2 S which is maximal in the sense that it is not a subset of any other element of S. Logic in Computer Science { p.14/19 Expansion Let F 1 and F 2 be two rst order systems. 1. If L(F 1 ) L(F 2 ), then we say that F 2 is an expansion of F 1 . 2. If L(F 1 ) L(F 2 ), then we say that F 2 is a proper expansion of F 1 . 3. F 2 is an expansion of F 1 i every constant of F 1 is a constant F 2 . Logic in Computer Science { p.15/19 Extension Let F 1 and F 2 be two rst order systems. 1 L(F 1 ) and 2 L(F 2 ). 1. If L(F 1 ) L(F 2 ) and Th(F 1 S 1 ) Th(F 2 S 2 ), then we say that F 2 S 2 is an extension of F 1 S 1 . 2. If for every A 2 L(F 1 ), 1 ‘ F 1 A i 2 ‘ F 2 A, then we say that F 2 S 2 is a conservative extension of F 1 S 1 . Logic in Computer Science { p.16/19 Expansion and Extension 1. If F 2 is an expansion of F 1 , then Th(F 1 ) Th(F 2 ). 2. If F 2 S 2 is a conservative extension of F 1 S 1 , then Th(F 1 [ 1 ) = Th(F 2 [ 2 ) \L(F 1 ) Logic in Computer Science { p.17/19 Expansion, Extension and Consistency 1. If F 2 S 2 is a conservative extension of F 1 S 1 , then F 1 S 1 is consistent i F 2 S 2 is consistent. 2. Let F 1 and F 2 be formulations of F, so that F 2 is an expansion of F 1 obtained by adding additional individual constants to the set of constants of F 1 . Let L(F 1 ), Then (a) F 2 S is a conservative extension of F 1 S , and (b) F 1 S is consistent i F 2 S is consistent. Logic in Computer Science { p.18/19 Frugal Interpretation An interpretation < D;I 0 > for F is said to be frugal i #D #L(F). An interpretation I is said to be a frugal model of if it is a frugal interpretation of . Logic in Computer Science { p.19/19