Enderton 3.3 Problem 2 (p223)

Prove Theorem 33C, stating that true (in $\displaystyle N$) quantifier-free sentences are theorems of $\displaystyle A_E.$

================================================== ========

Theorem 33C. For any quantifier-free sentence $\displaystyle \tau$ true in $\displaystyle N$, $\displaystyle A_E \vdash \tau$.

Proof in the textbook (incomplete)

Start with the atomic sentences; these will be of the form $\displaystyle t_1 = t_2$ or $\displaystyle t_1 < t_2$ for variable-free terms $\displaystyle t_1$ and $\displaystyle t_2$. Show that $\displaystyle A_E$ proves $\displaystyle \tau$ if $\displaystyle \tau$ is true in $\displaystyle N$, and refutes $\displaystyle \tau$ (i.e., proves $\displaystyle \neg \tau$) if $\displaystyle \tau$ is false in $\displaystyle N$.

================================================== ==============

Lemma. For any variable-free term t, there is a unique number n such that $\displaystyle A_E \vdash t = S^n0$.

================================================== ==============

The necessary definitions can be found in here. (slide 4 and 5)

Any hint that I can start with will be appreciated.

Re: Enderton 3.3 Problem 2 (p223)

I suspect most people trolling this subforum have Enderton's logic book. :)

Anyway. You're supposed to show that everything you can say about natural numbers with 0, successor, less-than, addition, multiplication, and exponentiation, has a proof from the axioms you're given. You need to do this inductively. Start with the two predicates = (from logic) and < and prove that for x and y of the form **$\displaystyle S^n0$**,when x = y, this follows from the axioms, and when x $\displaystyle \ne$ y, this also follows from the axioms; then do the same for <.

To prove it works for anything with +, show it works for x + 0 = x (and fails for the rejection), then apply induction to 0. There's really a lot to do, though, so I don't want to go through every single step. The basic idea is you're providing a framework where (4+2) * 5 + 2 = 2^5 is proven true by the axioms (which it is), by changing (4+2) to 6, 6 * 5 to 30, 30 + 2 to 32, 2^5 to 32, and evaluates 32=32 as true...and also evaluates all false predicate resolutions as false. So you just need to translate the operations into terms that only have S and 0 in some effective fashion.

Re: Enderton 3.3 Problem 2 (p223)

For a variable-free term t, let's write N(t) to denote the natural number that is the interpretation of t in N. The proof for atomic sentences consists of two parts. The first is a slight strengthening of the lemma on slide 7.

Lemma 1. For any variable-free term t, it is the case that $\displaystyle A_E \vdash t = S^{N(t)}0$.

This can be proved by modifying the inductive proof of the original lemma. Alternatively, by soundness theorem and the original lemma, for each variable-free term t there exists a number n such that, $\displaystyle A_E\vdash t=S^n0$ and $\displaystyle N\models t=S^n0$. The latter fact means that $\displaystyle N(t) = n$, i.e., $\displaystyle A_E\vdash t=S^{N(t)}0$.

The second part is what we need to prove, but only for terms of the form $\displaystyle S^n0$.

Lemma 2.

(a) If $\displaystyle N\models S^{n_1}0=S^{n_2}0$, then $\displaystyle A_E\vdash S^{n_1}0=S^{n_2}0$.

(b) If $\displaystyle N\not\models S^{n_1}0= S^{n_2}0$, then $\displaystyle A_E\vdash S^{n_1}0\ne S^{n_2}0$.

Lemma 3.

(a) $\displaystyle N\models S^{n_1}0<S^{n_2}0$, then $\displaystyle A_E\vdash S^{n_1}0<S^{n_2}0$.

(b) $\displaystyle N\not\models S^{n_1}0<S^{n_2}0$, then $\displaystyle A_E\vdash\neg S^{n_1}0<S^{n_2}0$.

Lemma 2(a) holds because $\displaystyle A_E$ is a theory with equality. 2(b) is proved by regular mathematical induction on $\displaystyle \max(n_1,n_2)$ using S1 and S2, similar to the lemma on slide 6. Lemma 3 can be proved from the lemma on slide 6 and Lemma 2.

Can you finish the proof for the atomic sentences?