Day 1: the axioms (L10) to (L15), the rule of generalization, and Fitch deductions with quantifiers and equality. Day 2: the Deduction Theorem for first-order logic, consistency, and the Soundness Theorem.
By the end of this week you will be able to:
Today we extend the deduction system of propositional logic with two axioms for \(\forall\), two axioms for equality, two axioms for \(\exists\) and the rule of generalization, and we write deductions in the new system.
Last week \(\Gamma\models\varphi\) was defined through all structures, and a proof of \(\Gamma_{\mathrm{gr}}\models\varphi\) was an argument about an arbitrary group. As in propositional logic, there is a second way to connect \(\Gamma\) and \(\varphi\): a finite list of formulas in which every line is an axiom, an assumption, or follows from earlier lines by a rule. Structures play no role in this definition. A theorem of mathematics is a first-order consequence of axioms, and its proof, written out in full, is such a list.
The formulas are those of a first-order language \(\mathcal L(\mathcal S)\). The connectives \(\neg,\wedge,\vee,\to\) keep their axioms (L1) to (L9) of Definition 8.24. The quantifiers \(\forall\) and \(\exists\) and equality get axioms of their own.
An axiom is any instance of one of the following fifteen schemes. Here \(\varphi,\psi,\chi\) are formulas of \(\mathcal L(\mathcal S)\), \(x\) and \(y\) are variables and \(t\) is a term.
| Group | Name | Axiom scheme | Side condition |
|---|---|---|---|
| Implication | (L1) | \(\varphi\to(\psi\to\varphi)\) | |
| (L2) | \((\varphi\to(\psi\to\chi))\to((\varphi\to\psi)\to(\varphi\to\chi))\) | ||
| Negation | (L3) | \((\neg\psi\to\neg\varphi)\to(\varphi\to\psi)\) | |
| Conjunction | (L4) | \((\varphi\wedge\psi)\to\varphi\) | |
| (L5) | \((\varphi\wedge\psi)\to\psi\) | ||
| (L6) | \(\varphi\to(\psi\to(\varphi\wedge\psi))\) | ||
| Disjunction | (L7) | \(\varphi\to(\varphi\vee\psi)\) | |
| (L8) | \(\psi\to(\varphi\vee\psi)\) | ||
| (L9) | \((\varphi\to\chi)\to((\psi\to\chi)\to((\varphi\vee\psi)\to\chi))\) | ||
| Quantifier \(\forall\) | (L10) | \(\forall x\,\varphi\to\varphi[t/x]\) | \(t\) is free for \(x\) in \(\varphi\) |
| (L11) | \(\forall x\,(\varphi\to\psi)\to(\varphi\to\forall x\,\psi)\) | \(x\) is not free in \(\varphi\) | |
| Equality | (L12) | \(x=x\) | |
| (L13) | \(x=y\to(\varphi\to\varphi')\) | \(\varphi\) is atomic; \(\varphi'\) results from \(\varphi\) by replacing any number of occurrences of \(x\) by \(y\) | |
| Quantifier \(\exists\) | (L14) | \(\varphi[t/x]\to\exists x\,\varphi\) | \(t\) is free for \(x\) in \(\varphi\) |
| (L15) | \(\forall x\,(\varphi\to\psi)\to(\exists x\,\varphi\to\psi)\) | \(x\) is not free in \(\psi\) |
There are two rules of inference.
Each new axiom and the new rule say something we accept about \(\forall\), about \(\exists\) or about \(=\).
(L1) to (L9) are the axioms of Definition 8.24, now with first-order formulas in place of \(\varphi,\psi,\chi\). Everything that was deduced from them with MP in Weeks 8 and 9 used the schemes only, so it stays available: in Fitch deductions we keep citing hypothetical syllogism (HS, Proposition 8.36) and Lemmas 9.4 and 9.5. The schemes (L10) to (L15) are new: no axiom about the connectives knows anything about \(\forall\), \(\exists\) or \(=\). (L14) and (L15) mirror (L10) and (L11), in the same way as the axioms for \(\vee\) mirror those for \(\wedge\).
Let \(\Gamma\) be a set of formulas of \(\mathcal L(\mathcal S)\). A deduction from \(\Gamma\) is a finite sequence of formulas \(\varphi_1,\dots,\varphi_n\) such that for each \(1\le i\le n\), either
We write \(\Gamma\vdash\varphi\) if there is a deduction from \(\Gamma\) whose last line is \(\varphi\), and \(\vdash\varphi\) for \(\varnothing\vdash\varphi\). In Fitch notation the justifications are (assump.), the name of the axiom, (\(j,k\) MP) and (\(j\) Gen).
An instance of (L10), (L11), (L14) or (L15) is an axiom only if its side condition holds. The side condition is part of the axiom, and it has to be checked each time.
Self-check only. Nothing here counts towards your grade.
For each formula decide whether it is an instance of the named axiom scheme. Check the side condition.
(a) Yes: \(t:=z\), and \(z\) is free for \(x\) in \(\exists y\,(x<y)\).
(b) No: \(t\) would be \(y\), which is captured by \(\exists y\).
(c) Yes: \(t:=y\). Only the free occurrence of \(x\), the one in \(P(x)\), is replaced; \(\forall x\,Q(x)\) is not touched, and no quantifier on \(y\) is present.
(d) Yes: \(t:=y\). The formula \(R(x,y)\) has no quantifier, so every term is free for \(x\) in it. That \(y\) already occurs in \(R(x,y)\) does not matter.
(e) No: the two occurrences of \(x\) in \(R(x,x)\) would have to be replaced by the same term, and \(R(x,y)\) replaces them by \(x\) and by \(y\).
(f) No: \(x\) is free in \(P(x)\).
(g) Yes: \(x\) is not free in \(P(y)\).
(h) Yes: \(\varphi\) is the atomic formula \(f(x)<x\), and \(f(y)<x\) replaces the first occurrence of \(x\) by \(y\).
(i) No: \(\neg(x<z)\) is not atomic. The formula is deducible, from the instance \(y=x\to(y<z\to x<z)\) of (L13), symmetry of equality and contraposition, but it is not an axiom.
(j) Yes: \(\varphi\) is \(R(x,y)\) and \(t:=y\); there is no quantifier in \(R(x,y)\) that could capture \(y\).
(k) No: \(\varphi\) is \(\exists y\,(x<y)\) and \(t\) would be \(y\), which is captured by \(\exists y\).
(l) No: \(x\) is free in the consequent \(Q(x)\).
Most deductions with quantifiers have three phases: remove the quantifiers with (L10), reason with the connectives as in propositional logic, and put the quantifiers back with Gen.
Lines 3 and 5 are instances of (L10) with \(t:=x\), as in Example 13.3(b). Lines 4, 6 and 7 use only MP. Line 8 puts the quantifier back.
Compare this with the proof of the same fact for \(\models\) in Example 12.26(d). There we took an arbitrary element \(a\), concluded \(Q(\bar a)\), and said "as \(a\) was arbitrary". The free variable \(x\) on lines 4 to 7 plays the role of the arbitrary element, and Gen on line 8 is the sentence "as \(a\) was arbitrary".
Let \(y\) be a variable that does not occur in \(\varphi\). Then \(\vdash\forall x\,\varphi\to\forall y\,\varphi[y/x]\).
Line 1: since \(y\) does not occur in \(\varphi\), no quantifier of \(\varphi\) can capture it, so \(y\) is free for \(x\) in \(\varphi\). Line 3 is (L11) with \(\forall x\,\varphi\) in the role of \(\varphi\), \(\varphi[y/x]\) in the role of \(\psi\) and \(y\) in the role of \(x\); the side condition holds because \(y\) is not free in \(\forall x\,\varphi\). For example, \(\vdash\forall x\,P(x)\to\forall y\,P(y)\).
Lines 2 to 4 show how (L11) is used: Gen puts a quantifier in front of an implication, and (L11) moves it to the consequent.
Two patterns from these examples are used so often that we state them once.
Proof. (a) Extend a deduction of \(\varphi\) from \(\Gamma\) by three lines: \(\forall x\,\varphi\) (Gen), \(\forall x\,\varphi\to\varphi[t/x]\) (L10), and \(\varphi[t/x]\) (MP).
(b) Extend a deduction of \(\varphi\to\psi\) from \(\Gamma\) by three lines: \(\forall x\,(\varphi\to\psi)\) (Gen), \(\forall x\,(\varphi\to\psi)\to(\varphi\to\forall x\,\psi)\) (L11), and \(\varphi\to\forall x\,\psi\) (MP). □
\(\vdash\forall x\,\forall y\,\varphi\to\forall y\,\forall x\,\varphi\), for every formula \(\varphi\).
Lines 1 and 2 remove the two quantifiers, each with (L10) and the variable itself as the term. Lines 4 to 6 put \(\forall x\) back in front of the consequent, and lines 7 to 9 do the same for \(\forall y\). The side conditions of (L11) on lines 5 and 8 hold because neither \(x\) nor \(y\) is free in \(\forall x\,\forall y\,\varphi\). With Lemma 13.6(b) the deduction is described in three steps: line 3, then Lemma 13.6(b) for \(x\), then Lemma 13.6(b) for \(y\).
\(\forall x\,(P(x)\to Q(x))\vdash\exists x\,P(x)\to\exists x\,Q(x)\).
The ordinary proof reads: take an \(x\) with \(P(x)\); then \(Q(x)\), so something has \(Q\). Lines 2 to 5 deduce "if \(P(x)\), then something has \(Q\)" for a free \(x\); line 4 is (L14) with \(t:=x\). Line 6 generalizes, and line 7 is (L15) with \(\psi:=\exists x\,Q(x)\), in which \(x\) is not free. Gen followed by (L15) is the step "take an \(x\) with \(P(x)\)".
In the same way, (L10) and (L14) with \(t:=x\) and HS give \(\vdash\forall x\,\varphi\to\exists x\,\varphi\), the formula of Example 12.26(b).
The axioms (L12) and (L13) are enough to deduce the usual properties of equality.
\(\vdash\forall x\,\forall y\,(x=y\to y=x)\).
Line 2 is (L13) with the atomic formula \(\varphi:=(x=x)\); \(\varphi'\) replaces the first occurrence of \(x\) by \(y\) and is \(y=x\). Lines 3 to 7 remove the middle antecedent \(x=x\), which we have on line 1: this is the pattern (L2), MP, (L1), MP, MP of Week 8. Lines 8 and 9 generalize.
Transitivity needs one instance of (L13) and one propositional step: \(y=z\to(x=y\to x=z)\) is an instance of (L13) for the variables \(y,z\) and the atomic formula \(x=y\), and swapping the two antecedents (Lemma 9.4(b)) gives \(\vdash x=y\to(y=z\to x=z)\).
(L12) and (L13) speak about variables. For terms we use Lemma 13.6(a). For example, for any term \(t\):
For all terms \(r,s,t\):
Proof. (a) is the deduction above. For (b), choose variables \(x,y\) that do not occur in \(s\) or \(t\). Lines 1 to 7 of Example 13.9 show \(\vdash x=y\to y=x\). This formula has no quantifiers, so every term is free for every variable in it. Lemma 13.6(a) with \(s\) for \(x\) gives \(\vdash s=y\to y=s\), and then with \(t\) for \(y\) it gives \(\vdash s=t\to t=s\); the second substitution does not change \(s\), because \(y\) does not occur in \(s\).
(c) and (d) are proved in the same way. For (c), start from \(\vdash x=y\to(y=z\to x=z)\) with variables that do not occur in \(r,s,t\). For (d), choose \(x,y\) that do not occur in \(\varphi\), \(s\) or \(t\); then \(x=y\to(\varphi[x/z]\to\varphi[y/z])\) is an instance of (L13), and substituting \(s\) for \(x\) and then \(t\) for \(y\) gives (d). □
The group axioms (G1), (G2), (G3) of Example 12.11 are sentences, and \(\Gamma_{\mathrm{gr}}\) is the set of these three sentences. A proof in group theory is a deduction from \(\Gamma_{\mathrm{gr}}\). We write one out.
Claim: \(\Gamma_{\mathrm{gr}},\ \forall x\,(x\cdot u=x\wedge u\cdot x=x)\vdash u=e\).
The algebra proof is one line: \(u=e\cdot u=e\). The first equality holds because \(e\) is an identity, by (G2) applied to \(u\). The second holds because \(u\) is an identity, by the assumption applied to \(e\). In the deduction, only (G2) is needed from \(\Gamma_{\mathrm{gr}}\).
Lines 3 to 6 are the step "\(e\cdot u=u\) by (G2)": (L10) with \(t:=u\), then (L5) to take the second part of the conjunction. Lines 7 to 10 are the step "\(e\cdot u=e\) by the assumption": (L10) with \(t:=e\), then (L4). Lines 11 to 13 are the step "therefore \(u=e\)": line 11 is Proposition 13.10(d) with \(s:=e\cdot u\), \(t:=u\) and the atomic formula \(z=e\), so that \(\varphi[s/z]\) is \(e\cdot u=e\) and \(\varphi[t/z]\) is \(u=e\).
Every step of the algebra proof became a short block of lines, and nothing else was needed. The deduction contains no step that looks at a particular group.
The side conditions of the quantifier axioms are easy to forget, and a deduction that ignores them can lead from true assumptions to a false conclusion.
In both cases the conclusion is not a semantic consequence of the assumptions. On Day 2 we prove that a correct deduction can never do this, so no correct deduction of these conclusions exists.
Before you write (L10), check that the term is free for the variable: no variable of \(t\) may fall into the scope of a quantifier on that variable. The same check is needed for (L14). Before you write (L11), check that \(x\) is not free in the antecedent \(\varphi\); before you write (L15), check that \(x\) is not free in the consequent \(\psi\).
Self-check only. Nothing here counts towards your grade.
Each of the four lists of formulas is a deduction. For each line choose the justification. For MP and HS enter the two line numbers, in either order; for Gen enter the one line number.
(a)
(b) Line 2 is (L10) with \(t:=y\). Lines 4 to 6 are the pattern of Lemma 13.6(b): Gen, (L11), MP. The side condition of (L11) holds because \(y\) is not free in \(P(c)\).
(c) Lines 2 to 4 are the pattern of Lemma 13.6(a): Gen, (L10), MP. Line 3 is (L10) with \(t:=f(x)\); the formula \(x=x\) has no quantifier, so \(f(x)\) is free for \(x\) in it.
(d) Line 1 is (L13) with the atomic formula \(P(x)\). Lines 2 to 4 replace the variable \(x\) by the constant \(c\), again by Gen, (L10) and MP.
Today we adapt the Deduction Theorem to the rule of generalization, and then we prove that every formula deducible from a set of sentences is true in every model of the set.
In propositional logic, \(\Gamma,\varphi\vdash\psi\) holds if and only if \(\Gamma\vdash\varphi\to\psi\) (Theorem 9.9). With the rule Gen, the direction from left to right is no longer true without a condition.
\(P(x)\vdash\forall x\,P(x)\), by a deduction with two lines:
But \(P(x)\to\forall x\,P(x)\) is not valid. Take the structure \(\mathcal A\) with domain \(\{0,1\}\) and \(P^{\mathcal A}=\{0\}\). A formula with a free variable is true in \(\mathcal A\) when its universal closure is, and \(\forall x\,(P(x)\to\forall x\,P(x))\) is false in \(\mathcal A\): for the element \(0\), the sentence \(P(\bar 0)\) is true and \(\forall x\,P(x)\) is false. By the Soundness Theorem of Section 9, a formula that is not valid is not deducible. So \(\nvdash P(x)\to\forall x\,P(x)\), although \(P(x)\vdash\forall x\,P(x)\).
The reason is the Gen step on line 2. As an assumption, \(P(x)\) is treated by Gen as if it had been established for an arbitrary \(x\). As the antecedent of an implication, \(P(x)\) speaks about one object \(x\).
Let \(\Gamma\) be a set of formulas and \(\varphi,\psi\) formulas.
Proof. (a) As in Theorem 9.9: a deduction of \(\varphi\to\psi\) from \(\Gamma\) is a deduction from \(\Gamma\cup\{\varphi\}\); add the lines \(\varphi\) (assump.) and \(\psi\) (MP).
(b) Call a deduction from \(\Gamma\cup\{\varphi\}\) admissible if Gen is never applied in it to a variable that is free in \(\varphi\). The first \(m\) lines of an admissible deduction form an admissible deduction, because MP and Gen only cite earlier lines. We prove by strong induction on \(n\ge1\): if \(\psi_1,\dots,\psi_n\) is an admissible deduction, then \(\Gamma\vdash\varphi\to\psi_n\).
Suppose the statement holds for all admissible deductions with fewer than \(n\) lines, and let \(\psi_1,\dots,\psi_n\) be admissible. There are four cases for the last line \(\psi_n\).
Case 1: \(\psi_n\) is an axiom or a member of \(\Gamma\). Then \(\psi_n\), \(\psi_n\to(\varphi\to\psi_n)\) (L1), \(\varphi\to\psi_n\) (MP) is a deduction from \(\Gamma\).
Case 2: \(\psi_n=\varphi\). Then \(\Gamma\vdash\varphi\to\varphi\) by Example 8.27.
Case 3: \(\psi_n\) follows by MP from \(\psi_i\) and \(\psi_j=\psi_i\to\psi_n\) with \(i,j<n\). By the induction hypothesis, \(\Gamma\vdash\varphi\to\psi_i\) and \(\Gamma\vdash\varphi\to(\psi_i\to\psi_n)\). The instance \((\varphi\to(\psi_i\to\psi_n))\to((\varphi\to\psi_i)\to(\varphi\to\psi_n))\) of (L2) and two applications of MP give \(\Gamma\vdash\varphi\to\psi_n\).
Case 4: \(\psi_n=\forall x\,\psi_i\) follows by Gen from \(\psi_i\) with \(i<n\). The deduction is admissible, so \(x\) is not free in \(\varphi\). By the induction hypothesis there is a deduction of \(\varphi\to\psi_i\) from \(\Gamma\), with \(m\) lines say. Add three lines:
| \(m+1\) | \(\forall x\,(\varphi\to\psi_i)\) | (\(m\) Gen) |
| \(m+2\) | \(\forall x\,(\varphi\to\psi_i)\to(\varphi\to\forall x\,\psi_i)\) | (L11) |
| \(m+3\) | \(\varphi\to\forall x\,\psi_i\) | (\(m+1,\ m+2\) MP) |
Line \(m+2\) is an axiom because \(x\) is not free in \(\varphi\). This is the only place where the condition is used. The result is a deduction of \(\varphi\to\psi_n\) from \(\Gamma\). □
Cases 1 to 3 are the proof of Theorem 9.9. Case 4 is new, and it is the reason why (L11) is among the axioms.
If \(\varphi\) is a sentence, then \(\Gamma,\varphi\vdash\psi\) if and only if \(\Gamma\vdash\varphi\to\psi\).
Proof. A sentence has no free variables, so every deduction from \(\Gamma\cup\{\varphi\}\) satisfies the condition of Theorem 13.14(b). □
The axioms of a mathematical theory are sentences, and so are most statements that are assumed in the course of a proof. For them the Deduction Theorem works exactly as in propositional logic. The condition matters only when an assumption has a free variable.
Self-check only. Nothing here counts towards your grade.
Each item shows a deduction from \(\Gamma\cup\{\varphi\}\). Decide whether Theorem 13.14(b) applies to this deduction.
(a) It does not apply: line 2 generalizes \(x\), which is free in \(P(x)\). This is Example 13.13.
(b) It applies: the only Gen step generalizes \(y\), and \(y\) is not free in \(P(x)\). So \(\forall y\,(P(x)\to Q(y))\vdash P(x)\to\forall y\,Q(y)\).
(c) It applies: \(\varphi\) is a sentence, so it does not matter which variable is generalized.
(d) It applies: line 2 generalizes \(z\), and the free variables of \(R(x,y)\) are \(x\) and \(y\). So \(\vdash R(x,y)\to\forall z\,R(x,y)\).
(e) It does not apply: line 6 generalizes \(z\), which is free in \(z<y\).
A set of formulas \(\Gamma\) is inconsistent if there is a formula \(\varphi\) with \(\Gamma\vdash\varphi\) and \(\Gamma\vdash\neg\varphi\). Otherwise \(\Gamma\) is consistent.
This is Definition 9.21 with the new \(\vdash\). For example, \(\{\forall x\,P(x),\ \neg P(c)\}\) is inconsistent, with \(\varphi:=P(c)\): the formula \(\neg P(c)\) is an assumption, and
\(\Gamma\) is inconsistent if and only if \(\Gamma\vdash\psi\) for every formula \(\psi\).
Proof. (\(\Leftarrow\)) Take any formula \(\varphi\); then \(\Gamma\vdash\varphi\) and \(\Gamma\vdash\neg\varphi\). (\(\Rightarrow\)) Let \(\Gamma\vdash\varphi\) and \(\Gamma\vdash\neg\varphi\), and let \(\psi\) be any formula. By Lemma 9.5(a), \(\vdash\neg\varphi\to(\varphi\to\psi)\). Two applications of MP give \(\Gamma\vdash\psi\). □
If the group axioms \(\Gamma_{\mathrm{gr}}\) were inconsistent, every sentence about groups would be a theorem, and the theory would be worthless. To show that \(\Gamma_{\mathrm{gr}}\) is consistent we would have to show that among the infinitely many deductions from \(\Gamma_{\mathrm{gr}}\) no two end in \(\varphi\) and \(\neg\varphi\). Inspecting deductions one by one cannot do this. The Soundness Theorem can.
From here on \(\Gamma\) is a set of sentences. A deduction from \(\Gamma\) may still contain formulas with free variables, such as lines 4 to 7 of Example 13.4. By Definition 12.23 a formula \(\varphi\) with free variables \(x_1,\dots,x_n\) is true in a structure \(\mathcal A\) when \(\forall x_1\cdots\forall x_n\,\varphi\) is, that is, when the sentence \(\varphi[\bar a_1/x_1,\dots,\bar a_n/x_n]\) is true in \(\mathcal A\) for all \(a_1,\dots,a_n\in A\). We call these sentences the closed instances of \(\varphi\) in \(\mathcal A\). So
\(\mathcal A\models\varphi\) if and only if every closed instance of \(\varphi\) in \(\mathcal A\) is true in \(\mathcal A\).
For example, the closed instances of \(P(x)\to Q(x)\) in a structure with domain \(\{0,1\}\) are \(P(\bar 0)\to Q(\bar 0)\) and \(P(\bar 1)\to Q(\bar 1)\). A sentence is its own only closed instance.
The proof of soundness has the same three parts as in propositional logic (Lemma 9.15, Lemma 9.16, Theorem 9.17): the axioms are true, the rules preserve truth, and an induction puts the two together. One fact about substitution is needed first.
Let \(\mathcal A\) be a structure, \(t\) a closed term of \(\mathcal L(\mathcal S_A)\) and \(a=[\![t]\!]_{\mathcal A}\). Then for every formula \(\varphi\) of \(\mathcal L(\mathcal S_A)\) with no free variable other than \(x\): \[\mathcal A\models\varphi[t/x]\quad\text{if and only if}\quad\mathcal A\models\varphi[\bar a/x].\]
Proof. By induction on the number of connectives and quantifiers in \(\varphi\). The terms \(t\) and \(\bar a\) have the same value \(a\). The value of a compound term is computed from the values of its parts (Definition 12.21), so \(s[t/x]\) and \(s[\bar a/x]\) have the same value for every term \(s\) with no variable other than \(x\). The truth of an atomic sentence depends only on the values of its terms (Definition 12.23), so the claim holds for atomic \(\varphi\). For a formula built with a connective the claim follows from the claim for the parts. For \(\forall y\,\psi\) with \(y\) different from \(x\): \(\mathcal A\models(\forall y\,\psi)[t/x]\) iff \(\mathcal A\models\psi[\bar b/y][t/x]\) for every \(b\in A\), iff \(\mathcal A\models\psi[\bar b/y][\bar a/x]\) for every \(b\in A\) (induction hypothesis for \(\psi[\bar b/y]\)), iff \(\mathcal A\models(\forall y\,\psi)[\bar a/x]\). The case \(\exists y\,\psi\) is the same with "some \(b\)" in place of "every \(b\)". For \(\forall x\,\psi\) and \(\exists x\,\psi\) there is no free \(x\), and both substitutions leave the formula unchanged. □
Example 12.26(a) used a case of this lemma: \(P(c)\) and \(P(\bar a)\) with \(a=c^{\mathcal A}\) have the same truth value.
If \(\alpha\) is an instance of (L1) to (L15), then \(\mathcal A\models\alpha\) for every structure \(\mathcal A\).
Proof. Let \(\mathcal A\) be a structure. We show that every closed instance of \(\alpha\) in \(\mathcal A\) is true.
(L1) to (L9). A closed instance of an instance of (L1) is again of the form \(\varphi\to(\psi\to\varphi)\), now with sentences \(\varphi,\psi\). By Definition 12.23 the truth value of a sentence built with \(\neg,\wedge,\vee,\to\) is computed from the truth values of its parts as in a truth table, and the scheme is a tautology (Lemma 9.15). The same holds for (L2) to (L9).
(L10). A closed instance of \(\forall x\,\varphi\to\varphi[t/x]\) has the form \(\forall x\,\varphi^*\to\varphi^*[t^*/x]\), where \(\varphi^*\) is \(\varphi\) with names in place of its free variables other than \(x\), and \(t^*\) is \(t\) with names in place of all its variables. So \(\varphi^*\) has no free variable other than \(x\), and \(t^*\) is a closed term. Here the side condition is used: since \(t\) is free for \(x\) in \(\varphi\), the variables of \(t\) are still free in \(\varphi[t/x]\), so they are replaced by names. Now suppose \(\mathcal A\models\forall x\,\varphi^*\). Then \(\mathcal A\models\varphi^*[\bar a/x]\) for every \(a\in A\), in particular for \(a=[\![t^*]\!]_{\mathcal A}\). By Lemma 13.19, \(\mathcal A\models\varphi^*[t^*/x]\).
(L11). A closed instance has the form \(\forall x\,(\varphi^*\to\psi^*)\to(\varphi^*\to\forall x\,\psi^*)\). Since \(x\) is not free in \(\varphi\), \(\varphi^*\) is a sentence. Suppose \(\mathcal A\models\forall x\,(\varphi^*\to\psi^*)\) and \(\mathcal A\models\varphi^*\). For every \(a\in A\) the sentence \((\varphi^*\to\psi^*)[\bar a/x]\) is \(\varphi^*\to\psi^*[\bar a/x]\), and it is true; hence \(\mathcal A\models\psi^*[\bar a/x]\). So \(\mathcal A\models\forall x\,\psi^*\).
(L14). A closed instance has the form \(\varphi^*[t^*/x]\to\exists x\,\varphi^*\), with \(\varphi^*\) and \(t^*\) as for (L10); the side condition is used in the same way. If \(\mathcal A\models\varphi^*[t^*/x]\), then \(\mathcal A\models\varphi^*[\bar a/x]\) for \(a=[\![t^*]\!]_{\mathcal A}\) by Lemma 13.19, so \(\mathcal A\models\exists x\,\varphi^*\).
(L15). A closed instance has the form \(\forall x\,(\varphi^*\to\psi^*)\to(\exists x\,\varphi^*\to\psi^*)\). Since \(x\) is not free in \(\psi\), \(\psi^*\) is a sentence. Suppose \(\mathcal A\models\forall x\,(\varphi^*\to\psi^*)\) and \(\mathcal A\models\exists x\,\varphi^*\). Then \(\mathcal A\models\varphi^*[\bar a/x]\) for some \(a\in A\). The sentence \((\varphi^*\to\psi^*)[\bar a/x]\) is \(\varphi^*[\bar a/x]\to\psi^*\), and it is true; hence \(\mathcal A\models\psi^*\).
(L12). A closed instance is \(\bar a=\bar a\), which is true because both sides have the value \(a\).
(L13). A closed instance is \(\bar a=\bar b\to(\varphi^*\to\varphi'^*)\), where the atomic sentence \(\varphi'^*\) results from \(\varphi^*\) by replacing some occurrences of \(\bar a\) by \(\bar b\). If \(\mathcal A\models\bar a=\bar b\), then \(a=b\), so corresponding terms of \(\varphi^*\) and \(\varphi'^*\) have the same values, and the two atomic sentences have the same truth value. □
The proof shows what goes wrong in Example 13.12(a). The formula \(\forall x\,\exists y\,(x<y)\to\exists y\,(y<y)\) is a sentence, and it is its own closed instance. Its consequent is not of the form \(\varphi^*[t^*/x]\) for a closed term \(t^*\): the substituted \(y\) was captured and could not be replaced by a name.
Let \(\mathcal A\) be a structure.
Proof. (a) Take a closed instance \(\psi^*\) of \(\psi\). Choose elements of \(A\) for the free variables of \(\varphi\) that are not free in \(\psi\); this is possible because \(A\) is not empty. Together they give closed instances \(\varphi^*\) of \(\varphi\) and \(\varphi^*\to\psi^*\) of \(\varphi\to\psi\). Both are true in \(\mathcal A\), so \(\psi^*\) is true in \(\mathcal A\).
(b) A closed instance of \(\forall x\,\varphi\) has the form \(\forall x\,\varphi^*\), where \(\varphi^*\) has no free variable other than \(x\). It is true in \(\mathcal A\) iff \(\varphi^*[\bar a/x]\) is true for every \(a\in A\). Each \(\varphi^*[\bar a/x]\) is a closed instance of \(\varphi\), and these are all true by assumption. □
Part (b) is about all closed instances together. From one true instance \(P(\bar 0)\) nothing follows about \(\forall x\,P(x)\). Gen is correct because a line of a deduction from sentences is true for all values of its free variables, as the next proof shows.
Let \(\Gamma\) be a set of sentences and \(\varphi\) a formula. If \(\Gamma\vdash\varphi\), then \(\Gamma\models\varphi\).
Proof. Let \(\mathcal A\) be a model of \(\Gamma\). We prove by strong induction on \(n\ge1\): if \(\psi_1,\dots,\psi_n\) is a deduction from \(\Gamma\), then \(\mathcal A\models\psi_n\).
Suppose this holds for all deductions with fewer than \(n\) lines, and let \(\psi_1,\dots,\psi_n\) be a deduction from \(\Gamma\). The first \(i\) lines form a deduction from \(\Gamma\) for every \(i<n\), so \(\mathcal A\models\psi_i\) for every \(i<n\).
Now let \(\Gamma\vdash\varphi\). The last line of a deduction of \(\varphi\) is true in \(\mathcal A\), and \(\mathcal A\) was an arbitrary model of \(\Gamma\). So \(\Gamma\models\varphi\). □
Figure 2 shows how the parts of the proof fit together and what follows from the theorem.
Let \(\Gamma\) be a set of sentences and \(\varphi\) a formula.
Proof. (a) is the theorem for \(\Gamma=\varnothing\), and (c) is its contrapositive. (b) Let \(\mathcal A\models\Gamma\), and suppose \(\Gamma\vdash\varphi\) and \(\Gamma\vdash\neg\varphi\). By the theorem, \(\mathcal A\models\varphi\) and \(\mathcal A\models\neg\varphi\). Take a closed instance \(\varphi^*\) of \(\varphi\). Then \(\varphi^*\) and \(\neg\varphi^*\) are both true in \(\mathcal A\), which is impossible. □
For a claim \(\Gamma\vdash\varphi\) with sentences \(\Gamma\) there are now two tools, as in Week 9: a deduction shows that the claim holds, and a structure shows that it fails.
Soundness goes in one direction. If you search for a deduction and do not find one, nothing is proved; only a structure as in Corollary 13.23(c) proves \(\Gamma\nvdash\varphi\). And if \(\Gamma\models\varphi\), soundness does not provide a deduction.
Is there always one? If a sentence is true in every model of \(\Gamma\), can it be deduced from \(\Gamma\) with these fifteen axiom schemes and two rules? For propositional logic the answer was yes (Week 10). For first-order logic the answer is also yes. This is the Completeness Theorem, proved by Kurt Gödel in 1929, and it is the subject of Week 14.
Self-check only. Nothing here counts towards your grade.
For each claim decide whether it holds. If it does not, build a structure on the domain \(\{0,1,2\}\) that shows this by the Soundness Theorem: tick the elements of \(P^{\mathcal A}\) and \(Q^{\mathcal A}\) and the pairs of \(E^{\mathcal A}\) (row \(a\), column \(b\) for \((a,b)\)). The page evaluates the assumption and the conclusion in your structure.
(a) Deducible:
(b) Not deducible: \(P^{\mathcal A}=\{0\}\), \(Q^{\mathcal A}=\{1,2\}\). Every element is in \(P^{\mathcal A}\) or \(Q^{\mathcal A}\), but neither \(\forall x\,P(x)\) nor \(\forall x\,Q(x)\) is true.
(c) Deducible:
(d) Not deducible: \(P^{\mathcal A}=\{0\}\). Some element has \(P\), not all.
(e) Not deducible: \(E^{\mathcal A}=\{(0,1),(1,2),(2,0)\}\). Every element points somewhere, and no element is pointed to by all three.
(f) Deducible. Line 4 is (L10) for the variable \(y\) with \(t:=x\); \(x\) is free for \(y\) in \(E(x,y)\).
There is no homework for Week 13 because of the Thanksgiving break. The next homework will be assigned in Week 14.