Appearance of proof relevance in "ordinary mathematics?"

I’ve been wondering recently what—if any—applications proof theory has to ordinary mathematics (by which I mean algebra, analysis, topology, and so on). In particular, I’d be fascinated to see a proof of a theorem about ordinary mathematical objects that relies on proof relevance. I’m afraid I’m unable to make the question more concrete, but what I would hope to see is something that "smells like" the following:

The proposition $$P$$ is simply connected, in the sense of HoTT. It follows that the ring $$R$$ is nilpotent-free.

Note that I don’t care at all what is proved, or about what kind of "ordinary" object; only that it’s a readily-understood "non-foundational" statement that isn’t completely trivial. The proof-theoretic ingredients should also not be too trivial: in particular, requiring "$$P$$ is inhabited" is not very unusual at all! Can you cook up anything like this? Has anything like it ever been used in a serious way?

MathOverflow Asked by mcncm on January 3, 2022

Proof mining (which even has a short Wikipedia article!), and area in large part developed by Kohlenbach, is mentioned briefly in the comments, and I thought it deserves a bigger mention. Roughly speaking, proof mining is the idea that from non-constructive proofs of existence one can often extract effective bounds. For example, from the standard proof of the irrationality of $$sqrt{2}$$ it is not hard to show that for any irreducible rational $$frac{a}{b} > 1$$ we must have that $$|frac{a}{b} - sqrt{2}| > frac{1}{2b^2}$$ (try it yourself!). This ties in with the irrationality measure of a real number.

Especially in its applications to functional analysis, such as in [Kohlenbach, U.; Leuştean, L.; Nicolae, A.; Quantitative results on Fejér monotone sequences. Commun. Contemp. Math. 20 (2018), no. 2], proof mining really shines through as a powerful set of techniques.

I attended a summer school in 2016 in which Kohlenbach presented these slides -- they are a gold mine of information, but can be rather dense at times. However, they provide an excellent overview for many important concepts in the area (such as Herbrand normal forms) and highlight many applications. A good introductory text is also this text by Kohlenbach and Oliva.

Answered by Carl-Fredrik Nyberg Brodda on January 3, 2022

Some proof relevance in classical mathematics is going to be quite hard to see. While in HoTT, which proof of equality you choose may matter, it classical mathematics all proofs of equality are the same, so you won't be able to leverage them.

Take a slightly less trivial situation: proofs of $$n leq m$$. Well, it turns out that the canonical such proof is (unsuprisingly) isomorphic to $$m-n$$. Classically, if you needed the 'content' of $$n leq m$$, you'd just use $$m-n$$ and move on. Note that any member of $$textsf{Fin}(m-n+1)$$ is a witness for $$n leq m$$. The point is that the set of all proofs is $$textsf{Fin}(m-n+1)$$, of cardinality $$m-n+1$$. If you are proof-relevant, then any of those witnesses will do, not just the "tightest" one. And your results will then depend on that choice. Because it is "too easy" to see what the best choice is, it is thus rare to not pick it.

Moving up a tiny bit more: when you say let $$X$$ be a finite set of size $$n$$, you definitely don't care about what is in $$X$$ but you might still find something odd: if you leverage all the information from the premise, in a proof-relevant setting, you get a full isomorphism between $$X$$ and $$textsf{Fin}(n)$$; but $$textsf{Fin}(n)$$ is canonically ordered, so you can induce an ordering on $$X$$. Which ordering? Well, the one that's in your proof! There are $$n!$$ such possibilities. In a classical setting, one usually assumes, silently, that you don't depend on the proof, so you assume that $$X$$ is unordered. [Constructively, you can't blithely assume this, which is explained very well in Brent Yorgey's PhD Thesis.] In other words, this might be a source of proof-relevance, if you're not careful! Some code I wrote for Species in Haskell ended up being accidentally proof-relevant because of exactly this.

It is worth remembering that a bijection between $$textsf{Fin}(m)$$ and $$textsf{Fin}(n)$$ is a witness that $$m=n$$. Some theorems about permutations, when de-categorified, are theorems about set cardinality. Which set isomorphism you pick matters, because it gives you a different permutation. This has non-trivial implications for reversible programming (see my work with Amr Sabry if you're curious).

My feeling is that there is in fact a lot of "proof relevant" statements in classical mathematics, they just have not yet been recognized as being such.

Answered by Jacques Carette on January 3, 2022

Related Questions

Example of an intersection complex not concentrated in a single degree

1  Asked on November 29, 2021

Is every proper regular relative algebraic space curve over a Dedekind domain projective?

1  Asked on November 26, 2021 by lisa-s

Examples of residually-finite groups

7  Asked on November 26, 2021 by yiftach-barnea

Reference: Packing under translation is in NP

1  Asked on November 26, 2021 by till

Representing a continuous time-inhomogeneous Markov chain by a stochastic integral

0  Asked on November 26, 2021

Convergence of empirical measure to Mc-Kean Vlasov equation for mean-field model with jumps

0  Asked on November 26, 2021 by sid-a

Values of a pair of determinants

1  Asked on November 26, 2021

What subsystem of third order arithmetic proves the real numbers are Dedekind complete?

1  Asked on November 26, 2021

Algebras Morita equivalent with the Weyl Algebra and its smash products with a finite group

1  Asked on November 24, 2021

Error rate implying regularity

0  Asked on November 24, 2021 by user69642

Pairing up vertices in a graph

1  Asked on November 24, 2021

Minimizing an f-divergence and Jeffrey’s Rule

0  Asked on November 24, 2021 by jw7642

Rational functions with trivial Weil symbols at every point

0  Asked on November 24, 2021 by daniil-rudenko

Regular singular point of non-linear ODE: $dot{x}(t) + t^{-1}Ax(t) = Q(x(t))$

1  Asked on November 24, 2021

Inverse problem of Chern Classes

4  Asked on November 22, 2021 by temitope-a

Reference for graduate-level text or monograph with focus on “the continuum”

5  Asked on November 22, 2021 by ruth-no

Do Poincaré residue and integrable log connection commute?

0  Asked on November 22, 2021

Numbers of the form $x^2(x-1) + y^2(y-1) + z^2(z-1)$ with $x,y,zinmathbb Z$

0  Asked on November 22, 2021

How to solve a differential equation in the form $frac{partial}{partial t}g(x,t)=g(x-Delta,t)+frac{partial^2}{partial x^2} g(x,t)$?

1  Asked on November 22, 2021

Multidimensional series: an application of quantum field theory

0  Asked on November 22, 2021 by andrea-t