Conversation

Notices

1. Embed this notice
   Martin Escardo (martinescardo@mathstodon.xyz)'s status on Saturday, 14-Dec-2024 02:59:39 JST Martin Escardo

   in reply to

   Martin-Löf type theory (MLTT) is a minimal foundation for mathematics, which is at the same time a programming language.

   (E.g. Agda is based on MLTT.)

   Compared to classical (non-constructive) mathematics, it lacks the principle of excluded middle.

   Compared to Brouwer's intuitionism, it lacks continuity and bar-induction principles.

   Compared to (the internal language of) topos theory, it lacks impredicativity and has a different treatment of the existential quantifier.

   Compared to Homotopy Type Theory (HoTT), it lacks the univalence axiom and higher-inductive types.

   The above mathematical theories can be accommodated in MLTT by simply postulating the required "missing" axioms (excluded middle, choice, propositional resizing, propositional truncations, univalence etc.)

   2/

   • Embed this notice
     Martin Escardo (martinescardo@mathstodon.xyz)'s status on Saturday, 14-Dec-2024 02:59:41 JST Martin Escardo

     Negative axioms can be postulated without loss of canonicity.

     In this thread I want to explain a 3-page research note Coquand, Danielsson, Norell, Xu and myself wrote with the above title, back in 2013 with revisions and additions in 2017:

     http://www.cs.bham.ac.uk/~mhe/papers/negative-axioms.pdf

     There are many reasons people may (or may not) be interested in constructive mathematics.

     * One is philosophical. For me, it is hard to agree (or even disagree) with the philosophical justifications, but this thread is not about this.

     * Another one is that mathematical objects of interest, such as toposes, are intrinsically intuitionistic in nature, even when they are developed in a classical meta-theory. It is this that I find very persuasive, and this is a purely mathematical view independent of philosophical considerations, but this thread is not about this either.

     * Yet another one, related to the first, but founded on a firm mathematical basis instead, is that "constructive proofs compute". I also find this persuasive.

     I usually write things here based on the second bullet point, but this thread is about the third one.

     1/

     alcinnz repeated this.