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 specified language and comparison class when no single first-order sentence in that language is true in exactly the structures in that class that have the property.[1][2] The language determines which relation and function symbols a sentence may use; the class determines which structures it must classify. Leaving either unstated can change the answer.
The failure concerns exact agreement across a class of structures. It does not assert that a particular structure lacks a description, that an ordinary-language sentence has no useful formalization, or that a richer logic is always required. A sentence has no free variables; a formula with free variables that selects a subset inside one structure poses a different definability question. Parameters, if admitted into a language, must be declared.
Two distinct failures show the same test. Finiteness of a domain cannot be defined by a first-order sentence over all equality structures, because compactness defeats every proposed sentence.[1] Connectivity cannot be defined by a first-order sentence over finite ordered graphs in the vocabulary of edge adjacency and linear order, because a definable construction would then give a first-order test for the parity of finite linear orders.[2]
Structural Signature¶
Sig role-map: first-order signature + comparison class + target property → candidate sentence → exact-agreement test over every structure in the class → nondefinability if every candidate fails.
- Signature. Fix the nonlogical symbols before asking what a first-order sentence can say. Pure equality is enough for the finiteness example; the graph example supplies adjacency and order.[1][2]
- Comparison class. Fix the domain of comparison, including whether infinite structures are permitted. Finiteness is nondefinable over all equality structures[1] but is trivially true throughout the class of finite equality structures.
- Target property. State the exact positive cases: finite domains in the first example, connected graphs in the second.
- Sentence-level failure. A proof must rule out each first-order sentence in the chosen signature as an exact classifier on the chosen class. It may do this by compactness, reduction or another valid obstruction; the proof method is not the identity.
- Satisfaction comparison. Interpret each candidate sentence in each structure in the declared class and compare its truth value with the target property's truth value. A counterexample for every candidate establishes failure; one exact candidate ends the claim.
What It Is Not¶
The logical compactness theorem is a proof tool for the finiteness case, not a synonym for nondefinability. It says that a first-order theory has a model when every finite subset is satisfiable.[1] Dawar's finite ordered-graph result instead uses a reduction from parity of finite linear orders; compactness across arbitrary structures alone does not prove that bounded-class result.[2]
Nor is this the same as second-order logic. Second-order vocabulary can express some properties that escape first-order sentences, but the present test asks whether a first-order sentence works in a declared signature and class. A successfully definable set is a subset or relation picked out by a formula in a structure, sometimes with parameters; it is a neighboring definability problem, not this class-level failure.
Scope of Application¶
Use the term only after specifying the language, comparison class, target property and the sort of defining expression. Changing from all structures to finite structures, adding an order relation, admitting constants or parameters, or allowing a theory rather than one sentence changes the question. A failure proved for one choice does not automatically transfer to another.
For example, the compactness proof for finiteness relies on structures of arbitrarily large finite size and on infinite models being in the comparison class.[1] In the finite ordered graph case, the order symbol is already available, so an argument that ignores it is insufficient; Dawar explicitly handles the ordered vocabulary.[2]
Clarity¶
This concept turns “first-order logic cannot express it” into a checkable four-argument claim. The analyst can ask which vocabulary is allowed, which structures count, which property is targeted, and whether one sentence must work everywhere. It reveals why “finiteness is undefinable” is false if the comparison class has already been restricted to finite structures, and why an unordered-graph argument does not settle an ordered-graph claim. It also separates a property of whole structures from a set defined by a formula inside one structure.
Manages Complexity¶
The signature/class/property/sentence map prevents unlike impossibility arguments from being conflated. It compresses each result into a reusable record with its own proof obligation: equality structures plus finiteness plus compactness,[1] or finite ordered graphs plus connectivity plus parity reduction.[2] The map does not replace either proof. It tells a reader which assumptions must accompany the proof and which change invalidates its reuse.
Abstract Reasoning¶
Reason by contradiction with a proposed sentence. In the finiteness case, the sequence of lower-bound sentences forces an infinite model by compactness while the proposed defining sentence demands a finite one.[1] In the finite ordered graph case, Dawar's definable construction transports a hypothetical connectivity sentence into a forbidden parity test.[2] These are two ways to show the same universal failure condition—every candidate sentence fails—under different carriers and assumptions. The source-bound proof, rather than the word “undefinable,” carries the inference.
Knowledge Transfer¶
The useful transfer is methodological within logic. When evaluating another property, first carry over the role map, then seek a proof suited to its signature and comparison class. A compactness proof transfers only if it has the requisite arbitrarily large finite satisfiability and an admissible infinite-model contradiction; a parity reduction transfers only after a source-valid interpretation in the target vocabulary. This makes the analogy diagnostic without assuming that every first-order limit has the same cause.
Examples¶
Canonical: finiteness across equality structures¶
Let the language contain equality and let the comparison class contain all finite and infinite structures in that language. Suppose a sentence F holds exactly in the finite ones. For every natural number n, a first-order sentence Bₙ requires at least n distinct objects.[1] Every finite subset of {F, B₁, B₂, ...} has a finite model large enough to satisfy it.[1] Compactness would give a model of the entire set: F calls that model finite, while all the Bₙ require it to be infinite.[1] This is impossible.
Mapped back: fixed equality signature → all-size comparison class → finite-domain target → no equivalent first-order sentence. The proof is stronger than needed: the source also rules out any first-order theory whose models are exactly the finite structures.[1] As a boundary test, restrict the comparison class to finite structures only; a tautology then defines the target, so this nondefinability claim exits.
Applied: connectivity in finite ordered graphs¶
Let finite graphs carry an edge relation E and a linear order <. Dawar proves that no sentence of first-order logic over (E,<) defines connectedness on all such graphs.[2] An assumed sentence would, through a first-order definable graph construction on finite linear orders, distinguish even from odd order sizes.[2] The constructed graph has one cycle when the order size is odd and two disjoint cycles when it is even.[2] First-order logic cannot define parity on finite linear orders, so the supposed connectivity sentence cannot exist.[2]
Mapped back: ordered graph signature → finite ordered comparison class → path-connected target → no equivalent first-order sentence. The carrier and proof obstruction differ from the finiteness case. To apply the result to another graph vocabulary, recheck that Dawar's reduction remains expressible there.
Structural Tensions¶
T1: More expressive vocabulary vs. easier impossibility proofs. A richer signature gives candidate sentences more tools, so a nondefinability theorem that survives the added symbols is more informative, but typically needs a proof that accounts for those symbols. A sparse signature makes an obstruction easier to obtain, but may miss the language in which the target is actually studied. Diagnostic: Is the result proved with every symbol in the claimed signature, especially the order relation in the graph case?
T2: Broad comparison class vs. relevant restricted class. A broad class may make nondefinability easier to show because one counterexample can lie outside the intended application; the resulting theorem may say too little about a finite-only setting. A restricted class gives a more relevant theorem, but removes some available obstructions and can make the property trivially definable. Diagnostic: Would the same proposed sentence still fail if comparison were limited to the structures of interest?
T3: Exact equivalence vs. useful bounded surrogates. Requiring one sentence to agree with a property on every structure in a declared class makes the result mathematically sharp, but can rule out a sentence that classifies a useful bounded subfamily correctly. Narrowing the class may recover a workable surrogate, at the cost of losing the original full-class guarantee. Diagnostic: Is a proposed formalization exact on the declared class or only on a smaller application family?
Structural–Framed Character¶
Vocabulary travels: “Definability” and “expressive limit” travel across logic and nearby formal settings, but “first-order sentence” and “structure” have technical meanings that do not transfer merely with the words. Evaluative weight: nondefinability is a theorem relative to a language and class; it does not rank the language as useful or deficient. Institutional origin: course texts and research traditions establish conventions and proofs, but no institution makes a property nondefinable. Human-practice bound: people select languages and comparison classes; once these are fixed, satisfaction and the proof obligation are mathematical. Import versus recognition: a new model-theory example satisfying the same role map is literal recognition, while “our policy cannot express this” without model semantics imports a metaphor. Its character: a formally constrained, domain-specific expressivity limit with reusable tests inside model theory.
Structural Core vs. Domain Accent¶
The portable skeleton is a failure of exact classification under a restricted expressive system. It poses an explicit future-Prime question about whether unlike nonlogical carriers share the same constrained-language, target-class and no-equivalent-expression structure; the present evidence supplies only formal-logical carriers. The domain-specific residual is indispensable: first-order syntax, structures interpreting a fixed signature, sentences evaluated across a stated class, and proof of no equivalent sentence. Those restrictions keep this entry below the Prime threshold. They also distinguish it from a broad claim that natural language cannot be formalized or from the existence of a second-order expression.
Instantiates / Related Primes¶
The entry is related to live Prime Representation because sentences can represent properties of structures, but this entry is a metatheoretic failure of such representation, not itself the structured target-to-medium mapping required by that Prime's full signature. Prime Formalization concerns the process of making implicit practice explicit; the present theorem can guide a choice of formalism but is not that process. Prime Formal System concerns the symbol/axiom/rule/derivation package; a bare first-order language and class-level definability question do not require a chosen axiom system. The entry also neighbors the live domain entries Definable Set and Second-Order Logic. Independent full-signature review found no necessary genus or prerequisite among these or the other tested catalog neighbors, so the typed placement is an approved unparented root, with no invented edge.
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¶
- A free-variable definable set. That is a subset or relation selected inside a structure; this entry concerns a sentence classifying whole structures.
- A fixed-model truth value. Agreement on one interpretation does not show agreement over the declared comparison class.
- Unrestricted graph connectivity. A compactness argument over arbitrary graphs does not by itself establish the finite ordered graph result.
- Geach–Kaplan sentence. The original source member also raises plural semantics, historical and arithmetic claims. Those are being separately reviewed; the original title is not an unqualified alias for this bounded entry.
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 ↩h ↩i ↩j ↩k ↩l
[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 ↩g ↩h ↩i ↩j ↩k