1

Euclid's Theorem is the statement that there is no largest prime. We might put it this way in first-order logic:

∀x ∃y (y >= x & Prime(y))

An informal proof is pretty straightforward:

Let n be an arbitrary natural number and try to prove that there exists a prime number at least as large as n. To prove this, let k be the product of all the prime numbers less than n. Thus each prime less than n divides k without remainder. So now let m = k + 1. Each prime less than n divides m with remainder 1. But we know that m can be factored into primes. Let p be one of these primes. Clearly, by the earlier observation, p must be greater than or equal to n. Hence, by existential generalization, we see that there does indeed exist a prime number greater than or equal to n. But n was arbitrary, so we have established our result.

How do we write out every step used in the informal proof above, specifying the first-order logic rule of inference used?

My attempt is below. I do not believe that it is correctly utilizing the methods of proof, especially general conditional proof.

The domain of discourse is all natural numbers.

-- Assumption: Let n be an object from the domain of discourse, ie an arbitrary natural number.

-- 1 Assumption: Let k be the product of all prime numbers less than n.

-- 2 Lemma from basic axioms about real numbers: Therefore each prime less than n divides k without remainder.

-- 3 Assumption: Let m = k + 1

-- 4 Lemma from basic axioms about real numbers: Then each prime less than n divides m with remainder 1.

-- 5 Lemma from number theory: m can be factored into primes.

---- 6 Assumption: Let p be one of such prime factors of m.

------ 7 Assumption: p is less than n.

------ 8 Then p is one of the primes that are smaller than n.

------ 9 Then p divides m with remainder 1.

------ 10 Then p is not a factor of m.

------ 11 Contradiction

---- 12 Negation Introduction: p is greater than or equal to n.

---- 13 & Intro: Prime(p) & p >= n

---- 14 ∃ Intro: ∃x (Prime(x) & x >= n)

-- 15 ∀ Intro: ∀n ∃x (Prime(x) & x >= n)

16 ∀ Intro: ∀n ∀n ∃x (Prime(x) & x >= n)

17 ∀n ∃x (Prime(x) & x >= n)

Specifically, I make assumptions on lines 1 and 3 that I would guess are the assumptions of conditional proofs. Are they?

Notice what happened between lines 6 and 14: I used a general conditional proof (GCP): I made an assumption where I named an arbitrary object of the domain of prime numbers, and I concluded a property about that arbitrary number, namely that ∃x (Prime(x) & x >= n). Then I applied universal generalization on line 15 to obtain the conclusion I ultimately want. But at that point I am still in a subproof that is using GCP. So I apply universal generalization again on line 16, which gives me two universal quantifiers in sequence ∀n ∀n, which is the same as having just one of them, so I conclude with 17.

Now, this seems like it can't be the most elegant way, even considering my approach.

Improve this question
5
  • 1
    Following your proof outline, your line 14 should be already outside its previous subproof since it's a ∃-Intro jump based on your assumption line 6. Then you no longer need line 15... Also seems you invoked too many assumptions, your assumption 1 & 3 ought to be dispensed as they can be fully expressed from previous assumptions in any reasonable 1st order number theory such as the usual PA...
    – Double Knot
    Commented Jan 22, 2022 at 3:18
  • I spent two hours writing it all out. The attempt in my question seems quite incorrect at this point. I am posting an answer with my written attempt. I think that the written answer is on the right track, though it seems that I may have missed certain details because with the need to express certain ideas in math, things get complicated quickly, even for such a relatively simple theorem. I realized the amount of lemmas used for simple results that are sort of implicit in the informal proof I provided.
    – xoux
    Commented Jan 22, 2022 at 5:39
  • The thing I have with "assumptions 1 & 3 ought to be dispensed" is that I noticed how there is really a subjective line separating what can be taken for granted and what can't. I agree that the number theory results should all not be in a proof of Euclid's Theorem made for anyone with a minimum level of knowledge of natural numbers. But adding them at this point in my learning of logic showed me what a lemma is and why its useful (I think).
    – xoux
    Commented Jan 22, 2022 at 5:55
  • This question would be much better placed on math.stackexchange.com, already alone because there is MathJax over there but not here.
    – Arno
    Commented Jan 22, 2022 at 9:18
  • @Arno I would tend to disagree. The point of the question is to understand the inference rules of first-order logic as applied to a real-world problem. It happens to be a math theorem, but it is a pretty simple math theorem, and the results it depends on are simple enough that anyone who studied philosophy in university has knowledge of them. In the Math Stack Exchange I would bet that there would be less people than here that know the details of FOL inference. I could be wrong though. I completely agree about the MathJax though.
    – xoux
    Commented Jan 22, 2022 at 10:22

1 Answer 1

Reset to default
2

Another attempt at this proof showed me the meaning of "in all gory detail". Here it is:

Page 1

Page 2

I do not believe that every statement in this proof is written completely correctly, in particular the mathematical formulas. I translated them to English in purple, but I wanted to write them out mathematically so I could see which quantifiers were used, so I could know which inference rules to use.

The interesting things here to me are:

  • How nested existential eliminations sort of cascade a result from the innermost subproof out to the outermost one.

  • The need to use lemmas, which are statements that have already been proven elsewhere and will aid the current proof. The lemmas are basic results from number theory I believe.

  • Just how many lemmas are taken for granted in a relatively simple math proof.

Improve this answer
2
  • 1
    Fair observations about Lemma invocations in a math theorem proof as termed by Gentzen’s cut rule in his sequent calculus, otherwise math proofs will quickly get extremely verbose if demanded as the cut-eliminated ideal way. It’s reflected in the difficulty of automated theorem prover and proof search industry. Also how to represent the general recursive functions in any reasonable arithmetic theory such as PA is nontrivial as shown by Godel’s numbering and incompleteness theorems…
    – Double Knot
    Commented Jan 23, 2022 at 1:39
  • 1
    In PA with signature (0, S, +, ×) to express and further represent the property of "a prime number less than n" is nontrivial as the following open wff: ψ(x, n)=x≠S(0)∧∃w(w≠0∧w+x=n)∧∀u∀v(u×v=x→(u=S(0)∨v=S(0))), where all the involved quantifiers are bounded actually. Then you can further express the product of all those primes < n using some nontrivial primitive recursive function via Godel's β function. One can see the complexity to follow any deduction system from this, and linear Hilbert system is best suited for math proofs...
    – Double Knot
    Commented Jan 23, 2022 at 22:51

You must log in to answer this question.

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