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/15F= 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