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.

Higher-order logic in general could be thought of as a first order theory with dependent types. There is a type VV called the domain of discourse, and for each type TT and each term t:Tt:T, a type of predicates on T T 𝒫(T)\mathcal{P}(T) whose terms P(t):𝒫(T)(t)P(t):\mathcal{P}(T)(t) are propositions dependent on tt. The system (𝒰,V:𝒰,𝒫:𝒰𝒰)(\mathcal{U}, V:\mathcal{U}, \mathcal{P}:\mathcal{U}\rightarrow\mathcal{U}) consisting of the type universe 𝒰\mathcal{U}, the domain of discourse VV, and the power type functor 𝒫\mathcal{P} is a natural numbers object.


  • 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 November 13, 2023 at 05:18:35. See the history of this page for a list of all contributions to it.