Skip to main content
Some thoughts about DLO and the random graph
Source Link
James E Hanson
  • 13.1k
  • 3
  • 37
  • 71
 

EDIT2: I didn't see this question before. Joel's argument works the same here: Once you pick a well-ordering of the language $\mathcal{L}$ you can encode it in ordinals and consider the inner model $L[\mathcal{L}]$ where global choice holds and you can construct class sized models easily. I think the EM functor construction accomplishes something slightly different in that having an EM functor for a theory (i.e. a Skolemization and then an EM type in the Skolemized theory) seems weaker than having a well-ordering of the language, which might be useful.


EDIT3: I realized that the random graph, $DLO$, and maybe some others have a property in common that allows this to work: There is a canonical procedure for, given a set of parameters $A$, constructing a complete $|S_1(A)|$-type whose component $1$-types hit every type in $S_1(A)$. For the random graph we can take an element for each subset of $A$ and add in no connections between the new elements and for $DLO$ we can add in each cut. Any theory with this property has a proper class monster model because we can just iterate it along $Ord$.

I think it's really close to something you can do with an arbitrary stable theory, specifically if every type in $S_1(A)$ is stationary you can take a product type, $\bigotimes_{p\in S_1(A)} p$ (I think?). The problem I'm having with this is that types over the new set of parameters won't necessarily be stationary, so I'd like to use strong types but it's not clear to me that there's a canonical way of passing from a set $A$ to its algebraic closure in $T^{eq}$. It seems like it might need some amount of global choice to do. But maybe that's how to get a counterexample? Something involving a model of $ZFC$ where global finite choice or global choice for pairs fails.

EDIT2: I didn't see this question before. Joel's argument works the same here: Once you pick a well-ordering of the language $\mathcal{L}$ you can encode it in ordinals and consider the inner model $L[\mathcal{L}]$ where global choice holds and you can construct class sized models easily. I think the EM functor construction accomplishes something slightly different in that having an EM functor for a theory (i.e. a Skolemization and then an EM type in the Skolemized theory) seems weaker than having a well-ordering of the language, which might be useful.

 

EDIT2: I didn't see this question before. Joel's argument works the same here: Once you pick a well-ordering of the language $\mathcal{L}$ you can encode it in ordinals and consider the inner model $L[\mathcal{L}]$ where global choice holds and you can construct class sized models easily. I think the EM functor construction accomplishes something slightly different in that having an EM functor for a theory (i.e. a Skolemization and then an EM type in the Skolemized theory) seems weaker than having a well-ordering of the language, which might be useful.


EDIT3: I realized that the random graph, $DLO$, and maybe some others have a property in common that allows this to work: There is a canonical procedure for, given a set of parameters $A$, constructing a complete $|S_1(A)|$-type whose component $1$-types hit every type in $S_1(A)$. For the random graph we can take an element for each subset of $A$ and add in no connections between the new elements and for $DLO$ we can add in each cut. Any theory with this property has a proper class monster model because we can just iterate it along $Ord$.

I think it's really close to something you can do with an arbitrary stable theory, specifically if every type in $S_1(A)$ is stationary you can take a product type, $\bigotimes_{p\in S_1(A)} p$ (I think?). The problem I'm having with this is that types over the new set of parameters won't necessarily be stationary, so I'd like to use strong types but it's not clear to me that there's a canonical way of passing from a set $A$ to its algebraic closure in $T^{eq}$. It seems like it might need some amount of global choice to do. But maybe that's how to get a counterexample? Something involving a model of $ZFC$ where global finite choice or global choice for pairs fails.

added 906 characters in body
Source Link
James E Hanson
  • 13.1k
  • 3
  • 37
  • 71

EDIT: There were requests for details on the EM model with $Ord$ for a spine construction. There might be some subtlety that I wasn't aware of regarding the model satisfying the theory but I'm fairly confident that you can literally construct the class. The construction is not completely uniform in that it needs the EM functor or at least a well-ordering of the languageor at least a well-ordering of the language as a parameter in the end.

(This only matters if you want to avoid picking a well-ordering of the set of Skolem functions, otherwise you can just pick representatives.) Since the Skolemized theory is complete the definition of Skolem function application on $C_0$ is consistent with $\sim$, so it defines functions on $C$. Then you can define predicates using a dumb encoding trick: Let $f_0$ be the 0-ary Skolem function for the formula $y=y$ and let $f_1$ be the 0-ary Skolem function for the formula $y\neq f_0$. Then for any $n$-ary predicate symbol $P$, let $f^\ast_P$ be the Skolem function corresponding to the formula $\left(P(\overline{x})\rightarrow y = f_0 \right) \wedge \left( \neg P(\overline{x}) \rightarrow y = f_1 \right)$. Then the predicate $P$ is defined by $P(\overline{x})$ if and only if $f^\ast_P(\overline{x})=\left[\left<f_0,0\right>\right]$. (EDIT2: Although note that this also works for formulas in general, so by Skolemizing a theory we've actually also constructed a truth predicate for models of the Skolemized theory.) Clearly we already have constants and functions defined in terms of the Skolem functions.

And really I think the only parameter you need is a well-ordering of the language, because given that you can canonically pick $T^{sk}$ and the EM type by expanding $\mathcal{L}$ with Skolem functions in the typical way to $\mathcal{L}^{sk}$ and extending the well-ordering to $\mathcal{L}^{sk}$; adding constants $I=\{c_i: i < \omega\}$ for a sequence of indiscernibles; adding the Skolem function axioms, $\forall \overline{x} (\exists y \varphi(y;\overline{x}) \rightarrow \varphi(f_\varphi(\overline{x});\overline{x}))$, and the indiscernible sequence axioms, $\varphi(\overline{c})\leftrightarrow \varphi(\overline{c}^\prime)$ and $c_0 \neq c_1$, for all $\varphi$ and strictly increasing tuples $\overline{c},\overline{c}^\prime$; and then picking a completion by going through the $\mathcal{L}^{sk}_I$ sentences $\{\varphi_i : i < \lambda \}$ according to the well-order and adding $\varphi_i$ if it is consistent (according to some fixed proof system) and $\neg \varphi_i$ otherwise.

EDIT2: I didn't see this question before. Joel's argument works the same here: Once you pick a well-ordering of the language $\mathcal{L}$ you can encode it in ordinals and consider the inner model $L[\mathcal{L}]$ where global choice holds and you can construct class sized models easily. I think the EM functor construction accomplishes something slightly different in that having an EM functor for a theory (i.e. a Skolemization and then an EM type in the Skolemized theory) seems weaker than having a well-ordering of the language, which might be useful.

EDIT: There were requests for details on the EM model with $Ord$ for a spine construction. There might be some subtlety that I wasn't aware of regarding the model satisfying the theory but I'm fairly confident that you can literally construct the class. The construction is not completely uniform in that it needs the EM functor or at least a well-ordering of the language as a parameter in the end.

(This only matters if you want to avoid picking a well-ordering of the set of Skolem functions, otherwise you can just pick representatives.) Since the Skolemized theory is complete the definition of Skolem function application on $C_0$ is consistent with $\sim$, so it defines functions on $C$. Then you can define predicates using a dumb encoding trick: Let $f_0$ be the 0-ary Skolem function for the formula $y=y$ and let $f_1$ be the 0-ary Skolem function for the formula $y\neq f_0$. Then for any $n$-ary predicate symbol $P$, let $f^\ast_P$ be the Skolem function corresponding to the formula $\left(P(\overline{x})\rightarrow y = f_0 \right) \wedge \left( \neg P(\overline{x}) \rightarrow y = f_1 \right)$. Then the predicate $P$ is defined by $P(\overline{x})$ if and only if $f^\ast_P(\overline{x})=\left[\left<f_0,0\right>\right]$. Clearly we already have constants and functions defined in terms of the Skolem functions.

And really I think the only parameter you need is a well-ordering of the language, because given that you can canonically pick $T^{sk}$ and the EM type by expanding $\mathcal{L}$ with Skolem functions in the typical way to $\mathcal{L}^{sk}$ and extending the well-ordering to $\mathcal{L}^{sk}$; adding constants $I=\{c_i: i < \omega\}$ for a sequence of indiscernibles; adding the Skolem function axioms, $\forall \overline{x} (\exists y \varphi(y;\overline{x}) \rightarrow \varphi(f_\varphi(\overline{x});\overline{x}))$, and the indiscernible sequence axioms, $\varphi(\overline{c})\leftrightarrow \varphi(\overline{c}^\prime)$ and $c_0 \neq c_1$, for all $\varphi$ and strictly increasing tuples $\overline{c},\overline{c}^\prime$; and then picking a completion by going through the $\mathcal{L}^{sk}_I$ sentences $\{\varphi_i : i < \lambda \}$ according to the well-order and adding $\varphi_i$ if it is consistent (according to some fixed proof system) and $\neg \varphi_i$ otherwise.

EDIT: There were requests for details on the EM model with $Ord$ for a spine construction. There might be some subtlety that I wasn't aware of regarding the model satisfying the theory but I'm fairly confident that you can literally construct the class. The construction is not completely uniform in that it needs the EM functor or at least a well-ordering of the language as a parameter in the end.

(This only matters if you want to avoid picking a well-ordering of the set of Skolem functions, otherwise you can just pick representatives.) Since the Skolemized theory is complete the definition of Skolem function application on $C_0$ is consistent with $\sim$, so it defines functions on $C$. Then you can define predicates using a dumb encoding trick: Let $f_0$ be the 0-ary Skolem function for the formula $y=y$ and let $f_1$ be the 0-ary Skolem function for the formula $y\neq f_0$. Then for any $n$-ary predicate symbol $P$, let $f^\ast_P$ be the Skolem function corresponding to the formula $\left(P(\overline{x})\rightarrow y = f_0 \right) \wedge \left( \neg P(\overline{x}) \rightarrow y = f_1 \right)$. Then the predicate $P$ is defined by $P(\overline{x})$ if and only if $f^\ast_P(\overline{x})=\left[\left<f_0,0\right>\right]$. (EDIT2: Although note that this also works for formulas in general, so by Skolemizing a theory we've actually also constructed a truth predicate for models of the Skolemized theory.) Clearly we already have constants and functions defined in terms of the Skolem functions.

And really I think the only parameter you need is a well-ordering of the language, because given that you can canonically pick $T^{sk}$ and the EM type by expanding $\mathcal{L}$ with Skolem functions in the typical way to $\mathcal{L}^{sk}$ and extending the well-ordering to $\mathcal{L}^{sk}$; adding constants $I=\{c_i: i < \omega\}$ for a sequence of indiscernibles; adding the Skolem function axioms, $\forall \overline{x} (\exists y \varphi(y;\overline{x}) \rightarrow \varphi(f_\varphi(\overline{x});\overline{x}))$, and the indiscernible sequence axioms, $\varphi(\overline{c})\leftrightarrow \varphi(\overline{c}^\prime)$ and $c_0 \neq c_1$, for all $\varphi$ and strictly increasing tuples $\overline{c},\overline{c}^\prime$; and then picking a completion by going through the $\mathcal{L}^{sk}_I$ sentences $\{\varphi_i : i < \lambda \}$ according to the well-order and adding $\varphi_i$ if it is consistent (according to some fixed proof system) and $\neg \varphi_i$ otherwise.

EDIT2: I didn't see this question before. Joel's argument works the same here: Once you pick a well-ordering of the language $\mathcal{L}$ you can encode it in ordinals and consider the inner model $L[\mathcal{L}]$ where global choice holds and you can construct class sized models easily. I think the EM functor construction accomplishes something slightly different in that having an EM functor for a theory (i.e. a Skolemization and then an EM type in the Skolemized theory) seems weaker than having a well-ordering of the language, which might be useful.

Details of EM model with Ord for a spine construction
Source Link
James E Hanson
  • 13.1k
  • 3
  • 37
  • 71

EDIT: There were requests for details on the EM model with $Ord$ for a spine construction. There might be some subtlety that I wasn't aware of regarding the model satisfying the theory but I'm fairly confident that you can literally construct the class. The construction is not completely uniform in that it needs the EM functor or at least a well-ordering of the language as a parameter in the end.

First run the typical EM functor construction: Given a consistent theory $T$ with infinite models, find a complete Skolemization $T^{sk}$ and then find an EM type of a non-constant indiscernible sequence in $T^{sk}$.

To construct an EM model, assuming we Skolemized the theory the 'dumb' way, it's sufficient to consider terms of the form $f(\overline{a})$ where $f$ is a Skolem function and $\overline{a}$ is a strictly decreasing tuple of indiscernibles, because any more complicated Skolem terms and terms with permutations of variables are equivalent to some base Skolem function corresponding to a formula of the form $y=t(\overline{x})$. So to construct the base class of the model, first let $$C_0 = \{\left<f,\alpha\right>:f\text{ an }n\text{-ary Skolem fn, }\alpha\in Ord\text{ with CNF }\omega^{\beta_0}+\dots+\omega^{\beta_{n-1}}\},$$

with the intended interpretation that $\left<f,\alpha\right>$ is equal to $f(\beta_0,\dots,\beta_{n-1})$. You can define Skolem function application by setting $f(\left<f_0,\alpha_0\right>,\dots,\left<f_{n-1},\alpha_{n-1}\right>)$ equal to $\left<g,\gamma\right>$ where you choose $g$ and $\gamma$ algorithmically from the list $f,f_0,\dots,f_{n-1}$ and the set of the exponents in the CNFs of $\alpha_0,\dots,\alpha_{n-1}$ (basically by the same kind of reasoning as why we don't need Skolem terms that are more complicated than just single Skolem functions applied to indiscernibles).

Then you define an equivalence relation on $C_0$ by $\left<f,\alpha\right> \sim \left<g,\gamma\right>$ for $\alpha = \omega^{\beta_0}+\dots+\omega^{\beta_{n-1}}$ and $\gamma = \omega^{\delta_0}+\dots+\omega^{\delta_{m-1}}$ by looking at a set of indiscernibles in the original indiscernible sequence with the same order type as $\{\beta_0,\dots,\beta_{n-1},\delta_0,\dots,\delta_{m-1}\}$ and then checking equality of the original corresponding terms. Let $\left[ \left<f,\alpha\right>\right]$ be the equivalence class of $\left<f,\alpha\right>$ (which may be a proper class). Then define the actual base class of the model by the typical kind of trick to avoid picking representatives:

$$ C = \{ \left[\left<f,\alpha\right>\right] \cap V_\beta : \left<f,\alpha\right> \in C_0 , \, \beta \text{ minimal s.t. } \left[\left<f,\alpha\right>\right] \cap V_\beta \neq \varnothing \}.$$

(This only matters if you want to avoid picking a well-ordering of the set of Skolem functions, otherwise you can just pick representatives.) Since the Skolemized theory is complete the definition of Skolem function application on $C_0$ is consistent with $\sim$, so it defines functions on $C$. Then you can define predicates using a dumb encoding trick: Let $f_0$ be the 0-ary Skolem function for the formula $y=y$ and let $f_1$ be the 0-ary Skolem function for the formula $y\neq f_0$. Then for any $n$-ary predicate symbol $P$, let $f^\ast_P$ be the Skolem function corresponding to the formula $\left(P(\overline{x})\rightarrow y = f_0 \right) \wedge \left( \neg P(\overline{x}) \rightarrow y = f_1 \right)$. Then the predicate $P$ is defined by $P(\overline{x})$ if and only if $f^\ast_P(\overline{x})=\left[\left<f_0,0\right>\right]$. Clearly we already have constants and functions defined in terms of the Skolem functions.

And then pretty much by construction this is a class model of the $\forall \exists$ part of $T^{sk}$ (uniformly? since it has bounded quantifier complexity and you can define truth in ZFC for sentences with bounded quantifier complexity), which entails all of $T^{sk}$. Also it seems like this should be uniform in the parameters $T^{sk}$ and the EM type.

And really I think the only parameter you need is a well-ordering of the language, because given that you can canonically pick $T^{sk}$ and the EM type by expanding $\mathcal{L}$ with Skolem functions in the typical way to $\mathcal{L}^{sk}$ and extending the well-ordering to $\mathcal{L}^{sk}$; adding constants $I=\{c_i: i < \omega\}$ for a sequence of indiscernibles; adding the Skolem function axioms, $\forall \overline{x} (\exists y \varphi(y;\overline{x}) \rightarrow \varphi(f_\varphi(\overline{x});\overline{x}))$, and the indiscernible sequence axioms, $\varphi(\overline{c})\leftrightarrow \varphi(\overline{c}^\prime)$ and $c_0 \neq c_1$, for all $\varphi$ and strictly increasing tuples $\overline{c},\overline{c}^\prime$; and then picking a completion by going through the $\mathcal{L}^{sk}_I$ sentences $\{\varphi_i : i < \lambda \}$ according to the well-order and adding $\varphi_i$ if it is consistent (according to some fixed proof system) and $\neg \varphi_i$ otherwise.

EDIT: There were requests for details on the EM model with $Ord$ for a spine construction. There might be some subtlety that I wasn't aware of regarding the model satisfying the theory but I'm fairly confident that you can literally construct the class. The construction is not completely uniform in that it needs the EM functor or at least a well-ordering of the language as a parameter in the end.

First run the typical EM functor construction: Given a consistent theory $T$ with infinite models, find a complete Skolemization $T^{sk}$ and then find an EM type of a non-constant indiscernible sequence in $T^{sk}$.

To construct an EM model, assuming we Skolemized the theory the 'dumb' way, it's sufficient to consider terms of the form $f(\overline{a})$ where $f$ is a Skolem function and $\overline{a}$ is a strictly decreasing tuple of indiscernibles, because any more complicated Skolem terms and terms with permutations of variables are equivalent to some base Skolem function corresponding to a formula of the form $y=t(\overline{x})$. So to construct the base class of the model, first let $$C_0 = \{\left<f,\alpha\right>:f\text{ an }n\text{-ary Skolem fn, }\alpha\in Ord\text{ with CNF }\omega^{\beta_0}+\dots+\omega^{\beta_{n-1}}\},$$

with the intended interpretation that $\left<f,\alpha\right>$ is equal to $f(\beta_0,\dots,\beta_{n-1})$. You can define Skolem function application by setting $f(\left<f_0,\alpha_0\right>,\dots,\left<f_{n-1},\alpha_{n-1}\right>)$ equal to $\left<g,\gamma\right>$ where you choose $g$ and $\gamma$ algorithmically from the list $f,f_0,\dots,f_{n-1}$ and the set of the exponents in the CNFs of $\alpha_0,\dots,\alpha_{n-1}$ (basically by the same kind of reasoning as why we don't need Skolem terms that are more complicated than just single Skolem functions applied to indiscernibles).

Then you define an equivalence relation on $C_0$ by $\left<f,\alpha\right> \sim \left<g,\gamma\right>$ for $\alpha = \omega^{\beta_0}+\dots+\omega^{\beta_{n-1}}$ and $\gamma = \omega^{\delta_0}+\dots+\omega^{\delta_{m-1}}$ by looking at a set of indiscernibles in the original indiscernible sequence with the same order type as $\{\beta_0,\dots,\beta_{n-1},\delta_0,\dots,\delta_{m-1}\}$ and then checking equality of the original corresponding terms. Let $\left[ \left<f,\alpha\right>\right]$ be the equivalence class of $\left<f,\alpha\right>$ (which may be a proper class). Then define the actual base class of the model by the typical kind of trick to avoid picking representatives:

$$ C = \{ \left[\left<f,\alpha\right>\right] \cap V_\beta : \left<f,\alpha\right> \in C_0 , \, \beta \text{ minimal s.t. } \left[\left<f,\alpha\right>\right] \cap V_\beta \neq \varnothing \}.$$

(This only matters if you want to avoid picking a well-ordering of the set of Skolem functions, otherwise you can just pick representatives.) Since the Skolemized theory is complete the definition of Skolem function application on $C_0$ is consistent with $\sim$, so it defines functions on $C$. Then you can define predicates using a dumb encoding trick: Let $f_0$ be the 0-ary Skolem function for the formula $y=y$ and let $f_1$ be the 0-ary Skolem function for the formula $y\neq f_0$. Then for any $n$-ary predicate symbol $P$, let $f^\ast_P$ be the Skolem function corresponding to the formula $\left(P(\overline{x})\rightarrow y = f_0 \right) \wedge \left( \neg P(\overline{x}) \rightarrow y = f_1 \right)$. Then the predicate $P$ is defined by $P(\overline{x})$ if and only if $f^\ast_P(\overline{x})=\left[\left<f_0,0\right>\right]$. Clearly we already have constants and functions defined in terms of the Skolem functions.

And then pretty much by construction this is a class model of the $\forall \exists$ part of $T^{sk}$ (uniformly? since it has bounded quantifier complexity and you can define truth in ZFC for sentences with bounded quantifier complexity), which entails all of $T^{sk}$. Also it seems like this should be uniform in the parameters $T^{sk}$ and the EM type.

And really I think the only parameter you need is a well-ordering of the language, because given that you can canonically pick $T^{sk}$ and the EM type by expanding $\mathcal{L}$ with Skolem functions in the typical way to $\mathcal{L}^{sk}$ and extending the well-ordering to $\mathcal{L}^{sk}$; adding constants $I=\{c_i: i < \omega\}$ for a sequence of indiscernibles; adding the Skolem function axioms, $\forall \overline{x} (\exists y \varphi(y;\overline{x}) \rightarrow \varphi(f_\varphi(\overline{x});\overline{x}))$, and the indiscernible sequence axioms, $\varphi(\overline{c})\leftrightarrow \varphi(\overline{c}^\prime)$ and $c_0 \neq c_1$, for all $\varphi$ and strictly increasing tuples $\overline{c},\overline{c}^\prime$; and then picking a completion by going through the $\mathcal{L}^{sk}_I$ sentences $\{\varphi_i : i < \lambda \}$ according to the well-order and adding $\varphi_i$ if it is consistent (according to some fixed proof system) and $\neg \varphi_i$ otherwise.

Source Link
James E Hanson
  • 13.1k
  • 3
  • 37
  • 71
Loading