WorksMathematics
Omitting Types for Infinitary Real-Valued Logic: A Topological Perspective
Abstract
For countable vocabularies, we extend the omitting types theorem for countable fragments of infinitary logic to Keisler's general real-valued structures by proving that the space of Henkin types of each such fragment is Čech-complete. The structures interpret function symbols arbitrarily and predicate symbols by bounded real-valued functions, while each formula carries a bound of its own. This extends the setting of Eagle's theorem from metric structures with a prescribed master metric to general structures whose vocabulary prescribes the sorts and bounds of the symbols. Following Keisler and Miller's treatment of logic without equality, we build models from closed terms. Morley's Baire category method then gives every satisfiable theory on a countable fragment a model with countable sorts omitting any countable family of types whose closed-term instances have empty interior in the space of Henkin types satisfying the theory.
Introduction
We extend the omitting types theorem to the infinitary logic of Keisler’s general real-valued structures by applying Morley’s Baire category method in a Čech-complete space of Henkin types. In this setting the function symbols are interpreted arbitrarily and the predicate symbols by bounded real-valued functions; each formula has a bound of its own. Eagle’s theorem [4] concerns metric structures whose signature prescribes a master metric and moduli of uniform continuity. Our theorem applies to Keisler’s general structures [14], whose vocabulary prescribes the sorts and bounds of the symbols, and its hypothesis is expressed by the interiors of closed sets of Henkin types.
The infinitary language extends Keisler’s first-order language by countable joins and infima, with only finitely many free variables in each formula. Each sentence takes its values in a bounded interval of its own. Hence the formal types, families of such values, are the points of a product of compact intervals that vary from sentence to sentence.
2020 Mathematics Subject Classification. Primary 03C75; Secondary 03C66, 03C25, 03B50, 54E52.
Key words and phrases. infinitary logic, real-valued logic, continuous model theory, omitting types theorem, Henkin types, Čech-complete spaces, Baire category theorem, logic without equality.
This version: November 4, 2026. The most recent version of this paper is available at https://utsa-quantum-math.github.io/resources/omitting-types-real-valued-logic/; it may supersede the version deposited on arXiv.
We expand the vocabulary by countably many new constants of each sort. Since the vocabulary has no equality symbol, the closed terms of the expanded vocabulary serve themselves as the elements of a structure, with no quotient to be taken. The Henkin conditions are the real-valued form of Henkin’s requirement of witnesses. The Henkin types, defined on the expanded language by these conditions, are exactly the types of such term structures. The Henkin types of a fragment are defined likewise on the fragment that it generates in the expanded language. For a countable vocabulary and a countable fragment, we show that the space of these Henkin types, with the product topology, is Čech-complete. Morley’s method therefore operates in this space, each point of which is the type of a term structure.
A type of the fragment in a finite tuple of variables is a set of expressions , with rational and with a formula of the fragment whose free variables are among . The type is omitted by a Henkin type of the fragment that satisfies none of the instances obtained by substituting closed terms of the expanded vocabulary for these variables.
Theorem A. Let a countable vocabulary be given, together with a formal type for a set of sentences of for this vocabulary. The formal type is realized by a structure whose sorts are countable if and only if it extends to a Henkin type. If the given sentences belong to a countable fragment, then the formal type is realized by some structure if and only if it extends to a Henkin type of the fragment.
Theorem B. Let a countable fragment of for a countable vocabulary be given, together with a theory on sentences of the fragment that has a model and a sequence of types of the fragment. Suppose that, for every instance of every type of the sequence, the Henkin types of the fragment that satisfy the theory and the instance form a set with empty interior in the space of Henkin types of the fragment that satisfy the theory. Then some Henkin type of the fragment that satisfies the theory omits every type of the sequence, and the theory has a model whose sorts are countable and in which no tuple of elements satisfies any type of the sequence.
The proof brings together four works of Keisler, which link the omitting types theorem to the treatment of structures without equality. His book on contains the theorem for countable fragments of classical , the statement that is extended here [12 Chapter 11]. His article on forcing contains a general omitting types theorem, whose hypothesis reappears in topological form in Theorem B [13]. With Miller he determined the form that the theorem takes in first-order logic without equality, in which the model is built from closed terms and the types to be omitted are tested through tuple of terms [15 Section 4]. His general structures, finally, interpret the function and predicate symbols by arbitrary mappings, the predicates being bounded, and they are the structures of our logic [14 Section 2.1].
These works belong to two lines of development, the one leading through the omitting types theorem and the other through equality. The first begins in 1969, when Makkai extended Smullyan’s method of consistency properties to the infinitary logics on admissible sets [16]. Two years later, Keisler made the model existence theorem for consistency properties the central method of his book on [12 Chapter 3], and in 1973 he built countable models by forcing with finite sets of sentences satisfiable in a given class of models [13 p. 100, Example 1.2]. In the same work he replaced principal types by formulas over a set of formulas of a countable fragment [Kei73, p. 107, Definition], and his general omitting types theorem gives conditions under which a $\forall\exists$ class contains a countable model in which countably many given $\forall\exists$ sentences hold [13 p. 108, General Omitting Types Theorem]. A year later, Morley derived the omitting types theorem for countable fragments from the Baire category theorem, applied to a space of countable structures that he showed to be a Baire space [Mor74]. In 2001, Keisler and Miller carried the theorem into first-order logic without equality, where principal types give way to locally realized types [15 Section 4]. In 2014, drawing in part on work of Caicedo and Iovino, Eagle applied Čech’s form of the Baire category theorem to a space of countable metric structures [4, 2]. The predicates of his structures take values in and are uniformly continuous, with moduli prescribed by the signature, with respect to a master metric [4 Definitions 1.4 and 1.5]. This master metric is the real-valued counterpart of equality in two precise senses: two elements are equal exactly when their distance is zero, and the uniform continuity of every predicate and function symbol with respect to the metric is the counterpart of the substitutivity of equals in atomic formulas.
The second line begins with the axioms of equality in first-order logic, which assert its reflexivity and the interchangeability of equal elements in every atomic formula, and which thereby make equality a congruence for the function and predicate symbols. In real-valued logic, their counterparts are axioms of continuity.1 A general form of these axioms, uniform continuity with moduli prescribed by the signature, was the setting of Iovino’s thesis of 1994 on stable Banach space structures, in which the role of equality passes to a uniform structure [9]. For a countable signature, the uniform structure has a countable base, and it is therefore induced by a single pseudometric (see [5 Section 8.1]). Iovino’s papers of 1999 on stable Banach spaces rest on the same framework [10, 11], and in 2002 Henson and Iovino presented the model theory of normed space structures in it [8 Sections 2 and 3]. In 2010, Ben Yaacov and Usvyatsov built moduli of uniform continuity into the signatures of continuous logic [1 Section 2]. In 2023, at last, Keisler obtained the pseudometric from the formulas themselves, for vocabularies with countably many function and predicate symbols [14 Section 3.3]. Every general structure for such a vocabulary expands to one with a distance predicate that is a uniform limit of formulas [14 Theorem 3.3.4]; this predicate is unique up to uniform equivalence, and every first-order formula is uniformly continuous with respect to it [14 Section 3.2 and Proposition 3.3.7].
The two lines meet in Keisler’s comparison of structures: general structures correspond to first-order structures without equality, as metric structures with a distance predicate correspond to first-order structures with equality [14 Section 1]. The passage from Eagle’s structures to Keisler’s is therefore the real-valued counterpart of the passage from logic with equality to logic without it, and for this passage the analysis of Keisler and Miller is the precedent that we follow in building our models from closed terms.
Keisler and Miller call a type locally realized when it is implied, through some tuple of terms, by a formula consistent with the theory [15 Definition 4.1], and they show that every type realized in every model of a consistent theory is locally realized [15 Theorem 4.2]. Caicedo and Iovino use tuples of terms in the same way in their -principal types [2 Definition 3.5], and Eagle does so in his principal types, crediting this use of terms to Keisler and Miller and to Caicedo and Iovino [4 Definition 4.10]. Keisler and Miller also state local realization topologically, as the existence of a term mapping between spaces of types under which the preimage of the type has nonempty interior [15 Section 4]. The hypothesis of Theorem B is a condition of the opposite kind, stated in the space of Henkin types that satisfy the theory: for every tuple of closed terms, the members of this space that satisfy the instance of the type at those terms must form a set with empty interior.
The hypothesis of Keisler’s general omitting types theorem can be read in the same way [13 p. 108, General Omitting Types Theorem]. For the comparison we work in classical two-valued logic and take Keisler’s formulas over the set of all formulas of the fragment. A model omits a type of the fragment exactly when it satisfies the sentence , which has the form, and for this sentence Keisler asks that every finite set of sentences satisfiable in the class remain satisfiable after the addition of , for every tuple of new constants. Equivalently, no finite set of sentences satisfiable in the class defines a subclass that consists of models of the instance ; in topological terms, every instance has empty interior with respect to the basic sets given by finite sets of sentences. Since, moreover, every sentence over the fragment holds in exactly the models that omit the type , this reading covers every sentence to which the theorem applies.
Theorem B differs from Keisler’s theorem in three respects: its space is the space of Henkin types that satisfy the theory, with basic open sets given by finite theories; its instances are taken at tuples of closed terms, as in the work of Keisler and Miller, rather than at tuples of constants; and its types consist of closed conditions in place of formulas. With these differences, Theorem B extends this case of the general omitting types theorem to Keisler’s general structures, and it explicates the hypothesis of that theorem as a statement about interiors in a Čech-complete space.
Organization of the paper {#sec:Organization of the paper}
Organization of the paper. In Section 2 we recall Čech’s form of the Baire category theorem, and in Sections 3–8 we set up the structures, languages, fragments, theories and formal types. In Section 9 we define Henkin types and prove Theorem A. In Section 10 we show that, in the countable case, the space of Henkin types of a fragment is a subset of the product of intervals in which it lies, and Theorem B, proved in § 11, then follows from Čech’s form of the Baire category theorem.
Topological Preliminaries
The topological fact on which the paper rests is Čech’s form of the Baire category theorem, which applies, in particular, to every countable intersection of open subsets of a compact Hausdorff space. We recall the definitions that the theorem involves, with Engelking’s General Topology [5] as our reference for topology.
A topological space is a Baire space if the intersection of every sequence of dense open subsets of the space is dense; Baire spaces were introduced by Bourbaki in 1948 (see [5 notes to Section 3.9]). The spaces to which this property will be applied are Tychonov spaces, that is, completely regular -spaces; every subspace of a compact Hausdorff space is one (see [5 Theorem 3.2.6]). Let be a Tychonov space. A sequence of open covers of is complete if every family of closed subsets of that has the finite intersection property, and that contains, for every , a member included in some element of , has nonempty intersection. The space is Čech-complete if it has a complete sequence of open covers. Čech [3] introduced these spaces in 1937, under the name of topologically complete spaces, as the Tychonov spaces that are subsets of their Stone–Čech compactifications. The characterization of Čech-complete spaces by sequences of open covers, adopted here as the definition, was established independently by Frolík in 1960 and by Arhangel’skiĭ in 1961 (see [5 Theorem 3.9.2 and the notes to Section 3.9]). By Theorems 3.9.1 and 3.9.2 of Engelking [Eng89], a Tychonov space is Čech-complete if and only if it is a subset of some, or equivalently of every, compactification of it. Consequently, every subset of a compact Hausdorff space is Čech-complete. The ambient compact spaces used below are products of real intervals with , endowed with the product topology; they are compact Hausdorff by Tychonov’s theorem (see [5 Theorem 3.2.4]). Čech also proved the following form of the Baire category theorem (see [5 Corollary 3.9.4 and the notes to Section 3.9]).
Theorem 1 (Baire category theorem; Čech [3]). Every Čech-complete space is a Baire space.
Vocabularies and Structures
The models whose existence the omitting types theorem asserts are real-valued structures. Such a structure consists of one or more nonempty sets, called its sorts, of functions from finite products of sorts to sorts, and of its predicates. The predicates of the structure are bounded real-valued functions on finite products of sorts. Classical first-order structures for vocabularies without equality correspond to the case in which every predicate takes only the values and , read as true and false, respectively. Formulas speak about structures through a vocabulary, which is a set of symbols for sorts, functions and predicates. A structure for the vocabulary interprets each symbol as an actual sort, function or predicate. Since symbols must be kept apart from their interpretations, the symbols of a vocabulary are printed in this color, and mathematical objects in black. For the same reason, the variables, the connectives and the formal expressions built from them are printed in this color.
A sort descriptor is a purely syntactic symbol . Let be a nonempty set of sort descriptors. A function symbol for is a purely syntactic symbol given together with
(i) a natural number , called the arity of , and
(ii) an -tuple of sort descriptors in , called the extended arity of .
We indicate the arity and the extended arity of by writing
A function symbol of arity 0 is called a constant symbol of sort . A predicate symbol for is a purely syntactic symbol given together with
(i) a natural number , called the arity of ,
(ii) an -tuple of sort descriptors in , called the extended arity of , and
(iii) a real number , called the a priori bound of .
We indicate the arity, the extended arity and the a priori bound of by writing
A vocabulary is a triple consisting of a nonempty set of sort descriptors, a set of function symbols for , and a set of predicate symbols for . The set is required to contain a nullary predicate symbol , called the logical unity constant, with a priori bound . The vocabulary is countable if the sets , and are countable. The a priori bounds provide the compactness on which the topology of the paper rests. Indeed, as we show in § 4, the value of a formula in a structure lies in an interval determined by the formula alone. Consequently, the types of all structures lie in a product of compact intervals, the compact Hausdorff space of formal types of § 8.
Given a vocabulary , a -structure, or real-valued structure with vocabulary , is a triple
in which
♠ the interpretation of each sort descriptor is a nonempty set,
♠ the interpretation of each function symbol in is a function
the interpretation of each predicate symbol in is a function
and
the interpretation of the logical unity constant is .
Here a nullary symbol is interpreted on the one-point set , and its interpretation is identified with its value.
First-Order and Infinitary Languages
Types, and later Henkin types, are formed from the values that structures assign to formulas. We therefore build, from the symbols of a vocabulary, the terms and the formulas of a first-order language and of its infinitary extension, and interpret them in structures.
For the rest of the paper, we fix a vocabulary .
For each sort descriptor , we fix a sequence of distinct symbols, not in , chosen so that the sequences for distinct sort descriptors have no symbol in common. Each symbol is called a variable of sort .
Terms of sort are defined recursively as follows:
every variable of sort is a term of sort ;
for every function symbol in and every tuple of terms such that is of sort for each , the expression is a term of sort .
In particular, every constant symbol of sort is a term of sort . For a natural number and a tuple of sort descriptors in , a tuple of terms such that is of sort for each is called a term of sort ; for , the only such term is the empty tuple. A term is closed if no variable occurs in it.
For a predicate symbol in and a term of sort , the expression is called an atomic -formula with a priori bound . The other -formulas are formed from the atomic ones by applying symbols called logical connectives:
for each rational number , the symbol is a logical connective;
the symbols and are logical connectives;
for each variable , the symbol is a logical connective.
The -formulas and their a priori bounds are defined recursively, starting from the clause that every atomic -formula is a -formula. If and are -formulas with a priori bounds and , respectively, then the expressions , , and are -formulas for every rational number and every variable . The a priori bounds of these four formulas are defined by
respectively. Since the connectives and are written before the formula to which they apply, the parentheses in and ensure that every -formula is formed in only one way. Hence the a priori bound of a -formula, like the other notions defined below by recursion on formulas, is well defined; we omit the parentheses when no ambiguity arises. The set of all -formulas is called the first-order language for and is denoted by .
The set of variables free in a -formula is defined recursively as follows:
if is atomic, of the form , then is the set of variables that occur in the terms of the tuple ;
if is of the form , then ;
if is of the form or , then ;
if is of the form , then .
A -sentence is a -formula with no free variables, that is, a -formula such that .
For a term and a tuple of distinct variables, we write to indicate that every variable occurring in is among . Similarly, for a formula , we write to indicate that every variable free in is among . If , where is a variable of sort for each , we write
and say that is a variable of sort . For a -structure , we write
The infinitary language is obtained by adding to the formation rules of a new logical connective , called the infinitary connective of countable join. More precisely, the language , together with the a priori bounds and the free variables of its members, is defined by recursion on the countable ordinals. Let be the set of atomic -formulas, and let for every countable limit ordinal . For , the set is obtained by adding to two kinds of expressions formed from its members. The first are the expressions , , and with , for all rational numbers and all variables ; their a priori bounds and free variables are given by the clauses stated for . The second concern the sequences of members of for which is finite and, for some finite tuple of variables, every is of the form . For every such sequence, the expression is added, with a priori bound
The free variables of are those of the formulas , that is,
a subset of the finite set of variables of . Finally, we set . Since is regular, every sequence of members of consists of members of some , and the set is therefore closed under all these formation rules.
We also write for , and we denote the set of sentences of by . A formula of may have infinite length, but only finitely many free variables. The two languages differ in size: if is countable, the first-order language is countable, whereas the infinitary language has the cardinality of the continuum. For this reason, the Baire category argument of this paper takes place in countable fragments (see § 6).
Let be a -structure, and let be a term of sort , where . The interpretation of in is the function defined recursively, for in , as follows:
the interpretation of the variable is the projection ;
if is a function symbol and is a term of sort , then the interpretation of the term is given by
The interpretation of a closed term is a function on the one-point set with empty, and is identified with its value, an element of . The interpretation of a formula of in is the function on defined recursively, for in , as follows:
if is atomic, of the form with , then
if is of the form , where is a rational number and , then
if is of the form , where , then
if is of the form , where , then
if is of the form , where , then
where, if is not among , the formula is regarded as a formula , and is the tuple ; if is the variable of , the formula is regarded as a formula , and is the tuple obtained from by replacing its entry by ;
if is of the form , where is a sequence of formulas of , then
An induction on formulas shows that the suprema in this definition are finite and that takes its values in . When is a sentence, the tuple may be taken empty, and is identified with its value, a real number in .
Several proofs below proceed by induction on formulas of infinite length, and for these we use the rank of a formula, defined recursively as follows. Atomic formulas have rank 0; the rank of and of is the rank of plus one; the rank of and of is the larger of the ranks of and plus one; and the rank of is the supremum of the ranks of the members of plus one. Every rank is a countable ordinal, and the rank of a proper subformula of a formula is smaller than the rank of the formula. Since substituting terms for variables changes only the atomic subformulas, it preserves the rank. These definitions apply to every vocabulary, and in particular to the expanded vocabulary of Section 5.
Expansion by Constants
In the method introduced by Henkin in 1949, the elements of a structure are named by new constant symbols; the first step is to add these symbols to the fixed vocabulary. Let be a set of distinct constant symbols, not in , such that is of sort for every and every . The expansion of by is the vocabulary , which is countable if is; the infinitary language is denoted by , and its set of sentences by .
Given a -structure , an expansion of to is a -structure
that agrees with on the symbols of , in the sense that for every , that for every , and that for every . Each expansion of to is determined by the elements of that interpret the new constant symbols. Conversely, every -structure is an expansion of exactly one -structure, its -reduct, obtained by forgetting the interpretations of the symbols in .
In the structures built by the Henkin construction, every element has a name. A -structure is canonical if, for every sort descriptor , every element of is the interpretation in of a closed -term of sort .
In a canonical structure, a supremum over a sort is a supremum over the values of closed terms, and it can be computed from sentences by substituting these terms for the variable. The following lemma, which justifies this computation, holds in every -structure. For a formula and a tuple of closed terms, we write for the formula obtained by substituting the terms of for the free occurrences of the corresponding variables of ; a closed term is free for every variable.
Lemma 2 (Substitution). Let be a -structure, let be a formula of , where is a tuple of distinct variables not among , and let be a tuple of closed -terms of sort . Then for every tuple .
Proof. The corresponding identity for terms is proved by induction on terms, and the lemma follows by induction on the rank of . The parameters are needed in the step for suprema, in which the variable of the supremum joins them.
Fragments
Countability is indispensable to the Baire category argument, which writes the Henkin types of § 9 as a countable intersection of open sets attached to sentences (see § 10). The infinitary language, however, has the cardinality of the continuum even when the vocabulary is countable (see § 4). The argument is therefore carried out in fragments: sets of formulas that contain the first-order language and are closed under the first-order connectives, under subformulas and under substitution of terms, and that are countable when they are generated by countably many formulas over a countable vocabulary.
Let be a formula of . The set of subformulas of is defined recursively as follows:
if is atomic, we set ;
if is of the form , we set ;
if is of the form or , we set ;
if is of the form , we set ;
if is of the form , we set .
A fragment of is a set with the following properties:
(F1) it contains ;
(F2) it is closed under subformulas, that is, for every ;
(F3) it is closed under the first-order connectives, that is, if , then for every rational number , , , and for every variable ;
(F4) it is closed under substitution of terms, that is, if and is a term of sort that is free for in (no free occurrence of in lies within a subformula of such that occurs in ), then the formula , obtained from by substituting for the free occurrences of , belongs to .
The intersection of a nonempty family of fragments of is a fragment, and the language is itself a fragment. Hence, for every set , the intersection of all fragments containing is the smallest fragment containing , which is called the **fragment generated by \mathcal{V}$ and are countable, then the fragment generated by is countable. Indeed, let ; for each , let be obtained by adding to the formulas that (F2)–(F4) require for members of . Since every formula has countably many subformulas, and since there are countably many rational numbers, variables and terms, an induction on shows that every set is countable. The union of the increasing sequence is a fragment that contains and is contained in every fragment containing . Consequently, the fragment generated by is this union, which is countable.
Let be a fragment of . Since is contained in the infinitary language of the expanded vocabulary of Section 5, we may consider the fragment of generated by , which we denote by . If and are countable, then so is , by the preceding paragraph applied to the countable vocabulary . We denote the set of sentences of by and the set of sentences of by .
Conditions and Theories
In real-valued logic, the role of the statements of classical logic is played by conditions, formal strict inequalities between a sentence and a rational number. Sets of conditions, called theories, specify the models to be constructed, whereas the types to be omitted are expressed by closed conditions. Strict conditions are taken as the basic ones because each of them defines an open set in the topology of Section 10, as the Baire category argument requires.
A lower-bound condition is a formal expression , and an upper-bound condition is a formal expression . Each of these expressions is formed from a sentence of the infinitary language of the expanded vocabulary (see Section 5) and a rational number . A condition is a lower-bound condition or an upper-bound condition, and a theory is a set of conditions. For a set of sentences, a -theory is a theory whose conditions are on sentences in .
For a rational number , we write
for the countable theory , and
for the countable theory .
The expressions and are called closed conditions.
Let be a -structure. We say that satisfies the condition , and write , if ; it satisfies the condition if . A -structure that satisfies every condition of a theory is called a model of the theory; the same term is used for -structures and theories whose conditions are on -sentences. Thus a structure satisfies the closed condition exactly when the value of in it is at least .
Under the reading of as true and as false, the connectives generalize those of classical first-order logic, as the following equivalences show. Each of these equivalences holds for every -structure and every rational number . Multiplication by plays the role of negation: for a sentence , if denotes the sentence obtained by applying the connective with , then
In particular, for , a -structure satisfies exactly when it satisfies . The binary connective is the counterpart of disjunction: for sentences $\varphi and , we have
The supremum takes the place of the existential quantifier: for a formula of , the condition is characterized as follows:
Finally, the join generalizes countable disjunction: for a sequence of sentences of whose join is a sentence of , the condition is characterized in the same way:
Types of Structures and Formal Types
The type of a structure records the values that the structure assigns to a set of sentences; formal types are families of such values that need not come from any structure. Among the latter are the Henkin types, which, as we show in Section 9, do come from structures, and which form a subspace of the compact space of formal types.
Let be a set of sentences of the infinitary language of the expanded vocabulary . We write for the product endowed with the product topology, where is the a priori bound of . In this topology, the product is a compact Hausdorff space (see Section 2); its elements are called formal -types. For a formal -type and a sentence , we write for the -coordinate of and say that satisfies a condition or if or , respectively. If is a -structure, the -type of is the formal -type
When is contained in the set of sentences of , the same definition applies to a -structure . The -type is called the full type of ; similarly, the full type of a -structure is its type for the set of sentences of .
Henkin Types
In his proof of the completeness theorem, Henkin [7] built a model of a consistent theory out of new individual constants, chosen to provide every existential sentence of the theory with a witness among them. The Henkin conditions below are the real-valued form of this requirement. They demand of a formal type that the value of a sentence formed with a connective from other sentences be computed from their values. The value of a supremum over a variable must likewise be the supremum of the values obtained by substituting closed terms for that variable. In this section we show that the formal types satisfying the Henkin conditions are exactly the types of canonical structures, structures in which every element is the value of a closed term. We also deduce, with the help of a downward Löwenheim–Skolem theorem for countable fragments, which formal types are realized by structures.
Let be a fragment of the infinitary language of the expanded vocabulary , and let be the set of its sentences. Let be a variable, let be a formula whose free variables are among , and let be a closed -term of sort . We write for the sentence obtained by substituting for the free occurrences of in , as in condition (F4) of the definition of a fragment (see § 6). A formal type is an -Henkin type if it satisfies the following Henkin conditions:
Every sentence that occurs in these conditions belongs to : the logical unity constant by (F1), and the sentences , , and by (F3). The members of belong to by (F2), since the free variables of are those of its members; the sentences belong to by (F4). The language is a fragment of itself, whose set of sentences is ; its -Henkin types lie in and are simply called Henkin types.
To pass from formal types back to structures, we follow Henkin and take as elements the closed terms themselves; the structure so obtained depends only on the values of the atomic sentences. Let be the set of atomic -sentences; by (F1), it is contained in for every fragment of . An atomic type is a formal type such that $1^{\mathfrak{a}}=1$. Every atomic type determines a -structure , the **term structure of M\in\mathcal{M}$, the set consists of the closed -terms of sort ; it is nonempty, since it contains the constants . Each function symbol of is interpreted syntactically, by , and each predicate symbol by . The interpretation is a function into , because the a priori bound of the atomic sentence is . Since, moreover, the logical unity constant satisfies , the term structure is a -structure. No quotient of the set of terms is needed, since the vocabulary has no equality symbol. An induction on terms shows that for every closed -term ; hence the term structure is canonical and satisfies -tp.
Lemma 3. Let be a fragment of .
(a) If is a canonical -structure, then its -tp is an -Henkin type.
(b) Two -Henkin types that agree on are equal.
(c) A formal type is the -type of a canonical -structure if and only if it is an -Henkin type; in that case, it is the -type of the term structure of its restriction to .
Proof. The idea is that the Henkin conditions repeat the recursive definition of the values of sentences, except that a supremum over a sort becomes a supremum over closed terms. The Henkin conditions therefore determine the value of every sentence from the values of the atomic ones, which is part (b). Part (a) asserts that the same conditions hold in a canonical structure, in which every element is the value of a closed term and the two suprema coincide. Part (b) is proved by induction on the rank of formulas (see § 4).
(a) Conditions (H1), (H2), (H3), (H4) and (H6) hold for the values of the sentences , by the definition of a -structure and the recursive definition of the interpretation of formulas. For (H5), let be a formula whose free variables are among . By the substitution lemma (Lemma 2), applied with empty, we have for every closed -term of sort . Since is canonical, every element of is of the form for a closed -term of sort ; this gives
(b) Let and be -Henkin types that agree on . We show by induction on the rank of that for every , the atomic case being the hypothesis. Suppose that is of the form , , or . In that case, the formulas , and the members of are sentences in of smaller rank, on which the types and agree by the induction hypothesis. Conditions (H2), (H3), (H4) and (H6), respectively, compute and alike from the values of these sentences. Suppose, finally, that is of the form . For every closed -term of sort , the sentence then belongs to and has smaller rank. The types and agree on each of these sentences for the same reason, and condition (H5) therefore gives .
(c) By (a), the -type of a canonical -structure is an -Henkin type. Conversely, let be an -Henkin type, and let be its restriction to , an atomic type by (H1). The term structure is canonical, with -tp. By (a), the -type of is an -Henkin type that agrees with on ; by (b), the two types are equal. ∎
Let be an atomic type. By Lemma 3(a), applied to , the full type -tp is a Henkin type that extends . Part (b) of that lemma shows that no other Henkin type extends . We call this full type the Henkin type of and denote it by . For every fragment of , the same lemma shows that the restriction of to is the only -Henkin type that extends .
Let be a -structure, and let -tp. If is canonical, then Lemma 3(a) shows that the full type -tp is a Henkin type that extends , and therefore equals . In other words, we have for every .
If is not canonical, the two values may differ, and in either direction. For example, suppose that has a single sort descriptor and no function symbols, and that the only predicate symbol of besides is . Let be the -structure with , and , in which every constant of is interpreted as . For a variable of sort , the sentence takes the value in , whereas , the constants being the only closed -terms. Applying the connective with to this sentence reverses the inequality.
Let be a subset of the set of sentences of , and let be given. We say that the formal type is realized if there is a -structure such that -tp; in that case, we say that realizes . When is countable, there are countably many closed -terms. In that case, a -structure can therefore have a canonical expansion to , to which Lemma 3 applies, only if its sorts are countable. The following form of the downward Löwenheim–Skolem theorem replaces every -structure by one whose sorts are countable and which assigns the same values to the sentences of a given countable fragment.
Lemma 4. Assume that the vocabulary is countable, and let be a countable fragment of . For every -structure there is a -structure whose sorts are countable such that for every in the set of sentences of .
Proof. The structure is obtained by closing countably many elements of under the functions of and under the choice of approximate witnesses for the suprema of formulas of . Let , let be a variable, and let be a finite tuple of distinct variables among which are the free variables of . For every tuple and every integer , choose an element such that , with the notation of the clause for suprema in Section 4. For each , let consist of one element of . For each and each , let consist of the elements of , the values in of the functions at tuples from , and the witnesses in with from . Here a tuple is from if each of its entries lies in the set of its sort . Since and are countable, and since there are countably many variables and finite tuples of variables, an induction on shows that every set is countable; hence so is . Moreover, the sets increase with , whence the family is closed under the functions . Let be the -structure whose sorts are the nonempty sets and whose functions and predicates are the restrictions of those of . By induction on the rank of (see Section 4), we show that for every tuple from of the appropriate sort. For atomic this holds because terms take the same values in and in . The steps for , , and follow from the definitions, the subformulas of members of being members of by (F2). Let be of the form , and let be a tuple from of sort , where is a finite tuple of distinct variables among which are the free variables of . The induction hypothesis gives , since the supremum defining ranges over a subset of . Conversely, the tuple is from for some . For every , the witness is therefore an element of , and the induction hypothesis applied to gives . The case of sentences is the lemma.
Recall from Section 6 that, for a fragment of , we write for the fragment of generated by , and for its set of sentences.
Proposition 5 (Henkin Realizability). Assume that the vocabulary is countable, and let and be given.
(a) The formal type is realized by a -structure whose sorts are countable if and only if it extends to a Henkin type in .
(b) If for a countable fragment of , then is realized if and only if it extends to an -Henkin type.
Proof. The idea is that, since is countable, a -structure has countable sorts exactly when it has a canonical expansion to . By Lemma 3, moreover, the types of canonical -structures are exactly the Henkin types. In part (b), Lemma 4 first replaces the realizing structure by one whose sorts are countable. (a) Suppose first that a -structure whose sorts are countable realizes . Since every sort of is countable and nonempty, there is an expansion of to in which, for each , the map carries onto , and every such expansion is canonical. By Lemma 3(a), applied to , the full type is a Henkin type. This Henkin type extends , because the value of a -sentence in is its value in . Conversely, let be a Henkin type that extends . By Lemma 3(c), applied to , the type is the full type of a canonical -structure , whose -reduct therefore realizes . Since is countable together with , there are only countably many closed -terms. The sorts of the -reduct of are therefore countable, every element of being the value of such a term.
(b) If a -structure realizes , then so does a -structure whose sorts are countable, by Lemma 4 and the inclusion . By Lemma 3(a), applied to , the -type of the canonical expansion constructed in (a) is an -Henkin type, and it extends . Conversely, let be an -Henkin type that extends . By Lemma 3(c), applied to , the type is the -type of a canonical -structure, whose -reduct realizes .
Topology on the Space of Henkin Types
Čech’s form of the Baire category theorem needs a Čech-complete space, and the Henkin types supply one. When the vocabulary and the fragment are countable, the Henkin types for the sentences of the expanded fragment form a subset of the compact Hausdorff space of all formal types for these sentences, and therefore a Čech-complete space and a Baire space.
Let be a fragment of , and recall from § 6 that is the set of sentences of the fragment of generated by . We denote the set of -Henkin types by . As recalled in § 2, the product of § 8, where is the a priori bound of , is a compact Hausdorff space when endowed with the product topology. The product topology is generated by the projections (see [5 Section 2.3 and Proposition 1.4.8]), and the open rays with rational endpoints form a subbasis of the topology of each interval . Together, these two facts show that the sets
where and , form a subbasis of the product topology. For an -theory , we write for the set of formal types that satisfy every condition of , in the sense of § 8. We say that satisfies if ; thus each is the intersection of the subbasic sets given by the conditions of , and the set is all of . For each , the projection is continuous on (see [5 Proposition 1.4.8]). Hence, for a closed condition with , the set is closed, being the preimage of the closed ray under the projection .
The sets in the proof of Proposition 6 below are likewise built from sets defined by equations and inequalities between finitely many coordinates: if and is continuous, then the set is open. Under the same hypotheses, the set , being the intersection of the open sets with , is a set.
Proposition 6. If the vocabulary and the fragment are countable, then the set of of -Henkin types is a subset of .
Proof. The idea is that the Henkin conditions consist of countably many equations, each either between finitely many coordinates or between one coordinate and the supremum of countably many others. Each such equation is, moreover, equivalent to countably many requirements defining sets. All the index sets below are countable: since is countable, so are , the set of variables and the set of closed -terms. The fragment is countable as well, by § 6.
By the continuity of the projections, every set in the following list is a subset of . In addition, for each , a formal type belongs to all the sets listed under if and only if it satisfies the Henkin condition :
(H1) the set ;
(H2) for and , the set ;
(H3) for , the set ;
(H4) for , the set ;
(H5) for each variable and each formula whose free variables are among , the closed sets with a closed -term of sort , and the set
which is a set because each union is open;
(H6) for each sentence , the closed sets with , and the set
Each set listed under (H1), (H2), (H3) and (H4), and each closed set listed under (H5) and (H6), is the zero set of a continuous function of finitely many coordinates (such as ). Each union listed is a union of sets of the form ; in both cases, the remark preceding the proposition therefore applies. Being indexed by countable sets, the family of all these sets is countable, and its intersection is . Since a countable intersection of sets is a set, the proposition follows. □
Corollary 7. If the vocabulary and the fragment are countable, then is Čech-complete and a Baire space.
Proof. By Proposition 6, the space is a subset of the compact Hausdorff space . As recalled in Section 2, every such subset is Čech-complete, and the Baire category theorem for Čech-complete spaces (see Theorem 1) shows that it is a Baire space. □
In Section 11 we express in terms of conditions that a set of Henkin types has empty interior. For this purpose we use a basis of the topology of described by finite theories. Since is a finite intersection of subbasic open sets whenever is a finite -theory, the sets with finite form a basis of the topology of (see [5 Sections 1.1 and 2.1]).
Omitting Types Theorem
The Henkin types satisfying a theory are the types of the canonical structures (those in which every element is the value of a closed term) whose reducts are models of the theory. To omit countably many types in a model of the theory, it therefore suffices to find such a Henkin type that realizes none of them. In this section we show that, when the vocabulary and the fragment are countable and the theory has a model, the Henkin types satisfying the theory form a nonempty Baire space. We also show that the required Henkin type exists if, for each instance of each of the given types, the members of this space satisfying the instance form a nowhere dense set. The members of this space that realize one of the given types then form a meager subset, and the Baire category theorem provides a Henkin type outside it.
Henceforth, assume that the vocabulary and the fragment of Section 10 are countable. We also fix an -theory (a theory whose conditions are on sentences of ) that has a model. Recall from Section 10 that is the set of -Henkin types, where is the set of sentences of the fragment of generated by . The set of -Henkin types that satisfy (see Section 10) is nonempty. Indeed, by Lemma 4, the theory has a model whose sorts are countable. The canonical expansion of constructed in the proof of Proposition 5(a) satisfies , since the values of -sentences in are their values in . By Lemma 3(a), the -type of belongs to . Conversely, by Lemma 3(c), every member of is the -type of a canonical -structure, whose -reduct is a model of . Thus the members of are exactly the -types of the canonical -structures whose -reducts are models of . Since is countable, so is the theory , whence the set is a countable intersection of open sets. By Proposition 6, the set is therefore a subset of the compact Hausdorff space . As recalled in Section 2, a subset of a compact Hausdorff space is Čech-complete; by Theorem 1, the space is a nonempty Baire space.
Let be a finite tuple of distinct variables. An -type in is a set of expressions , where and is a formula whose free variables are among . Substituting closed terms for turns each of these expressions into a closed condition in the sense of Section 7. For a tuple of closed -terms of sort , the instance of is the union of the closed conditions for the members of . Each of these conditions is a countable theory; the instance is an -theory because the fragment is closed under substitution of terms (see (F4) in Section 6). An -Henkin type realizes if it satisfies some instance , that is, if for some tuple ; otherwise it omits . Similarly, if is a -structure, a tuple satisfies in if for every member of . We say that has nonempty interior in if there exist a tuple of closed -terms of sort and a finite -theory such that
Otherwise, we say that has empty interior in . The sets , with a finite -theory, form a basis of the topology of (see Section 10). Consequently, the type has nonempty interior in this space exactly when, for some tuple , the closed subset of this space has nonempty interior. An -type is expressed by closed conditions so that this subset, being an intersection of the closed sets , is closed (see Section 10). When this subset has empty interior, its complement in is therefore a dense open set. The Baire category theorem applies to countable intersections of such dense open sets, as the proof of Theorem 8 shows.
Theorem 8 (Omitting Types Theorem). Assume that the vocabulary and the fragment are countable, and let be an -theory that has a model. Let be a sequence of -types each of which has empty interior in . Then there is an -Henkin type that omits every , and the theory has a model whose sorts are countable and in which, for every , no tuple of elements satisfies .
Proof. The idea is to write the set of Henkin types that satisfy and omit every as a countable intersection of open dense subsets of the nonempty Baire space . Fix , let and , and let be a tuple of closed -terms of sort . Since the set is closed for every member of (see Section 10), the set is closed in the space . By the definition of empty interior, this closed set has empty interior in , and the complement
is therefore an open dense subset of . Since is countable, there are only countably many tuples ; consequently, the set of members of that omit is a countable intersection of open dense subsets of . As was arbitrary, the same holds for each set , and hence for the set of members of that omit for every . Since is a nonempty Baire space, the set is dense in it, and in particular nonempty.
Let be a member of . By Lemma 3(c), the type is the -type of a canonical -structure , whose -reduct is a model of . The sorts of are countable, since every element of is the value of one of the countably many closed -terms. Now fix and a tuple . Since is canonical, we may write for a tuple of closed -terms. By the substitution lemma (Lemma 2), with empty, we have for every formula whose free variables are among . Since omits , it does not satisfy , and the tuple therefore does not satisfy in .
References
DEPARTMENT OF MATHEMATICS, THE UNIVERSITY OF TEXAS AT SAN ANTONIO, SAN ANTONIO, TX 78249, USA Email address: [email protected]
DEPARTMENT OF MATHEMATICS, THE UNIVERSITY OF TEXAS AT SAN ANTONIO, SAN ANTONIO, TX 78249, USA Email address: [email protected]
DEPARTMENT OF MATHEMATICS, THE UNIVERSITY OF TEXAS AT SAN ANTONIO, SAN ANTONIO, TX 78249, USA Email address: [email protected]
References
- [1][BU10] I. Ben Yaacov and A. Usvyatsov, Continuous first order logic and local stability, Trans. Amer. Math. Soc. 362 (2010), no. 10, 5213–5259; arXiv:0801.4303.DOI
- [2][CI14] X. Caicedo and J. Lovino, Omitting uncountable types, and the strength of [0, 1]-valued logics, Ann. Pure Appl. Logic 165 (2014), no. 6, 1169–1200; arXiv:1202.5981.arxiv.org/abs/1202.5981
- [3][Čec37] E. Čech, On bicompact spaces, Ann. of Math. (2) 38 (1937), no. 4, 823–844.
- [4]C. J. Eagle, Omitting types for infinitary [0, 1]-valued logic, Ann. Pure Appl. Logic 165 (2014), no. 3, 913–932; arXiv:1304.5208.DOI
- [5]R. Engelking, General topology, revised and completed ed., Sigma Series in Pure Mathematics, vol. 6, Heldermann Verlag, Berlin, 1989.
- [7]L. Henkin, The completeness of the first-order functional calculus, J. Symbolic Logic 14 (1949), no. 3, 159–166.DOI
- [8]C. W. Henson and J. Iovino, Ultraproducts in analysis, Analysis and logic (Mons, 1997), London Math. Soc. Lecture Note Ser., vol. 262, Cambridge Univ. Press, Cambridge, 2002, pp. 1–110.
- [9]J. Iovino, Stable theories in functional analysis, Ph.D. thesis, University of Illinois at Urbana-Champaign, 1994.
- [10]J. Iovino, Stable Banach spaces and Banach space structures. I. Fundamentals, Models, algebras, and proofs (Bogotá, 1995), Lecture Notes in Pure and Appl. Math., vol. 203, Dekker, New York, 1999, pp. 77–95.
- [11]J. Iovino, Stable Banach spaces and Banach space structures. II. Forking and compact topologies, Models, algebras, and proofs (Bogotá, 1995), Lecture Notes in Pure and Appl. Math., vol. 203, Dekker, New York, 1999, pp. 97–117.
- [12]H. J. Keisler, Model theory for infinitary logic: Logic with countable conjunctions and finite quantifiers, Studies in Logic and the Foundations of Mathematics, vol. 62, North-Holland, Amsterdam–London, 1971.
- [13]H. J. Keisler, Forcing and the omitting types theorem, Studies in model theory (M. D. Morley, ed.), MAA Stud. Math., vol. 8, Math. Assoc. America, Buffalo, NY, 1973, pp. 96–133.
- [14]H. J. Keisler, Model theory for real-valued structures, Beyond First Order Model Theory, Vol. II (J. Iovino, ed.), Chapman & Hall/CRC, Boca Raton, FL, 2023, Chapter 2; arXiv:2005.11851.arxiv.org/abs/2005.11851
- [15]H. J. Keisler and A. W. Miller, Categoricity without equality, Fund. Math. 170 (2001), no. 1, 87–106.DOI
- [16]M. Makkai, An application of a method of Smullyan to logics on admissible sets, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 17 (1969), 341–346.