Has somebody worked out a typed higher order logic? I mean something like type theory but not with this intuitionistic touch. Is there a natural deduction system for this logic?

  • 6
    $\begingroup$ "Type theory in classical logic" sounds like a description of Russell and Whitehead's "Principia Mathematica" and lots of simplifications and variations. Also, to get classical type theory from your favorite intuitionistic type theory, you could just add the law of the excluded middle as an axiom. If neither of those observations answers your first question, then you should probably clarify the question. $\endgroup$ Sep 16, 2015 at 17:01

2 Answers 2


Russell & Whiteheads theory is perhaps a bit on the heavy side, but here are some references to support Andreas Blass' comment:

In general most kinds of intuitionistic type theory are agnostic about excluded middle and you can simply turn them into classical theories by postulating excluded middle.


From the viewpoint of semantics, higher order intuitionistic logic is what you get from the internal logic of an (elementary) topos.

For classical higher-order logic, take a boolean topos.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.