The arithmetical validity of P₀

The new principle P₀ is next seen to be arithmetically valid. The argument is due to Albert Visser and can be presented in five basic steps. We will use here standard notation and well-known facts of arithmetization. For a good background one can consult very clear texts like for example [Vis90], [JdJ98]. In the sequel of this paragraph $\Box$ and $\rhd$ will stand again for formalized provability and interpretability respectively. These notions are dependent on the base theory in which they are formalized. In case of possible confusion we will write this base theory by indexing the operator, e.g. $\Box_T$. We have to prove that in any reasonable arithmetical theory $A\rhd \Diamond B\rightarrow \Box (A\rhd B)$ is derivable.

For any reasonable arithmetical theory T:

1.

 Suppose $A\rhd \Diamond B$ and reason within the theory. We thus have $(T+A)\rhd (T+\Diamond B)$.

2.

 We can now take a finite subtheory T₀ of T which is sufficiently strong. We will not be too precise about this. The actual constraints on T₀ can be distilled from the following argument. It seems natural to demand that T₀ can code the Henkin construction used in the completeness theorem. By this one can obtain a stronger variant of J5 as is outlined later on. We have $(T+A)\rhd (T_0+\Diamond B)$, which turns out to be a $\Sigma^0_1$-sentence as T₀ is a finite theory. The $\Pi^0_2$-sentence (modulo notational inaccuracies) $\forall y({\mathit Ax_{T_0}}(y)\rightarrow \Box_T(A\rightarrow y^J))$ can be replaced by the $\Sigma^0_1$-sentence $\Box_T(A\rightarrow \tau^J)$, where J is the interpretation used in 1 an $\tau$ is the conjunction of all the axioms of T₀.

3.

 We can thus conclude $\Box_T((T+A)\rhd (T_0+\Diamond B))$. This follows from 2 and the provable $\Sigma^0_1$-completeness of T.

4.

  The axiom $J5 : \Diamond B\rhd B$ reflects the completeness theorem. As the whole Henkin construction can be coded within T, in T one can prove
$(T+{\mathit Con}(T+B))\rhd(T+B)$. But actually something stronger holds as well. The finite theory T₀ is chosen strong enough to perform the Henkin construction for T. So within T one can prove
$(T_0+{\mathit Con}(T+B))\rhd(T+B)$. With necessitation one obtains $\Box_T(T_0+{\mathit Con}(T+B)\rhd(T+B))$.

5.

 The final step consists of combining 3 and 4. The transitivity of $\rhd$ under the $\Box$ yields the desired result, that is $\Box (A\rhd B)$.