Girard's paradox constructs a non-normalizing proof of False. You could read Hurken's "A simplification of Girard's paradox", or maybe Kevin Watkin's formalization in Twelf.
In general, these questions are not equivalent, though they often coincide. A "reasonable" type theory will by inspection have no normal proofs of False, and so then normalization implies consistency. The inverse (non-normalization => proof of False) is much less obvious, and it is certainly possible to construct reasonable paraconsistent type theories, where non-termination is confined under a monad and does not result in a proof of False.
No comments:
Post a Comment