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

2 AnswersProof 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

1 Asked on November 29, 2021

ag algebraic geometry etale cohomology intersection cohomology perverse sheaves reference request

1 Asked on November 26, 2021 by lisa-s

7 Asked on November 26, 2021 by yiftach-barnea

1 Asked on November 26, 2021 by till

algorithms computational complexity computational geometry linear programming reference request

0 Asked on November 26, 2021

limits and convergence markov chains pr probability stochastic processes

0 Asked on November 26, 2021 by sid-a

limits and convergence markov chains pr probability stochastic differential equations stochastic processes

1 Asked on November 26, 2021

1 Asked on November 24, 2021

ag algebraic geometry differential operators ra rings and algebras reference request sg symplectic geometry

0 Asked on November 24, 2021 by user69642

ap analysis of pdes fa functional analysis reference request

0 Asked on November 24, 2021 by jw7642

0 Asked on November 24, 2021 by daniil-rudenko

1 Asked on November 24, 2021

ca classical analysis and odes cv complex variables ds dynamical systems real analysis

4 Asked on November 22, 2021 by temitope-a

5 Asked on November 22, 2021 by ruth-no

infinite games real analysis reference request set theory textbook recommendation

0 Asked on November 22, 2021

ag algebraic geometry complex geometry dg differential geometry hodge theory

0 Asked on November 22, 2021

1 Asked on November 22, 2021

0 Asked on November 22, 2021 by andrea-t

eisenstein series nt number theory quantum field theory sequences and series

Get help from others!

Recent Answers

- kjetil b halvorsen on How to test consistency of responses?
- DMGregory on MouseLook Script “Pops” back to the last value when the script is enabled after being disabled or destroyed
- Justin Markwell on Unity app crashes when using unmodified custom Android manifest (didn’t find class “UnityPlayerActivity”)
- eric_kernfeld on How to test consistency of responses?
- Philipp on How do i draw a ray in unity

Recent Questions

- MouseLook Script “Pops” back to the last value when the script is enabled after being disabled or destroyed
- Unity app crashes when using unmodified custom Android manifest (didn’t find class “UnityPlayerActivity”)
- How do i draw a ray in unity
- How to test consistency of responses?
- How can I understand these variograms?

© 2022 AnswerBun.com. All rights reserved.