reducing a theorem to set theory using first order logic - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-25T06:13:56Z http://mathoverflow.net/feeds/question/30182 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/30182/reducing-a-theorem-to-set-theory-using-first-order-logic reducing a theorem to set theory using first order logic Andrei 2010-07-01T13:25:06Z 2010-07-01T14:53:57Z <p>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</p> http://mathoverflow.net/questions/30182/reducing-a-theorem-to-set-theory-using-first-order-logic/30183#30183 Answer by supercooldave for reducing a theorem to set theory using first order logic supercooldave 2010-07-01T13:33:26Z 2010-07-01T13:33:26Z <p><a href="http://www.amazon.com/Naive-Theory-Undergraduate-Texts-Mathematics/dp/0387900926" rel="nofollow"><em>Naive Set Theory</em></a> by Paul Halmos could help provide a naive solution.</p> http://mathoverflow.net/questions/30182/reducing-a-theorem-to-set-theory-using-first-order-logic/30188#30188 Answer by Timothy Chow for reducing a theorem to set theory using first order logic Timothy Chow 2010-07-01T14:11:40Z 2010-07-01T14:11:40Z <p>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 <a href="http://planetmath.org/encyclopedia/VonNeumannOrdinal.html" rel="nofollow">von Neumann ordinals</a>. 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.</p> <p>If you really want to go through this exercise, then I would recommend learning <a href="http://mizar.uwb.edu.pl/" rel="nofollow">Mizar</a>, 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.</p> http://mathoverflow.net/questions/30182/reducing-a-theorem-to-set-theory-using-first-order-logic/30189#30189 Answer by Carl Mummert for reducing a theorem to set theory using first order logic Carl Mummert 2010-07-01T14:37:40Z 2010-07-01T14:53:57Z <p>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 ]$$</p> <p>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. </p>