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.
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.