I'm reading Kunen's "Set Theory" (Revised edition 2013).

On page 108 he defines for axiomatic set theories $\Lambda, \Gamma$ which are strong enough to formalize finitistic arguments (e.g. ZFC, Z, BST...)

$$\Gamma \triangleleft \Lambda \quad\text{ :iff }\quad \Lambda \vdash Con(\Gamma) $$


$$\Gamma \leq \Lambda \quad\text{ :iff }\quad \text{we have a finitistic proof that } Con(\Lambda) \rightarrow Con(\Gamma)$$

Then he states

Lemma II.1.3

  1. $\Gamma \triangleleft \Lambda \rightarrow \Gamma \leq \Lambda$
  2. $\Gamma \leq \Lambda \ \wedge\ \Lambda \triangleleft \Theta \rightarrow \Gamma \triangleleft \Theta$
  3. /4. ...

Proof. For (1): Assuming $\Lambda \vdash Con(\Gamma)$, we may argue finitistically that if we had a formal proof of contradiction from $\Gamma$, then $\Lambda \vdash \neg Con(\Gamma)$, which would give us a contradiction in $\Lambda$. So, $Con(\Lambda) \rightarrow Con(\Gamma)$.
For (2): Assuming $\Gamma \leq \Lambda \ \wedge\ \Lambda \triangleleft \Theta$, then working in $\Theta$, we can prove $Con(\Lambda)$ and $Con(\Lambda) \rightarrow Con(\Gamma)$, and hence $Con(\Gamma)$.

At the beginning of this chapter Kunen says:

The definitions and lemmas in this section are informal, and are intended to give an overview of the types of consistency results you will find in this book and in other works on set theory. The reader who is familiar with proof theory will see how to make them precise and formal. These remarks take place in the metatheory, using just finitistic reasoning.

My question: What is a precise formulation of 1. and 2.?

I see two possibilities.

Let $\vdash_{fin}$ denote the syntactic consequence relation of a finitistic system like PRA (Primitive Recursive Arithmetic). We write $\ulcorner \varphi \urcorner$ for the statement $\varphi$ encoded into PRA and let $\square \varphi$ be an abbreviation for $\ulcorner \vdash_{fin} \varphi \urcorner$.

Option a):

  1. $\vdash_{fin} \ulcorner\Lambda \vdash \neg Incon(\Gamma) \urcorner \rightarrow \square( Incon(\Gamma) \rightarrow Incon(\Lambda) )$
  2. $\vdash_{fin} \square( Incon(\Gamma) \rightarrow Incon(\Lambda) ) \ \wedge\ \ulcorner\Theta \vdash \neg Incon(\Lambda) \urcorner \rightarrow \ulcorner\Theta \vdash \neg Incon(\Gamma) \urcorner$

Option b):

  1. $\vdash_{fin} \ulcorner\Lambda \vdash \neg Incon(\Gamma) \urcorner \rightarrow ( Incon(\Gamma) \rightarrow Incon(\Lambda) )$
  2. $\vdash_{fin} ( Incon(\Gamma) \rightarrow Incon(\Lambda) ) \ \wedge\ \ulcorner\Theta \vdash \neg Incon(\Lambda) \urcorner \rightarrow \ulcorner\Theta \vdash \neg Incon(\Gamma) \urcorner$

In case of option a) I have a problem in proving 1, in b) in proving 2.

I use: Since we can assume that $Incon(\Gamma)$ is $\Sigma_1$, we have $\vdash_{fin} Incon(\Gamma) \rightarrow \square Incon(\Gamma)$. But for $Incon(\Gamma) \rightarrow Incon(\Lambda)$ this doesn't work.

Can anyone prove option a) or b)? Or am I completely missing the point here?


1 Answer 1


Let's look at $(1)$. The right way to interpret "$\Gamma\triangleleft\Lambda\implies\Gamma\le\Lambda$" is as $$(\Lambda\vdash Con(\Gamma))\implies [PRA\vdash (Con(\Lambda)\implies Con(\Gamma))].$$ This is just a direct translation of $(1)$: "If $\Lambda$ proves the consistency of $\Gamma$, then there is a finitistic proof that the consistency of $\Lambda$ implies the consistency of $\Gamma$."

Your versions have extraneous external $\vdash_{fin}$s; e.g. your version of $(1)$ says "$(1)$ is finitistically provable." Of course, this is a priori stronger than just saying that $(1)$ is true.

Now what about the proof?

Proving this formalization of $(1)$ is not trivial: we need to use $\Sigma_1$-completeness in a slightly clever way. Suppose $\Lambda\vdash Con(\Gamma)$. By $\Sigma_1$-completeness, $PRA$ proves "$\Lambda\vdash Con(\Gamma)$" (ignoring Godel-numbering issues). Now since $\Lambda$ is sufficiently strong, $\Lambda$ itself is $\Sigma_1$ complete, and this means that $Incon(\Gamma)\implies \Lambda\vdash Incon(\Gamma)$ is true.

Moreover, $PRA$ proves that $\Lambda$ is $\Sigma_1$ complete! This is the crucial trick. Put another way, we have $PRA\vdash Incon(\Gamma)\implies \Lambda\vdash Incon(\Gamma)$. To prove this, you have to go back to the proof that $\Lambda$ is $\Sigma_1$ complete and check carefully that it goes through in $PRA$. This is straightforward but tedious, so I'll leave it as an exercise to the reader. :P (Note that this whole mess is subsumed by Kunen's statement "we may argue finitistically.")

So we have that $PRA$ proves both of the following statements:

  • $\Lambda\vdash Con(\Gamma)$.

  • $Incon(\Gamma)\implies \Lambda\vdash Incon(\Gamma)$.

Putting these together, we get $$PRA\vdash Incon(\Gamma)\implies \Lambda\vdash Con(\Gamma)\wedge Incon(\Gamma),$$ and in particular $$PRA\vdash Incon(\Gamma)\implies Incon(\Lambda).$$ And this finishes the proof. $\quad\Box$.

Formalizing and proving $(2)$ is similar.

Incidentally, the same argument as above can also be used to prove the stronger statements you write down.

  • $\begingroup$ Thanks! Isn't proving (2) trivial with your interpretation (or my option a)), since $\Lambda$ is strong enough to formalize finitistic arguments? The reason for my external $\vdash_{fin}$ was Kunen's comment: "These remarks take place in the metatheory, using just finitistic reasoning." $\endgroup$ Apr 2, 2018 at 14:18
  • $\begingroup$ @PopovFlorino Well, it depends what you mean by "trivial." :P What you need to do is show that $\Theta$ knows that $\Lambda$ would see any inconsistency in $\Gamma$, and hence (since $\Lambda$ proves that $\Gamma$ is consistent) would be inconsistent if $\Gamma$ were inconsistent. So again, you're not just using the strength of $\Lambda$, but also the more subtle strength of $\Theta$; namely, that $\Theta$ can prove that $\Lambda$ is $\Sigma_1$ complete. $\endgroup$ Apr 2, 2018 at 14:33
  • $\begingroup$ This subtlety - that we need provable $\Sigma_1$ completeness instead of just $\Sigma_1$ completeness - also crops up in this question which you might find interesting (see the statement $(*)$ in my answer). (Incidentally, in that question there is a separate subtlety which crops up, but which turns out to be unnecessary - see the followup question here.) $\endgroup$ Apr 2, 2018 at 14:34
  • $\begingroup$ I thought "$\Theta$ is strong enough to formalize finitistic arguments" means (ignoring Godel-numbering issues), that $(\vdash_{fin} \varphi) \Rightarrow (\Theta \vdash \varphi)$. (I meant "$\Theta$ is strong enough ..." in my first comment). With this we can argue: If $\vdash_{fin} Incon(\Gamma) \rightarrow Incon(\Lambda)$ and $\Theta \vdash \neg Incon(\Lambda)$, then $\Theta \vdash \neg Incon(\Lambda) \wedge Incon(\Gamma) \rightarrow Incon(\Lambda)$, i.e. $\Theta \vdash \neg Incon(\Gamma)$. What is wrong with this proof for (2)? $\endgroup$ Apr 2, 2018 at 17:54
  • $\begingroup$ @PopovFlorino That does work. I may have worked a bit too hard in my answer, I'll look at it when I have more time. $\endgroup$ Apr 2, 2018 at 19:11

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .