2 ms·

The larger point is should a foundation serve logicians interested in designing mathematical foundations or practitioners interested in formalising proofs (and

by pron 4y ago

The larger point is should a foundation serve logicians interested in designing mathematical foundations or practitioners interested in formalising proofs (and specifications)? It's easy to see why such theories would be interesting to logicians, who should certainly study them, but they may not help furthering formal mathematics or the use of formal logic in the field. Of course, putting more meta-theory into the logic should be explored, and it's even possible that it may turn out to have other desired effects. However, a foundation is usually not of interest to practitioners for the same reasons it is of interest to logicians, and it is that point that logicians sometimes miss. They try selling a particular theory on the basis of things that are of interest to them (we've put isomorphism in the language) rather than things that are of interest to practitioners (proofs are shorter, written in a more natural way, easier for machines to assist with etc.). The reasons to research a topic are often not those that best sell it to others. In other words, would it also be "the point" for a practitioner "to be able to generalise beyond that"?

zozbot234 4y ago
> The larger point is should a foundation serve logicians interested in designing mathematical foundations or practitioners interested in formalising proofs (and specifications)? I think this question can easily be answered in the affirmative. A key point of HoTT and univalence is that being able to work with isomorphism as if it was equality, and freely transport proofs and functions 'across' isomorphisms, makes for more intuitive proofs that get less bogged down in issues of logical formalism and closer to what a practitioner would want to write.
- AnimalMuppet 4y ago
  Do the practitioners agree with that? (I don't know, and I don't have a dog in this fight, being neither a practitioner nor a logician. I'm asking because, following the thread of the discussion, I could easily see a logician saying "Of course this will make it easier for the practitioners" about something that, in actual practice, the practitioners don't care about at all.)
- pron 4y ago
  I think that transporting proofs "for free" is of less interest since we're talking about formal, and so mechanised, proofs [1], but the matter of writing proofs more naturally could definitely be a selling point. Can you point to some examples of that? [1]: A computer can formally apply meta-logical transformations as a proof tactic, too. Why not put that into the logic if it can be done formally? To keep it simpler and easier for practitioners to learn. (Some systems, like TLA+, allow you to specify and prove higher order theorems that aren't expressible as formulas in the logic; so while you might not be able to express the general notion of an isomorphism in this way, you can express a theorem that can then be used by the proof assistant to transfer proofs based on isomorphisms with respect to some specific number of operators with some specific arities)
  - pron 4y ago
    P.S. Come to think of it, there's another aspect I don't understand. The validity of a theorem depends only on the assumptions used in the proof (so, for example, if I have a formal set theory proof that depends only on group axioms, then it applies to all groups). That is not a property that is usually expressible in the the logic -- it's a property of the proof theory of the logic -- but it is nevertheless true. Not being a logician, I'm not interested in writing proofs about my logic's proof theory, I don't need to define new proof rules as I don't develop new logics, and my logic's proof assistant is free to rely on theorems about the logic's proof theory. What do I, as a practitioner, gain by making the proof theory part of the logic?

by pron 4y ago

zozbot234 4y ago

> The larger point is should a foundation serve logicians interested in designing mathematical foundations or practitioners interested in formalising proofs (and specifications)? I think this question can easily be answered in the affirmative. A key point of HoTT and univalence is that being able to work with isomorphism as if it was equality, and freely transport proofs and functions 'across' isomorphisms, makes for more intuitive proofs that get less bogged down in issues of logical formalism and closer to what a practitioner would want to write.

AnimalMuppet 4y ago
Do the practitioners agree with that? (I don't know, and I don't have a dog in this fight, being neither a practitioner nor a logician. I'm asking because, following the thread of the discussion, I could easily see a logician saying "Of course this will make it easier for the practitioners" about something that, in actual practice, the practitioners don't care about at all.)
pron 4y ago
I think that transporting proofs "for free" is of less interest since we're talking about formal, and so mechanised, proofs [1], but the matter of writing proofs more naturally could definitely be a selling point. Can you point to some examples of that? [1]: A computer can formally apply meta-logical transformations as a proof tactic, too. Why not put that into the logic if it can be done formally? To keep it simpler and easier for practitioners to learn. (Some systems, like TLA+, allow you to specify and prove higher order theorems that aren't expressible as formulas in the logic; so while you might not be able to express the general notion of an isomorphism in this way, you can express a theorem that can then be used by the proof assistant to transfer proofs based on isomorphisms with respect to some specific number of operators with some specific arities)
- pron 4y ago
  P.S. Come to think of it, there's another aspect I don't understand. The validity of a theorem depends only on the assumptions used in the proof (so, for example, if I have a formal set theory proof that depends only on group axioms, then it applies to all groups). That is not a property that is usually expressible in the the logic -- it's a property of the proof theory of the logic -- but it is nevertheless true. Not being a logician, I'm not interested in writing proofs about my logic's proof theory, I don't need to define new proof rules as I don't develop new logics, and my logic's proof assistant is free to rely on theorems about the logic's proof theory. What do I, as a practitioner, gain by making the proof theory part of the logic?