Can a term on normal form prove an illogical assertion? Suppose we take a language such as Agda and disable the features that make it consistent; for example, universe polymorphism, structural recursion checks and similar. Suppose then that we take a term in normal form, i.e., with no redex left. Could that term prove an absurd claim such as, for example, 1 = 2, despite the fact it is normalised (and, thus, doesn't include infinite loops)?
I'll turn my comments into an answer: In general, if you do not have any axioms or "stuck" terms, you cannot have a normal proof of $\mathrm{False}\simeq\forall X:*,X$ in a system like the CoC (or extensions of it). The (classical) proof I outlined here applies, crucially using inversion in several places.

I believe it's not hard to have a normal proof of $\mathrm{True}\rightarrow\mathrm{False}$ in an inconsistent system, however, by "blocking" some of the redexes with a variable. Applying this proof to any closed term of type $\mathrm{True}$ would then lead to non-termination.



This leads to a pretty natural question, which I will also outline here: is it possible to reason correctly about programs in an inconsistent language, as long as every "proof-like" term is normalized?

The answer to this seems to be mostly affirmative, though the meta-theory is quite finicky: it's easy to lose even type preservation if one is not careful!

The most comprehensive exploration of this idea to my knowledge is the PhD dissertation of Vilhelm Sjöberg: A Dependently Typed Language with Nontermination.