basic constructions:
strong axioms
further
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 called the domain of discourse, and for each type and each term , a type of predicates on whose terms are propositions dependent on . The system consisting of the type universe , the domain of discourse , and the power type functor is a natural numbers object.
propositional logic (0th order)
predicate logic (1st order)
higher order logic
higher-order set theory?
Last revised on May 28, 2023 at 19:53:29. See the history of this page for a list of all contributions to it.