Results 1 to 3 of 3

Math Help - Enderton 3.3 Problem 2 (p223)

  1. #1
    Junior Member
    Joined
    Nov 2011
    Posts
    59

    Enderton 3.3 Problem 2 (p223)

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

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

    Proof in the textbook (incomplete)

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

    ================================================== ==============
    Lemma. For any variable-free term t, there is a unique number n such that 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.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Member
    Joined
    Aug 2011
    Posts
    127

    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 S^n0,when x = y, this follows from the axioms, and when x \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.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,527
    Thanks
    773

    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 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, A_E\vdash t=S^n0 and N\models t=S^n0. The latter fact means that N(t) = n, i.e., A_E\vdash t=S^{N(t)}0.

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

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

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

    Lemma 2(a) holds because A_E is a theory with equality. 2(b) is proved by regular mathematical induction on \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?
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Enderton 3.7 Problem 1
    Posted in the Discrete Math Forum
    Replies: 1
    Last Post: January 14th 2012, 09:55 AM
  2. Enderton 3.4 Problem 1
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: December 24th 2011, 06:17 AM
  3. Enderton 3.3 Problem 5
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: December 19th 2011, 07:34 AM
  4. Enderton 3.3 Problem 8
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: December 19th 2011, 05:46 AM
  5. Enderton 3.1 problem 1 (p.193)
    Posted in the Discrete Math Forum
    Replies: 8
    Last Post: December 4th 2011, 10:30 AM

Search Tags


/mathhelpforum @mathhelpforum