nLab higher-order logic





The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



A higher-order logic is any logic which features higher-order predicates, which are predicates of predicates or of operations. If we think of a predicate as a function to truth values, then a higher-order predicate is a function on a power set or a function set.

Typed higher-order logic may be called higher-order type theory. Typed higher-order intuitionistic logic is often identified with the internal logic of a topos.

There are also examples of dependently typed higher-order logics. One example of a dependently typed higher-order logic is a dependent type theory with a separate type judgment, identity types, dependent sum types, dependent product types, weak function extensionality, a type of all propositions, and a natural numbers type. This uses the propositions as some types interpretation of dependent type theory.


  • Colin Rothgang?, Florian Rabe?, Christoph Benzmüller?, Theorem Proving in Dependently-Typed Higher-Order Logic – Extended Preprint, The 29th International Conference on Automated Deduction (CADE-29), July 1-5, 2023. (arXiv:2305.15382)

Last revised on January 5, 2024 at 00:24:56. See the history of this page for a list of all contributions to it.