First-order, second-order, and higher-order logics form a hierarchy of increasing expressive power. Each level builds on the previous, allowing quantification over more complex entities and capturing more sophisticated mathematical concepts.
However, this increased expressiveness comes at a cost. While first-order logic has nice properties like completeness and compactness, higher-order logics sacrifice these for greater power. This trade-off shapes their use in different areas of mathematics and computer science.
Logical Properties
Expressive Power and Limitations
Top images from around the web for Expressive Power and Limitations Frontiers | Cortical Contributions to Higher-Order Conditioning: A Review of Retrosplenial ... View original
Is this image relevant?
Frontiers | Cortical Contributions to Higher-Order Conditioning: A Review of Retrosplenial ... View original
Is this image relevant?
1 of 2
Top images from around the web for Expressive Power and Limitations Frontiers | Cortical Contributions to Higher-Order Conditioning: A Review of Retrosplenial ... View original
Is this image relevant?
Frontiers | Cortical Contributions to Higher-Order Conditioning: A Review of Retrosplenial ... View original
Is this image relevant?
1 of 2
First-order logic has limited expressiveness compared to higher-order logics
Cannot quantify over predicates or functions, only variables
Struggles to express concepts like infinity, finiteness, or connectedness
Second-order logic extends first-order logic by allowing quantification over predicates and functions
Can express properties of relations and functions directly (continuity)
Captures important mathematical concepts first-order logic cannot (Peano arithmetic, real analysis)
Higher-order logics further extend quantification to predicates and functions of higher types
Even more expressive than second-order logic (can define truth predicates)
Useful for formalizing mathematics and computer science (type theory, category theory)
Decidability and Completeness Properties
First-order logic is semi-decidable
Valid formulas are recursively enumerable, but invalid ones may not be
Has a complete proof system (all valid sentences are provable)
Second-order logic and higher-order logics are not decidable in general
Validity is not recursively enumerable due to higher expressiveness
Do not have complete proof systems (Gödel's incompleteness theorems)
Restricted fragments of higher-order logics can be decidable (propositional, monadic)
Compactness and Löwenheim-Skolem Properties
First-order logic has the compactness property
If every finite subset of a set of sentences has a model, the whole set has a model
Useful for constructing models (ultraproducts, nonstandard analysis)
First-order logic satisfies the Löwenheim-Skolem theorems
If a sentence has an infinite model, it has models of all infinite cardinalities
Leads to non-categoricity of first-order theories (Peano arithmetic has nonstandard models)
Second-order logic and higher-order logics do not have compactness or Löwenheim-Skolem properties in general
Due to the expressive power to characterize infinite structures up to isomorphism (standard model of arithmetic)
Theoretical Foundations
Model-Theoretic Semantics
First-order logic has a well-developed model theory based on structures and interpretations
Structures consist of a domain of discourse and interpretations of function and predicate symbols
Satisfaction relation defined inductively on the structure of formulas
Second-order logic extends first-order semantics with second-order variables and quantifiers
Variables range over subsets and functions on the domain
Full semantics vs. Henkin semantics (nonstandard models)
Higher-order logics have a more complex model theory due to the hierarchy of types
Often interpreted in typed structures or extensional models (all functions and predicates included)
Can also have intensional or nonstandard semantics (general models)
Proof-Theoretic Aspects
First-order logic has a variety of complete proof systems
Hilbert-style systems, natural deduction , sequent calculus
Proofs are finite syntactic objects, can be checked algorithmically
Second-order logic does not have a complete proof system with standard semantics
Categorical theories like Peano arithmetic are not recursively axiomatizable
Henkin semantics allow for a wider class of models and complete proof systems
Higher-order logics have proof systems based on typed lambda calculi
Curry-Howard correspondence relates proofs and programs (dependent type theory)
Proof assistants implement higher-order proof systems (Coq, Isabelle/HOL)
Computational Aspects
Computational Complexity and Decidability
First-order logic has many decidable fragments used in computer science applications
Propositional logic is decidable and NP-complete (SAT solvers)
Monadic first-order logic and two-variable logic are decidable (description logics, modal logics)
Second-order logic is not decidable, but has decidable fragments
Monadic second-order logic over finite structures (WS1S) used in verification (Buchi automata)
Weak second-order logic restricts quantification to finite sets (decidable)
Higher-order logics are generally not decidable, but have important computable fragments
Higher-order recursive functions (System T) and polymorphic lambda calculus (System F)
Constructive type theories used in proof assistants (Calculus of Constructions)
Abstraction Levels and Applications
First-order logic is used in many areas of computer science for specification and modeling
Database query languages (SQL), knowledge representation (description logics)
Program verification (Hoare logic), model checking (temporal logics)
Second-order logic can express important program properties not captured by first-order logic
Transitive closure, graph connectivity (monadic second-order logic)
Program schemes and software synthesis (weak second-order logic)
Higher-order logics are used in programming language theory and formal verification
Type systems and semantics of functional programming languages (polymorphic lambda calculus)
Hardware and software verification using proof assistants (Coq, Isabelle/HOL)
Automated theorem proving in higher-order logic (TPS, LEO)