Welcome to MathOverflow

Question

4

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

edited Jul 1 2010 at 14:12

Timothy Chow
14.6k●1●68●137

asked Jul 1 2010 at 13:25

Andrei
41●1

1

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? – Iddo Tzameret Jul 1 2010 at 14:33

Any clues on how to derive divisibility from Set Theory ? Thanks – Andrei Jul 6 2010 at 15:17

Timothy Chow · Answer 1 · 2010-07-01 14:11:40Z UTC

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.

Carl Mummert · Answer 2 · 2010-07-01 14:53:57Z UTC

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.

supercooldave · Answer 3 · 2010-07-01 13:33:26Z UTC

2

Naive Set Theory by Paul Halmos could help provide a naive solution.

answered Jul 1 2010 at 13:33

supercooldave
1,314●8●13

2

Sections 12 to 13 in particular discuss the standard interpretation of arithmetic in ZFC. – Carl Mummert Jul 1 2010 at 15:00

reducing a theorem to set theory using first order logic

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

3 Answers

You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.