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

• 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)