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.
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.
propositional logic (0th order)
predicate logic (1st order)
higher order logic
Last revised on January 5, 2024 at 00:24:56. See the history of this page for a list of all contributions to it.