First-Order Nondefinability¶
A property of structures for which no sentence in a specified first-order language exactly separates its instances within a declared comparison class.
Core Idea¶
A property is first-order nondefinable relative to a particular language and class of structures when no one sentence in that language is true in exactly the structures in the class that have the property.[1][2] The language, comparison class and property are essential parts of the claim. Changing any of them can change whether a defining sentence exists.
This does not say that a natural-language statement can never be formalized, or that a property cannot be described in a richer language. It says that the stated first-order sentence-level classification fails on the stated class.
Scope of Application¶
The test applies to properties of whole structures under a declared first-order signature. Finiteness is nondefinable over the class of all equality structures, finite and infinite.[1] Connectivity is nondefinable over finite ordered graphs when sentences may use both adjacency and linear order.[2] These are different mathematical carriers and require different proofs.
Clarity¶
Ask four questions: Which nonlogical symbols are allowed? Which structures count? What property is being classified? Must one sentence agree with the property on every structure in that class? This avoids calling finiteness “undefinable” on a class that contains only finite structures, where a tautology suffices. It also distinguishes a sentence classifying whole structures from a formula with free variables defining a subset inside one structure.
Manages Complexity¶
The same four-part record keeps proof obligations attached to the cases they actually support. Zach's finiteness argument uses first-order compactness over finite and infinite equality structures.[1] Dawar's ordered-graph connectivity argument uses a definable reduction from parity on finite linear orders.[2] The word “nondefinable” does not let one substitute the first proof for the second.
Abstract Reasoning¶
For finiteness, assume a sentence defines exactly the finite structures. Add sentences requiring at least one, two, three and so on distinct elements.[1] Every finite subset is satisfiable in a sufficiently large finite structure.[1] Compactness would make the entire collection satisfiable; that model would have to be both finite and infinite.[1]
For finite ordered graphs, assume a sentence defines connectivity. Dawar constructs a graph from each finite linear order so that the graph is connected or disconnected according to the order's parity.[2] The assumed sentence would then define parity, which first-order logic cannot do on finite linear orders.[2]
Knowledge Transfer¶
The reusable step is to name the language, comparison class, target and required sentence before seeking an impossibility proof. Compactness, parity reductions and other proof tools are local: carry them to a new problem only if their hypotheses still hold. A result about all structures does not automatically establish the corresponding result over finite ordered structures.
Examples¶
Finiteness. In equality structures of arbitrary size, no first-order sentence picks out exactly the finite domains.[1] Mapped back: equality signature → all-size class → finite target → compactness rules out an exact sentence. Limit the class to finite structures and this example exits.
Ordered-graph connectivity. In the (E,<) language on finite ordered graphs, no first-order sentence picks out exactly the connected graphs.[2] Mapped back: adjacency-plus-order signature → finite ordered graph class → connected target → parity reduction rules out an exact sentence.
Neighborhood in Abstraction Space¶
First-Order Nondefinability sits in a sparse region of the domain-specific corpus (70th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Graph Structures & Combinatorial Objects (46 abstractions)
Nearest neighbors
- A-paracompact Space — 0.84
- Universal property — 0.84
- Wilf Equivalence — 0.84
- Emptiness problem — 0.83
- Complete variety — 0.83
Computed from structural-signature embeddings · 2026-10-25
Not to Be Confused With¶
Definable Set concerns a formula-selected subset or relation in one structure, sometimes with parameters. Second-Order Logic is a richer syntax and semantic family; it is not a prerequisite to this first-order failure test. Formal System requires axioms, inference rules and derivation closure, which a semantic definability question does not. Independent full-signature review therefore leaves this entry an approved unparented root, without an invented parent edge. The frozen Geach–Kaplan sentence source member has other claims still under review and is not an unqualified alias here.
References¶
[1] Richard Zach, Intermediate Logic (course edition based on The Open Logic Text), Example 8.26, printed p. 124 (physical PDF p. 131). https://builds.openlogicproject.org/courses/phil310/phil310-ebook.pdf registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g
[2] Anuj Dawar, Topics in Logic and Complexity, Handout 3, parity and connectivity proof/reduction, physical PDF pp. 15–19. https://www.cl.cam.ac.uk/teaching/2122/L15/notes3.pdf registry ↩a ↩b ↩c ↩d ↩e ↩f