Validity in first-order logic is undecidable

Identifier: F:fol-validity-undecidable
Proof route: Not assigned
External status: proved
Axiom footprint: Empty

Recorded description

There is no algorithm that, given an arbitrary sentence of first-order logic with at least one binary relation symbol, decides whether it is valid in every model.

Formal statement

; NOT EXPRESSIBLE. The proposition quantifies over algorithms and over the set of all first-order sentences. axeyum has no term for either, and the statement is about the non-existence of a decision procedure rather than about the truth of any sentence, so no assertion of ours has it as a consequence of unsatisfiability.

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

Provenance

{
  "date": "2026-08-14",
  "established_by": "not established in this ledger",
  "source": "authored from the S:logic-and-proof strand of the math-education concept graph; statement written here, not copied",
  "prior_art": [
    {
      "citation": "Church 1936; Turing 1936",
      "establishes": "the theorem, long settled"
    }
  ]
}