Are those conditions sufficient for a theory to prove existence of a model of it?

69 Views Asked by At

If $T$ is a first order theory with a single extra-logical primitive that is the set membership binary relation $\in$. Now let $A_1,..,A_n$, where $n$ is finite, be all of axioms of $T$.

Now suppose that $\langle \rangle$ is a two place function symbol that is definable in $T$, and that $T$ proves it to fulfill the characteristic property of ordered pairs.

Also suppose that $T$ can speak about arithmetical sentences.

Now if $T$ proves the following theorem:

$\exists M: Trs^\in (M) \land \exists R \ (R= \{\langle x,y \rangle: x,y \in M \land x \in y\} \land A_1^{MR} \land ... \land A_n^{MR})$

where $Trs^\in $ means is $\in$ -transitive, $A_i^{MR}$ means writing the $i^{th}$ axiom by bounding all of its quantifiers by $M$ and substituting every atomic formula $x_j \in x_k$ in them by $\exists p \in R :p=\langle x_j, x_k \rangle$.

Doest it follow that $T \vdash \exists M(M \models T)$, and thereby: $T \vdash Con(T)$?

If it fails, then why?