(7975.88.72) Updates on Euclid's theorem

#proof-theory #philosophy-of-math

In recent work, Pistone proposes a category-theoretic notion of proof identity for first- and second-order natural deduction that relies on the characterization of natural deduction rules as natural transformations between functors arising from . In particular, he conjectures these rules give rise to natural transformations on precisely $Sequents / Perm$ , i.e. these transformations are natural precisely when derivations differing by free permutations of natural deduction rules are viewed as equivalent.

This notion of equivalence is extended in this note, by introducing Sieg's notion of "lemmas-as-rules" in his natural formalization framework; we claim that the notion of proof identity arising from viewing lemmas-as-rules as natural transformations conforms more closely to a mathematician's informal notion of proof identity, and indeed yields coherent notions of identity, reduction, simplicity, and purity between (some) informal mathematical proofs, making headway toward the use of categorical techniques to solve Hilbert's 24th problem. We will provide a case study for this second point with the use of three proofs of Euclid's theorem that there are infinitely many primes.

The basic idea, by which we will claim that these three proofs are related, is as follows:

Find a common "proof skeleton" in which each proof fits. This proof skeleton will be expressed as a partial natural deduction derivation using "lemmas-as-rules" in the style of Sieg's intercalation calculus.
Writing the schematic formulae in this proof skeleton as parametric formulas, we will express each step of the proof skeleton as a functor from $Formulas$ to $Sequents$ .
The natural deduction rules and lemmas-as-rules applications will be natural transformations precisely when we consider those proofs that fit into the proof skeleton as equivalent. In other words, the quotient category obtained by the quotient of $Formulas$ by the proof skeleton is the full subcategory of $Formulas$ on which the lemmas-as-rules and natural deduction rules furnish natural transformations.

The case study in question is Euclid's theorem, that there are infinitely many primes. In 1955, Harry Furstenburg gave a "topological" argument for this result. It is paraphrased as follows:

We introduce a topology into the space of integers S, by using the arithmetic progressions (from
$- \infty$ to $+ \infty$ ) as a basis. It is not difficult to verify that this actually yields a topological space...Each arithmetic progression is closed as well as open, since its complement is the union of other arithmetic progressions (having the same difference). As a result the union of any finite number of arithmetic progressions is closed. Consider now the set $A = ⋃ A_{p}$ , where $⋃ A_{p}$ consists of all multiples of $p$ , and $p$ runs through the set of primes $\geq 2$ . The only numbers not belonging to $A$ are $- 1$ and $1$ , and since the set ${- 1, 1}$ is clearly not an open set, $A$ cannot be closed. Hence $A$ is not a finite union of closed sets which proves that there are an infinity of primes.

Several authors {Mercer, Conrad} have claimed that Furstenburg's proof is not fundamentally topological, in that it does not use any topological results beyond the basic definitions of a topological space. Idris Mercer gives a "variant of" Furstenburg's proof which is devoid of topological language, using only basic properties of sets and prime numbers to demonstrate the "'real reason' that Furstenburg's approach works."

Conrad goes further, claiming that Furstenburg's proof is "based on the same idea as Euclid's proof of the infinitude of primes." It is therefore desirable to extract the underlying idea that these mathematicians reference; we will use three proofs of this theorem as a case study to provide support for a rigorous way of comparing informal mathematical proofs based on their "underlying ideas," with a view towards a precise notion of proof-theoretic simplification and methodological purity. My conception is based on the notion of equivalence with respect to natural formalization framework introduced by Sieg, but it extends this notion to account for a reduction relation between proofs, rather than simple equivalence. Furthermore, I aim to unify this account with Pistone's equivalence of natural deduction proofs up to free permutation via natural transformations; with a similar set of naturality constraints on the mappings induced by Sieg's lemmas-as-rules as Pistone introduced for the usual natural deduction rules, we obtain a richer notion of equivalence that better captures informal notions of equivalence between mathematical proofs.

Sieg considers naturally formalized proofs to be equivalent if they each arise via direct substitutions into a fixed proof schema: we extend this to an ordering relation on naturally formalized proofs when they coincide in the same sense at some level of generality. That is, applications of lemmas-as-rules in the natural formalization framework generate nested subgoals that are filled by further applications of lemmas-as-rules and natural deduction rules: roughly, we will say that a naturally formalized proof $P^{'}$ is a reduction of another such proof $P$ if there exist non-negative integers $p \leq p^{'}$ such that the open goals of $P$ at depth $p$ and the open goals of $P^{'}$ at depth $p^{'}$ both arise as direct substitutions into a fixed proof schema. In other words, they are equivalent (in Sieg's sense) at some level of generality. The motivation for this idea is that two such proofs will be related in this sense if they rely on the same collection of key lemmas, which are justified in the same way. This conception will be given concrete justification in the case example that follows, followed by more general considerations.

The idea is that these proofs $P$ and $P^{'}$ "look the same" after a certain point in their Fitch diagrams (depth $p$ , in this case); in this way, the justificatory steps for respective proofs become indistinguishable, so we can pass at will between the two proofs to reach the ultimate goal. This commutative structure motivates the naturality conditions extending Pistone, which will ultimately provide the concrete mathematical underpinning and formal definition of this relation. But first, an illustrative example.

This tree $(*)$ is the proof schema from which each of the three proofs arises as a direct substitution.

\begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} Fin (D) \end{matrix} \\ \exists \tilde{p} Prime (\tilde{p}) π_{D} \in AP (0, \tilde{p}) \end{matrix} & \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} Fin (D) \end{matrix} \\ π_{D} \equiv 1 (\mod d_{i}) \end{matrix} \end{matrix} \\ π_{D} \in ⋂_{d_{i} \in D} (AP (0, d_{i})^{C}) \end{matrix} \end{matrix} \\ \tilde{p} \neq d_{i} \forall d_{i} \in D \end{matrix}

Here is a natural formalization (given in Gentzen natural deduction style rather than Fitch style for convenience) of each of the three proofs, at the top level of generality.

Furstenburg

\begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix}  \end{matrix} \\ Topo (Z, τ) \end{matrix} λ_{1} \end{matrix} \\ \forall {Clo}_{τ} (S_{i}) . S = ⋃_{i \leq n} S_{i} \to {Clo}_{τ} (S) \end{matrix} & \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix}  \end{matrix} \\ Z ∖ A = {- 1, 1} \end{matrix} λ_{2} \end{matrix} \\ \neg {Clo}_{τ} (A) \end{matrix} \end{matrix} \\ \neg \exists A_{1}, \dots A_{n} . A = ⋃_{i \leq n} A_{i} \end{matrix} & \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix}  \end{matrix} \\ Topo (Z, τ) \end{matrix} λ_{1} \end{matrix} \\ \forall (n, d) \in Z^{2} {Clo}_{τ} (AP (n, d)) \end{matrix} & \begin{matrix} \begin{matrix}  \end{matrix} \\ Fin (P) \end{matrix} H - i \end{matrix} \\ \exists A_{p_{1}}, \dots, A_{p_{k}} . A = ⋃_{i \leq k} A_{p_{i}} \end{matrix} \end{matrix} \\ \neg Fin (P) \end{matrix} H - e

with the following predicates and definitions:

\begin{aligned} Topo (X, T) & : The set X is a topological space with respect to the topology T \\ {Clo}_{T} (X) & : The set X is closed with respect to the topology T \\ Fin (S) & : S is a finite set of integers \\ Prime (z) & : The integer z is prime \\ - - - \\ AP (n, d) & := {z \in Z : z \equiv n (\mod d)} \\ τ & := ⟨ {AP (n, d) : n, d \in Z} ⟩ \\ B & := {AP (n, d) : n, d \in Z} \\ P & := {z \in Z : Prime (z)} \\ A & := ⋃_{p \in P} AP (0, p) \end{aligned}

We have also made use of the following lemmas-as-rules:

\begin{aligned} λ_{1} & : (\forall z \in Z, \exists (n, d) \in Z^{2} . z \in AP (n, d)) \land \\ (\forall B_{1}, B_{2} \in B, z \in B_{1} \cap B_{2}, \exists B_{3} \in B . z \in B_{3} \subseteq B_{1} \cap B_{2}) \\ λ_{2} & : \forall z \in Z ∖ {- 1, 1}, \exists Prime (p) . p ∣ z \end{aligned}

$λ_{1}$ is the justification that $(Z, τ)$ is indeed a topological space via direct verification of the topological basis axioms and $λ_{2}$ is the Fundamental Theorem of Arithmetic (every integer apart from $1$ and $- 1$ has a prime factor).

Mercer

\begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix}  \end{matrix} \\ (⋃_{p \in P} AP (0, p))^{C} = {- 1, 1} \end{matrix} ℓ_{1} \end{matrix} \\ ⋂_{p \in P} (AP (0, p)^{C}) = {- 1, 1} \end{matrix} ℓ_{2} & \begin{matrix} \begin{matrix}  \end{matrix} \\ Fin (P) \end{matrix} H-i \end{matrix} \\ | {- 1, 1} | = 0 \lor | {- 1, 1} | = \infty \end{matrix} ℓ_{3} & | {- 1, 1} | = 2 \end{matrix} \\ \neg Fin (P) \end{matrix} H-e

with the following lemmas-as-rules:

\begin{aligned} ℓ_{1} & : \forall z \in Z ∖ {- 1, 1}, \exists Prime (p) . p ∣ z \\ ℓ_{2} & : \forall S_{1}, S_{2} (S_{1} \cup S_{2})^{C} = S_{1}^{C} \cap S_{2}^{C} \\ ℓ_{3} & : \forall {B_{i}}_{i \leq n} . B_{i} \in B, | ⋂_{i} B_{i} | = 0 \lor | ⋂_{i} B_{i} | = \infty \end{aligned}

so $ℓ_{1}$ is again the Fundamental Theorem of Arithmetic, $ℓ_{2}$ is DeMorgan's Law (here presented pairwise, but this extends to arbitrary countable unions/intersections), and $ℓ_{3}$ is Mercer's Claim 1 that a finite intersection of arithmetic progressions is either empty or infinite.
Euclid

\begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix}  \end{matrix} \\ Fin () \end{matrix} H-i \end{matrix} \\ \forall p_{i} \in P, π_{P} \equiv 1 (\mod p_{i}) \end{matrix} l_{1} \end{matrix} \\ π_{P} \notin ⋃_{p \in P} AP (0, p) \end{matrix} \end{matrix} \\ π_{P} \in ⋂_{p \in P} (AP (0, p)^{C}) \end{matrix} & \begin{matrix} \begin{matrix}  \end{matrix} \\ ⋂_{p \in P} (AP (0, p)^{C}) = {- 1, 1} \end{matrix} l_{2} \end{matrix} \\ π_{P} = 1 \lor π_{P} = - 1 \end{matrix} & π_{P} > 1 \end{matrix} \\ \neg Fin (P) \end{matrix} H-e

where for any set of integers $D = {d_{i}}$ , $π_{D}$ is the quantity

π_{D} := 1 + \prod_{i} d_{i}

with the following lemmas-as-rules:

\begin{aligned} l_{1} & : \forall {d_{i}} \in Z^{2}, 1 + \prod_{i \leq n} d_{i} \equiv 1 (\mod d_{i}) \\ l_{2} & : \forall z \in Z ∖ {- 1, 1}, \exists Prime (p) . p ∣ z \end{aligned}

so that $l_{1}$ is the fact that $π_{P}$ is congruent to $1$ modulo each of the $p \in P$ (so contains no $p \in P$ as a factor) and $l_{2}$ is the again the Fundamental Theorem of Arithmetic.

The key intuition is the similarity between the lemmas-as-rules: while some of the $λ_{i}, ℓ_{i},$ and $l_{i}$ coincide exactly (e.g. the Fundamental Theorem of Arithmetic), the others are closely linked insofar as their mathematical equivalence.