3
$\begingroup$

If I understand correctly constructivism is not the only difference between intensional Martin-Löf type theory and a first-order set theory (e.g. ZFC). Can we drop constructivism and yet have a dependent type theory?

Curry-Howard correspondence would probably be false for it but it might be interesting nonetheless.

Improve this question
$\endgroup$
4
  • $\begingroup$ I'm not sure offhand what the precise type theory is underlying the proof assistant Lean is, but it is used by people doing mathematics using classical logic. So my guess is yes, but I don't have precise examples to hand. Hopefully an expert can point to a source. $\endgroup$
    – David Roberts ♦
    Commented Jan 16, 2021 at 14:11
  • 2
    $\begingroup$ Welcome to MathOverflow, masala! Yes, we can add various forms of the law of excluded middle to dependent type theory, similar to how we can add the law of excluded middle to intuitionistic logic. A reference includes the introduction of the homotopy type theory book and more specifically Section 3.4. $\endgroup$
    – Ingo Blechschmidt
    Commented Jan 16, 2021 at 16:31
  • $\begingroup$ It depends on what you mean by non-constructive, but it's in general not possible due to the fact that having classical sum type renders Type Theory inconsistent: researchgate.net/profile/Herman_Geuvers/publication/… There are experiments in this direction though: hal.archives-ouvertes.fr/hal-01519929 $\endgroup$
    – Matteo
    Commented Jan 16, 2021 at 17:43
  • 1
    $\begingroup$ The Geuvers paper uses the fact that the $\mathsf{Set}$ universe was impredicative (by default) in Coq, which is no longer the case. Martin-löf type theory is also predicative in this sense. So, the paper appears to be specific to those quirks of Coq at the time, not a proof that type theories in general cannot be classical. $\endgroup$
    – Dan Doel
    Commented Jan 21, 2021 at 16:17

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .