0
$\begingroup$

My question is how I show the corollary 32B(a) from the book A mathematical introduction to logic by Herbert Enderton. Corollary 32B(a) on page 196 says that:

Cn$A_{L}$ is complete.

where $A_{L}=(\mathbb{N};0,S,<)$ and $\text{Cn} A_L$ is the set $\{\sigma \mid A_L \models \sigma\}$ of consequences of $A_L$.

The proof of Corollary 32B(a) simply says:

The argument that followed the proof of Theorem 31G is applicable here also.,

Theorem 31G (on page 191) says that another theory admits quantifiers elimination, however I don't know how to write the proof of Corollary 32B(a) more formally.

$\endgroup$
5
  • 5
    $\begingroup$ You may get a wider audience if you don't require us to know what theorem 31G or CnAL are. $\endgroup$
    – John Douma
    Nov 14, 2020 at 0:57
  • 1
    $\begingroup$ Yes, you're right, although I mentioned the book. $\endgroup$ Nov 14, 2020 at 21:41
  • $\begingroup$ Your question does not seem to make sense. Under you definition, the theory you want to show is complete is just the set of sentences true in $\mathbf N$, so it is trivially complete. $\endgroup$
    – tomasz
    Nov 17, 2020 at 9:24
  • 1
    $\begingroup$ @tomasz - Indeed, this is a point I explained in my answer. The problem is that writing $A_L = (\mathbb{N}, 0, S , <)$ doesn't make sense. But, if everything were clear, what is the meaning of this site? Apart from that incoherence, the question is valid. $\endgroup$ Nov 17, 2020 at 9:32
  • $\begingroup$ @Taroccoesbrocco: It would be, yes. That is one of the reasons why we have the edit functionality. $\endgroup$
    – tomasz
    Nov 18, 2020 at 18:14

1 Answer 1

4
$\begingroup$

You don't have to use Theorem 31G (which states theory of natural numbers with successor admits elimination of quantifiers), but you have to develop an argument similar to the one explained after (the proof of) Theorem 31G on page 192, to show that from the elimination of quantifiers in $\text{Cn}A_L$(Theorem 32A) it follows that $\text{Cn}A_L$ is complete (Corollary 32B.a).


First, a clarification on what we are talking about. In Enderton's book (Chapter 3), $A_L$ is the finite set of axioms $\{S3, L1, L2, L3, L4, L5\}$ below, in the first-order language with a constant symbol $\mathbf{0}$, a unary function symbol $\mathbf{S}$ and a binary relation symbol $\mathbf{<}$. \begin{align} (S3)&&& \forall y \, (y \neq \mathbf{0} \to \exists x \, y = \mathbf{S}x) \\ (L1)&&& \forall x\forall y \, (x \mathbin{\mathbf{<}} \mathbf{S}y \leftrightarrow x \mathbin{\mathbf{\leq}} y) \\ (L2) &&& \forall x \ x \not\!\!\mathbin{\mathbf{<}} \mathbf{0} \\ (L3) &&& \forall x \forall y \, (x \mathbin{\mathbf{<}} y \lor y \mathbin{\mathbf{<}} x \lor x = y) \\ (L4) &&& \forall x \forall y \, (x \mathbin{\mathbf{<}} y \to y \mathbin{\not\!\!\mathbf{<}} x) \\ (L5) &&& \forall x \forall y \forall z \, (x \mathbin{\mathbf{<}} y \to y \mathbin{\mathbf{<}} z \to x \mathbin{\mathbf{<}} z) \end{align}

The structure $\mathfrak{N}_L = (\mathbb{N}; 0, S, <)$ interprets the symbols $\mathbf{0}$ (zero), $\mathbf{S}$ (successor) and $\mathbf{<}$ (order) as expected in the domain $\mathbb{N}$ of natural numbers.

When you write $A_L = (\mathbb{N}; 0, S, <)$ you are confusing two distinct notions: a finite set of axioms $A_L$ (a syntactic object) and a structure $\mathfrak{N}_L$ (a semantic object).

Clearly, $\mathfrak{N}_L$ is a model of $A_L$ and actually, $A_L$ finitely axiomatizes the theory of $\mathfrak{N}_L$ (i.e. $A_L$ is a finite axiomatization of the theory of natural numbers with successor and natural order), but this is not relevant to answer your question.

Notations: $\text{Cn} A_L$ is the set $\{\sigma \mid A_L \models \sigma\}$ of theorems (sentences) that can be proved starting from the axioms in $A_L$; while $\text{Th}\,\mathfrak{N}_L$ is the theory of $\mathfrak{N}_L$, i.e. the set of sentences that are true in the structure $\mathfrak{N}_L$.

Saying that of $\text{Cn} A_L$ is complete means that $A_L \models \sigma$ or $A_L \models \lnot \sigma$ for every sentence $\sigma$ in the first-order language with $\mathbf{0}$, $\mathbf{S}$ and $\mathbf{<}$.


How to prove that $\text{Cn} A_L$ is complete, knowing that $\text{Cn}A_L$ admits elimination of quantifiers? Let $\sigma$ be a sentence. The quantifier elimination procedure gives a quantifier-free sentence $\tau$ such that $$\tag{1} A_L \models (\sigma \leftrightarrow \tau).$$ Now, I claim that either $A_L \models \tau$ or or $A_L \models \lnot \tau$. Indeed, $\tau$ is built up from atomic sentences by means of $\lnot$ and $\to$. Any atomic sentence is of the form $\mathbf{S}^i\mathbf{0} = \mathbf{S}^j \mathbf{0}$ or $\mathbf{S}^i\mathbf{0} \mathop{\mathbf{<}} \mathbf{S}^j \mathbf{0}$. It can be easily proven that $A_L \models \mathbf{S}^i\mathbf{0} = \mathbf{S}^j \mathbf{0}$ if $i = j$, otherwise $A_L \models \lnot (\mathbf{S}^i\mathbf{0} = \mathbf{S}^j \mathbf{0})$ ($*$); similarly, $A_L \models \mathbf{S}^i\mathbf{0} \mathop{\mathbf{<}} \mathbf{S}^j \mathbf{0}$ if $i < j$, otherwise $A_L \models \lnot (\mathbf{S}^i\mathbf{0} \mathop{\mathbf{<}} \mathbf{S}^j \mathbf{0})$ ($**$). Thus, in $A_L$, every atomic sentence can be proved or refuted (i.e. its negation can be proved), so every quantifier-free sentence $\tau$ can be proved or refuted, and hence by $(1)$ every sentence $\sigma$ can be proved or refuted. Therefore, $A_L$ is complete.


($*$) Indeed, Enderton shows (p. 194) that $A_L \models S1$ and $A_L \models S2$ where \begin{align} (S1) &&& \forall x \ \mathbf{S}x \neq \mathbf{0} \\ (S2) &&& \forall x \forall y \, (\mathbf{S}x = \mathbf{S}y \to x = y) \end{align}

From that, it is easy to prove, by induction on $j \in \mathbb{N}$, that $A_L \models \mathbf{S}^i\mathbf{0} = \mathbf{S}^j \mathbf{0}$ if $i = j$, otherwise $A_L \models \lnot (\mathbf{S}^i\mathbf{0} = \mathbf{S}^j \mathbf{0})$.

Base case ($j = 0$ and hence $\mathbf{S}^j\mathbf{0} $ is $\mathbf{0}$). If $i = j = 0$, then $A_L \models \mathbf{0} = \mathbf{0}$ because $=$ is reflexive. Otherwise, $i \neq j = 0$ and hence $$A_L \models \mathbf{S} \overbrace{\mathbf{S} \dots \mathbf{S}}^{i-1 \text{ times}}\mathbf{0} \neq \mathbf{0}$$ because of $S1$, taking $x = \overbrace{\mathbf{S} \dots \mathbf{S}\mathbf{0}}^{i-1 \text{ times}}$.

Inductive case ($j>0$ and hence $\mathbf{S}^j\mathbf{0}$ is $ \mathbf{S}\overbrace{\mathbf{S} \dots \mathbf{S}}^{j-1 \text{ times}}\mathbf{0}$). If $i = 0 \neq j$, then $\mathbf{S}^i\mathbf{0}$ is $ \mathbf{0}$ and hence $$A_L \models \mathbf{0} \neq \mathbf{S} \overbrace{\mathbf{S} \dots \mathbf{S}}^{j-1 \text{ times}}\mathbf{0}$$ because of $S1$, taking $x = \overbrace{\mathbf{S} \dots \mathbf{S}\mathbf{0}}^{j-1 \text{ times}}$, and commutativity of $=$. Otherwise, $i > 0$ and hence $\mathbf{S}^i\mathbf{0} $ is $ \mathbf{S}\overbrace{\mathbf{S} \dots \mathbf{S}}^{i-1 \text{ times}}\mathbf{0}$. There are two sub-cases:

  1. If $ i = j$, then $\mathbf{S}^i \mathbf{0}$ and $ \mathbf{S}^j \mathbf{0}$ are the same term, and thus $A_L \models \mathbf{S}^i \mathbf{0} = \mathbf{S}^j \mathbf{0}$ by reflexivity of $=$.
  2. If $i \neq j$, then $\mathbf{S}^{i-1} \mathbf{0}$ and $\mathbf{S}^{j-1} \mathbf{0}$ are distinct terms, and $A_L \models \mathbf{S}^{i-1} \mathbf{0} \neq \mathbf{S}^{j-1} \mathbf{0}$ by the inductive hypothesis (since $i-1 \neq j-1$). Therefore, $$A_L \models \mathbf{S}\mathbf{S}^{i-1} \mathbf{0} \neq \mathbf{S}\mathbf{S}^{j-1} \mathbf{0}$$ according to (the contrapositive of) $S2$, taking $x = \mathbf{S}^{i-1} \mathbf{0}$ and $y = \mathbf{S}^{j-1} \mathbf{0}$.

The proof of ($**$) is analogous to the one for ($*$). You have to use properties similar to $S1$ and $S2$, concerning $\mathbf{<}$ instead of $\mathbf{S}$.

Hint. Axiom $L2$ seems very similar to $S1$.

$\endgroup$
3
  • $\begingroup$ Thanks for your help, but I don't understand one thing in your answer, how I show that $A_{L}\models\boldsymbol{S^{i}0}=\boldsymbol{S^{j}0}$ if $i=j$? $\endgroup$ Nov 14, 2020 at 21:38
  • $\begingroup$ @BrigitteEliana- I edited my answer to show also this point. $\endgroup$ Nov 15, 2020 at 13:35
  • $\begingroup$ Thanks for the help $\endgroup$ Nov 17, 2020 at 5:07

Not the answer you're looking for? Browse other questions tagged .