New Foundations is consistent

8.2 Term models

Definition 8.8
#

Let \( L \) be a \( \Sigma \)-language. A 1-\( L \)-formula of sort \( A \) is an \( L \)-bounded formula on \( \operatorname {\mathsf{Empty}} \) with one additional free variable of sort \( f : \operatorname {\mathsf{Fin}}1 \to \Sigma \) given by \( f(x) = A \).

Definition 8.9
#

Let \( L \) be a \( \Sigma \)-language. The witness symbols for \( L \) is the language \( L_W \) consisting of a single constant of sort \( A \) for every 1-\( L \)-formula of sort \( A \).

Proposition 8.10

Let \( M \) be a nonempty \( L \)-structure. Then \( M \) has an \( L_W \)-structure such that for each 1-\( L \)-formula \( \phi \) of sort \( A \), there is a constant symbol \( c : \operatorname {\mathsf{Functions}}(0, \# [], A) \) such that

\[ \forall x : M_A,\, \phi (x) \to \phi (c) \]
Proof

We define the interpretation of the constant for \( \phi \) to be some \( x : M \) such that \( M \vDash \phi (x) \) if one exists, or an arbitrary \( y : M \) otherwise. 1 This defines an \( L_W \)-structure for \( M \), and clearly \( M \) satisfies the required property.

Definition 8.11
#

For each \( n : \mathbb N \), we define

\[ L^{(0)} = L;\quad L^{(n+1)} = L^{(n)} \oplus (L^{(n)})_W \]

This forms a directed diagram of languages, which has a colimit \( L^{(\omega )} \). There are natural morphisms \( L \to L^{(\omega )} \) and \( L^{(n)} \to L^{(\omega )} \) which are expansions on \( M \).

Proposition 8.12
#

Let \( M \) be a nonempty \( L \)-structure. Then \( M \) has an \( L^{(\omega )} \)-structure such that for each 1-\( L^{(\omega )} \)-formula \( \phi \) of sort \( A \), there is a constant symbol \( c : \operatorname {\mathsf{Functions}}(0, \# [], A) \) such that

\[ \forall x : M_A,\, \phi (x) \to \phi (c) \]

Then, by the Tarski–Vaught test (which must be proven in the many-sorted case), the set \( N \subseteq M \) comprised of all of the interpretations of \( L^{(\omega )} \)-terms, is the domain of an \( L^{(\omega )} \)-elementary substructure of \( M \).

This will take substantial work.

  1. Use mathlib’s Classical.epsilon.