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?

  • $\begingroup$ Does nonstandard analysis count? $\endgroup$ – none Jul 24 '20 at 19:04
  • 5
    $\begingroup$ Regarding the specific point on proof-relevance:That is really just the distinction between a "property" and a "structure": type theory at some point tended to forgot the distinction between a type and a proposition, but if you have some "property" of an object, saying that it is "proof-relevant" is exactly saying that it is actually not a property but a structure. I'm sure every body has some examples where the distinction property/structure is important in mathematics and listing such example might not be so interesting. $\endgroup$ – Simon Henry Jul 24 '20 at 19:05
  • $\begingroup$ Do you mean "does nonstandard analysis count as 'ordinary'?" Sure, I'm perfectly happy to mean "not a statement about mathematical logic per se" by 'ordinary', and I'd happily count nonstandard analysis in there. $\endgroup$ – mcncm Jul 24 '20 at 19:06
  • 2
    $\begingroup$ Per @SimonHenry's mention of property and structure: nLab on property and structure, and specifically examples. There's also much discussion on the nCat café; the first example that came up when I searched is a post on structure-like properties. $\endgroup$ – LSpice Jul 24 '20 at 20:06
  • 2
    $\begingroup$ You might be interested in Kohlenbach's works. This is the link of his book which is related to your question: springer.com/gp/book/9783540775324 $\endgroup$ – Erfan Khaniki Jul 25 '20 at 2:21

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.

  • 1
    $\begingroup$ I'm confused. The slides are titled "Proof mining", not "Gold mining". Are you saying that proofs are like gold? And how many proofs have you mined from these slides? $\endgroup$ – Asaf Karagila Jul 25 '20 at 17:14
  • 1
    $\begingroup$ @AsafKaragila Fort Knox is actually just a library containing all copies of The Book. $\endgroup$ – Carl-Fredrik Nyberg Brodda Jul 25 '20 at 17:39
  • $\begingroup$ "Then what do you suggest? A daring daylight robbery of Fort Knox on elephant back. That's the dumbest thing I ever heard." $\endgroup$ – Asaf Karagila Jul 25 '20 at 17:40
  • $\begingroup$ [Appears to be a quote from Futurama. imdb.com/title/tt0584453/characters/nm0921942] $\endgroup$ – Gerry Myerson Jul 26 '20 at 9:49

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.