Precise definition of relative consistency in Kunen's "Set Theory"

Question

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) $$

and

$$\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?

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.