Is this theory trying to capture the theory of the minimal model of ZFC correctly formalized

axiomsfirst-order-logiclogicset-theory

I'm trying to capture theory $T_0$ written by Noah's answer to a prior posting of mine.

First we add a constant symbol $\mathcal M$ to the language of set theory.

Now we add all axioms of $\sf ID$ and $\sf ZFC$ in the language of set theory (i.e. just using $\sf FOL(=,\in)$, in particular not using the symbol $\mathcal M$), add the axiom of existence of a transitive model of $\sf ZFC$, the open explansion of which is a sentence in the language of set theory.

Add the axiom of transitivity of $\mathcal M$

Add the following scheme:

Minimality: if $\psi$ is a sentence in the first order language of set theory, then:

$\sf \forall N \, ( (N \overset{mt}\models ZFC) \implies (N \models \psi)) \implies \psi^\mathcal M$

Where $\sf \overset {mt} \models$ denotes "is a minimal transitive model of"; $\psi^\mathcal M$ stands for bounding all quantifiers of $\psi$ by "$\in \mathcal M$"

Call this theory $\sf ZFC + mTm$

where $\sf mTm$ stands for theory of the minimal transitive model of ZFC, which are the axioms of the above theory other than ZFC axioms.

This way all theorems provable in "ZFC + there exists a transitive model of ZFC" to be satisfied by the minimal transitive model of ZFC, would be true sentences of the world $\mathcal M$.

Let $\sf minZFC$ stand for a constant set of sentences, i.e. some constant theory, so it is a constant symbol of the meta-language, then axiomatize:

Extraction: if $\psi$ is a formula in the language of set theory, then: $$\sf minZFC \vdash \psi \iff [ ZFC+mTm] \vdash \psi^\mathcal M$$

Is theory $\sf minZFC$ effectively generated, i.e. its theorems are recursively enumerable?

I think that $T_0= \sf minZFC$, however I'm not sure if the above way of formalization is correct. I mean I don't see the axioms of $\sf minZFC$, so is this a correct way of defining an effective theory?

Best Answer

The $T_0$ I had in mind was just the set of all sentences $\varphi$ such that $\mathsf{ZFC}\vdash$ "$\varphi$ is true in every transitive model $M$ of $\mathsf{ZFC}$ such that $M$ has no $M$-definable proper transitive submodels." The bit after the "such that" is a strong type of minimality - in particular, it's stronger than merely demanding that $M\models$ "$\mathsf{ZFC}$ has no transitive models."

Here are some statements which are in $T_0$:

  • Every axiom of $\mathsf{ZFC}$ (since $\mathsf{ZFC}\vdash$ "Every model of $\mathsf{ZFC}$ satisfies $\mathsf{ZFC}$," rather boringly.)

  • "$\mathsf{ZFC}$ has no transitive models."

    • Note that we don't actually need to allow parameters from $M$ in the definability condition: if $M$ has a definable-with-parameters transitive set model of $\mathsf{ZFC}$, then it has a parameter-freely definable one (via reflection to $L^M$).

  • $\mathsf{V=L}$. Reasoning in $\mathsf{ZFC}$, if $M$ were a transitive model of $\mathsf{ZFC+\neg V=L}$, then $L^M$ would be a proper transitive submodel of $M$ definable in $M$.

    • In fact, the definition of $T_0$ above is equivalent to "the set of all $\varphi$ such that $\mathsf{ZFC}\vdash$ "$\varphi$ is true in every transitive model of $\mathsf{ZFC+V=L+}$ "$\mathsf{ZFC}$ has no transitive (set) models.""

  • $\mathsf{Con(\mathsf{ZFC^-+ZFC\mbox{ has a transitive model}})}$ (where $\mathsf{ZFC^-}$ is the correct version of $\mathsf{ZFC}$ without powerset). This is because any transitive model $M$ of $\mathsf{ZFC}$ satisfies all true arithmetic sentences, and $\mathsf{ZFC}\vdash$ "If there is a transitive model of $\mathsf{ZFC}$, then $\mathsf{ZFC^-}$ + "There is a transitive model of $\mathsf{ZFC}$" is consistent." (There's less to this than meets the eye; really, the point is $\mathsf{ZFC}\vdash$ "Every set is an element of a transitive model of $\mathsf{ZFC^-}$.")

Related Question