next up previous contents
Next: Concluding Up: A new principle Previous: A relation between M

   
The arithmetical validity of P0

The new principle P0 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 T0 of T which is sufficiently strong. We will not be too precise about this. The actual constraints on T0 can be distilled from the following argument. It seems natural to demand that T0 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 T0 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 T0.

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


next up previous contents
Next: Concluding Up: A new principle Previous: A relation between M
Joost Joosten
2000-02-07