By semantic paradoxes, I mean like the Liar paradox, Curry paradox, Knower paradox, etc.
In classical (logic) settings, we would need to extend the language with a predicate P (truth or is-known predicate) and its corresponding intro and elim inference rules/axioms to get a paradoxical derivation.
P(⌜φ⌝) ⊢ φ and φ ⊢ P(⌜φ⌝)
(while φ is a proposition, ⌜φ⌝ is a constant denoting the proposition)

I'm wondering, given that it (seems to me) is possible to modify type theory with the above extension (we'd probably need at least λP to get predicate?), can we prove a version of any of the semantic paradoxes? I'm pretty new to type theories in general so I'm not sure.

If it is possible: Could anyone point me in the right direction? I would love to do it as an exercise. My background in type theory is having read the first half of Type Theory and Formal Proof.

If it is impossible: It is known that any proof of the Liar paradox has no normal form (nf of proofs). Is the normal form of terms the corresponding concept in type theory by the Curry Howard Isomorphism? Is this why there is no such proof in type theory because of Strong Normalization?



Your Answer

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

Browse other questions tagged or ask your own question.