Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Consider a finitely axiomatized theory $T$ with axioms $\phi_1,...,\phi_n$ over a first-order language with relation symbols $R_1,...,R_k$ of arities $\alpha_1,...,\alpha_k$. Consider the atomic formulas written in the form $(x_1,...,x_{\alpha_j})\ \varepsilon R_j$.

Translate this theory into a (finite) set-theoretic definition

$T(X) :\equiv (\exists R_1)...(\exists R_k) R_i \subseteq X^{\alpha_i} \wedge \phi'_1 \wedge ... \wedge \phi'_n$

where $\phi'_i$ is $\phi_i$ with $(\forall x)$ replaced by $(\forall x \in X)$ and $(x_1,...,x_{\alpha_j})\ \varepsilon R_j$ replaced by $(x_1,...,x_{\alpha_j})\ \in R_j$ with $(x_1,...,x_{\alpha_j})$ an abbreviation for ordered tuples.

To show that $T$ has a model — i.e. to show that $T$ is consistent — is to prove the statement $(\exists x) T(x)$ from the axioms of set theory.

It is essential that the relations fulfill the conditions $\phi_i$ simultaneously. Thus it is not clear at first sight, how the existence of a model of a theory can be proved (or even be stated set-theoretically) that is not finitely axiomatizable, since it cannot be translated into a finite sentence.

Some other things are not clear (to me):

  1. In this setting, doesn't the consistency of every theory dependend on the consistency of the choosen set theory? (If the set theory isn't consistent, every theory has a model.)

  2. Furthermore, doesn't the consistency of a theory depend on the choice of the set theory in which $(\exists x) T(x)$ is proved? (In some set theories $(\exists x) T(x)$ can be proved, in others maybe not.)

  3. What conditions has a theory to fulfill to be able to play the role of set theory in this setting? [It doesn't have to be the element relation $\in$ which $\varepsilon$ is mapped on. But one needs to be able to build ordered tuples of arbitrary length. What else? Something like powersets (since $R_i \subseteq X^{\alpha_i}$ is $R_i \in \mathcal{P}(X^{\alpha_i})$)? Is extensionality necessary? What is the general framework to discuss such questions?]

share|cite|improve this question
You're not thinking ‘big’ enough. Assuming that the first-order theory in question can be specified as a set of axioms over a set of relation symbols etc. then it is, of course, possible to construct a sentence asserting the existence (or non-existence) of a model of that theory: we want a set of relations satisfying a set of conditions, and so on. In essence, you have to internalise the entire apparatus of first-order logic inside set theory. [...] – Zhen Lin Aug 16 '11 at 7:07
As for your actual questions: (1) doesn't make sense, since an inconsistent set theory has no model; (2) seems to be based on a misunderstanding (the consistency of a theory is defined in terms of syntax, not semantics); and (3) needs clarification, since there are weak systems which admit models of theories but (as far as I know) are not first-order, say. (For example, the internal logic of a Heyting category is first-order intuitionistic logic, but I don't think the theory of Heyting categories is first-order.) – Zhen Lin Aug 16 '11 at 7:10

The method you describe for making "set-theoretical sense" of consistency of first-order theories is correct, but only applicable to finitely axiomatisable theories. Another possibility is to encode formulas by sets. Something along these lines (let $\phi_\alpha$ denote the formula encoded by $\alpha$):

  • $\langle j, i_1, ..., i_{\alpha_j} \rangle$ denotes the formula $R_j(x_{i_1}, ..., x_{i_{\alpha_j}})$
  • $\langle k + 1, \alpha \rangle$ denotes $\lnot \phi_\alpha$
  • $\langle k + 2, \alpha, \beta \rangle$ denotes the formula $\phi_\alpha \lor \phi_\beta$
  • $\langle k + 3, i, \alpha \rangle$ denotes the formula $\exists x_i \phi_\alpha$.

Now you can have a formula $models(X, R_1, ..., R_k, \alpha)$, which would express "the structure $\langle X, R_1, ..., R_k \rangle$ is a model of $\phi_\alpha$". Now if you have a theory (i.e. a set of formulas) $T$, then its consistency can be expressed by the formula $\exists X, R_1, ..., R_k \forall \alpha \in T~models(X, R_1, ..., R_k, \alpha)$.

However, one can also take the syntactic approach (i.e. a theory is consistent if and only if $\bot$ is not provable) and express the consistency in arithmetic. Now to your questions:

  1. It is not strictly correct to say that the consistency of a theory depends on set theory. However if your set theory is inconsistent it can prove everything, including the consistency of every theory.

  2. Yes. Apart from trivial examples. ZFC does not prove $con(\rm ZFC)$, but ZFC + "there is an inaccessible cardinal" does.

  3. As previously noted, any theory that includes arithmetic can express consistency.

share|cite|improve this answer

Once we have a method for quantifying over models, we can prove Gödel's completeness theorem in ZFC: a theory $T$ has a model if and only if there is no proof of a contradiction from axioms in $T$. This gives a different way to tell whether a theory is consistent. But to prove the completeness theorem, we first have to have a way to express "$T$ has a model" in set theory. So the question I am going to answer is:

Suppose $T$ is an infinite set of (Gödel numbers of) sentences in some language. How can we define, in set theory, what is means for a structure $M$ to be a model of $T$?

As the question points out, you can't just write down a single sentence in the same way as if $T$ was a finite theory. Instead, you have to go through the truth function (satisfaction relation) of the model. ZF proves that, for any (set) model $M$, there is a function $f$ that takes a Gödel number of a formula $\phi$ and returns either 0 or 1 depending on whether $\phi$ is true or false in $M$. Moreover, the $T$-schema allows us to give an implicit definition of such an $M$ using a single formula $\operatorname{TFunc}(f,M)$, which is true if and only if $f$ is a truth function for the model $M$ (the formula depends on the language but not the model). The formula for TFunc just follows the inductive definition in the $T$-schema: if $\phi$ is atomic, we can directly define what $f(\phi, M)$ should be, using $M$, while if $\phi$ is not atomic we can define what $f(\phi,M)$ should be in terms of the values of $f$ on subformulas of $\phi$. This is only an implicit definition, but that's going to be good enough.

Now, if we want to say "$M$ is a model of $T$", we say it with this formula: "For every $f$, if $\operatorname{TFunc}(f,M)$ then for every sentence $\phi$ in $T$, $f(\phi,M) = 1$." Because ZF proves there is a truth function for $M$, the quantifier and implicit definition of $f$ combine to allow us to access the truth function. We could also use an existential quantifier: "$M$ satisfies $T$ if there is an $f$ such that $\operatorname{TFunc}(f,M)$ and for every $\phi \in T$, $f(\phi) = 1$. "

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.