2

How can one formalize Euclid's theorem (i. e. that there are infinitely many prime numbers) in Peano-Arithmetic (firstorder)?

asdfusername
  • 59

1 Answers1

2

$$\forall x(\exists y > x)[y > 1 \land (\forall w \leq y)(\forall z \leq y)(w \times z = y \to (w = 1 \lor z = 1))]$$

For any number $x$, there is a larger number $y$ which is prime, i.e. greater than one and such that for any pair of factors $w, z$ one of them has to be unity.

Depending on how you have set up the formal language for PA, you'll then need to unpack the restricted quantifiers in your favoured way -- but that's routine.

You don't need, strictly speaking, to restrict the third and fourth quantifiers: but regimenting "$y$ is prime" by

$$y > 1 \land (\forall w \leq y)(\forall z \leq y)(w \times z = y \to (w = 1 \lor z = 1)))$$

makes it clear that primeness is a so-called $\Delta_0$ property, that doesn't require unbounded quantifiers in its definition -- you can settle primeness without any unbounded searches.

(Fine print: you don't need the $y > 1$ clause in the first formula above, as because of the initial quantifiers you get something equivalent without it: but if you want to "follow the English" more closely then you should include it.)

Peter Smith
  • 54,743
  • According your definition, 1 is a prime number. Can you fix this bug? – asdfusername Jul 13 '15 at 12:34
  • @asdfusername Ah, the dangers of cut'n'paste again! – Peter Smith Jul 13 '15 at 13:08
  • Am I right? Is 1 a prime number according your definition? – asdfusername Jul 13 '15 at 13:33
  • If you look you'll see I have already "fixed the bug" by adding the clause $y > 1$ in the final para. It is evidently redundant in the initial formula for that is indeed true iff there are infinitely many primes. You could add it of course. – Peter Smith Jul 13 '15 at 13:37
  • Thanks. And why don't you need the $y>1$ clause in the initial formula? What do you mean with this sentence? Do you mean that it wouldn't change the truth of the Euclid-statement? – asdfusername Jul 13 '15 at 13:49
  • With or without that clause gives something provably equivalent. But OK, we can add it to make the ensuing English gloss read closer to the formal version, which is probably on reflection a good thing! – Peter Smith Jul 13 '15 at 14:28
  • 1
    Why is your definition of 'prime number' equivalent to the normal definition? – asdfusername Jul 13 '15 at 16:06
  • The definition of $y$ is prime, given in the last formula, is equivalent to the standard definition if we assume that factors of a number are not greater than that number. – Peter Smith Jul 13 '15 at 17:08