I'm trying to reduce a simple theorem from number theory (i.e. there are infinitely many primes) to set theory. What do I need to read in order to achieve this? Are there any examples somewhere ? I want to deduce the truth of the theorem using only the axioms of Zermelo Frankel set theory. I know it is possible for most of the theorems. Thank you
$\begingroup$
$\endgroup$
2
-
1$\begingroup$ Do you want to do this for the sake of exercising formalization of things in ZFC, or for the sake of providing a proof that some elementary statements are provable in ZF? If it is the latter that you want, then why not work within Peano Arithmetic (PA) (which is simpler for your purposes), and then use some general result on ZF being able to carry over the same proofs? $\endgroup$– Iddo TzameretJul 1, 2010 at 14:33
-
$\begingroup$ Any clues on how to derive divisibility from Set Theory ? Thanks $\endgroup$– AndreiJul 6, 2010 at 15:17
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
Deducing a non-trivial theorem directly from ZFC is a tedious business. First you will need to define the integers in terms of sets. The natural numbers are most commonly encoded as von Neumann ordinals. Then you have to define addition and multiplication. These are functions, which are typically encoded as sets of ordered pairs from $\mathbb{N}\times\mathbb{N}$ to $\mathbb N$. An ordered pair is typically encoded as $(x,y) := \lbrace\lbrace x\rbrace,\lbrace x,y\rbrace\rbrace$. Then you will have to define primes, etc.
If you really want to go through this exercise, then I would recommend learning Mizar, which is a system for formal proofs. Mizar is based on Tarski-Grothendieck set theory, which is a slight extension of ZFC. Most of the groundwork that I've described above has already been done by previous users of Mizar, so that you just need to "drill down" through the existing definitions in order to figure out how to do things, and don't have to encode it all from scratch yourself.
answered Jul 1, 2010 at 14:11
$\begingroup$
$\endgroup$
You may find that just formally stating and proving that theorem from the axioms of Peano arithmetic (in the language with +, $\times$, 0, and 1) is somewhat challenging if you have never tried to do so before. It's not overly difficult with practice, though, because the techniques are somewhat routine for elementary number theory. One candidate for a formal statement of the theorem in PA is $$ (\forall m)(\exists p)(\exists t)\big[p = m + t +1+1\land (\forall r)(\forall s)(rs = p \Rightarrow (r = p \lor s = p))\big ] $$
Once you have proved the theorem in PA, the transition to ZFC is routine but long. As Timothy Chow says, you just define an interpretation of PA in ZFC and then rework your proof in PA into a proof in ZFC using this interpretation.
answered Jul 1, 2010 at 14:37
1
-
2$\begingroup$ Sections 12 to 13 in particular discuss the standard interpretation of arithmetic in ZFC. $\endgroup$ Jul 1, 2010 at 15:00