MathOverflow is a question and answer site for professional mathematicians. 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

Define $Ind(ZFC,\sigma)$ to be the assertion "The sentence $\sigma$ is independent from ZFC".

I am looking for theorems in the form $Ind(ZFC, Ind (ZFC,\sigma))$.

Are there such theorems in set theory?

Of course the first order inexpressibility is a problem in these theorems and many of them are theorem schemas.

share|cite|improve this question

Almost all instances of independence are instances of your further phenomenon, for the following general reason. Namely, if there is a model of ZFC which believes that "$\sigma$ is independent of ZFC" is true, then there is another model of ZFC which believes that it is false, since any assertion of independence fails in a model of ZFC plus $\neg$Con(ZFC), as there are no independent assertions for an inconsistent theory.

Another way to say this is that if it is consistent with ZFC that your sentence is independent, then this assertion is itself never provable in ZFC, because to prove an instance of independence is to prove consistency, which is impossible by the incompleteness theorem.

One might like to say that all instances of independence are instances of your further phenomenon, but unfortunately, we cannot quite prove that without further hypotheses. Indeed, it is consistent with ZFC that there are independent statements, but no instances of Ind(ZFC,Ind(ZFC,$\sigma$)). To see this, consider any model $M$ of ZFC+Con(ZFC)+$\neg$Con(ZFC+Con(ZFC)). Such a model exists by the incompleteness theorem, and in this model we'll have Con(ZFC) and hence all kinds of independent statements, but inside $M$ we will have no models of ZFC+Con(ZFC), and thus $M$ thinks that there are no models of Ind(ZFC,$\sigma$) for any $\sigma$, and hence $M$ thinks Ind(ZFC,Ind(ZFC,$\sigma$)) always fails.

share|cite|improve this answer
In (dual to algebraic) topological semantics of the corresponding logical calculi, the provability predicate becomes modeled by the Cantor-Bendixson derivative operator on subsets of some space, with iterates which may extend transfinitely. Moreover getting stronger and stronger theories with their own provability, with their own notions of provability is similarly modeled by Japaridze's polymodal logic GLP. Recently Beklemishev and Gabelaia constructed in "Topological completeness of the provability logic GLP" an interesting topological model for it. – მამუკა ჯიბლაძე Feb 25 '14 at 6:49

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.