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.