### Create a StudySoup account

#### Be part of our community, it's free to join!

Already have a StudySoup account? Login here

# C2P2L PHI 113

UCD

### View Full Document

## 7

## 1

## Popular in Metalogic

## Popular in Department

This 42 page Class Notes was uploaded by Vishal Chakraborty on Tuesday May 3, 2016. The Class Notes belongs to PHI 113 at University of California - Davis taught by in Spring 2016. Since its upload, it has received 7 views.

## Reviews for C2P2L

### What is Karma?

#### Karma is the currency of StudySoup.

#### You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 05/03/16

2 2 C P L The Completeness of Classical Propositional and Predicate Logic Aldo Antonelli University of California, Davis antonelli@ucdavis.edu 22 April 2012 Contents I Introduction 2 II The propositional case 2 1. Preliminaries, p. 2 ▯ 2. Semantics for propositional logic, p. 4 ▯ 3. Proof theory for propositional logic, p. 5 ▯ 4. Soundness and Completeness of propositional logic, p. 10 III The predicate case 11 5. Preliminaries, p. 11 ▯ 6. Semantics of predicate logic, p. 12 ▯ 7. Proof theory of predicate logic, p. 14 ▯ 8. Soundness and completeness of predicate logic, p. 16 IV Extensions and applications 20 9. Rudiments of model theory, p. 20 ▯ 10. Non-standard models of arithmetic, p. 25 ▯ 11. The interpolation theorem, p. 27 ▯ 12. Lindström’s Theorem, p. 32 V Problems Sets 36 13. Problem Set I: syntactic matters, p. 36 ▯ 14. Problem Set II: semantic matters, p. 37 ▯ 15. Problem Set III: applications of compactness, p. 39 ▯ 16. Problem Set IV: the game semantics, p. 40 ▯ 17. Problem Set V: Deﬁnability, p. 41 This work is licensed under the Creative Commons Attribution–ShareAlike 3.0 Unported License. To view a copy of this 1 Part I Introduction Kurt Gödel’s completeness theorem for the ﬁrst-order predicate calculus (1929–30) is one of the deepest classical results in metalogic, perhaps of deeper foundational signiﬁcance than Gödel’s own incomplete- ness theorem for arithmetic (1931). The theorem establishes the extensional equivalence of two very different notions of consequence for ﬁrst-order formulas, validity and provability, the ﬁrst one of which involves an unbounded universal quantiﬁcation over the class of possible interpretations, while the second one merely asserts the existence of certain ﬁnite sequences of formulas. The purpose of these notes is to chart a direct and self-contained route to a proof of the completeness theorem for ﬁrst-order logic. Since the heart of the combinatorial argument is already present in the proof of the propositional case, the propositional case is treated independently. Once the proof strategy for the propositional case is laid out, the further complications required to handle existential witnesses in the predicate case are introduced. Thus, the completeness proof takes up the ﬁrst two parts of what follows. The third part is devoted to further results and applications, while the last part collects some problem sets that introduce further material and might be useful for classroom use. It should be mentioned that where proofs are routine they have been merely sketched or even omitted (the full details to be supplied at the chalkboard), but any unexpected steps are explicitly mentioned. Part II The propositional case 1. Preliminaries The language L o0 classical propositional logic comprises as basic symbols countably many proposi- tional variables p ,p ,... as well as symbols for the connectives ▯ (not), ▯ (if ...then) and the two 0 1 parentheses ( and ). We assume that these symbols are all distinct and no one occurs as a part of another one. We refer to the set of the propositional variables as theAte0of the atomic sentences. 1. Deﬁnition: The set F 0f the formulas of the language L i0 inductively deﬁned as the smallest set of strings over the alphabet containinAt0 and such that if ’ and are in 0 , then so are: É (▯’); É (’ ▯ ). 2 . Theorem: Principle of induction on formulas: If some property P holds of all the propositional license, visit http://creativecommons.org/licenses/by-sa/3.0/ or send a letter to Creative Commons, 444 Castro Street, Suite 900, Mountain View, California, 94041, USA. Comments, criticisms, and suggestions for improvement are much appre- ciated and can be sent directly to the email address above. 2 variables and is such that it holds for (▯’) and (’ ▯ ) whenever it holds for ’ and , then P holds of all formulas in F0. Proof. Let S be the collection of all formulas with property P, so that, in particular, S ▯ F . 0hen S contains the propositional variables and is closed under the connectives; since F is the smallest such 0 class, also 0 ▯ S. So F 0 S, and every formula has propery P. 3. Exercise: Prove that any formula in F is0balanced, in that it has as many left parentheses as right ones. Also, prove that no formula begins with ▯ and that no proper initial segment of a formula is a formula. The formulas (’ _ ) and (’ ^ ) abbreviate ((▯’) ▯ ) and ▯(’ ▯ (▯ )), respectively. Sim- ilarly, ’ ▯ abbreviates (’ ▯ ) ^ ( ▯ ’). Parentheses around ▯’ are usually dropped, with the understanding that ▯ binds the shortest formula that follows it; outermost parentheses are likewise usually dropped. 4. Theorem (Unique Readability): Any formula ’ in F has e0actly one parsing as one of the following 1. p nor some p 2n At 0 2. (▯ ) for some in F0; 3. ( ▯ ▯) for some ,▯ in F . 0 Moreover, such parsing is unique, in that, e.g., ’ cannot have the form (▯ ) in two different ways. Proof. By induction of ’. For instance, suppose that ’ has two distinct readings as ( ▯ ▯) and 0 0 0 ( ▯ ▯ ). Then and must be the same (or else one would be a proper initial segment of the other); so is the two readings of ’ are distinct it must be because ▯ and ▯ are distinct readings of the same sequence of symbols, which is impossible by the inductive hypothesis. 5. Theorem: Principle of deﬁnition by recursion: for any set V and functions i : At0 ! V and h ,h1 2 from V and V ▯ V, respectively, into V, there exists exactly one function f : F ! V 0atisfying the following equations: f (pn) = i(pn) f (▯’) = h 1f (’)) f (’ ▯ ) = h2(f (’), f ( )) Proof. Let F be the class of all functions g s.t.: É dom(g) is ﬁnite and closed under subformulas; É whenever ’ is in dom(g) then g satisﬁes the equation corresponding to ’. S Put f = F. It is easy to see that: (a) No two functions g and g in F disagree on any of the arguments on which they are both deﬁned. Hence, f is well-deﬁned as a function. (This requires unique readability.) 3 (b) f satisﬁes the equations. (c) f is unique. (d) f is total, i.e., dom(f ) = F0. These are established by induction on formulas. 6. Deﬁnition: Uniform substitution. If ’ and are formulas, and p ii a propositional variable, then ’[ = pi] denotes the result of replacing each occurrence of p byian occurrence of in ’; similarly, the simultaneous substitution of p ,1..,p bynformulas 1,..., n is denoted by ’[ = 1p1,..., = pn]. 7. Exercise: Give a mathematically rigorous deﬁnition of ’[ = pi using Theorem 5. 2. Semantics for propositional logic 8. Deﬁnition: Let f t,fg be the set of the two truth values, “true” and “false.” A valuation for L is 0 function v assigning either t or fto the propositional variables of the language, i.e., v : At 0! f t,fg. 9. Theorem: Every valuation v can be “lifted” to a unique function v : F ! f 0 t,fg such that: v(p n = v(p n; 8 < t if v(’) = f; v(▯’) = : f otherwise. 8 < t if v(’) = f or v( ) = t; v(’ ▯ ) = : f if v(’) = t and v( ) = f. Proof. Apply Theorem 5. 10. Exercise: Show that the valuation clauses for ▯ and ▯ give the right truth tables for ^ and _: ’ ’ ^ ’ _ t t t t t f f t f t f t f f f f 11. Theorem: Local Determination: Suppose that v and v a1e valua2ions that agree on the proposi- tional letters occurring in ’, i.e., 1 (pn) = v2(pn) whenever p ocnurs in ’. Show that they also agree on ’, i.e., v1(’) = v 2’). Proof. By induction on ’. 12. Deﬁnition: Deﬁne the following semantic notions: 4 É A formula ’ is satisﬁable if for some v, v(’) = t; it is unsatisﬁable if for no v it holds v(’) = t; É A formula ’ is a tautology if v(’) = t for all valuations v; É A formula ’ is contingent if it is satisﬁable but not a tautology; É if ▯ is a set of formulas, ▯ j= ’ (“▯ entails ’”) if and only if v(’) = tfor every valuation v on which v( ) = t for every 2 ▯. É if ▯ is a set of formulas, ▯ is satisﬁable if there is a valuation v on which v( ) = t for every 2 ▯, and ▯ is unsatisﬁable otherwise. 13. Exercise: The following can all be proved with little more than “deﬁnition chasing”: É ’ is a tautology if and only if ? j= ’; É ▯ j= ’ if and only if ▯[f▯’g is unsatisﬁable; É if ▯ j= ’ and ▯ j= ’ ▯ then ▯ j= ; É if ▯ is satisﬁable then every ﬁnite subset of ▯ is also satisﬁable; É Monotony: if ▯ ▯ ▯ and ▯ j= ’ then also ▯ j= ’; É Cut: if ▯ j= ’ and ▯[f’g j= then ▯[▯ j= ; É Deduction theorem: ▯ j= ’ ▯ if and only if ▯[f’g j= . 3. Proof theory for propositional logic 14. Deﬁnition: The set of Ax of the Axioms of propositional logic comprises all formulas of the follow- ing forms: [Ax1] ’ ▯ ( ▯ ’); [Ax2] (’ ▯ ( ▯ ▯)) ▯ ((’ ▯ ) ▯ (’ ▯ ▯)); [Ax3] (▯’ ▯ ▯ ) ▯ ( ▯ ’). 15. Deﬁnition: If ▯ is a set of formulas of L and 0 a formula, then a proof of ’ from ▯ is a ﬁnite sequence ’ ,1..,’ of normulas such that ’ = ’ ann for each i ▯ n one of the following holds: É ’ 2i▯; or É ’ ii an axiom; or É there are j,k < i that ’ is ’ ▯ ’ . j k i The last clause just says that ’ can be obtained from previously occurring ’ and ’ ▯ ’ by i k k i modus ponens (MP). We write ▯ ‘ ’ (“▯ proves ’,” or “’ is provable from ▯”) to mean that there is a proof of ’ from ▯. When ▯ is empty, we write ‘ ’ to mean ? ‘ ’. 16. Proposition: The following are provable: (a) Transitivity: f’ ▯ , ▯ ▯g ‘ ’ ▯ ▯; (b) ‘ ’ ▯ ’. 5 Proof. For part (a), the following instances of Ax1. and Ax2. are needed: ( ▯ ▯) ▯ (’ ▯ ( ▯ ▯)); (’ ▯ ( ▯ ▯)) ▯ ((’ ▯ ) ▯ (’ ▯ ▯)). For part (b), consider the instance of Ax1.: ’ ▯ ((’ ▯ ’) ▯ ’) and distribute the outermost implication by Ax2. 17. Proposition: For any set ▯ of formulas: (a) If ’ is an axiom then ▯ ‘ ’; (b) If ’ is in ▯ then ▯ ‘ ’; (c) Monotony: if ▯ ▯ ▯ and ▯ ‘ ’ then also ▯ ‘ ’; (d) ▯ ‘ ’ if and only if there is a ﬁnite subs0t ▯ of ▯ such th0t ▯ ‘ ’. 18. Theorem: Let Thm (▯) = f’ : ▯ ‘ ’g. ThenThm (▯) is the smallest set of formulas containing the axioms, every formula in ▯, and closed under modus ponens (from ’ and ’ ▯ infer ). Proof. We know from Proposition 17 that Thm (▯) has the desired properties; so we need to show that it is the smallest such. Let A be any other set of formulas containing the axioms and ▯ and closed under modus ponens. Prove that Thm (▯) ▯ A by induction on the length of a proof of ’ from ▯. 19. Corollary: Principle of induction on theorems: any property P that holds of the axioms, of formulas in ▯, and is preserved by modus ponens holds of every formula iThm (▯). 20. Theorem: Deduction Theorem: ▯[f’g ‘ if and only if ▯ ‘ ’ ▯ . Proof. The “if” direction is immediate; if ▯ ‘ ’ ▯ then also ▯ [ f’g ‘ ’ ▯ , so there is a proof of ’ ▯ from ▯[f’g, and one more application of modus ponens gives ▯[f’g ‘ . For the converse, proceed by induction on theorems. If 2 ▯ or is an axiom then also ▯ ‘ ▯ (’ ▯ ) by Ax1, and modus ponens gives ▯[ ‘ ’ ▯ ; and if 2 f’g then ▯ ‘ ’ ▯ because the last sentence is the same as ’ ▯ ’. For the inductive step, suppose is obtained by modus ponens from ▯ ▯ and ▯. Then ▯ [ f’g ‘ ▯ ▯ and ▯[f’g ‘ ▯. By inductive hypothesis, both ▯ ‘ ’ ▯ (▯ ▯ ); ▯ ‘ ’ ▯ ▯. But also ▯ ‘ (’ ▯ (▯ ▯ )) ▯ ((’ ▯ ▯) ▯ (’ ▯ )), by Ax2, and two applications of modus ponens give ▯ ‘ ’ ▯ , as required. 6 Notice how Ax1 and Ax2 were chosen precisely so that the Deduction Theorem would hold. The following proposition collects useful facts about provability that will be needed in the next section. 21. Proposition: The following are all provable: (a) ‘ (’ ▯ ) ▯ (( ▯ ▯) ▯ (’ ▯ ▯); (b) Contraposition: if ▯[f▯’g ‘ ▯ then ▯[f g ‘ ’; (c) Ex Falso Quodlibet: f’,▯’g ‘ ; (d) Double Negation: f▯▯’g ‘ ’; (e) if ▯ ‘ ▯▯’ then ▯ ‘ ’; Proof. Part (a) follows from Prop. 16, part (a) by two applications of the Deduction Theorem. For part (b): 1. ▯[f▯’g ‘ ▯ hyp. 2. ▯[ ‘ ▯’ ▯ ▯ Ded. Thm. 3. ▯ ‘ (▯’ ▯ ▯ ) ▯ ( ▯ ’) Ax3. and monotony 4. ▯ ‘ ▯ ’ MP 5. ▯[f g ‘ ’ Ded. Thm. For part (c) we have f▯’,▯ g ‘ ▯’ by Prop 17, part (b), and f’,▯’g ‘ follows by (b). Part (d): since f▯▯’,▯’g ‘ ▯▯▯’ by ex falso quodlibet, apply (b). Now for part (e), ▯ ‘ ▯▯’ ▯ ’ by the previous part, the deduction theorem, and monotony, so if ▯ ‘ ▯▯’ also ▯ ‘ ’ by MP. 22. Theorem: Cut: if ▯ ‘ ’ and ▯,’ ‘ ▯ then ▯[▯ ‘ ▯. Proof. The following shows that the conclusion is derivable: 1. ▯ ‘ ’ hyp. 2. ▯[▯ ‘ ’ monotony, 1. 3. ▯,’ ‘ ▯ hyp. 4. ▯[▯,’ ‘ ▯ monotony, 3. 5. ▯[▯ ‘ ’ ▯ ▯ Ded. Thm., 4. 6. ▯[▯ ‘ ▯ MP 2, 5. “Monotony” refers to Prop. 17, part (c). 23. Lemma: ’ ▯ ,’ ‘ . Proof. Clearly ’ ▯ ‘ ’ ▯ . Apply the Deduction Theorem. 24. Lemma: ’ ▯ ▯’ ‘ ▯’. Proof. The following shows the conclusion is derivable. 7 1. ▯▯’ ‘ ’ Double negation 2. ▯▯▯▯’ ‘ ▯▯’ Double negation 3. ▯▯(’ ▯ ▯’) ‘ ’ ▯ ▯’ Double negation 4. ▯’ ‘ ▯▯▯’ contraposition, 2 5. ▯▯(’ ▯ ▯’),’ ‘ ▯’ Deduction theorem, 3 6. ▯▯’,▯▯(’ ▯ ▯’) ‘ ▯’ Cut, 1, 5 7. ▯▯’,▯▯(’ ▯ ▯’) ‘ ▯▯▯’ Cut 4, 6 8. ▯▯’ ‘ ▯(’ ▯ ▯’) Contraposition, 7 9. (’ ▯ ▯’) ‘ ▯’ contraposition, 8. 25. Proposition: The following hold: (a) ‘ ▯▯ (b) ’ ▯ ▯ , ‘ ▯’ (c) ’ ▯ ,’ ▯ ▯ ‘ ▯’. (d) if ▯[f’g ‘ and ▯[f’g ‘ ▯ then ▯ ‘ ▯’. Proof. For part (a), we have ▯▯▯ ‘ ▯ by double negation, whence ‘ ▯▯ by Prop. 21, part (b). For part (b) we have: 1. ‘ (▯▯’ ▯ ▯▯▯ ) ▯ (▯▯ ▯ ▯’) Ax3 2. ▯▯’ ▯ ▯▯▯ ,▯▯ ‘ ▯’ 1, Ded. Thm., twice 3. ‘ ▯▯ Double Neg. 4. ▯▯’ ▯ ▯▯▯ , ‘ ▯’ 2, 3, Cut 5. ▯ ▯ ▯▯▯ ,’ ▯ ▯ ‘ ’ ▯ ▯▯▯ Transitivity (Prop. 16, part (a)) 6. ‘ ▯ ▯ ▯▯▯ Double Neg. + Ded. Thm. 7. ’ ▯ ▯ ‘ ’ ▯ ▯▯▯ 5, 6, Cut 8. ‘ ▯▯’ ▯ ’ Double. Neg + Ded. Thm. 9. ▯▯’ ▯ ’,’ ▯ ▯▯▯ ‘ ▯▯’ ▯ ▯▯▯ Transitivity 10. ’ ▯ ▯▯▯ ‘ ▯▯’ ▯ ▯▯▯ 8, 9, Cut 11. ’ ▯ ▯ ‘ ▯▯’ ▯ ▯▯▯ 7, 10, Cut 12. ’ ▯ ▯ , ‘ ▯’ 4, 11, Cut. Part (c) follows because: 1. ’ ▯ ,’ ‘ lemma 23 2. ’ ▯ ▯ , ‘ ▯’ part (b) 3. ’ ▯ ,’ ▯ ▯ ,’ ‘ ▯’ 1, 2, Cut. 4. ’ ▯ ,’ ▯ ▯ ‘ ’ ▯ ▯’ deduction theorem 5. ’ ▯ ▯’ ‘ ▯’ lemma 24 6. ’ ▯ ,’ ▯ ▯ ‘ ▯’ 4, 5, Cut. 8 Finally, for part (d): from the hypotheses by the deduction theorem, ▯ ‘ ’ ▯ and ▯ ‘ ’ ▯ ▯ ; from part (c) and monotony, ▯,’ ▯ ,’ ▯ ▯ ‘ ▯’; two applications of Cut give the desired result. 26. Deﬁnition: A set ▯ of formulas is consistent if and only if there is a formula ’ such that ▯ 6‘ ’; it is inconsistent otherwise. 27. Proposition: ▯ is inconsistent if and only if there is a formula ’ such that both ▯ ‘ ’ and ▯ ‘ ▯’. Proof. The “only if” direction is obvious. For the converse, suppose that ▯ ‘ ’ and ▯ ‘ ▯’. Then by Proposition 21, part (c) and monotony, ▯[f’,▯’g ‘ for any formula , and now two applications of Cut give ▯ ‘ for any , so ▯ is inconsistent. 28. Proposition: ▯ ‘ ’ if and only if ▯[f▯’g is inconsistent. Proof. If ▯ ‘ ’ then also ▯,▯’ ‘ ’ by monotony, and ▯,▯’ ‘ ▯’ by reﬂexivity, so ▯ [ f▯’g is inconsistent. Conversely, suppose ▯ [ f▯’g is inconsistent. Then ▯▯’ ‘ ▯ and ▯▯’ ‘ ▯▯ for some ▯. By Prop. 25 part (d), ▯ ‘ ▯▯’. But also ▯▯’ ‘ ’, by double negation so that by cut ▯ ‘ ’. 29. Proposition: If ▯ is consistent, then for any formula ’, either ▯[f’g is consistent or ▯[f▯’g is consistent. Proof. From Prop. 28 we have that if ▯[f▯’g is inconsistent, then ▯ ‘ ’; if ▯[f’g is also inconsistent, then ▯[f’g ‘ for any . But then by Cut ▯ ‘ for any , so ▯ is inconsistent. 30. Proposition: ▯ is consistent if and only if every ﬁnite subset ▯0▯ ▯ is consistent. Proof. For the non-trivial direction: if ▯ is inconsistent, then ▯ ‘ and ▯ ‘ ▯ for some ; each proof involves only ﬁnitely many formulas from ▯; collect the ones occurring in the ﬁrst proof into the ﬁnite set ▯1, and those occurring in the second proof into the ﬁnite set 2 . Then ▯0= ▯ 1▯ is2a ﬁnite subset of ▯ that is a inconsistent. 31. Exercise: Show that the following hold by exhibiting proofs from the axioms (i.e., without using meta-theoretic facts such as Cut, Monotony, the Deduction Theorem, etc.): É f’ ▯ , ▯ ▯g ‘ ’ ▯ ▯; É ‘ ’ ▯ ’; É ‘ ▯’ ▯ (’ ▯ ); É ‘ ’ ▯ (▯’ ▯ ). 9 4. Soundness and Completeness of propositional logic 32. Theorem: (Soundness) If ▯ ‘ ’ then ▯ j= ’. Proof. By induction on theorems. If ’ is an axiom then j= ’ and hence a fortiori ▯ j= ’. Similarly if ’ 2 ▯, ▯ j= ’. For the inductive step, suppose ’ is obtained by modus ponens from ▯ and ▯ ▯ ’; also assume as inductive hypothesis that the theorem holds for ▯ ▯ ’ and ▯. The third item in Exercise 13 gives the desired result. 33. Corollary: If ▯ is satisﬁable, then ▯ is consistent. Hence, propositional logic is consistent. 34. Deﬁnition: A set ▯ of formulas is maximally consistent if it is consistent and if ▯ is a consistent set such that ▯ ▯ ▯ then ▯ = ▯. 35. Proposition: (Truth Lemma) let ▯ be maximally consistent; then: (a) ▯ ‘ ’ if and only if ’ 2 ▯; (b) ’ 2 ▯ if and only if ▯= ▯; (c) ’ ▯ 2 ▯ if and only if eithe= ▯ or 2 ▯. Proof. By the way of example, let ’ 2 ▯; if also ▯’ 2 ▯, then ▯ is inconsistent; and if neither ’ nor ▯’ is in ▯ then by Proposition 29 one of ▯ [ f’g and ▯ [ f▯’g is consistent, which means that ▯ is not maximal. The left-to-right of item (a) of the Truth Lemma is the deductive closure of ▯, i.e., if ▯ ‘ ’ then ’ 2 ▯. 36. Theorem: (Completeness) if ▯ is consistent then ▯ is satisﬁable. Proof. Let ’ ,’ ,... be an exhaustive listing of all the formulas of the language. Recursively deﬁne an 0 1 increasing sequence of sets of formula0 ▯1,▯ ,..., by putting: ▯ = ▯ 0 8 < ▯ [f’ g if ▯ [f’ g is consistent; ▯ = n n n n n+1 : ▯ nf▯’ g n otherwise. Then deﬁne: [ ▯ = ▯n. 0▯n The proof now proceeds by establishing, in turn, the following facts: (a) For each n, the sen ▯ is consistent (by induction on n, using Proposition 29); ▯ (b) ▯ is consistent; ▯ (c) ▯ is maximal. 10 Then deﬁne a valuation v by putting v(p ) =i tif and only if pi2 ▯ . By induction on ’ it is then shown that membership in ▯ coincides with truth according to v also for more complex sentences: v(’) = t ▯ ▯ ▯ if and only if ’ 2 ▯ . In particular, v satisﬁes ▯ , and since ▯ ▯ ▯ , also ▯ is satisﬁable, as desired. 37. Corollary: If ▯ j= ’ then ▯ ‘ ’. Proof. If ▯ 6‘ ’ then ▯[f▯’g is consistent, by Proposition 28. So by the theorem ▯[f▯’g is satisﬁable, so ▯ 6j= ’. 38. Proposition: (Compactness Theorem) ▯ is satisﬁable if and only if every ﬁnite subset ▯ of ▯ is 0 satisﬁable. Proof. ▯ is unsatisﬁable if and only if it is inconsistent, if and only if some ﬁnite subset ▯ of ▯ 0s inconsistent, if and only if some ﬁnite subset ▯ o0 ▯ is unstasﬁable. 39. Corollary: ▯ j= ’ if and only if for some ﬁnite subset ▯ of ▯, ▯ j= ’. 0 0 Part III The predicate case 5. Preliminaries The language L of1classical predicate logic comprises the connectives ▯ and ▯, the universal quantiﬁer 8, parentheses ( and ) as well as: É denumerably many individual variables v ,v ,.0.; 1 É countably many (i.e., ﬁnitely or denumerably many) individual constants c ,c ,...; 0 1 É for each n > 0, countably many n-place predicate symbols, including at least the 2-place symbol . = for identity; É for each n > 0, countably many n-place function symbols. 40. Deﬁnition: We deﬁne the sets comprising the terms, atomic formulas and formulas of L : 1 É The set T o1 the terms L is d1ﬁned as the smallest set containing the constants, the variables, and such that if t 1..., tnare terms and f is an n-place function symbol, then f t ... 1 is anso a term. É The set At of the atomic formulas comprises all expressions of the form Pt ... t , where t ,..., t 1 1 n .1 n are terms and P is an n-place predicate symbol as well as all expressions of the form t = t 1 2 É The set F o1 the formulas of L is 1eﬁned as the smallest set containing the atomic formulas and such that if ’ and are formulas and x is a variable, then (▯’), (’ ▯ ) and 8x’ are formulas (the formula ’ is the scope of the quantiﬁer 8x). 11 We adopt the same conventions for dropping parentheses as in the propositional case as well as the same abbreviations for (’ ^ ) and (’ _ ). Moreover, we abbreviate ▯8x ▯’ by 9x’. Just as in the propositional case, we have a principle of induction on both terms and formulas, as well as a principle of deﬁnition by recursion (also on both terms and formulas). 41. Deﬁnition: The following notions relate to the occurrence of variables in formulas: 1. A variable x occurs free in a formula ’ if it does not fall within the scope of a quantiﬁer 8x. This can be deﬁned recursively on the complexity of ’: x is always free in ’ if ’ 2 At 1; x is free in ▯ or ▯ ▯ if it is free in or ▯; and x is free in 8y if it is free in and not the same variable as y. 2. If ’ is a formula and x ,...1 x are nistinct variables, we denote by ’(x ,..., x ) th1 fact thnt all of the variables occurring free in ’ are among x ,..., x 1 n 3. If no variable occurs free in ’, then ’ is a sentence . 0 0 42. Deﬁnition: We deﬁne t[ = t x], the result of replacing t for every occurrence of x in t, recursively 0 on the complexity of t: if t is a constant c or a variable other than x then t[ = t x ] is just t; if t is x then 0 0 0 0 0 t[ = x] is t ; and if t is f t1... tnthen t[ = t x] is f t1[ = x]... tn[ = x]. 43. Deﬁnition: We deﬁne ’[ = t x], the result of replacing t for every free occurrence of x in ’, recur- sively on the complexity of ’: . 0 0 0 . 0 É if ’ is Pt .1. t on t = 1 then2’[ = t x] is P f 1 [ =x]... t n = x] or t1[ = x] = t 2 =t x], respectively; 0 0 0 É if ’ is ▯ or ▯ ▯ then ’[ = t x] is ▯( [ = t x]) or [ = x] ▯ ▯[ =t x], respectively; É if ’ is 8y (where y is a variable other than x), then ’[ = t x] is 8y(’[ = t x]); É if ’ is 8x then ’[ = t x] is just ’. 44. Deﬁnition: A term t is free for x in ’ if x does not occur in ’ within the scope of a quantiﬁer 8y binding a variable y occurring in t. Needless to say, the previous deﬁnition can be more precisely given as a recursion on ’. 6. Semantics of predicate logic 45. Deﬁnition: A structure A for L provide1 a non empty domain or universe jAj = A as well as: (a) for each constant symbol c of L , an el1ment c 2 A; A . (b) for each n-place predicate symbol P of L (other t1an =), an n-ary relation P ▯ A ; A n (c) for each n-place function symbol f of L , an n-a1y function f A : A ! A. 46. Deﬁnition: An assignment to the variables is a function s that assigns to each variable x a member s(x) of A. if s is an assignment x a variable, and a 2 A, then s( = a x) is the assignment deﬁned as follows: 8 < a, if y is x; s( =x)(y) = : s(y), otherwise. 12 a The function s( = x) is the result of shifting s at x and is called an x-variant of s. 47. Proposition: Each assignment can be “lifted” to a function s : T ! A ass1gning a member s(t) of the domain A to each term t in T , re1ursively as follows: s(x) = s(x), A s(c) = c , A s(f t1,..., tn) = f (s(t 1,...,s(t )n. 48. Theorem: Local Determination I: If s and 1 are as2ignments that agree on the variables occurring in a term t, then they assign the same denotation to t, i.e., s (t)1= s (t)2 Proof. By induction on t. 49. Deﬁnition: The notion of satisfaction of a formula ’(x ,..., x1) by annassignment s in a structure A, written A j= ’[s], is deﬁned by recursion on ’: A É A j= Pt ..1 t [sn if and only if P (s(t ),.1.,s(t )); n . É A j= (t =1t )[s2 if and only if s(t ) =1s(t ); 2 É A j= (▯’)[s] if and only if A j6= ’[s]; É A j= (’ ▯ )[s] if and only if either A 6j= ’[s] or A j= [s]; É A j= 8x’[s] if and only if A j= ’[s( = a x)] for every a 2 A. 50. Theorem: Local Determination II: If s and 1 are a2signments that agree on the variables occurring free in a formula ’, then A j= ’[s ] i1 and only if A j= ’[s ]. 2 Proof. By induction on ’. 51. Corollary: If ’ is a sentence, then A j= ’[s] for some s if and only if A j= ’[s] for every s. 52. Corollary: A j= ’[s] for every structure A and assignment s, if and only if A j= 8x’[s] for every structure A and assignment s. 53. Deﬁnition: The following notions concern the satisfaction of formulas and sets thereof: 1. A sentence ’ is true in a structure A, written A j= ’, if and only if for some (equivalently: every) assignment s, A j= ’[s]. 2. Where ▯ is a set of formulas, s satisﬁes ▯ in A, written A j= ▯[s], if and only if A j= [s] for every in ▯. 3. ▯ entails ’, written ▯ j= ’, if and only if for every structure A and assignment s, if A j= ▯[s], then A j= ’[s]. 54. Substitution Theorem: if s is an assignment in A: 0 t s(t ) 1. for all terms t and t , s(t[ = x]) = s( =x)(t); t s(t) 2. if t is free for x in ’, then A j= ’[ = x][s] if and only if A j= ’[s( = x)] 13 Proof. By induction on t and ’. At the inductive step for 8y’ (with y a variable other than x), the hypothesis is employed as follows: since t is free for x in 8y’, the variable y does not occur in t, and a hence s and s( = y) agree on t, by local determination. 7. Proof theory of predicate logic 55. Deﬁnition: A formula ’ of predicate logic is a tautological instance if and only if there is a tautology (p1,...,p n of propositional logic and ﬁrst-order formulas ▯ ,1..,▯ sunh that ’ = [ = p1,..., = pn]. 56. Deﬁnition: The set Ax of the Axioms of predicate logic comprises all formulas obtained by preﬁxing any number of universal quantiﬁers to the following: [Ax0] ’, where ’ is a tautological instance; [Ax1] 8x ▯ [ =x], if t is free for x in; [Ax2] 8x(’ ▯ ) ▯ (8x’ ▯ 8x ); [Ax3] ▯ 8x , if x is not free in ; . [Ax4] x = x; . x y [Ax5] x = y ▯ ( [ = z] ▯ [ =z]), if both x and y are free for z in . 57. Deﬁnition: A proof from ▯ is a ﬁnite sequence of formulas, each one of which is either an axiom, or a member of ▯, or obtained by previous formulas by modus ponens. A formula ’ is provable from ▯, written ▯ ‘ ’, if there is a proof from ▯ ending in ’. 58. Deﬁnition: Thm = f’ : ▯ ‘ ’g. ▯ 59. Proposition: Thm ▯ is the smallest set of formulas containing ▯, the axioms, and closed under modus ponens. Accordingly, we have a principle of proof by induction on the theorem of ▯. For example, let us show that 8x ‘ 9x (where the formula on the right of the turnstile is just an abbreviation for ▯8x ▯ ): 1. 8x ▯ ▯ ▯ [ =x] Ax1: c free for x in ▯ c c 2. (8x ▯ ▯ ▯ [ =x]) ▯ ( [ = x] ▯ ▯8x ▯ )) Ax0 3. [ =x] ▯ ▯8x ▯ 1, 2, MP 4. 8x ▯ [ =x] Ax1: c free for x in 5. 8x hyp. 6. [ =x] 4, 5, MP 7. ▯8x ▯ 3, 6, MP Since tautological instances are all axioms, the following proposition follows immediately by n applica- tions of modus ponens. Accordingly, from now on we freely employ purely propositional steps in proofs and justify them by reference to “Proposition T.” 60. Proposition T: If ▯ ‘ ’ ,...▯ ‘ ’ and ’ ▯ (’ ▯ ▯▯▯ ▯ (’ ▯ )▯▯▯) is a tautological instance, 1 n 1 2 n then ▯ ‘ . 14 Proof. The formula ’ ▯ (’ 1 ▯▯▯ ▯ (2 ▯ n )▯▯▯) is a tautological instance and hence an axiom; n applications of MP give the desired result. 61. Remark: Since the axioms for predicate logic comprise all the propositional axioms, and the only rule (viz., MP) is the same, all the propositional proof-theoretic properties such the Deduction Theorem, Cut, Monotony, etc., carry over to the predicate case. 62. Theorem: (Generalization) If ▯ ‘ ’ and x is not free in any formula in ▯, then ▯ ‘ 8x’. Proof. By induction on Thm ▯: if ’ is an axiom, so is 8x’. If ’ 2 ▯ then x is not free in ’, so that ’ ▯ 8x’ is an axiom (Ax3), and ▯ ‘ 8x’ by MP. Now suppose ’ follows by MP because ▯ ‘ and ▯ ‘ ▯ ’. By induction hypothesis, ▯ ‘ 8x and ▯ ‘ 8x( ▯ ’). But by Ax2 also ▯ ‘ 8x( ▯ ’) ▯ (8x ▯ 8x’), and two applications of MP give ▯ ‘ 8x’ as desired. 63. Theorem: (Weak Generalization on Constants) If ▯ ‘ ’ and c is a constant not in occurring in ▯, then there is a variable x not in ’ such that ▯ ‘ 8x ’[ = x c], and the proof does not involve c. Proof. Let ’ ,.1.,’ be anproof of ’ from ▯, so that ’ = ’ . Pick a variabne x not in ’ ,...,’ , and 1 n consider the new sequence: ’ [ = 1 x ],...,’ [n= x c]. Such a sequence is a proof of ’[ = x c] from ▯. In fact, for each i = 1,...,n: É if ’ is an axiom, then so is ’ [ = i x c]; É if ’ 2i▯, then since c is not in ▯, we have ’ [ = i x c] = ’ 2i▯; x x É if ’ ii obtained from ’ and ’ ▯ j then ’ [j= i i c] follows by MP from ’ [ = j c] and (’ ▯ j x x x ’ i[ = c] = ’ [j= c] ▯ ’ [i= c]. 0 It is clear that the constant c no longer occurs in the new sequence. Now let ▯ comprise those formulas x 0 0 x from ▯ that appear in the proof of ’[ = c]; then x is not free in any formula in ▯ and ▯ ‘ ’[ = c]. By 0 x x generalization (Theorem 62) ▯ ‘ 8x ’[ = c], whence by monotony ▯ ‘ 8x ’[ = c], as desired. Our goal is to replace the requirement in Theorem 63 that x does not occur in ’ (at all) by the weaker requirements that x is not free in ’ and it is free for c in ’. Clearly this can be accomplished by a change of bound variable — so that is what we set out to prove ﬁrst. 64. Lemma: If x is free for c in ’ and y is not free in ’, then x is free for y in ’[ = y c]. Proof. If x is not free for y in ’[ = y x], then some free occurrence of y in ’[ = y ] falls within the scope of a quantiﬁer 8x. But y is not free in ’, by hypothesis, so all such occurrences come from the substitution y [ = c]. So some occurrence of c falls within the scope of 8x and x is not free for c in ’. 65. Lemma: (Change of Bound Variable) If x and y are not free in ’ and they are both free for c in ’, x y then ‘ 8x’[ = c] ▯ 8y’[ = c] (and the proof does not involve c). 15 Proof. From the hypotheses, y is free for c in ’ and x is not free in ’, so by the previous lemma 64, y x x x y is free for x in ’[ = c]. It follows that 8x’[ = c] ▯ ’[ = ][ = x ] is an axiom (Ax1). Since x is not free in ’, we have ’[ = x c][ = x] = ’[ = y c], so that ‘ 8x’[ = x c] ▯ ’[ =y ], and by the Deduction Theorem 8x’[ = x ] ‘ ’[ =y ]. Since y is not free in ’, it also not free in 8x’[ = x c], so that by Generalization 8x’[ = x ] ‘ 8y’[ = y c], and the Deduction Theorem again gives ‘ 8x’[ = x c] ▯ 8y’[ = y c]. The proof of ‘ 8y’[ = y c] ▯ 8x’[ = x c] is perfectly symmetric, so that the conclusion follows by Proposition T. 66. Theorem: (Strong Generalization on Constants) If ▯ ‘ ’, the constant c does not occur in ▯, and x is not free in ’ but it is free for c in ’, then ▯ ‘ 8x ’[ = x c]. Proof. Since ▯ ‘ ’ and c is not in ▯, then by Weak Generalization there is a variable y not in ’ such y that ▯ ‘ 8y ’[ = ]. Since y is not in ’ (at all), it is not free in ’ and it is also free for c in ’; if moreover (by hypothesis) x is not free in ’ and free for c in ’, then the requirements for a change of x y x bound variable are met, so ‘ 8x ’[ = c] ▯ 8y ’[ = c], whence ▯ ‘ 8x ’[ = c]. We conclude this section by collecting facts about identity. . 67. Proposition: ▯ ‘ t = t, for any term t and set ▯. . . Proof. 8x(x = x) is an axiom, and any term t is free for x in x = x. t . 0 0 t0 68. Proposition: If ▯ ‘ ’[ = z] and ▯ ‘ t = t , and both t and t are free for x in ’, then ▯ ‘ ’[ = z]. 0 Proof. Pick variables x and y not occurring ’, t, or t (at all). Then . 8x8y(x = y ▯ (’[ = x z] ▯ ’[ = y z])) . 0 t is an axiom (Ax5), since x and y are free for z in ’. By Ax1 and MP (twice), ▯ ‘ (t = t ▯ (’[ = z] ▯ ’[ =0 z])), whence the conclusion follows by two further applications of MP. 8. Soundness and completeness of predicate logic 69. Proposition: If ’ is an axiom of predicate logic, then A j= ’[s] for each structure A and assign- ment s. Proof. We ﬁrst verify that the schemas Ax0–Ax5 are valid. For instance, here is the case for Ax1: suppose t is free for x in ’, and assume A j= 8x’[s]. Then by deﬁnition of satisfaction, for each a 2 A, also A j= ’[s( = a x)], and in particular this holds when a = s(t), i.e., A j= ’[s( s(t= x)]. By the 16 Substitution Theorem, A j= ’[ = t x ][s]. This shows that A j= (8x’ ▯ ’[ = t x])[s]. After verifying the schemas, we see that their universal closures are also valid, by Corollary 52. 70. Theorem: (Soundness) If ▯ ‘ ’ then ▯ j= ’. Proof. By induction on theorems. By the previous proposition, all the axioms are valid, and hence if ’ is an axiom then ▯ j= ’. Similarly if ’ 2 ▯. And if ▯ ‘ and ▯ ‘ ▯ ’ then ▯ j= ’. 71. Theorem: (Completeness) If ▯ j= ’ then ▯ ‘ ’. This follows as a corollary, in the usual way, from the Theorem that if ▯ is consistent then ▯ is satisﬁable (Theorem 80 below). Some more work is need to before we can give the proof. In particular, in order to prove the theorem, assuming that ▯ is satisﬁable, we will build a structure A and an assignment s satisfying ▯. In so doing we need to extend ▯ to a maximally consistent set ▯, in such a t way that if a formula 9x’ is in the set, ’[ = x] is also in the set for some t. This is arranged by making t sure that the maximally consistent set ▯ extending ▯ contains all formulas 9x’ ▯ ’[ = x] for some appropriate witness t. 72 . Lemma: If ▯ is consistent in L and L is obtained from L by adding countably many new constants c ,c ,..., then ▯ is consistent in L . 0 0 1 Proof. Let L be obtained by expanding L as described. If ▯ is consistent in L but not consistent in L , then for some formula ▯(c ,...,c ) 2 L both ▯ ‘ ▯ and ▯ ‘ ▯▯. By hypothesis the ﬁnitely many 1 n new constants c ,..1,c occunring in ▯ do not occur in ▯. By strong generalization on constants there are variables x ,1.., x non in ▯ such that the following are provable in L: ▯ ‘ 8x ...8x ▯[ = x1 c ,..., =n c ], 1 n 1 n x x ▯ ‘ 8x ..18x ▯▯[ n 1 c1,..., =n cn]. Since in particular the variables x ,..., x are free for the corresponding constants c ,...,c , by Ax1 1 n 1 n also ▯ ‘ ▯[ =x1 c ,..., =n c ], 1 n x x ▯ ‘ ▯▯[ = 1 1 ,..., =n n ], and ▯ is inconsistent. 73. Deﬁnition: A set ▯ of formulas of a language L is saturated if and only if for each formula ’ 2 L c and variable x there is a constant c such that ▯8x’ ▯ ▯’[ = x] is in ▯. 0 74. Deﬁnition: Fix an enumeration h’ , x i,h’ 0 x 0,... 1f a1l formula-variable pairs of L , and deﬁne the sentence ▯ by necursion on n. For ▯ let c be t0e ﬁrst0new constant that does not occur in ’ 0 and let ▯ b0 the formula ▯8x ’ ▯ ▯’ [ 0 0 0 c0 x0]. Assuming ▯ ,...0 have neen deﬁned, denote by 17 c the ﬁrst new constant not occurring in ▯ ,...▯ , and let ▯ be the formula: ▯8x ’ ▯ n+1 0 n n+1 n+1 n+1 ▯’ [cn+=x ]. Finally, put ▯ = f▯ : n ▯ 0g. n+1 n+1 n 75. Proposition: (Saturation) Every consistent set ▯ can be extended to a saturated consistent set. Proof. Given a consistent ▯, expand the language by adding countably many new constants. By Lemma 72, ▯ is still consistent in the richer language. Further, let ▯ be as in Deﬁnition 74; then ▯ [ ▯ is saturated by construction. To show that it is also consistent it sufﬁces to show, by induction on n, that each set of the form ▯[f▯ ,..0▯ g isnconsistent. For the basis of the induction, suppose that ▯ [ f▯ g is inconsistent. It follows by Proposition 28 0 that ▯ ‘ ▯▯ , whence both the following hold by Proposition T: 0 ▯ ‘ ▯8x ’ 0 0 ▯ ‘ ’[ =0 x0]. c But c 0oes not occur in ▯ and the variable x is not 0ree in ’[ = 0 x0]. Moreover, x is0free for c 0 in ’[ =0 x0] (since by choice of c t0e only occurrences of c in ’[0= c0 x0 derive from the substitution [ = x0] and therefore fall outside the scope of any quantiﬁer binding x ). By0Strong Generalization on Constants, from the latter of these we obtain ▯ ‘ 8x ’ [ = 0 0 c0 x0[ =0 0], i.e., ▯ ‘ 8x 0 ,0and ▯ itself is inconsistent. The inductive step is perfectly analogous. 76. Proposition: Every consistent set ▯ can be extended to a maximally consistent saturated set ▯ . ▯ Proof. Let ▯ be consistent, and ▯ as in Deﬁnition 74. By proposition 75, ▯ [ ▯ is a consistent satu- rated set in the richer language with the countably many new constants. We deﬁne ▯ exactly as in▯ propositional logic: let ’ ,’ ,... be an enumeration of all the formulas of L . Deﬁne ▯ = ▯[▯ and 0 1 0 8 < ▯ nf’ g n if ▯n[f’ gnis consistent; ▯ n+1 = : ▯ [f▯’ g otherwise. n n ▯ S 0 ▯ Putting ▯ = n▯0 ▯n, we obtain a maximally consistent set in L ; since ▯[▯ is saturated, so is ▯ . Our plan is to extract from ▯ a structure A satisfying ▯ in L , which can then be turned into a structure A satisfying ▯ in L simply by “forgetting” the interpretation of the new constants c . Honever, if the universe A of A is simply taken to be the set of all closed terms, this leads to a problem, in that . we might have ▯ ‘ t = t for distinct terms t and t . This motivates the following deﬁnition of an 1 2 1 2 equivalence relation and the corresponding detour through the resulting quotient. 0 0 ▯ . 0 77. Deﬁnition: Deﬁne a relation ▯ over the set of terms of L by setting t ▯ t if and only ▯ ‘ t = t . 78. Lemma: The relation ▯ is an equivalence over the terms of L . 0 18 Proof. Reﬂexivity is given by Proposition 67; symmetry and transitivity follow, in a similar way to ▯ . 0 . 0 . Proposition 68. For instance, symmetry: by Ax5 and Ax1, ▯ ‘ t = t ▯ (t = t ▯ t = t), so that if 0 . 0 . ▯ 0 . 0 t ▯ t then ▯ ‘ t = t ; but also ▯ ‘ t = t, as we just saw, so ▯ ‘ t = t, i.e., t ▯ t. 0 0 0 79. Deﬁnition: For each term t of L , the equivalence class ft : t ▯ t g of t relative to ▯ is denoted by [t]. We are now ready to complete the proof of the main theorem. 80. Theorem: If ▯ is consistent then ▯ is satisﬁable. ▯ 0 Proof. Given a consistent ▯, we extend it to a maximally consistent saturated set ▯ of formulas of L , 0 0 using Proposition 76. We deﬁne a structure A for L and an assignment s as follows: 0 0 É jA j = A= f[t] : t 2 L g; A 0 0 É c = [c] for each constant c of L . A0 ▯ É h[t ]1...,[t ]in2 P if and only if ▯ ‘ Pt ...1t , fnr each n-place predicate symbol P; É f A0([t ],...,[t ]) = [f t ... t ], for each n-place function symbol f ; 1 n 1 n É s(x) = [x]. It is important to notice that the deﬁnitions of P A 0 and f A0 are “independent of the representatives,” since the relation ▯ is a congruence with respect to P A 0and f A 0. For instance, if t ▯ t then ▯ ‘ t = t . 0 whence also ▯ ‘ f t ... t ... t = f t ... t ... t so that f t ... t ... t ▯ f t ... t ... t . It follows 0 1 n 0 1 n 1 n 1 n that f A ([t ],...,[t],...,[t ]) = f A ([t ],...,[t ],...,[t ]) and the deﬁnition is independent of the 1 n 1 n representative. Next, one easily shows that for each therm t, s(t) = [t] (by induction on t). Similarly, we prove that A j= ’[s] if and only if ’ 2 ▯ , whence in particular s satisﬁes ▯ . The proof that A j= ’[s] if 0 and only if ’ 2 ▯ is by induction on ’, the crucial case being the one for the universal quantiﬁer: ▯ If A 6j= [s], then for some term t, A 6j= 0 [s( =] x)], i.e., A 6j= [s(s(t= x)]. Using Lemma 65 (Change of Bound Variable), successively rename each quantiﬁer 8y in as needed to obtain a formula 0 such that t is free for x in 0and ‘ ▯ . It follows that A 6j= 0[s(s(t=x )], and by the Substitution Theorem (theorem 54), also A 6j= 0 0[ = x][s]. By the inductive hypothesis, 0[ = x] = ▯ , whence 8x 0 = ▯ . But by deductive closure and ‘ ▯ 0, we have 8x = ▯ . ▯ If 8x 2= ▯ , then by maximality ▯8x 2 ▯ , and by saturation for some c, also ▯ [ = x] 2 ▯ , so that by consistency [ = x] = ▯ . By the inductive hypothesis, A 6j= 0 [ =x][s], so that A 6j= 0 [s( s(c=x )] by the Substitution Theorem. The conclusion A 6j= 8x [s] follows. 0 Finally, let A be the structure for L obtained from A by dropping the interpretations of the new 0 constants c .nUsing induction of formulas ’ of L one can show that A j= ’[s] if and only if A j= ’[s], so that s satisﬁes ▯ in A. 81. Deﬁnition: A set ▯ of formulas is ﬁnitely satisﬁable if and only if every ﬁnite ▯ ▯ ▯ is satisﬁa0le. 82. Corollary: (Compactness Theorem) 19 (i) if ▯ j= ’ then there is a ﬁnite ▯ ▯ ▯ such that ▯ j= ’; 0 0 (ii) ▯ is satisﬁable if and only if it is ﬁnitely satisﬁable. Part IV Extensions and applications 9. Rudiments of model theory 83. Deﬁnition: A signature s is a set of predicate symbols, function symbols and individual constants. n n A structure A for s assigns subsets of A , functions from A to A, and members of A to the A signature s is a set of predicate symbols and individual constants in the signature. 84. Deﬁnition: Given signatures s ▯ t and a structure A for t, the reduct of A to s is the structure B obtained from A by dropping interpretations for the symbols in t but not in s. Similarly, we say that A is an expansion of B to t. 85. Deﬁnition: Given structures A and B for the same signature, we say that A is a substructure of B, and B an extension of A, written A ▯ B, if A▯ B and moreover: É For each constant c in the signature, c = c ;B É For each predicate symbol P and a ,.1.,a innA, P (a ,..1,a ) honds if and only if P (a ,..1,a ) n holds. A B É For each function symbol f in the signature and a ,.1.a innA, f (a ,...1 ) = n (a1,...,a n. 86. Remark: If the signature contains no constant or function symbols, then each A ▯ B determines a A B n substructure A of B with universe A by putting P = P \A . 87. Deﬁnition: If a structure A satisﬁes a set ▯ of sentences, then we say that A is a model of ▯. 88. Proposition: (Downward Löwenheim-Skolem Theorem) If ▯ is consistent then it has a countable model, i.e., it is satisﬁable in a structure whose domain is either ﬁnite or denumerably inﬁnite. Proof. If ▯ is consistent, the structure A delivered by the proof of Theorem 80 has a universe A whose 0 cardinality is bounded by that of the set of the terms of the language L . So A is at most denumerably inﬁnite. 89. Remark: (Skolem’s paradox) By the Löwenheim-Skolem theorem, Zermelo-Fränkel set theory, ZF, is satisﬁable in a countable structure, and yet ZF ‘ 9x(x is uncountable). 90. Theorem: If a set ▯ of sentences has arbitrarily large ﬁnite models, then it has an inﬁnite model. Proof. Expand the language of ▯ by adjoining countably many new constants c ,c ,... and consider . 0 1 the set ▯ [ f▯c i c : j 6= jg. To say that ▯ has arbitrarily large ﬁnite models means that for every . m > 0 there in n ▯ m such that ▯ has a model of cardinality n. This implies that ▯ [ f▯c = i : ij6= jg 20 . is ﬁnitely satisﬁable. By compactness, ▯ [ f▯c i c :ji 6= jg has a model A whose domain must be inﬁnite, since it satisﬁes all inequalities ▯c = c . i j 91. Proposition: There is no sentence ’ of any ﬁrst-order language L that is true in a structure A if and only if the domain A of the structure is inﬁnite. Proof. If there were such a ’, its negation ▯’ would be true in all and only the ﬁnite structures, and it would therefore have arbitrarily large ﬁnite models but it would lack an inﬁnite model, against Theorem 90. 92. Deﬁnition: Given two structures A and B for the same language L, we say that A is elementarily equivalent to B, written A ▯ B, if and only if for every sentence ’ of L, A j= ’ if and only if B j= ’. 93. Deﬁnition: Given two structures A and B for the same language L, we say that A is isomorphic to B, written A ’ B, if and only if there is a functihn: A! B such that: 1. h is one-one: ih(a ) = h (a ) then a = a ; 1 2 1 2 2. h is onto B: for every b 2 B there is a 2 A such tha(a) = b; A B 3. for every constant c:h(c ) = c ; A B 4. for every n-place predicate symbol P: h1 ,...,n i 2 P if and only ifh(a1),...,h(an)i 2 P ; 5. for every n-place function symbol f h(f (a 1...,a n) = f B (h(a1),...,h(an)). 94. Theorem: If A ’ B then A ▯ B. Proof. Leth be an isomorphism of A onto B; for any assignment s, h▯ s is the composition oh and s, i.e., the assignment in B such thath(▯s)(x) = h(s(x)). We proceed by induction on t ’ and prove the stronger claims: h(s(t)) =h ▯s(t); A j= ’[s] if and only if B j= ’h▯s]. Make sure to take note at each step of how each of the ﬁve properties characterizing isomorphisms is used. 95. Deﬁnition: Given a structure A, the theory of A is the setTh (A) of sentences that are true in A, i.e.Th (A) = f’ : A j= ’g. We also use the term “theory” informally to refer to sets of sentences having an intended interpretation, whether deductively closed or not. 96. Proposition: For any A, Th (A) is maximally consistent. Hence, if B j= for every 2 Th (A), then A ▯ B. 21 Proof. Th (A) is consistent because satisﬁable (by deﬁnition). It is maximal since for any sentence ’ either ’ is true in A or its negation is. It immediately followTh(A) ▯ Th (B) and Th (B) ▯ Th (A), whence A ▯ B. 97. Remark: Consider R = (R,<), the structure whose domain is the set R of the real numbers, in the language comprising only a 2-place predicate interpreted as the < relation over the reals. Clearly R is uncountable; however, since Th (R) is obviously consistent, by the Löwenheim-Skolem theorem it has a countable model, say S, and by Proposition 96, R ▯ S. Moreover, since R and S are not isomorphic, this shows that the converse of Theorem 94 fails in general. 98. Deﬁnition: Given two structures A and B, a partial isomorphism from A to B is a ﬁnite function p taking arguments in A and returning values in B, satisfying the isomorphism conditions from Deﬁnition 93 on its domain: 1. p is one-one; A A B 2. for every constant c: if c is in the domain of p, then p(c ) = c ; A 3. for every n-place predicate symbol P: if1a ,...na are in the domain of p, then 1a ,...na i 2 P B if and only if hp1a ),...,pna )i 2 P ; 4. for every n-place function symbol f : if a ,...,a are in the domain of p, then p(f (a ,...,a )) = 1 n 1 n fB (p(a1),...,p(an)). Notice that the empty map ? is a partial isomorphism between any two structures. 99. Deﬁnition: Two structures A and B, are partially isomorphic, written A ’ p, if and only if there is a non-empty set I of partial isomorphisms between A and B satisfying the back-and-forth property: 1. (Forth) For every p 2 I and a 2 A there is q 2 I such that p ▯ q and a is in the domain of q; 2. (Back) For every p 2 I and b 2 B there is q 2 I such that p ▯ q and b is in the range of q. 100. Theorem: If A ’ B and A and B are countable, then A ’ B. p Proof. Since A and B are countable, let A= fa0,a1,...g and B = fb0, 1 ,...g. Starting with an arbitrary p02 I, we deﬁne an increasing sequence of partial isomorphisms p ▯0p ▯ 1 ▯ ▯2▯ as follows: É if n+1 is odd, say n = 2r, then using the Forth property ﬁnd a n+1 2 I such that pn▯ p n+1 and aris in the domain of pn+1; É if n+1 is even, say n+1 = 2r, then using the Back property ﬁnd a p n+1 2 I such that pn▯ p n+1 and b is in the range of p . r n+1 If we now put: [ p= pn, n▯0 We have that p is a an isomorphism of A onto B. 101. Theorem: If A and B are structures in a purely relational signature (a signature containing only predicate symbols, and no function symbols or constants), then A ’ B, implies A ▯ B. p 22 Proof. By induction on formulas, one shows that if a ,...,a 1nd b ,.n., b ar1 such tnat there is a partial isomorphism p mapping each a to b aid s (i ) = a 1nd i (x )i= b (fo2 i i 1,...in), then A j= ’[s ] if and only if B j= ’[s ]. The case for n = 0 gives A ▯ B. 1 2 If function symbols are present, the previous result is stil true, but one needs to consider the iso- morphism induced by p between the substructure of A generated by a ,...,a and the substructure of 1 n B generated by b ,.1., b . nut we will not need this more general case in what follows. The previous result can be “broken down” in stages by establishing a connection between the num- ber of nested quantiﬁers in a formula and how many times the relevant partial isomorphisms can be extended. 102. Deﬁnition: For any formula ’, the quantiﬁer rank of ’, denoted by qr(’) 2 N, is recursively deﬁned as the highest number of nested quantiﬁers in ’. Two structures A and B are n-equivalent, written A ▯ Bn if they agree on a

### BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.

### You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

## Why people love StudySoup

#### "Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

#### "I used the money I made selling my notes & study guides to pay for spring break in Olympia, Washington...which was Sweet!"

#### "Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

#### "Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

### Refund Policy

#### STUDYSOUP CANCELLATION POLICY

All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email support@studysoup.com

#### STUDYSOUP REFUND POLICY

StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here: support@studysoup.com

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to support@studysoup.com

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.