type theory, homotopy type theory
material set theory
structural set theory
axioms of choice:
large cardinal axioms:
Edit this sidebar
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.
Higher-order intuitionistic logic is often identified with the internal logic of a topos.
propositional logic (0th order)
predicate logic (1st order)
higher order logic