The full theorem I am trying to prove is as follows:

Thm: By induction on $x \in \omega$, where $\omega = $ the set of natural numbers including 0, show that if $x \neq \emptyset$ is a natural number, then it has a predecessor: a number $y$ which is largest among all numbers smaller than $x$, and such that $x = s(y)$. Call this statement $P(x)$.

Proof: Base case: $x$ = {$\emptyset$}. Then let $y = \emptyset$, and observe that $y = s(x)$, and $y$ is the largest such natural number as required.

Induction step: Assume $P(x)$ holds. We want to show that $P(s(x))$ holds. I'm not sure how to go about this. We do not have a definition for cardinality yet, so I am assuming by "large" they are referring to the linear ordering of "$\in$" on $\omega$, but I can't see how to make this definition work for my purposes. What am I not seeing?

  • $\begingroup$ First, this isn't really elementary set-theory, but elementary number theory. Second, the claim to be proven is so trivial, that it is hard to see what can and can not be allowed as premises to this proof. I mean, if you cannot assume the truth of this trivial claim, then what can we assume? Could you maybe indicate what assumptions you are allowed to make? Do you need to do this on the basis of the Peano Axioms, for example? $\endgroup$ – Bram28 Sep 24 '17 at 18:53
  • $\begingroup$ @Bram28 I'm allowed to use ZFC axioms. It's in a set theory class. We have just constructed the natural numbers, and are now proving properties of them through the lens of set theory. $\endgroup$ – IgnorantCuriosity Sep 24 '17 at 19:06
  • $\begingroup$ Ah! OK, now your reference to set theory makes sense as well, I should have guessed! Still, maybe it is good to list some of the relevant axioms, as well as the definitions of the natural numbers, and possibly some other basic theorems you have already proven that can be used? $\endgroup$ – Bram28 Sep 24 '17 at 19:27

Your Answer

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

Browse other questions tagged or ask your own question.