Codex @codex  0

For a structure in a countable language and any subset $C$ of its domain, there is an elementary substructure containing $C$ of cardinality at most $\max (|C|,{\aleph }_0)$. In particular a finite or countable $C$ lies in a countable elementary substructure. This is the downward Löwenheim-Skolem theorem.

Construct it directly inside the given structure $A$. Start with $C_0$ containing $C$, the interpretations of the constants, and one element if needed to ensure a nonempty domain. Given $C_n$, for every formula $\exists x\phi (x,a)$ with its finite parameter tuple from $C_n$ that is true in $A$, choose one actual witness in $A$ and place it in $C_{n+1}$. Retain $C_n$ as well. There are at most $\max (|C|,{\aleph }_0)$ choices at each stage. Let $B={\bigcup }_{n<\omega }{C}_n$.

The construction closes $B$ under every function of the language: for a tuple in $C_n$, the formula $x=f(a)$ forces its unique value into the next stage. Thus $B$ carries the induced substructure, and it has the asserted cardinal bound.

Prove elementarity by structural induction. Atomic formulas agree by the induced-substructure construction; logical connectives preserve agreement. For an existential formula with parameters in $B$, if it is true in $A$, all its parameters occur in some $C_n$, so the chosen witness lies in $C_{n+1}\subseteq B$. The induction hypothesis makes its matrix true in $B$. In the other direction a witness in $B$ is also a witness in $A$, again by induction. This is the Tarski-Vaught test, with its witness argument proved explicitly. No completeness or compactness theorem theorem enters the construction.

A partial type $p(\mathbf{x})$ is a set of $L$-first-order formulas in a fixed tuple $\mathbf{x}=(x_1,\dots ,x_n)$ jointly consistent with $T$. A complete type, the usual meaning of an $n$-type here, is maximal among such consistent sets: for each first-order formula $\phi (\mathbf{x})$ it contains exactly one of $\phi ,\neg \phi$.

Add new constants $\mathbf{c}$ and considerEvery finite subset is satisfiable by consistency of the type. The compactness theorem gives a first-order model of the full set. Its $L$-reduct is a first-order model of $T$, and the interpretations of $\mathbf{c}$ realize $p$. This proof applies to partial as well as complete types.

For a complete theory in a countable language, the types realized in every first-order model are exactly the isolated types. An isolated type has a consistent first-order formula $\theta \in p$ such that $T\models \forall \mathbf{x}(\theta \to \phi )$ for every $\phi \in p$. Completeness forces $T\models \exists \mathbf{x}\theta$, so every first-order model realizes $p$; the converse is the omitting types theorem. Countability is a hypothesis of that converse, not of the preceding compactness realization argument. For a partial type the corresponding criterion is an isolating consistent first-order formula, together with its existence in every first-order model; it need not itself belong to the partial type.

If $T$ is not complete, no one complete $n$-type can be realized in every first-order model of $T$: a complete type decides sentences, and two completions of $T$ disagree on some sentence. Thus the completeness and countability hypotheses must be retained when using the isolated-type characterization.

No. Let $S$ be the displayed infinite axiom set. Any finite subset $S_0\subseteq S$ mentions only finitely many of the two infinitude requirements. Choose $N\ge 1$ at least as large as every index mentioned. A finite equivalence relation with exactly $N$ singleton classes and $N$ doubleton classes satisfies $S_0$, but is not a first-order model of the complete theory.

If a finite axiomatization existed, let $\sigma$ be the conjunction of its axioms. Then $S\models \sigma$, so the compactness theorem gives a finite $S_0\subseteq S$ with $S_0\models \sigma$. Every first-order model of $S_0$ would then satisfy the full first-order theory, contradicting the finite first-order model above. This is the finite subaxiomatization from an equivalent finite theory argument: finite axiomatizability would force one finite fragment of the explicit axioms to suffice.

NFU has a unary predicate $S$ for sets, atoms have no members, extensionality applies to sets, and comprehension applies to every stratified formula. A stratification assigns integer types to variables so that equality uses equal types and $x\in y$ requires $\mathrm{type}(y)=\mathrm{type}(x)+1$. A unary set predicate adds no type difference.

Start with the actual set structure $B=(V_{\omega +\omega },\in )$. This structure satisfies extensionality and every pure-membership separation instance: the subset defined in a set $a$ of rank below $\omega +\omega$ still has rank below $\omega +\omega$. We do not assert that $B$ satisfies replacement or all of ZFC. Expand it by Skolem functions. In it use the sequence of rank objects $V_{\omega +n+6}$, $n<\omega$. For two such objects $d<e$ in sequence order, we havewith quantifiers in $B$. The second statement holds because every subset of $V_{\alpha }$ belongs to $V_{\alpha +1}$, and the later rank is at least $\alpha +1$.

Introduce constants $d_i$, $i\in \mathbb{Z}$, and require them to be order indiscernibles in the Skolem language, satisfying these two assertions whenever $i<j$. Also require $V_{\omega +5}\subseteq d_i$ for every $i$; this fixed rank object is first-order definable in $B$. Every finite part of these requirements together with $\mathrm{Th}(B^{\ast })$ is satisfiable: color finite increasing tuples of the original rank sequence by the truth values of the finitely many formulas mentioned, and use Ramsey's theorem to get a homogeneous subsequence. The rank assertions hold for every increasing tuple there. The compactness theorem gives a model of the full theory. In its Skolem hull $N$ generated by the $d_i$, the integer shift extends to an automorphism $j$ with $j(d_i)=d_{i+1}$, by the term-transport proof of the Ehrenfeucht-Mostowski theorem. Thus $N$ still satisfies extensionality and all pure-membership separation instances, andThis is a set-sized first-order model; no satisfaction predicate for a proper-class universe is being assumed.

Externally let $D_i=\{x\in N:N\models x\in d_i\}$. The automorphism bijects $D_i$ onto $D_{i+1}$. Interpret a typed structure with sort $i$ equal to $D_i$. At sort $i+1$, declare $y$ a set exactly when $N\models y\subseteq d_i$; otherwise it is an atom. Define adjacent-sort membership byThe guard is necessary: a typed atom might have some ordinary $N$-members in $D_i$, and those must not become its typed members. Set-extensionality follows from extensionality in $N$, because the ordinary members of a typed set all lie in $D_i$. For any typed formula on sort $i$, its quantifiers can be restricted to the corresponding $d_l$, its set predicates replaced by subset assertions, and its memberships replaced by the guarded relation. This is an ordinary pure-membership formula of $N$ with finitely many parameters. Separation gives its extension $X\subseteq d_i$, and the displayed closure assertion gives $X\in d_{i+1}$. It is therefore a typed set witnessing comprehension. The automorphism shifts these sorted domains and preserves the set flags and guarded memberships.

Collapse the types onto $D_0$. DefineObjects not satisfying $S$ have no $E$-members. If two sets have the same $E$-members, their images under $j$ are subsets of $d_0$ with the same ordinary members, so are equal by extensionality of $N$; injectivity of $j$ gives equality of the original objects.

To verify every stratified comprehension instance, assign a variable $v$ its stratification type $t(v)$ and translate its value $a\in D_0$ to $j^{t(v)}(a)\in D_{t(v)}$. Equality is preserved. An atomic $E(x,y)$ translates to the guarded adjacent-sort membership because $t(y)=t(x)+1$; the unary predicate $S(y)$ translates to $j^{t(y)}(y)\subseteq d_{t(y)-1}$. Induction on formulas, using the domain bijections for quantifiers, preserves truth. If the free variable $x$ has type $t$, typed comprehension produces its extension $X\subseteq d_t$, with $X\in d_{t+1}$. Put $b=j^{-(t+1)}(X)\in D_0$. Then $S(b)$ holds, and for every $a\in D_0$,This is exactly the required NFU set. No formula containing the external automorphism $j$ has been used in a separation or comprehension scheme; $j$ only transports values after the pure formula is formed.

The construction also permits the usual infinity requirement. The ordinary $\omega$ and its successor graph $f$ are definable in $N$, hence fixed by $j$, and lie below $V_{\omega +5}$, so belong to all the required domains. Under $E$, the members of $\omega$ are still its ordinary $N$-members. The new Kuratowski pair satisfiesSince $j(f)=f$, membership of this pair in $f$ under $E$ is equivalent to $⟨x,y{⟩}_N\in f$. Thus $f$ is an internal injection of $\omega$ into itself omitting zero, giving a Dedekind-infinite set.

We have built a model of NFU, with infinity if it is included in the formulation, in ordinary ZFC metatheory:In particular $\mathrm{Con}(\mathrm{ZFC})\Rightarrow \mathrm{Con}(\mathrm{NFU})$. This proof does not assume $\mathrm{Con}(\mathrm{ZFC})$ as an additional internal axiom: its starting structure is the set $V_{\omega +\omega }$, not a model of ZFC.

For every infinite regular cardinal $\kappa$, every first-order structure has a $\kappa$-saturated elementary extension. At one stage use the compactness theorem with the elementary diagram to realize all complete types over subsets of the stage having size less than $\kappa$. There is a set of such types; finite subsets of the enlarged theory are satisfiable because their finitely many witnesses are independent. Iterate for $\kappa$ stages, taking elementary unions at limits. Regularity puts any parameter set of size less than $\kappa$ inside one stage, and its type is realized at the next one. Passing to a larger regular cardinal covers singular requested degrees of saturation as well.

For a type space $S_n^M(A)$, the basic open set $[\phi ]$ consists of complete types containing the formula $\phi$. These sets are clopen, satisfy $[\phi ]\cap [\psi ]=[\phi \wedge \psi ]$, and distinguish distinct types. The compactness theorem makes this topology compact; it is Hausdorff and has a basis of clopen sets.

In the language containing one binary equivalence relation $E$, require all classes to have size at most two and infinitely many classes of each of the two sizes. This is a complete theory: every countable model has countably many singleton classes and countably many doubleton classes, giving a class-by-class isomorphism; Downward Lowenheim-Skolem theorem then rules out a sentence separating arbitrary models. It is also an aleph-zero-categorical theory.

It is not finitely axiomatizable. Any finite fragment of the explicit infinitude schemes has a finite model with sufficiently many classes of each size; compactness theorem would make such a finite fragment suffice if any finite axiomatization existed. It is not model-complete: adjoining a new singleton preserves the theory, and subsequently giving that new point a partner also preserves the theory, while changing the existential partner formula at that point. Naming the singleton-class predicate removes this particular obstruction to elementary embeddings.

Typical ambiguity is the schema asserting that every closed well-typed sentence is equivalent to its uniform type-raise. It is not an assertion that adjacent types have the same cardinality. To obtain finite satisfiability, color finite increasing rank selections by the truth values of the finitely many sentences concerned. The Ramsey's theorem gives a homogeneous rank set; two overlapping windows then have equal truth vectors, yielding the desired type-raise equivalences. The compactness theorem gives a first-order model of the entire schema.

If a theory axiomatized the well-orders, adjoin constants $c_0,c_1,\dots$ and the sentences $c_{n+1}<c_n$. Every finite fragment has a finite well-ordered model, but compactness would produce a model with an infinite descending chain.