Independence results concerning P₀

In this paragraph the new principle will be compared to the previous principles from a modal viewpoint. Our modal semantics, Veltman models, does not provide a sufficiently strong tool for our analysis. As far as Veltman models are concerned P₀ implies M₀. But without modal completeness for $\mathit{ILP_0}$ we do not know whether the notion of semantical consequence coincides with the notion of derivable consequence. In other words we can say nothing about the derivability of M₀ in $\mathit{ILP_0}$ on these grounds. And there was no reason for conjecturing $\mathit{ILP_0}\vdash M_0$. On the contrary, the odds were against this inference. A nice comparison leads the intuition. $\mathit{ILM}$ is known to be modally complete with respect to its class of characteristic frames. Another principle sometimes called $\mathit{KM_1}$, see [Vis90], has the same frame condition, but is not equivalent to M over $\mathit{IL}$. Here $\mathit{KM_1}$ is the formula $A\rhd \Diamond B \rightarrow \Box (A \rightarrow \Diamond B)$. Indeed, below $\mathit{ILP_0}$ will be shown to be incomplete.

$\mathit{IL}$ is known to be sound w.r.t. Veltman semantics. That is, every derivable principle holds on all Veltman frames. Close inspection of the soundness proof shows the enormous amount of freedom one has in defining the semantics for $\mathit{IL}$. Various generalizations of Veltman semantics are known. (See e.g. [Sve91].) We will introduce here the notion of an $\mathit{IL_{set}}$-frame, an idea of Dick de Jongh for catching Svejdar's models in a general notion, as it was presented by Rineke Verbrugge in an unpublished document [Ver]. In the classical Veltman semantics there is the S relation. One can have xS_x0y. The yhere is another world in the model. The main idea in the $\mathit{IL_{set}}$semantics is to replace this y with a set of worlds. So, we could have $xS_{x_0}\{y\}$ for example. One can now define $x \Vdash A \rhd B \Leftrightarrow \forall y (xRy \rightarrow \exists Y( yS_xY \wedge \forall y' \in Y ( y' \vdash B )))$ and still have $\mathit{IL}$ sound w.r.t. the new semantics. As we work with an existential quantifier in the old definition we will exclude the empty set as a possible S-successor: the axiom $A \rhd B \rightarrow (\Diamond A \rightarrow \Diamond B)$ demands $S_x \subset x \uparrow \times (\wp (x \uparrow) \setminus \{ \varnothing \})$. Again the axiom $\Diamond A \rhd A$ demands that R can somehow be seen as embedded in S_x. In our case this reads $xRyRz \rightarrow yS_x\{z\}$. The axiom $\Box (A \rightarrow B) \rightarrow A \rhd B$ imposes a sort of reflexivity on our semantics; that is $yS_x\{y\}$. The transitivity clause leaves a lot of choice. The axiom states: $A\rhd B \wedge B \rhd C \rightarrow A\rhd C$. There is no first choice in how to adapt transitivity in the new semantics. It is sufficient to set $y_0S_xY\rightarrow \exists y'\in Y (\forall Y'(y'S_xY'\rightarrow y_0S_xY'))$. One could also replace the existential quantor by a universal quantor to obtain the definition of [Ver]. This will be our choice as well. Another possibility would be to demand $yS_xY \rightarrow \forall Z ( \forall z ( z \in Z \leftrightarrow \exists y' \in Y \exists Y'( yS_x Y' \wedge y' \in Y \wedge z \in Y')) \rightarrow yS_xZ)$. The axiom $A\rhd C \wedge B\rhd C \rightarrow A \vee B \rhd C$ did not impose anything on the old semantics and the axiom maintains this special status. Thus we have:

Definition 6.1   An $\mathit{IL_{set}}$-frame is a triple $( W,R,\{ S_w\mid w\in W\} )$satisfying the following properties.

• (W,R) is an L-frame, that is, W is a nonempty set and $R\subset W\times W$ is such that R is transitive, irreflexive and conversely well-founded.
• For each w in W we have
  • $S_w\subset w\uparrow \times (\wp (w\uparrow )\setminus \{ \varnothing \} )$
  • $wRx\rightarrow xS_w\{ x\}$
  • $wRxRy\rightarrow xS_w\{ y\}$
  • $y_0S_xY\rightarrow \forall y'\in Y\ \forall Y'(y'S_xY'\rightarrow y_0S_xY')$ (*)

Definition 6.2   An $\mathit{IL_{set}}$-model is a pair $(F,\Vdash)$ where F is an $\mathit{IL_{set}}$-frame and $\Vdash$ a forcing relation between worlds and proposition letters. The forcing relation is extended to sentences in the usual way when it comes to connectives or boxes. Furthermore the $\rhd$-operator is incorporated by $x\Vdash A\rhd B\Leftrightarrow \forall y(xRy \wedge y\Vdash A\rightarrow \exists Y(yS_xY\wedge \forall y'\in Y(y'\Vdash B)))$.

This new semantics yields strong enough a tool to allocate the principle P₀ in the landscape of other interpretability principles. It turns out that P₀ has the highest possible degree of independence with respect to the principles M₀ and W. This result is stated in the next theorem.

Theorem 6.3   The principles M₀, W and P₀ are maximally incomparable, that is to say it is not possible to derive one of the principles over $\mathit{IL}$using the remaining two as axiom schemes.

In order to have a complete comparison we note that $\mathit{ILM}\vdash P_0$and ${\mathit ILP}\vdash P_0$. P₀ holds on every $\mathit{ILM}$ respectively $\mathit{ILP_0}$ frame. This fact combined with the modal completeness results gives the derivability of P₀ over both $\mathit{ILM}$ and $\mathit{ILP}$. Of course the odds are for ${\mathit ILW^*P_0}$ to be an incomplete logic, but we have not been able to prove this due to the lack of a candidate for a valid but underivable principle.