1

I need to create a formal proof of there not being the largest number, with only the definition of "less than" being given with Peano arithmetic. $s(x)$ means successor of $x$ or $x + 1$.

$$ \text{Premise}\\ \forall x\forall y (x \lt y \iff \exists z(x + s(z) = y)\\ \text{Prove}\\ \forall x \exists y (x < y) $$

I've tried proof by contradiction, but the resources online don't seem to translate well into a formal proof. In particular, the strategy of "assume there is a largest number, add one, done" doesn't really translate with formal proof steps.

Daniel Hast
  • 5,095
Kevin
  • 41
  • 4
    Can you prove $\forall x ~(x \lt s(x))$? – Robert Shore Mar 20 '21 at 23:18
  • I can try. I am only really allowed that premise, so I don't think I can use any of the other Peano rules. Also did you edit my question? I didn't know you could do that. – Kevin Mar 20 '21 at 23:20
  • Other MSE users with enough reputation can edit your questions, but I don't think Robert's edits are justifiable.I have flagged that. – Rob Arthan Mar 20 '21 at 23:43
  • 1
    It suffices to let $y=x+s(x)$. Then $x\lt y$ is guaranteed by letting $z=x$. – Barry Cipra Mar 20 '21 at 23:43
  • 1
    So do you actually need a pedantic formal first order logic explicit rules of inference proof, or are you looking for an informal proof where the arithmetic axioms are used explicitly but the rest is informal? – DanielV Mar 20 '21 at 23:55
  • 1
    I need the former. With only the premise I gave, I need to give explicit steps like $\forall$ elimination/introduction, $\exists$ elimination/introduction, etc. – Kevin Mar 21 '21 at 00:09
  • My main problem has been since the premise is a biconditional, I don't know how I would produce an absolute statement like x < y from that. The only other "relevant" topic in my class is Peano induction, but I don't really see how that would help – Kevin Mar 21 '21 at 00:15
  • From $\forall x \forall y( x < y \iff \exists z ( \dots))$ infer $x < y \iff \exists z ( \dots))$ then infer $\exists z (\dots) \to x < y$ then use that. – DanielV Mar 21 '21 at 00:16
  • I don't see how that second inference benefits me in any way. you're just saying the biconditional works the other direction. But that's still just a "conditional". You don't have any concrete information if that makes sense. – Kevin Mar 21 '21 at 00:36
  • @Kevin You should be able to tell that a statement of the form $A \to B$ is useful when you are trying to prove $B$. – DanielV Mar 21 '21 at 03:08
  • @RobArthan All I did was put the math formulas $s(x), x,$ and $x+1$ in MathJax. I don't know how those other words got removed, but I certainly didn't intend to do that. I think someone else may have been editing at the same time I was -- perhaps the two edits got combined somehow under my name. – Robert Shore Mar 21 '21 at 04:35
  • Do you know that $s(0)=1$? – Robert Shore Mar 21 '21 at 04:39
  • In response to your last comment, @DanielV I understand that if I know $A \to B$ and I have $A$, then I have $B$. In your example, $A$ would be $\exists z (x + s(z) = y)$ but I don't know where I could just pull that out of nowhere. My guess would be to assume $\neg A$ and try to get a contradiction. – Kevin Mar 21 '21 at 14:54

3 Answers3

1

Solved!

The key to solving this was with "creating the right half" of the original premise: $\exists z (x + s(z) = y)$

Kevin
  • 41
0

So you want to prove that for all $x$, there exists a $y$ such that $x$ is less than $y$. To do that, imagine you are given an $x$ (maybe $x=99$) and try to come up with a $y$ that is greater than $x$. How about $x + 1$ (i.e., $100$ if $x = 99$)? So there's your proof: as $y = x + 1 > x$ for any $x$, then for all $x$, there exists a $y$ such that $x < y$.

Proof by contradiction is best regarded as a last resort: to be used only if working forward from the positive information that you have isn't getting you anywhere.

Rob Arthan
  • 48,577
  • I really appreciate your response. Although since I need step-by-step proof steps like the universal introduction/elimination, I don't know if this translates so well – Kevin Mar 21 '21 at 00:54
0

Using the idea of Barry Cipra in the comments:

$$\forall x \exists y~(y=s(x)) \\ \forall x \exists y \exists w ~(x+y=x+s(x)=w) \\ (\forall x \exists z (=x)~(x +s(z)=w)) \Rightarrow x \lt w \Rightarrow \exists w~(x \lt w)$$

Robert Shore
  • 23,332
  • I don't entirely understand this, especially the last step. But your first line seems to just come from nowhere. May I remind you that I only get the definition of less than. I could just assume that first step, but that doesn't really help I don't think. – Kevin Mar 21 '21 at 15:51
  • The first step just says that $s$ is a function that is defined on your entire domain on discourse. The last step is modus ponens. – Robert Shore Mar 21 '21 at 17:38