Next: More principles and frame
Up: The modal logic of
Previous: The modal logic of
The language of the modal interpretability logic is the language of
provability logic extended with a binary modality
.
So we have
at our disposal an enumerable supply of propositional variables, a
unary modality
and a binary modality
.
We can either use
all the Boolean connectives or just constrain ourselves to
and
.
We adhere to some reading conventions as to omit
parentheses without introducing ambiguities. The negation, the diamond
and the box bind stronger than
and
,
which in turn bind
stronger then
and
.
Finally we say that
binds stronger than
.
So
,
for example, is short for
.
Definition 3.1
The basic interpretability logic
![$\mathit{IL}$](img19.gif)
has the following axiom
schemes:
The rules of inference are modus ponens and necessitation, that is, if
one has
![$\vdash A\rightarrow B$](img80.gif)
and
![$\vdash A$](img81.gif)
,
then also
![$ \ \vdash B$](img82.gif)
,
resp.
![$\vdash A\Rightarrow \ \vdash \Box A$](img83.gif)
.
Just as with provability logic, a Kripke-like semantics is given for
.
By S we mean
.
The elements of W will
also be called worlds or nodes.
Definition 3.3
An
![$\mathit{IL}$](img19.gif)
-model is an
![$\mathit{IL}$](img19.gif)
-frame together with a forcing relation
![$\Vdash$](img89.gif)
between worlds and propositional letters.
![$\Vdash$](img89.gif)
is
extended to formulas by defining
![$\Vdash$](img89.gif)
to commute with the Boolean
connectives and defining
- -
-
,
- -
-
.
One could also first define
and later determine the
conditions on the binary relations Sw. In this manner one notices
some frame correspondences. We see that J4 imposes 2, J1corresponds with 4, J2 corresponds with 5 and
J5 corresponds with 3. The axiom J3 has a special status
as it does not impose anything on the frames.
Definition 3.4
-
and
are equivalent expressions.
-
means that for all w in M,
.
-
If F is a Veltman-frame,
means that for any
,
.
-
We say that A holds as a scheme on a frame F if all instantiations
of A hold at F.
-
Let
be a class of Veltman-frames. We define
iff
.
As every axiom of
is valid on every Veltman-frame, and this
validity is preserved under the rules of inference, we see that
is sound w.r.t. Veltman-frames. That is, all
-derivable formulas
hold on all Veltman-frames. The logic is modally complete as well. See
[JV91]. So if a formula holds on all
-frames, it must
be derivable in
.
This completeness result is also presented for
example in [JdJ98].
Throughout this paper we will use some very basic results of
.
Most of them are very easy to verify. In the next lemma we
expose some facts of
.
These facts are indeed easy to verify as is partly done in
[JdJ98]. Formal proofs in
are quite laborious
to write down. A Gentzen proof system is most likely hard to find.
Next: More principles and frame
Up: The modal logic of
Previous: The modal logic of
Joost Joosten
2000-02-07