I have to solve the following problem: Using $\exists$ Introduction prove that PA$\vdash x\leq y \wedge y\leq z \longrightarrow x\leq z$: I used that if $x\leq y$ then $\ \exists \ r\ x+r=y$ and in the same way $\exists t \ y +t=z$, but in logic term I don't know how to use these equalities and the Peano's axioms to get the result.

  • $\begingroup$ What are the axioms you are using for PA? The usual axioms for PA literally include the principle you are proving, because they include all the axioms of a discrete ordered semiring. If you are working with some other set of axioms (e.g. ones that do not include $\leq$) then it is necessary to say exactly what they are. $\endgroup$ – Carl Mummert Nov 4 '13 at 22:41
  • $\begingroup$ @CarlMummert: where are you getting your "usual axioms for PA" from? In all the accounts of PA that I know, $x \le y$ is an abbreviation for $\exists\,i\cdot x + i = y$. $\endgroup$ – Rob Arthan Nov 4 '13 at 23:01
  • $\begingroup$ @Rob Arthan: e.g. Richard Kaye, Models of Peano Arithmetic, Kossack/Schmerl Structure of Models of Peano Arithmetic, and other texts on PA use the signature of discretely ordered semirings. If some other axiomatization is intended, it would be less clear which axioms are included unless they are explicitly stated. For example, looking below, is associativity of addition then an axiom? It is an axiom of semirings. $\endgroup$ – Carl Mummert Nov 4 '13 at 23:54
  • 1
    $\begingroup$ @CarlMummert: I should have said that $x \le y$ is taken as an abbreviation in the usual introductory accounts of $PA$. In this case, I think it is reasonable to assume that the OP is looking at a presentation along the lines of en.wikipedia.org/wiki/… (which has equality as the only predicate symbol). $\endgroup$ – Rob Arthan Nov 9 '13 at 17:50

Well, you know that $x+r=y$ that $y+t=z,$ so, if we know that addition is associative, then it follows that $x+(r+t)=(x+r)+t=y+t=z.$ Since $r+t\in\Bbb N$ for any $r,t\in\Bbb N,$ then putting $s=r+t,$ we have shown that there exists $s$ such that $x+s=z,$ and so $x\le z$ by definition of the relation "$\le$."

All that we need to do, then, is show that addition is, in fact, associative, so that the above reasoning completes the proof of your result.

Claim: $\forall k,m,n\in\Bbb N,$ we have $(k+m)+n=k+(m+n).$

Proof Outline: Take any $k,m\in\Bbb N.$ We proceed by induction on $n,$ with the $n=0$ case being clear by two applications of property (vi) from your comment below. Suppose, then, that $$(k+m)+n=k+(m+n)$$ for some $n\in\Bbb N.$ It follows, then, with two applications of property (vii) from your comment below, that $$(k+m)+S(n)=k+\bigl(m+S(n)\bigr),$$ so by induction, the Claim holds. $\Box$

  • 1
    $\begingroup$ I need to use the Peano's axioms from a logic viewpoint. $\endgroup$ – Andres Bernal Nov 4 '13 at 19:51
  • $\begingroup$ I'm not quite sure what you mean. Do you have a result/definition that says $$x\le y \iff \exists r\:(x+r=y),$$ or do you only have a single direction of this implication? If you have only a single direction, then how is $x\le y$ defined? $\endgroup$ – Cameron Buie Nov 4 '13 at 19:54
  • $\begingroup$ I have $x \leq y \Longrightarrow \exists r(x+r=y)$ as a definition, but, what we really need to prove it by using the axioms. I understand what you are doing, but I need to derive the result using only logic Peano's axioms $\endgroup$ – Andres Bernal Nov 4 '13 at 20:12
  • $\begingroup$ Bear in mind that, in the case of definition, the implication is actually two-directional, as discussed here and here. By Peano's axioms, I presume you mean that (i) $0\in\Bbb N;$ (ii) for all $n\in\Bbb N,$ $S(n)\in\Bbb N;$ (iii) for all $n\in\Bbb N,$ $S(n)\ne 0;$ (iv) for all $m,n\in\Bbb N,$ if $S(m)=S(n),$ then $m=n;$ (v) [induction, in some form]. Am I correct in this? Also, how is addition defined for you? $\endgroup$ – Cameron Buie Nov 4 '13 at 20:22
  • $\begingroup$ The five you write are well, and there are also $vi) \forall x(x+0=x)$, $vii)\forall x\forall y(x+S(y)=S(x+y))$, for multiplication one have $viii)\forall x(x\times 0=0)$, $\forall x\forall y(x+S(y)=(x \times y+x))$, $x) \forall x(x^0=S(0))$, $xi) \forall x\forall y(x^{S(y)}=x^y \times x)$ $\endgroup$ – Andres Bernal Nov 4 '13 at 20:34

See Wikipedia Peano Axioms.

The point of this answer is to show that you can define an ordering of the natural numbers before you define addition.

Proposition 1: If $n$ is any number except $0$, there exist an $m$ such that

$n = S(m)$

Moreover, if the successor of both $m$ and $m^{'}$ is equal to $n$, then $m = m^{'}$.

Proof: Exercise


The Decrement mapping $D$

$ n \mapsto D(n)$

sends any nonzero number $n$ to $m$, where $S(m) = n$.

We also define $1$ to be $S(0)$. Note that $D(1) = 0$

Note for any nonzero $n$ we have the 'keep decrementing unless you can't' number expressions:

(1) $D(n)$, $D(D(n))$, $D(D(D(n)))$, ...

It is understood that this list might terminate since you can't apply $D$ to $0$.

Proposition 2: If $n$ is any nonzero number, the decrementing terms (1) ends in the number $0$.

Proof: It is true for $n$ = 1.

Assume it is true for $n$, and consider $S(n)$. But $D(S(n)) = n$, so that for $S(n)$, compared to the terms for $n$, you simply get a new starting term.


These logical expressions,

$m \ne n \;\; iff \;\; D(m) \ne D(n)$

are true provided both $m$ and $n$ are nonzero. By repeatedly applying Proposition 2 you will find that either $m$ or $n$ gets decremented to $0$ first.

Definition: If $m$ and $n$ are two distinct nonzero numbers, we say that $m$ is less than $n$, written $m \lt n$. if $m$ is decremented to zero before $n$.

We define the relation $\le$ in the obvious fashion and agree that for all natural numbers $n$, $\;0 \le n$.

Proposition 3: $x\leq y \wedge y\leq z \longrightarrow x\leq z$

Proof: Assume $x, y, z$ are three distinct nonzero numbers.

$x\leq y \wedge y\leq z \longrightarrow x\leq z$


$D(x)\leq D(y) \wedge D(y)\leq D(z) \longrightarrow D(x)\leq D(z)$

As before, you see that $x$ is decremented to zero before both $y$ and $z$, so that $x \le z$.

We leave it to the reader to finish the proof.

  • 1
    $\begingroup$ Your key definition ($<$ in terms of decrement) is not first-order. $\endgroup$ – Andrés E. Caicedo May 29 '17 at 15:10
  • 1
    $\begingroup$ It is irrelevant to the problem at hand, which specifically requires an argument in first-order PA. The decrement function is not first-order, and you really have not specified the fragment of PA where its (intended) definition takes place. Yes, you provide a link to a Wikipedia page, but the axiomatic system described there is first-order and includes $+$, so it is not at all clear what the system you are using is. $\endgroup$ – Andrés E. Caicedo May 29 '17 at 15:16
  • 1
    $\begingroup$ As stated, it is an informal definition. I think it could be formalized in second-order logic if you already have working integers. But doing that formalization without already have an ordering on those integers is going to be tricky. $\endgroup$ – Henning Makholm May 29 '17 at 15:16
  • 1
    $\begingroup$ @AndrésE.Caicedo: As far as I can see the problem at hand only says "Peano's axioms" -- and what Peano actually published was most like a second-order system. But I agree that the OP probably (3+ years ago) wanted something in first-order PA, without saying so specifically. $\endgroup$ – Henning Makholm May 29 '17 at 15:21
  • 1
    $\begingroup$ @HenningMakholm The existential introduction rule is first-order. $\endgroup$ – Andrés E. Caicedo May 29 '17 at 15:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.