Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 8 Logic in Computer Science { p.1/18 Semantics Logic in Computer Science { p.2/18 Interpretation An interpretation I of F is < D;I 0 >, where D is a non-empty set called the domain of individuals. I 0 is a mapping de ned on the constants of F satisfying 1. If c is an individual constant, then I 0 (c) 2 D. 2. If f n is an n-ary function constant, then I 0 (f n ) : D n ! D. 3. If p is a propositional constant, then I 0 (p) 2 fT; Fg. 4. If P n is an n-ary predicate constant, then I 0 (P n ) : D n ! fT; Fg. Logic in Computer Science { p.3/18 Assignment Given an interpretation I =< D;I 0 >, an assignment into I is a function de ned on the variables of F and satisfying 1. If x is an individual variable, then (x) 2 D. 2. If f n is an n-ary function variable, then (f n ) : D n ! D. 3. If p is a propositional variable, then (p) 2 fT; Fg. 4. If P n is an n-ary predicate variable, then (P n ) : D n ! fT; Fg. If x is variable (of any type) and 1 and 2 are assignments, then 1 and 2 agree o x i 1 (y) = 2 (y) for all variables y (of any type) distinct from x. Logic in Computer Science { p.4/18 Semantics of Terms Given I =< D;I 0 > and 2 I , I( )(t), the value of term t with respect to in I, is de ned as follows 1. I(c)( ) = I 0 (c) if c is an individual constant. 2. I(x)( ) = (x) if x is an individual variable. 3. I(f n t 1 t n )( ) = I 0 (f n )I(t 1 )( ) I(t n )( ) if f n is an n-ary function constant, and t 1 ; ;t n are terms. 4. I(f n t 1 t n )( ) = (f n )I(t 1 )( ) I(t n )( ) if f n is an n-ary function variable, and t 1 ; ;t n are terms. Logic in Computer Science { p.5/18 Semantics of W s Given an interpretation I =< D;I 0 > and an assignment , I( )(A), the value of A with respect to in I, for each w , is de ned as follows I(p)( ) = I 0 (p) if p is a propositional constant. I(p)( ) = (p) if p is a propositional variable. I(P n t 1 t n )( ) = I 0 (P n )I(t 1 )( ) I(t n )( ) if P n is an n-ary predicate constant, and t 1 ; ;t n are terms. I(P n t 1 t n )( ) = (P n )I(t 1 )( ) I(t n )( ) if P n is an n-ary predicate variable, and t 1 ; ;t n are terms. Logic in Computer Science { p.6/18 I( )(A) I( A)( ) = :I(A)( ) if A is a w . I(A _ B)( ) = I(A)( )_I(B)( ) if A and B are w s. If A is a w and x is an individual variable, I(8xA)( ) = 8 > > > > < > > > > : F if there exists d 2 D such that I(A)( [x=d]) = F T otherwise Logic in Computer Science { p.7/18 A set of Important De nitions 1. satis es A in I (j= (I; ) A) i I(A)( ) = T 2. A is satis able in I i there is 2 I such that j= (I; ) A. 3. A is satis able i there is an interpretation in which A is satis able. 4. A is valid in I (j= I A) i for every assignment 2 I , j= (I; ) A. 5. A is valid i A is valid in every interpretation. 6. A is contradictory or unsatis able i for every interpretation I and every assignment , I(A)( ) = F. Logic in Computer Science { p.8/18 De nitions (continued) 1. A set of w is satis able in I i there is an assignment 2 I such that for all B 2 , j= (I; ) B. 2. A set of w is satis able i there is an interpretation I such that of w is satis able in I. 3. A set of w is unsatis able i it is not satis able. 4. A model for a set of w s is an interpretation in which each of the w s is valid. 5. logically implies A ( j= A) i for every interpretation I and every 2 I , j= (I; ) A provided that j= (I; ) B for every B. Logic in Computer Science { p.9/18 Proposition on Semantics of Terms and W s Let A be a w , t a term and I =< D;I 0 > an interpretation, and 1 ; 2 2 I . 1. If 1 and 2 agree on all variables which occur in t, then I(t)( 1 ) = I(t)( 2 ) 2. If 1 and 2 agree on all variables which occur free in A, then I(A)( 1 ) = I(A)( 2 ) Logic in Computer Science { p.10/18 Valid vs Satis able Let A be a w and I an interpretation. 1. j= I A i A is not satis able in I. 2. j= A i A is not satis able. 3. A is satis able in I i A is not valid in I. 4. A is satis able i A is not valid. 5. j= I A i j= I 8xA. 6. j= A i j= 8xA. 7. A is satis able in I i 9xA is satis able in I. 8. A is satis able i 9xA is satis able. Logic in Computer Science { p.11/18 Closure of a w For any w of B of which the free variable are precisely x 1 ; x n , the universal closure of B is de ned as B = 8x 1 8x n B the existential closure of B is de ned as B = 9x 1 9x n B Logic in Computer Science { p.12/18 Closures of W s 1. B and B are closed w s. 2. If B is a closed w , then B = B = B. 3. ‘ B B and ‘ B B 4. ‘ B i ‘ B. 5. For any interpretation I, B is valid in I i B is valid in I, and B is satis able in I i B is satis able in I. 6. B is valid i B is valid, and B is satis able i B is satis able. Logic in Computer Science { p.13/18 is free on A Let t 1 ; ;t n be terms and A a w . = S x 1 ; ;x n t 1 ; ;t n is free on A i for each free variable x of A, (x) is free for x in A. Logic in Computer Science { p.14/18 Given an interpretation I, an assignment 2 I , a substitution for free occurrences of individual variables, is an assignment into I such that (x) = I( (x))( ) for each individual variable x. (x) = (f) for each function variable f. (p) = (p) for each propositional variable p. (P) = (P) for each predicate variable P. Logic in Computer Science { p.15/18 Substitution Value Theorem Let A be a w , t a term and I an interpretation. 1. If 2 I , then I( (t))( ) = I(t)( ) for any . 2. If 2 I and is free on A, then I( (A))( ) = I(A)( ) Logic in Computer Science { p.16/18 A Corollary If t is a term free for the individual variable x in the w A, then I(S x t A)( ) = I(A)( S x t ) Logic in Computer Science { p.17/18 Soundness Theorem Let A be a w and a set of w s. 1. If ‘ A, then j= A. 2. If ‘ A, then j= A. Logic in Computer Science { p.18/18