4 ms·
> except serve as a basis for practical formalization of proofs That might well be true for advanced mathematics, but in practical software engineering, TLA+,
by pron 4y ago
> except serve as a basis for practical formalization of proofs
That might well be true for advanced mathematics, but in practical software engineering, TLA+, which uses ZFC for its "data" portion (its computational portion is based on a linear temporal logic called TLA), is not only the most popular of the "deep" specification languages (although that's not saying too much), but one of the most successful practical applications by ordinary practitioners (i.e. not logicians or other academic researchers) of deep formal logic in the history of formal logic. True, most users don't bother writing deductive proofs in the TLA+ proof assistant and prefer using model checkers available for TLA+ because they have a higher ROI, but still.
> My view is that all the "philosophical" arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play.
Perhaps ironically, it is precisely the power of the notion of isomorphism that means it is often simpler and more practical to keep it in the meta-logic and work with a particular representative with a particular equality rather than baking the very notion of isomorphism into the heart of the logic itself (which is very interesting from a logician's perspective, but doesn't necessarily lead to better pragmatic results for practitioners). I.e. it is because isomorphism is so fundamental that we don't need it in the logic, and it can serve as the foundation for a foundation rather as the foundation itself. Of course, logicians enjoy exploring taking as much of the meta-logic and philosophy and putting it into the logic. That's pretty much what logicians are meant to do. Unfortunately, not too many of them are also interested in the question of how to make a logic more friendly to practitioners.
- zozbot234 4y ago> work with a particular representative with a particular equality HoTT lets you do this when such a canonical representative exists. The point is to be able to generalize beyond that.
- layer8 4y agoWhy does it need to be canonical?
- pron 4y agoThe 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 agoDo 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