9
$\begingroup$

Euclid's proof of the infinitude of primes requires me to take an arbitrary finite set of primes and multiply them together. If I want to formalize this proof in Peano Arithmetic, I need to know that any finite set of numbers has a product. Carl Mummert's comment on Russell O'Connor's answer to this question points out that this is trickier than it sounds, since "finite" means "indexed by a natural number", which is not the same thing as "indexed by a standard natural number". So one needs an inductive definition of the product to prove it exists.

The obvious inductive definition is:

$$\prod_{k=1}^{S(n)}a_k = a_{S(n)}\prod_{k=1}^n a_k$$

where I write $S$ for "successor". Is this enough to fill the "gap" in Euclid's proof, or am I missing something? (I ask because, in the discussion linked above, there seems to be a hint that it's not quite this simple.)

Improve this question
$\endgroup$
8
  • 1
    $\begingroup$ I think what you need is totality of exponentiation (to code tuples). $\endgroup$
    – user5810
    Commented Sep 20, 2011 at 21:10
  • 2
    $\begingroup$ You need to be precise about what symbols you have in your version of PA. If you are using first order sentences concerning $+$, $\times$, $0$, $1$, $=$ etcetera, then it is quite a challenge to even represent the concept of a finite set of integers. I blogged about this at sbseminar.wordpress.com/2009/12/07/… If your notation lets you talk about finite sets, then life is easier and you can roughly do what you say. $\endgroup$
    – David E Speyer
    Commented Sep 20, 2011 at 21:54
  • 2
    $\begingroup$ IIRC the proof is formalized in even weaker theories e.g. $\mathsf{I\Delta_0}+Exp$. Coding finite sets is not difficult if you use a goof coding, e.g. write number in binary, add symbol 2 between them, read the resulting string in base 4. $\endgroup$
    – Kaveh
    Commented Sep 20, 2011 at 22:11
  • $\begingroup$ @Kaveh: I'm wondering -- why do you call it a "goof" coding? $\endgroup$
    – The_Sympathizer
    Commented Sep 21, 2011 at 1:30
  • 2
    $\begingroup$ Mike: D and F are adjacent on US (and Canadian, since Kaveh is in Toronto) keyboards. $\endgroup$
    – François G. Dorais
    Commented Sep 21, 2011 at 1:36

2 Answers 2

Reset to default
14
$\begingroup$

The definition of iterated product is the easy part of the proof, the bottleneck is elsewhere. Even quite weak theories of bounded arithmetic, such as PV (this is an open theory with function symbols for polynomial-time functions), can prove that the product of a sequence of natural numbers exists (and is divisible by each element of the sequence), by formalizing the usual inductive definition in a straightforward way.

The next thing you need is to show that every number greater than one is divisible by a prime. PV is not known (and not expected) to prove this, but it is provable in the slightly stronger theory $S^1_2$. Thus, $S^1_2$ can formalize Euclid’s proof as the statement “there is no sequence containing all primes”.

As Carl noted, this is not a very natural rendering of the statement “there are infinitely many primes” (especially in weak theories, where sequences can only have logarithmic length). The statement one really wants to prove is “the set of primes is unbounded”. In order to infer this from Euclid’s proof, you need the principle that any bounded set can be put in a sequence, and this is equivalent to the axiom that exponentiation is total. Thus, formalization of Euclid’s proof in this sense can be done in $I\Delta_0+\mathrm{EXP}$ (and a fortiori in very strong theories like PRA).

It is possible to prove that there exist unboundedly many primes in theories weaker than $I\Delta_0+\mathrm{EXP}$, but this requires a much more elaborate proof than Euclid’s. Paris, Wilkie and Woods have shown the unboundedness of primes in the theory $I\Delta_0+\Omega_1$ (where $\Omega_1$ roughly says that $x^{\log x}$ exists for every $x$), and more precisely, in its subtheory $I\Delta_0+\mathrm{WPHP}(\Delta_0)$ (the latter is the weak pigeonhole principle: there is no $\Delta_0$-definable injection from $[0,2x]$ to $[0,x]$). It can be seen that their proof actually goes through in the theory $S^1_2+\mathrm{rWPHP}(\Theta)$ (itself included in $T^3_2$ and $S^4_2$), where $\Theta$ is the set of provably total $\Sigma^b_2$-definable functions of $S^1_2$ (which coincides with functions from the complexity class $\mathrm{FP}^{\mathrm{NP}[\mathrm{wit},\log n]}$), and $\mathrm{rWPHP}(\Theta)$ is a version of WPHP where the injection is supplied with an explicit retraction, both coming from $\Theta$. To the best of my knowledge, this is the weakest theory known to prove the unboundedness of primes.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Do you know if Sylvester's theorem (described at the end of that article) is also provable in $\hspace{1.09 in}$ that "weakest theory known ... unboundedness of primes"? $\;$ $\endgroup$
    – user5810
    Commented Sep 22, 2013 at 10:20
  • $\begingroup$ A reasonable guess is that Sylvester’s theorem is provable in this or a slightly stronger theory, but I haven’t read Alan Woods’s PhD thesis to verify this. I may look at it later. $\endgroup$
    – Emil Jeřábek
    Commented Sep 28, 2013 at 15:15
  • $\begingroup$ I have convinced myself that Woods’s proof of Sylvester’s theorem can be formalized in $S^1_2+\mathrm{rWPHP}(\Theta)$, with the caveat that the weak pigeonhole principle needs to be stated as going from something like $x+x/\log x$ to $x$ rather than from $2x$ to $x$. (These kinds of variants are often equivalent, but in this case I don’t think that the needed amplification can be carried out in $S^1_2$, one would need to raise the base theory to $T^1_2$.) $\endgroup$
    – Emil Jeřábek
    Commented Sep 30, 2013 at 15:45
  • $\begingroup$ Also, what I wrote about “the weakest theory known” is not literally true. $I\Delta_0+\mathrm{WPHP}(\Delta_0)$ is (likely) incomparable with $S^1_2+\mathrm{rWPHP}(\Theta)$: the latter includes the totality of the $\omega_1$ function (not provable in the former theory), while apart from that, it has induction and WPHP for a much smaller class of formulas. $\endgroup$
    – Emil Jeřábek
    Commented Sep 30, 2013 at 15:51
  • 1
    $\begingroup$ @DavidRoberts You can find a proper definition in §V.4(b) of Hájek&Pudlák, Metamathematics of first-order arithmetic. But briefly, $S^1_2$ is a subtheory of $I\Delta_0+\Omega_1$ whose main axiom is a form of induction for formulas expressing NP predicates; it’s not the usual induction schema (which would give the stronger theory $T^1_2$), but the so-called polynomial induction schema $\phi(0)\land\forall x\,(\phi(\lfloor x/2\rfloor)\to\phi(x))\to\forall x\,\phi(x)$. In some ways, the relationship of $S^1_2$ to PV is similar to the relationship of $I\Sigma_1$ to PRA. $\endgroup$
    – Emil Jeřábek
    Commented Jul 20, 2020 at 7:15
13
$\begingroup$

Two points. The first is that one theory that is sufficient for the task is PRA - primitive recursive arithmetic - or any theory that interprets it. The definition in the question works fine in that setting. There are weaker theories where you can code things, as well. The key point is that in PRA there is a definable unary function Set($n)$ which says $n$ codes a "finite" set, and a definable binary relation Element($n$,$k)$ which says that $n$ is an element of the set coded by $k$. These have the property that for every $l$ in any model of PRA there is a $k$ which codes the "finite" set of numbers $n < l$ that are prime.

This sort of coding requires quite a bit of work to set up, but it is viewed as completely routine unless you try to really plumb the depths of the weakest possible theory. PRA is already an extremely weak theory.

Second, there is some benefit to rephrasing things before formalizing them. Rather than proving "no finite set of primes includes all the primes", it is more natural in arithmetic to prove "the set of primes is not bounded". These are equivalent in the real world, but the latter entirely avoids the issue of coding finite sets. We still have to prove, by induction, that for every $k$ there is an $n$ that is a multiple of every prime less than $k$ (using the method from the question to define $k!$); that if $a | n$ then $a \not | n+1$; and that every number has a prime factor. None of these requires coding finite sets.

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ I agree about benefiting from avoiding sets, because coding is an unpleasant distraction. On the other hand, it may be worth noting that the proof outlined in Carl's third paragraph uses $\Sigma^0_1$ induction (to get the existence of something like factorials), and that this much induction would also suffice to code finite sets if one wanted to. So what one gains by avoiding sets is not a reduction in the needed axioms but rather a clearer view of the essentials of the proof. $\endgroup$
    – Andreas Blass
    Commented Sep 21, 2011 at 13:01

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .