Post #952394
2025-12-18 14:13 UTC
Learned recently from Simon Boulier et al.’s paper on syntactic models and subsequent papers to give a model of type theory which refutes, for example, the function extensionality. The syntactic model is fairly easy to construct and instructive. I wonder if there are classical principles, such as LEM, that can be refuted easily this way. 🤔
Replies (1)
-
@yforster@types.pl 2025-12-18 14:37
@ltchen exceptional type theory by Tabareau and Pédrot (which predates the Boulier et al paper I think) has a model refuting even LPO! (well, even MP, but that's a corrollary)