Higher-order logic takes first-order logic up a notch. It lets us talk about functions and predicates as objects themselves, not just things that act on other objects. This opens up a whole new world of expressiveness in our logical language.
The syntax and semantics of higher-order logic build on what we know from first-order logic. We get new types, terms, and formulas that let us quantify over functions and predicates. This power comes with some trade-offs in completeness and compactness.
Syntax of Higher-Order Logic
Types and Type Constructors
- Higher-order logic extends first-order logic by allowing quantification over predicates and functions, in addition to quantification over individuals
- Types in higher-order logic can be built from base types using type constructors
- Base types include individuals and truth values
- Type constructors include function types and product types
- Function types represent the type of functions from one type to another (e.g., $\alpha \rightarrow \beta$ represents functions from type $\alpha$ to type $\beta$)
- Product types represent the type of tuples or ordered pairs of elements from different types (e.g., $\alpha \times \beta$ represents pairs of elements from types $\alpha$ and $\beta$)
Terms and Formulas
- Terms in higher-order logic include variables, constants, function applications, and lambda abstractions
- Variables represent arbitrary elements of a given type
- Constants represent fixed elements of a given type
- Function applications represent the result of applying a function to an argument
- Lambda abstractions represent anonymous functions
- Formulas in higher-order logic are built from atomic formulas using logical connectives and quantifiers, similar to first-order logic
- Atomic formulas include predicate applications and equalities between terms
- Logical connectives include conjunction ($\land$), disjunction ($\lor$), implication ($\rightarrow$), and negation ($\neg$)
- Quantifiers include universal quantification ($\forall$) and existential quantification ($\exists$) over variables of any type
- Higher-order logic allows for the construction of more expressive formulas compared to first-order logic
- Quantification over predicates enables expressing properties of predicates (e.g., $\forall P. P(a) \rightarrow P(b)$)
- Quantification over functions enables expressing properties of functions (e.g., $\exists f. \forall x. f(x) = x$)
Semantics of Higher-Order Logic
Typed Lambda Calculus and Interpretation
- The semantics of higher-order logic is based on a typed lambda calculus, which provides a foundation for interpreting terms and formulas
- In higher-order logic, the domain of discourse includes not only individuals but also functions and predicates
- The interpretation of a higher-order logic formula assigns meanings to the non-logical symbols (constants and variables) and determines the truth value of the formula
- Constants are assigned specific elements of the appropriate type in the domain
- Variables are assigned arbitrary elements of the appropriate type in the domain
- Function symbols are assigned functions of the appropriate type in the domain
- Predicate symbols are assigned relations of the appropriate type in the domain
Expressiveness and Meta-Logical Properties
- Higher-order logic allows for the interpretation of predicates and functions as elements of the domain, enabling quantification over them
- Predicates can be interpreted as subsets of the domain or as characteristic functions
- Functions can be interpreted as mappings between elements of the domain
- The semantics of higher-order logic is more expressive than first-order logic, as it can capture properties and relations of functions and predicates
- Higher-order logic can express concepts like inductive definitions, recursion, and continuity
- Higher-order logic can formalize mathematical theories like topology, analysis, and category theory
- However, the increased expressiveness of higher-order logic comes at the cost of some meta-logical properties, such as completeness and compactness, which hold for first-order logic
- Gödel's incompleteness theorems apply to sufficiently expressive higher-order theories
- The compactness theorem does not hold for higher-order logic in general
Inference Rules for Higher-Order Logic
Extending First-Order Inference Rules
- Higher-order logic extends the rules of inference from first-order logic to accommodate the additional features of higher-order syntax and semantics
- The basic rules of inference, such as modus ponens, modus tollens, and hypothetical syllogism, still apply in higher-order logic
- Modus ponens: from $\varphi$ and $\varphi \rightarrow \psi$, infer $\psi$
- Modus tollens: from $\varphi \rightarrow \psi$ and $\neg \psi$, infer $\neg \varphi$
- Hypothetical syllogism: from $\varphi \rightarrow \psi$ and $\psi \rightarrow \chi$, infer $\varphi \rightarrow \chi$
- Additional rules of inference are introduced to handle the higher-order features, such as rules for lambda abstraction and application, and rules for quantification over predicates and functions
- Beta-reduction: $(\lambda x. t) s$ can be reduced to $t[s/x]$ (substituting $s$ for $x$ in $t$)
- Eta-conversion: $\lambda x. f x$ can be converted to $f$ (if $x$ is not free in $f$)
- Quantifier instantiation and generalization rules for higher-order quantifiers
Constructing Proofs and Automated Reasoning
- The rules of inference in higher-order logic allow for the construction of proofs by deriving new formulas from given premises using valid inference steps
- Proofs in higher-order logic can be more complex than those in first-order logic due to the increased expressiveness of the language
- Higher-order proofs often involve reasoning about functions and predicates
- Induction principles and recursive definitions are commonly used in higher-order proofs
- Automated theorem proving systems and proof assistants, such as HOL Light and Coq, provide tools for constructing and verifying proofs in higher-order logic
- These systems implement the inference rules and provide tactics for automating proof steps
- Interactive theorem provers allow for the development of large-scale formal proofs in various domains (e.g., mathematics, computer science, and logic itself)