Higher-Order Logic
Definition
Higher-order logic extends second-order logic by allowing variables for objects built over lower types, such as relations between relations or functions that take functions as arguments. Type theory is the systematic typed presentation of this idea: variables come with types, and well-formed expressions respect those types.
Why It Matters
Higher-order logic is the conceptual neighborhood of proof assistants, typed programming languages, and mechanized mathematics. It gives enough structure to express functions, predicates, quantification over predicates, and proof objects in a disciplined way, which is why many proof systems use some higher-order or type-theoretic core.
Formalism / Key Objects
- A simple type hierarchy starts with an individual type, often written
i, and builds function or relation types from lower types. - Second-Order Logic is the first higher step: it allows variables for relations and functions over individuals.
- Higher orders allow variables whose values depend on lower-type objects, such as a predicate on predicates:
- In proof assistants, propositions can often be represented as types and proofs as terms inhabiting those types.
- Lean Theorem Prover is not merely “second-order logic in software”; it sits in a dependent type-theoretic ecosystem with inductive types, universes, elaboration, and tactics.
Connections
- Second-Order Logic supplies the immediate predecessor and many of the semantic issues that higher-order logic inherits.
- Intuitionistic Logic is connected through propositions-as-types and constructive proof readings.
- Lean Theorem Prover gives a practical, modern route from higher-order/type-theoretic logic to machine-checked mathematics.
- Lean Proof Terms and Tactics captures the proof-term/tactic interface that makes the type-theoretic route operational.
- Formal Methods uses higher-order and type-theoretic systems for mechanized proof, verified programs, and formalized mathematics.
Common Confusions
- Higher-order logic is not automatically the same thing as set theory, although set theory is often used as a metatheory for its semantics.
- Type theory is not just syntax decoration; types determine which higher-order objects can be formed and quantified over.
- Proof assistants vary: some use classical higher-order logic, some use dependent type theory, and some add classical axioms on top of constructive cores.