#proof-theory #philosophy-of-math

In the last post, I suggested that Furstenburg, Mercer, and Euclid's proofs are essentially the same proof, insofar as there is a natural notion of reduction between them, in the direction

where these arrows are furnished by implications between corresponding auxiliary lemmas in respective proofs. Sieg's natural formalization ^[1] schema is particularly well-suited for this application. It uses ZF as its deductive framework (but could equally well use Martin-Lof type theory, higher order logic, etc...) and Gentzen's natural deduction as an inferential mechanism, with two key additions:

1. lemmas as rules: we can "reason with gaps" by applying lemmas directly as inferential rules, with each instance generating a new subgoal (the proof of that lemma). Of course, these proofs of lemmas can rely on lemmas of their own, and so on. This structure can be conveniently captured in Fitch diagram notation.
2. intercalation: this allows us to "close the gaps" created applying lemmas as rules by reasoning both "forward" and "backward," in the natural way (as, e.g is implemented in automated proof solvers). That is, we can apply a lemma $P\to Q$ in one of two ways to a goal $A\to B$:
   • forward: if $A$ matches $P$, the goal becomes $Q\to B$
   • backward: if $B$ matches $Q$, the goal becomes $A\to P$

To better understand this notion of "reduction of informal proofs" in terms of implications between corresponding auxiliary lemmas, consider the following renderings ^[2] of the proofs by Mercer and Euclid, presented in the previous note.

As discussed in the first note, we have the implication ${\lambda }_1⟹{\mathfrak{l}}_1$ and ${\lambda }_3⟹{\mathfrak{l}}_2$ between lemmas, each of which is used as a \textit{rule} above. In fact, the proofs of these implications might give a good notion of reduction between these proofs. For example, we have the implication ${\lambda }_1⟹{\mathfrak{l}}_1$:

To show that ${\lambda }_1⟹{\mathfrak{l}}_1$ we require $((A⟹B)\wedge C)⟹D$. But here we have, literally, $A=C$, so we need only show $B⟹D$. This proof is as follows:

where the rule/lemma $l_1$ expresses that $\pi =1+\prod p$ satisfies $\pi \notin \{-1,1\}$ (in particular, it is positive and greater than $1$). Again, the proof of this lemma generates another subgoal, and so on. Note that the first three lines of this proof of ${\lambda }_1⟹{\mathfrak{l}}_1$ are pasted directly from Mercer's proof; this yields something like an explicit literal reduction of Mercer's proof to Euclid's proof. I think this is a promising direction that I'm currently working to flesh out. Similarly we have to show ${\lambda }_3⟹{\mathfrak{l}}_2$ gives a good notion of reduction. For reasons discussed in the original note (that these lemmas correspond to the "same step" in both proofs), I think that this is tractable with the same technique; I'll do this in the next days, as well. Then, of course, it remains to make explicit the corresponding reduction in the Furstenburg $⟹$ Mercer case; there are no apparent obstructions beyond some small linguistic decisions to be made.

Future directions

Though Euclid's proof gives a nice prototype, it remains to find a more general method that will not become inordinately difficult when evaluating more complex mathematical proofs. Promising directions thus far are:

• finding a corresponding graph-theoretic or combinatorial reduction, in analog to Hughes' and Strassburger's first order combinatorial proofs. Finding such a combinatorial criterion for proof equivalence and reduction would both avoid syntactic complications and make this computationally tractable.
• introducing a category-theoretic framework in which to understand proofs, in which certain "minimal" proofs (Euclid's, in this case) can be viewed as terminal objects or fixed points in appropriately conceived categories, with proofs between corresponding auxiliary lemmas furnishing the morphisms, for example. This approach will likely build on Hughes' "Deep inference proof theory equals categorical proof theory minus coherence"^[3] framework, as the deep inference mechanism seems very promising in this application.
• In the example above, the implication $\frac{A}{B}⟹\frac{C}{D}$ forms the commutative diagram below. It remains to understand the proof-theoretic implications of mathematical criterion like this (i.e. diagrams between lemmas commuting/not-commuting, etc...). This is of course related to the category-theoretic approach above.

\usepackage{tikz-cd}
\begin{document}
\begin{tikzcd}
	A &&& C \\
	\\
	B &&& D
	\arrow[from=1-1, to=1-4]
	\arrow[from=1-1, to=3-1]
	\arrow[from=1-4, to=3-4]
	\arrow[from=3-1, to=3-4]
\end{tikzcd}
\end{document}

• We can also talk about mathematical purity in this sense. In particular, can we give a precise proof-theoretic characterization of mathematical purity based on this notion of reduction? And, say, if proof $\mathrm{\Pi }$ is pure and ${\mathrm{\Pi }}^{\prime }\to \mathrm{\Pi }$, is ${\mathrm{\Pi }}^{\prime }$ pure as well? This is motivated by the fact that mathematical purity was one of the primary considerations for this notion of proof reduction; in particular, methodologically distinct proofs of the infinitude of primes (say, Gauss' or Euler's proof) don't fit into the "Furstenburg $⟹$ Mercer $⟹$ Euclid" framework; different methodologies inhabit connected components in the class of all proofs of this proposition. Some notion of analyzing these connected components topologically/graph-theoretically is also possible, way down the line.