Phil 2250 18JUN26

Shared on June 18, 2026

Second‑Order Logic – Lecture Notes

Overview

The lecture explains why the usual predicate logic (first‑order logic, FOL) cannot capture certain natural‑language sentences and mathematical principles.

It introduces second‑order logic (SOL) as a language that can quantify over predicates (properties) in addition to objects.

SOL is strictly more expressive than FOL, enabling the formalization of mathematical induction, identity, and many set‑theoretic notions.

However, this expressive power comes at a cost: SOL is undecidable, the Löwenheim–Skolem theorem fails, and no sound and complete derivation system exists for SOL.

Key Concepts

Concept	What It Is	Why It Matters
Quantification over predicates	∀X, ∃X where X is a predicate variable	Allows sentences like “There exists a collection of critics” that cannot be expressed in FOL.
Mathematical induction	Expressed as ∀P[(P(0) ∧ ∀n(P(n) → P(n+1))) → ∀m P(m)]	Requires quantification over all properties P of natural numbers; not expressible in FOL.
Identity via Leibniz’s Law	∀t₁,t₂(t₁ = t₂ ↔ ∀X(Xt₁ ↔ Xt₂))	Defines equality purely in terms of shared properties; a purely logical notion of identity.
Undecidability of SOL	No algorithm can determine validity for all SOL sentences	Solves the “decision problem” for all logical truths? No.
Löwenheim–Skolem failure	No guarantee of countable or finite models for every consistent SOL theory	Contrasts with FOL, where every satisfiable theory has a countable model.
Incomplete derivation system	No finite rule set can derive all valid SOL entailments	Makes SOL less practical for automated proof search.
Derivation system 2D	Extension of FOL’s derivation rules with two new rules for each second‑order quantifier	Sound but provably incomplete.

Detailed Notes

1. Limitations of First‑Order Logic

First‑order quantifiers (∀x, ∃x) range over objects only.

Sentences that speak about collections or properties of collections (e.g., “some critics admire only each other”) cannot be symbolized.

Example:

  ∃x[Cx ∧ ∀y(Axy → Cy)]   (FOL attempt)

fails to capture “the entire collection of critics” because it only quantifies over individuals, not over the set of all critics.

2. Extending to Second‑Order Logic

Predicate variables (capital letters X, Y, Z, …) are introduced.

Quantification rules:

  (∀X)φ   (∀X) introduces a universally quantified predicate.
  (∃X)φ   (∃X) introduces an existentially quantified predicate.

Syntax & semantics:

A predicate variable X denotes a subset (or more generally a relation) of the universe.

A sentence ∀X Xa is true iff every property of the universe contains a.

Expressive power:

Induction, identity, and many set‑theoretic definitions become expressible.

Example of induction in SOL:

    ∀P[(P(0) ∧ ∀n(P(n) → P(n+1))) → ∀m P(m)]
    ```
### 3. Defining Identity in SOL
- **Leibniz’s Law**:

t1 = t2 iff ∀X(Xt1 ↔ Xt2)

- This definition is *purely logical*: two terms are equal exactly when they share every property.
### 4. Meta‑theoretic Properties of SOL
- **Undecidable**:  
  - Because SOL can encode any FOL sentence, it inherits FOL’s undecidability.  
  - No algorithm can decide validity for all SOL sentences.
- **No Löwenheim–Skolem**:  
  - Consistent SOL theories may have only uncountable models; countable models are not guaranteed.
- **No Complete Derivation System**:  
  - Derivation systems are finite sequences of symbols; there are *uncountably many* SOL entailments (due to quantification over all subsets of the universe).  
  - Hence any finite derivation system must miss some valid entailments.
### 5. The Derivation System 2D
- **Base**: All rules of the first‑order system (e.g., SD for sentential logic, PD for predicate logic).  
- **Added rules**:  
  - For each second‑order quantifier, an introduction and elimination rule (four new rules total).  
- **Soundness**: 2D preserves truth—every derivation in 2D is a valid entailment in SOL.  
- **Incomplete**: 2D cannot derive all valid SOL entailments; thus it is not useful for a complete proof system.
### 6. Practical Implications
- **Formalizing mathematics**:  
  - SOL allows us to formalize concepts that require quantification over properties (e.g., set theory, arithmetic induction).  
  - However, due to incompleteness and undecidability, SOL is rarely used as a proof engine; instead, FOL or fragments with good algorithmic properties are preferred.  
- **Philosophical insight**:  
  - The limits of SOL illustrate that increasing expressive power inevitably reduces decidability and completeness—an important lesson in logic and the philosophy of mathematics.
---
**Take‑away:**  
Second‑order logic extends first‑order logic by allowing quantification over predicates, enabling the formalization of induction, identity, and many set‑theoretic concepts. This extra expressiveness, however, comes at a high cost: SOL is undecidable, lacks the Löwenheim–Skolem property, and admits no sound and complete derivation system. As a result, while SOL is theoretically powerful, it is seldom used in practical automated reasoning.