I’m very excited that Steve Awodey is on his way here to deliver the first Calgary Mathematics & Philosophy Lecture tomorrow! He’s speaking on “Univalence as a New Principle of Logic.” If you’re in Calgary, you should come. It’ll be exciting. Thursday, 3:30 pm, in Engineering Building A aka ENA 101 on the UofC campus. Here’s the abstract:
It is often convenient or useful in mathematics to treat isomorphic structures as the same. The Univalence Axiom for the foundations of mathematics elevates this idea to a foundational principle in the setting of Homotopy Type Theory. It states, roughly, that isomorphic structures can be identified. In his talk, Prof. Awodey will explain this principle and how it can be taken as an axiom, and explore the motivations and consequences, both mathematical and philosophical, of making such an assumption.
Steve will give a more technical talk in the Math Department on Friday at 2pm.
Also check out the sweet poster:
Taking this idea seriously in the context of classical logic implies that disjunction and conjunction should get identified as the same since the algebras ({True, False), disjunction) and ({True, False}), conjunction are isomorophic. It also implies that negation implies sameness, since truth-function negation is an isomorphism. It also collapses the distinction between disjunction and conjunction in plenty of multi-valued logics, and Lukasiewicz infinite-valued logic.
This leads to a joke… what’s the difference between an algebraist and a logician? An algebraist can’t tell the difference between “AND” and “OR”.