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/15First 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