Higher-order logic

Summary

Higher-order logic extends first-order logic with variables, and quantifiers, for relations on elements, relations on such relations, and so on at every finite level. Each variable carries a type that says at which level it lives. It is the logic behind simple type theory and several proof assistants, such as Isabelle/HOL.