reducing a theorem to set theory using first order logic - MathOverflow

reducing a theorem to set theory using first order logic

2010-07-01T13:25:06Z

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

Answer by supercooldave for reducing a theorem to set theory using first order logic

2010-07-01T13:33:26Z

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

Answer by Timothy Chow for reducing a theorem to set theory using first order logic

2010-07-01T14:11:40Z

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.

Answer by Carl Mummert for reducing a theorem to set theory using first order logic

2010-07-01T14:37:40Z

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.