Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn Lecture 11 FOL with equality Logic in Computer Science - p 1/15
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
Syntax Logic in Computer Science – p.2/15
F F=F+“=”+2 Axiom schemata axiom schema 6 c= x Axiom Schema 7 =y)(SzA) SZ A)where a is an atomic wff A first order theory is a first-order theory wit equality if it has a binary predicate such that the wffs above are theorem of the theory Logic in Computer Science-p.3/15
F= F= = F + “ = ” + 2 Axiom Schemata Axiom Schema 6 x = x. Axiom Schema 7 x = y ⊃ (SzxA ⊃ SzyA) where A is an atomic wff. A first order theory is a first-order theory with equality if it has a binary predicate = such that the wffs above are theorem of the theory. Logic in Computer Science – p.3/15
Properties of“=” C=yDy=E 2.Fx=y2(y=22x=2 3. F=y)(S2A= S, A)where a and y are free for e in a 4.Fx=y(S2t=S2+) 5.}m1=91∧…∧x f(g1,., yn) for any n-ary function symbol f 6.x1=91A…∧xn )for any n-ary predicate symbol P Logic in Computer Science -p 4/15
Properties of “=” 1. ` x = y ⊃ y = x 2. ` x = y ⊃ (y = z ⊃ x = z) 3. ` x = y ⊃ (SzxA ≡ SzyA) where x and y are free for z in A. 4. ` x = y ⊃ (Szxt = Szy t) 5. ` x1 = y1 ∧ · · · ∧ xn = yn ⊃ f(x1, · · · , xn) = f(y1, · · · , yn) for any n-ary function symbol f. 6. ` x1 = y1 ∧ · · · ∧ xn = yn ⊃ (P(x1, · · · , xn) ≡ P(y1, · · · , yn)) for any n-ary predicate symbol P. Logic in Computer Science – p.4/15
First Order Theory with Equality Let t be a first-order theory with a binary predicate constant= such that T0= 2.+rm1=1∧…∧ →f(x℃ m f(9,…,yn) for any n-ary function symbol∫ Frm1=A…∧xn=9n(P(m1, an)三 (y1,., gn))for any n-ary predicate symbol P Then T is a first order theory with equality Logic in Computer Science-p.5/15
First Order Theory with Equality Let T be a first-order theory with a binary predicate constant = such that 1. `T x = x 2. `T x1 = y1 ∧ · · · ∧ xn = yn ⊃ f(x1, · · · , xn) = f(y1, · · · , yn) for any n-ary function symbol f. 3. `T x1 = y1 ∧ · · · ∧ xn = yn ⊃ (P(x1, · · · , xn) ≡ P(y1, · · · , yn)) for any n-ary predicate symbol P. Then T is a first order theory with equality. Logic in Computer Science – p.5/15