4
$\begingroup$

I am wondering about relative consistency of various Martin-Löf type theories, when compared to one another, I will use MLTT for the intensional Martin-Löf type theory with $\Pi$, $\Sigma$, $\mathbb{N}$, Id, unit and empty types.

Let's formulate consistency as lack of term of empty type and relative consistency being a proof that given the rules of itself T1 and assumption that they are consistent, we can deduce that another type theory T2 is consistent. So here are the variants.

  1. MLTT + Predicative Set universes (ala Agda without induction recursion)
  2. MLTT + Predicative (S)Prop and Set universes (ala Agda without induction recursion and with -prop)
  3. MLTT + Impredicative (S)Prop (ala Coq)
  4. MLTT + Impredicative Set at the bottom (ala Coq with -impredicative-set but without Prop)
  5. MLTT + Impredicative (S)Prop + Impredicative Set (ala Coq with -impredicative-set)
  6. Combinations of the above with large (agda-style) induction-recursion

In the last case I am not even aware of consistency results for the combination with impredicative universes. Related question seems to be: Relative consistency of PA and some type theories, but the answer there does not take into account universes. I am mostly looking for references discussing the relative consistency of these.

Improve this question
$\endgroup$
3
  • 2
    $\begingroup$ It's odd to call it "Martin-Löf type theory" without having the identity types also. Did you just forget them, or is there a reason for excluding them? $\endgroup$
    – Andrej Bauer
    Commented Mar 11, 2021 at 13:02
  • 1
    $\begingroup$ @AndrejBauer just forgot thanks for catching that $\endgroup$
    – Ilk
    Commented Mar 11, 2021 at 13:03
  • 2
    $\begingroup$ It might also be worth spelling out what you mean by "relative consistency", precisely. Presumably you'd also explain what consistency is in this case, is it "there is no closed term of type $\mathtt{empty}$? $\endgroup$
    – Andrej Bauer
    Commented Mar 11, 2021 at 13:04

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.