[johncolanduoni]

You’ve actually hit on the difference here: in the type theory the witness term plus the reduction trace is equivalent to the ZFC proof. It’s true that checking this combination is decidable, regardless of consistency. The intentionality does not eliminate the limitations of this property, it only provides that the reduction trace is implicit given the witness term. The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem, which assumes consistency of the type theory.

Let’s come at this from the other direction. Suppose I find a non-normalizing term X of type false (like that produced by Girard’s paradox if we leave off stratification). What happens when I try to type check this?

id(X): ==(X, rec_0(0, X))

Where id is the constructor of the propositional equality type and rec_0 is the recursor for False.

[Kutta]

What you say is kind of interesting but I get the impression that we are talking past each other.

id(X): ==(X, rec_0(0, X))

Sorry, what's this supposed mean, is it a definition? The propositional equality type has two or three arguments, I only see one (X) here, if as you say "id" is propositional equality.

In any case, nothing peculiar happens when we check a trace-annotated proof of bottom. We are free to use any particular finite-step unfolding of the non-normalizing proof.

We also don't need any paradox or inconsistency for a non-normalizing term, it is enough to work in ETT in a typing context which implies bottom, or which contains an undecidable equational theory, e.g. the rules of the SK-calculus.

> The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem

Decidability of type checking is always relative to a particular surface/raw syntax. A trace-annotated raw syntax does not need a normalization assumption for type checking.

[johncolanduoni]

I left the first argument of the equality type implicit, written fully it’s ==(0, X, rec_0(0, X)) since those terms are both of type 0.

The overall expression is shorthand for any term whose typechecking involves that type assertion. For example, type checking passing the term to the left of the colon to an identity lambda with argument type of the term to the right of the colon (λ(x: ==(0, X, rec_0(0, X))).x)(id(X)) will pass iff the left term’s type is right term.

I’m not talking about extensional type theories here (as Idris/MLTT is not extensional), so I don’t think I understand the relevance of the trace annotated proof. Idris will let you write the term I have above without any trace annotations so its typechecker must do something with it.

You’re right that a trace-annotated raw syntax doesn’t need normalization assumptions, but Idris is not trace annotated; the type checking algorithm is required to perform any normalization required without further direction from the user.