Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 11 FOL with Equality Logic in Computer Science { p.1/15 Syntax Logic in Computer Science { p.2/15 F = F = = F + \ = " + 2 Axiom Schemata Axiom Schema 6 x = x. Axiom Schema 7 x = y (S z x A S z y A) where A is an atomic w . A rst order theory is a rst-order theory with equality if it has a binary predicate = such that the w s above are theorem of the theory. Logic in Computer Science { p.3/15 Properties of \=" 1. ‘ x = y y = x 2. ‘ x = y (y = z x = z) 3. ‘ x = y (S z x A S z y A) where x and y are free for z in A. 4. ‘ x = y (S z x t = S z y t) 5. ‘ x 1 = y 1 ^ ^ x n = y n f(x 1 ; ;x n ) = f(y 1 ; ;y n ) for any n-ary function symbol f. 6. ‘ x 1 = y 1 ^ ^ x n = y n (P(x 1 ; ;x n ) P(y 1 ; ;y n )) for any n-ary predicate symbol P. Logic in Computer Science { p.4/15 First Order Theory with Equality Let T be a rst-order theory with a binary predicate constant = such that 1. ‘ T x = x 2. ‘ T x 1 = y 1 ^ ^ x n = y n f(x 1 ; ;x n ) = f(y 1 ; ;y n ) for any n-ary function symbol f. 3. ‘ T x 1 = y 1 ^ ^ x n = y n (P(x 1 ; ;x n ) P(y 1 ; ;y n )) for any n-ary predicate symbol P. Then T is a rst order theory with equality. Logic in Computer Science { p.5/15 9! and 9!! 9!xA stands for 9xA ^8x8y(A ^ S x y A x = y) 9!!xA stands for 8x8y(A ^ S x y A x = y) where y is the rst individual variable distinct from x and all variables which occur in A. Logic in Computer Science { p.6/15 Sequent Rules ;A 1 ; ;A k ) ) where, A 1 ; ;A k are of the following forms t = t s 1 = t 1 ^ ^ s n = t n f(s 1 ; ;s n ) = f(t 1 ; ;t n ) s 1 = t 1 ^ ^ s n = t n ^ P(s 1 ; ;s n ) P(t 1 ; ;t n ) Logic in Computer Science { p.7/15 Semantics Logic in Computer Science { p.8/15 Equality-Interpretation An interpretation [model] < D;I 0 > for a rst order language with an equality predicate = is an equality-interpretation [model] i I 0 (=) is the identity relation on D. Logic in Computer Science { p.9/15 Soundness Theorem If M is an equality-model for a set of sentences and ‘ F = A, then j= M A. Logic in Computer Science { p.10/15 Elementarily Equivalent Interpretations M and N are elementarily equivalent i for every sentence A of F, j= M A i j= N A Logic in Computer Science { p.11/15 Equality-Model Let M =< D;I 0 > be any model for Axioms 6 and 7. Then there is an equality-model N =< D 0 ;I 0 0 > such that 1. #D 0 #D, and 2. N is elementarily equivalent to M. Logic in Computer Science { p.12/15 Completeness 1. Let be a set of sentences consistent in F = . Then has a frugal equality-model. 2. Let be a set of sentences, and A be a w , of F = . Then ‘ F = A i A is valid in all the frugal equality-models satisfying . Logic in Computer Science { p.13/15 Compactness Let L 0 (F = ). The following parts are equivalent. 1. is consistent. 2. Every nite subset of is consistent. 3. is has an equality-model. 4. Every nite subset of has an equality-model. 5. is has a frugal equality-model. 6. Every nite subset of has a frugal equality-model. Logic in Computer Science { p.14/15 Size of Models Let L 0 (F = ). 1. If has arbitrarily large nite equality-models, then it has an in nite equality-model. 2. Lowenheim-Skolem-Tarski Theorem If has an in nite equality-model, and is any cardinal number such that #(L(F = )), then has an equality-model of cardinality . Logic in Computer Science { p.15/15