8
$\begingroup$

The Stack Exchange bot reminded me that I had committed myself to asking some questions, but please allow a possibly naive question, possibly of a philosophical nature rather than mathematical/computer-theoretical.

So, is it conceivable that the development of proof assistants make mainstream mathematicians switch their framework, from a set theoretical one, to a type theoretical one.

It is not that mathematicians all know about the axioms of ZFC, I'm certain most don't and most don't care, but mathematics are full of idiosyncratic set-theoretical gimmicks such as saying that a group is a 3-tuple consisting of a set, a law, a neutral element, and some people (most students) pay attention to the fact that it is a 3-tuple and not something else. (I have been asked which component of a similar 5-tuple a submodule should be…)

Type theory (especially how it is implemented) simultaneously departs from such constructions, and insists on the list of objects/axioms (so that the computer-definition of a group also contains a proof of associativity, etc.).

On the other hand, the concept of a set is clearly an important one.

Similarly, some constructions are built on sets in a way which might look unnatural — say defining the quotient set as a set of equivalence classes — but are now well understood, and can be avoided by a more categorical point of view.

I also have in mind more advanced notions of algebra/number theory where set theoretical notions look less avoidable, such as the definition of an ideal. (One could try to replace them by the epimorphism to the quotient ring, but that does not look very easy to handle.)

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Is this question asking about the effectiveness of proof assistants as a marketing tool for non-ZFC foundations for math? Is it specifically about the part of the mathematical community that isn't explicitly interested in formalization? I can't answer on behalf of the mathematical community, but in my limited experience, proof assistants are very effective at generating interest in mathematics and its foundations among programmers. $\endgroup$
    – Greg Nisbet
    Commented Feb 15, 2022 at 17:42
  • 7
    $\begingroup$ I think PAs might make mathematicians more aware of their framework. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Feb 15, 2022 at 18:43

2 Answers 2

Reset to default
12
$\begingroup$

The following is a made up opinion piece based on the observation of a statistically small sample of mathematicians. Please take it with a grain of salt.

A typical working mathematician has little time for and only cursory interest in the foundations of mathematics. They are able to operate perfectly well without stressing over formalities of whatever foundation they imagine standing on. They don't particularly care what foundation they are using, as long as it does not interfere with their work. They think of a foundation as a necessary thing that is useful on a grand scale of things, but is not really crucial in their everyday work. Often they profess using a particular foundation, but their mathematical texts are closer to another one. What I am saying is that mathematicians do not actually use foundations that they could switch between.

When such mathematicians start using proof assistants, they are forced to pay attention to foundations. They become more proficient in logic, they learn about introduction and elimination rules, they learn that some proofs are better than others etc. But what really matters, in my opinion, is that they actually start to believe that proofs are mathematical objects. Instead of just converting coffee to proofs, they start thinking about proofs. Even better, instead of just applying techniques and tricks to do math, they start thinking about the techniques and tricks, and how to express them in proof assistants.

To address the question directly, I would say that the typical experience is not that of “switching from one framework or foundation to another” but rather “actually learning a foundation and adopting it as a real working tool". If you write your proofs in LaTeX then you have little direct use for foundations, but if you write your proofs in a proof assistant then the foundation and the proof development techniques are your new everyday tools.

Let me also point to Penelope Maddy's paper What Do We Want a Foundation to Do? in which she nicely identifies the different purposes and roles that a foundation may have. While I do not entirely agree with her assessment of the role of univalent foundations, I appreciate her point that there's a difference between a foundation that studies what can be formalized in principle, and one that is supposed to be used to actually formalize mathematics. This difference may explain why the foundations of the early 20th century do not fit our current needs.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ I wish I could upvote 10 times for just the phrase "But what really matters, in my opinion, is that they actually start to believe that proofs are mathematical objects." $\endgroup$
    – Jacques Carette
    Commented Feb 18, 2022 at 13:47
8
$\begingroup$

I am not asking that much! If there is one thing I would like mathematician to get from the use of dependent type theory, this is the revolutionary notion of bound variables.

For some mysterious reason, the standard mathematical practice shuns the notion of higher-order syntax and relies on weird idiosyncratic notations when it is necessary. You can even see that in the insistence of category theory to reduce everything to a binder-free syntax, despite higher-order being pervasive in this setting.

Being able to write a λ-abstraction is liberating.

Improve this answer
$\endgroup$
5
  • 2
    $\begingroup$ Can you elaborate a little bit ? I am not sure to see what examples you allude to in the last two paragraphs, nor to what you mean by the notion of bound variables that would be specific to dependent type theory. $\endgroup$
    – ACL
    Commented Feb 16, 2022 at 18:10
  • $\begingroup$ A simple example is the definition of a cartesian closed category. The standard definition is based on the adjunction A × B ⊢ C ≅ A ⊢ B ⇒ C. This is similar to a presentation via SK combinators, and there is no notion of bound variable nor first-class contexts there. Instead, we only have access to toplevel types. An even worse situation happens with the categorical presentation of dependent types. There, everything is done backwards via fibers, because there is simply no syntax to write a type in a context. $\endgroup$
    – Pierre-Marie Pédrot
    Commented Feb 16, 2022 at 22:47
  • $\begingroup$ Bound variables are not specific to dependent type theory, but they are literally the only feature of the λ-calculus. Since the former contains the latter, it provides an elegant way to handle subtitution by construction. Then, once you have a higher-order syntax, many things become more natural to express. $\endgroup$
    – Pierre-Marie Pédrot
    Commented Feb 16, 2022 at 22:49
  • 2
    $\begingroup$ I find most mathematicians write lambdas as say $x \mapsto x+1$. The concept is there but with a different notation. (But I also agree in general with your answer.) $\endgroup$
    – Jason Rute
    Commented Feb 17, 2022 at 11:07
  • $\begingroup$ @JasonRute: Like this? $\endgroup$
    – user21820
    Commented Mar 30, 2022 at 13:27

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