∞-many primes

• Hover cursor over text of this color to see a popup reference for the symbol or name. Click elsewhere to make the popup disappear.
• Expand and collapse sections of the argument using the

, and other buttons.
• The axioms used to prove a given lemma (including the main Goal) are listed before the lemma or as children of the lemma. The ones listed before are those that define or introduce symbols that are used in the statement of the lemma (i.e. the ones that are required for understanding the lemma).
• An Assertion is an axiom that I expect to be uncontroversial relative to the axioms designated Assumption. It is a vague and subjective designation. If the language interpretation guide entries (the informal textual semantics) for the symbols that the axiom depends on do not make it clear to you that this axiom should be true, then you should criticize this designation. Depending on the specifics of your criticism, I can respond by improving the entries in the language interpretation guide for some of those symbols, or else by changing the designation to "Assumption" or "Claim".
• A Definitional Axiom is an axiom that should be be absolutely uncontroversial among the intended audience for this argument. Usually, if not always, it will have a very objective/mathematical character.
• ✓Lemma and ✓Goal denote sentences that have been formally proved (computer checkable) to be logical consequences of the definitions, axioms and lemmas that precede them, and the definitions, axioms and lemmas that are their children (immediate descendants only). A Lemma has an informal proof. A Claim is a statement that is used as a Lemma but has neither been formally nor informally proved.
• A Defn~ introduces a symbol together with a sentence that intuitively defines it, but does not technically yield a definitional extension of the theory. Usually such symbols could be turned into proper definitions with the use of a definite description operator.

Variables x, y, n, m are reserved for sort

ℕ^{+}

ℕ^{+}

ℕ^{+}

ℕ^{+}

ℕ^{+}

Sort

ℕ^{+}

- Positive integers

Divides :

ℕ^{+}

ℕ^{+}

→ 𝔹 - The first number divides the second.

ℕ^{+}

ℕ^{+}

→ 𝔹

The first number divides the second.

< :

ℕ^{+}

ℕ^{+}

→ 𝔹 - The usual ordering on the natural numbers.

ℕ^{+}

ℕ^{+}

→ 𝔹

The usual ordering on the natural numbers.

Show axioms for <, ≤, >, ≥ etc

Hide axioms for <, ≤, >, ≥ etc

Axiom 1: ∀x,y,n. (x < y) ∧ (y ≤ n) ⇒ (x < n)

Axiom 2: ∀x,y,n. (x ≤ y) ∧ (y ≤ n) ⇒ (x ≤ n)

Axiom 3: ∀x,y. Exactly one of (x < y), (y < x), or x = y holds.

Defn ≤ :

ℕ^{+}

ℕ^{+}

→ 𝔹 - ∀n,m. (n ≤ m) ⇔ ((n < m) ∨ n = m)

ℕ^{+}

ℕ^{+}

→ 𝔹

(∀n,m. (n ≤ m) ⇔ ((n < m) ∨ n = m))

Defn > :

ℕ^{+}

ℕ^{+}

→ 𝔹 - ∀n,m. (n > m) ⇔ (m < n)

ℕ^{+}

ℕ^{+}

→ 𝔹

(∀n,m. (n > m) ⇔ (m < n))

Defn ≥ :

ℕ^{+}

ℕ^{+}

→ 𝔹 - ∀n,m. (n ≥ m) ⇔ (m ≤ n)

ℕ^{+}

ℕ^{+}

→ 𝔹

(∀n,m. (n ≥ m) ⇔ (m ≤ n))

ℕ^{+}

ℕ^{+}

1, 2 :

ℕ^{+}

ℕ^{+}

Defn Prime :

ℕ^{+}

→ 𝔹 - n is a prime iff it's at least 2 and no smaller (prime) divides it. This combines a normal definition of prime with the lemma: "Every non-prime number > 1 is divisible by a prime."

∀n. Prime(n) ⇔ ((n ≥ 2) ∧ ¬(∃m < n. Divides(m, n) ∧ Prime(m)))

ℕ^{+}

→ 𝔹

(∀n. Prime(n) ⇔ ((n ≥ 2) ∧ ¬(∃m < n. Divides(m, n) ∧ Prime(m))))

n is a prime iff it's at least 2 and no smaller (prime) divides it. This combines a normal definition of prime with the lemma: "Every non-prime number > 1 is divisible by a prime."

Defn MaxPrime :

ℕ^{+}

→ 𝔹 - True iff n is the largest prime number.

∀n. MaxPrime(n) ⇔ (Prime(n) ∧ (∀m > n. ¬Prime(m)))

ℕ^{+}

→ 𝔹

(∀n. MaxPrime(n) ⇔ (Prime(n) ∧ (∀m > n. ¬Prime(m))))

True iff n is the largest prime number.

T h e o r e m

: There are infinitely-many primes.

∀n. ¬MaxPrime(n)

Note that the theorem is a logical consequence (verified by a first-order theorem prover) of AXIOM3, Lemma 1, and the definitions and axioms that precede the statement of the theorem.

! :

ℕ^{+}

→

ℕ^{+}

- factorial

ℕ^{+}

→

ℕ^{+}

factorial

+ :

ℕ^{+}

ℕ^{+}

→

ℕ^{+}

- addition

ℕ^{+}

ℕ^{+}

→

ℕ^{+}

addition

Axiom 4: ∀n. n + 1 > n

Axiom 5: ∀n. n! ≥ n

Lemma 1: ∀n. MaxPrime(n) ⇒ Prime(n! + 1)

Lemma 2: ∀n. ¬(n! + 1 < 2)

Lemma 3: ∀n,m. MaxPrime(n) ∧ Prime(m) ⇒ (m ≤ n)

Axiom 8: ∀n. ∀m ≤ n. Divides(m, n!)

Axiom 9: ∀x. ∀m ≥ 2. Divides(m, x) ⇒ ¬Divides(m, x + 1)