国防科学技术大学：《数理逻辑》（英文版）Lecture 11 Syntax

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

彐!and彐! 彐! a stands for xA∧vxVy(A∧SAx=y) 彐!! A stands for VnVy(A∧SAx=y) y where y is the first individual variable distinct from and all variables which occur in a Logic in Computer Science-p.6/15

∃! and ∃!! ∃!xA stands for ∃xA ∧ ∀x∀y(A ∧ Sxy A ⊃ x = y) ∃!!xA stands for ∀x∀y(A ∧ Sxy A ⊃ x = y) where y is the first individual variable distinct from x and all variables which occur in A. Logic in Computer Science – p.6/15

Sequent rules T,A1,…,Ak→△ → Where,A1,……, Ak are of the following forms s1=t1∧…∧Sn=tnf( Sn) f(t ∧…∧Sn=tn^P(1 Logic in Computer Science-p.7/15

Sequent Rules Γ, A1, · · · , Ak ⇒ ∆ Γ ⇒ ∆ where, A1, · · · , Ak are of the following forms • t = t • s1 = t1 ∧ · · · ∧ sn = tn ⊃ f(s1, · · · , sn) = f(t1, · · · ,tn) • s1 = t1 ∧ · · · ∧ sn = tn ∧ P(s1, · · · , sn) ⊃ P(t1, · · · ,tn) Logic in Computer Science – p.7/15

SEMANTICS Logic in Computer Science-p.8/15

Semantics Logic in Computer Science – p.8/15

Equality-Interpretation An interpretation model D, Io> for a first order language with an equality predicate is an equality-interpretation (model iff Io()is the identity relation on D Logic in Computer Science-p.9/15

Equality-Interpretation An interpretation [model] for a first order language with an equality predicate = is an equality-interpretation [model] iff I0(=) is the identity relation on D. Logic in Computer Science – p.9/15

Soundness theorem If M is an equality-model for a set r of sentences and THe= A, then Fm A Logic in Computer Science- p10/15

Soundness Theorem If M is an equality-model for a set Γ of sentences and Γ `F= A, then |=M A. Logic in Computer Science – p.10/15