A canonical first-order structure is generated by its names: every element is the value of a closed term. In the function-free setting permitted here, this means every element is the interpretation of a constant symbol. Equivalently, the natural map from closed terms modulo logical equality in the first-order structure onto its carrier is surjective. When canonical is defined specifically using constant names, the same definition and all the arguments below apply in this function-free setting.
A full set of first-order sentences has the witness property in its own first-order language: whenever it proves an existential sentence , some closed term satisfies that the set proves . In a deductively closed set, one can equivalently state this using membership of the first-order sentences. In the function-free setting the witness first-order term is a constant symbol. This is the Henkin witness property; fullness does not by itself replace the separate requirements of first-order consistency and completeness.
A sufficient condition is that be first-order consistent, complete, and full in its own first-order language. Work in the allowed function-free setting. Since proves the logically valid first-order sentence , fullness guarantees at least one constant and a nonempty collection of names.
Form the carrier from equivalence classes of constant symbols under
Logical equality logic makes this an equivalence relation. Interpret a constant by its class and interpret each relation symbol by
Substitution of equals makes this independent of representatives. This defines a canonical first-order structure because every carrier element is named by a constant.
The truth lemma, proved by induction on logical formulas with constants substituted for their free variables, says
Atomic formulas hold by construction; completeness and first-order consistency give the Boolean steps. For the existential step, a witness in the first-order structure is a named class, so its truth gives a proved instance and hence a proved existential sentence. Conversely a proved existential sentence has a constant witness by fullness, and the induction hypothesis realizes that instance in the first-order structure. The universal case follows by negation. Thus , proving
The witness condition is needed in the original first-order language; adding new constants produces a canonical first-order structure in an expanded first-order language, which is a different assertion.
A prime model of a complete theory is a first-order model admitting an elementary embedding of first-order structures into every first-order model of . Let be canonical and . For each closed term , define
Every element of has a name, so this defines the desired map on all of . If two first-order terms agree in , their logical equality first-order sentence holds in one first-order model of the complete theory and therefore in every first-order model of it; they agree in . This proves well-definedness. If they are distinct in , their inequality holds throughout the complete theory as well, proving injectivity.
For every logical formula and named tuple , the substituted first-order sentence has the same truth value in the two first-order models by completeness of . Consequently
Thus is elementary. Since was arbitrary, every such canonical first-order structure is prime. This formal proof also handles closed-term generation when function symbols are present; under the constant-name convention one simply uses constants as the first-order terms.
A first-order theory is a set of first-order sentences in a fixed first-order language, often identified with its deductive closure. It is -categorical if it has a first-order model of cardinality and all first-order models of that cardinality are isomorphic as first-order structures in that same first-order language. In particular, an isomorphism must preserve the named constants as well as the order.
A first-order theory is complete if it is first-order consistent and decides every first-order sentence: for each it entails either or . Equivalently all its first-order models satisfy exactly the same first-order sentences. First-order consistency is included to exclude the vacuous first-order theory with no first-order models. The distinctions matter here: naming infinitely many ordered points changes countable categoricity without destroying completeness.
Use two expansions of the rational order. In the first interpret , so the named sequence is unbounded above. In the second interpret , so the named sequence is strictly increasing but has upper bounds in the rational order. Both expansions are countably infinite first-order models of the specified first-order theory.
An isomorphism preserving each would preserve the existence of an element greater than all the named constants, since any such element in one first-order structure would map to such an element in the other. The first first-order structure has none and the second has, for instance, . They cannot be isomorphic. Thus
The property of lying above all is an infinite partial type rather than a single first-order sentence. This is why its realization can distinguish the two first-order models without contradicting the completeness established in (iv).
In a countable first-order model, the finitely many named constants split the order into the open intervals
together with the named points. Each interval is a countable dense linear order without endpoints in its induced order. It is nonempty and infinite by density and the absence of endpoints.
Use Cantor's classification of countable dense linear orders without endpoints: each such interval is isomorphic to the rational order. It follows by a back-and-forth method extending finite increasing partial bijections alternately along enumerations of the two orders. Given two first-order models of , choose isomorphisms between their corresponding intervals and send each named point to its counterpart. Their union is an increasing bijection preserving all constants, hence an isomorphism in .
There are countable first-order models, for example any finite increasing list in the rational order. Therefore
For , the same argument is just the classification theorem for the whole order.
Use the completeness of the first-order theory of dense linear orders without endpoints and its quantifier elimination. After naming finitely many increasing constants, quantifier elimination still holds in the expanded first-order language: treat these constants as fixed parameters when eliminating quantifiers. Every quantifier-free sentence is a Boolean combination of logical equalities and order comparisons of the named constants, all decided by their stated strict increasing order. Hence is complete.
An alternative formal proof of this finite case uses the stated general theorem that a first-order theory in a countable first-order language with only infinite first-order models and a unique countable first-order model is complete: if first-order models disagreed on a first-order sentence, downward Löwenheim-Skolem would give disagreeing countable first-order models. Part (iii) supplies the uniqueness.
Every first-order sentence of mentions only finitely many constant symbols, hence belongs to some . Its truth is decided by , and every first-order model of has a reduct satisfying that finite first-order theory. Thus the larger first-order theory also decides every first-order sentence. The rational-order examples in (ii) establish first-order consistency. Consequently
There is no contradiction with (ii): completeness is agreement on individual finite first-order sentences, while categoricity requires a global isomorphism respecting all constants simultaneously.
An -type over a first-order theory is a set of logical formulas in the displayed free variables first-order consistent with . A complete type chooses exactly one of and for each such logical formula. Equivalently it is a maximal consistent such set. For parameter-free partial types the logical formulas use the original first-order language; partial types over parameters use additional names for those parameters.
A partial type is principal if some logical formula first-order consistent with implies every member of modulo :
Such a is a principal formula of a type of the partial type. For a complete type it isolates that partial type, so principal complete types are exactly isolated types.
For a tuple in a first-order structure , its parameter-free partial type is
It is a complete type over because the first-order structure decides the truth of every logical formula at that tuple.
Let , with finite, and put . There are only finitely many competing tuples . For each whose complete type differs from that of , choose a logical formula true at and false at . Such a logical formula exists by the inequality of their complete types, negating a distinguishing logical formula if necessary.
Let be the conjunction of this finite list, or logical truth if the list is empty. It is true at , and every tuple satisfying it has the same partial type as . For each , the first-order sentence
is therefore true in and belongs to . The logical formula is first-order consistent with because it is realized at . It is consequently a principal formula of a type of the partial type, proving every partial type realized in a finite first-order structure is principal. Finiteness of the first-order structure, rather than finiteness of the first-order language, is what makes the conjunction finite.
Every automorphism preserves all logical formulas by induction on their construction, so an automorphism taking to necessarily gives equal partial types.
For the converse, first note that a finite first-order structure is atomic by (ii). Thus in both cases every realized finite-tuple partial type has an isolating logical formula. Suppose two finite tuples have the same complete type, and choose a new element to extend the first tuple. Let isolate the realized partial type of . Since
logical equality of partial types gives . Choose a witness . Isolation ensures and have the same complete type. In particular, if is distinct from the entries already used, their inequality logical formulas ensure is distinct from its corresponding entries. The resulting finite map is injective and partial elementary.
Start from , which is well-defined even for repeated coordinates because their logical equality patterns agree. Enumerate the carrier and extend alternately to include the next missing element in the domain and the next missing element in the range. For a range step apply the same extension argument to the inverse finite map. The union is an elementary bijection from onto itself: every finite tuple and every logical formula involving it is handled at some stage. It is therefore an automorphism taking to . In the finite case the construction terminates once all elements have been included.
Hence
Countability makes the back-and-forth numeralwise enumeration in arithmetic exhaust the entire first-order structure; it cannot simply be dropped.
Use the first-order language with one equivalence relation . Let have exactly two equivalence classes, one countably infinite and one uncountable, with no further first-order structure. Its complete theory says that there are exactly two classes and both are infinite.
This first-order theory has quantifier elimination. To eliminate one existential logical variable from a conjunction of atomic formulas and negated atomic formulas, a logical equality either fixes its value, or finitely many inequalities exclude finitely many points. Its required equivalence-class membership is determined by the finitely many existing classes represented among the parameters. A required unused class exists exactly when fewer than two classes have already been used. Once its class is possible, infinitude supplies a point avoiding the finite exclusions. These tests are quantifier-free logical equality and equivalence conditions on the parameters. Disjunctive normal form and induction eliminate all quantifiers and also show completeness.
Thus a finite tuple's complete type is isolated by its finite equality-and-equivalence pattern. Every realized finite-tuple partial type is principal, so is atomic. In particular all individual elements have the same complete one-type, isolated by .
Choose in the countable class and in the uncountable class. Any automorphism taking to would give a bijection from their whole equivalence classes, impossible because their cardinalities differ. Therefore
Its uncountability is precisely what avoids the conclusion of (iii).
Here means a substructure, so the smaller carrier contains all named constants, is closed under every function symbol, and has each relation restricted from the larger first-order structure. First-order term evaluation on tuples from agrees in the two first-order structures. Consequently atomic formulas agree, and induction on Boolean connectives makes every quantifier-free formula agree as well.
Write an arbitrary universal sentence of as with quantifier-free matrix. Every tuple from is also a tuple from , so holds at that tuple in . Quantifier-free agreement transfers it to . Since the tuple was arbitrary, satisfies the universal sentence. Thus
An arbitrary subset without the substructure operations and relation restrictions would not be the hypothesis used by this formal proof.
The set of closed-term values is nonempty because the first-order language has a constant. It contains the value of every constant. If is an -ary function symbol and are closed terms, then
which is another closed-term value. Hence the set is closed under every operation. Restrict the operations and relations of to it; this defines a substructure whose carrier is exactly the specified set.
Part (i) now applies to the universal first-order theory, giving
It is the substructure generated by the first-order language's constants, often called the ground-term substructure. The source's constant-symbol assumption ensures its nonemptiness, even when no other elements can be generated.
Adjoin to the negations of all closed-term instances of . If the resulting set had a first-order model , its ground-term substructure from (ii) would still first-order model . The assumed existential consequence therefore supplies a tuple in satisfying . Each is the value of a closed term .
Quantifier-free agreement between a substructure and its ambient first-order structure gives
contradicting the adjoined negation of this very ground instance. Thus
is unsatisfiable. Compactness theorem gives a finite unsatisfiable subset. Its finitely many ground negations imply that, for some finite list of first-order term tuples,
If the finite subset already shows itself inconsistent and supplies no ground negations, choose any one closed-term tuple using the available constant; then any first-order sentence is a consequence of , so suffices. Otherwise the selected list is nonempty. This also explains why the conclusion contains a finite disjunction rather than necessarily one universal choice of a witness first-order term.

Articles by others on the same topic (0)

There are currently no matching articles.