Logics and Provability
Katsumi Sasaki

Abstract:
Logics and provability
Katsumi Sasaki


In this thesis, we treat three kinds of propositional logics.  The
first kind connects with a non-modal propositional logic, called
formal propositional logic (FPL), another is an intuitionistic modal
logic, and the third kind consists of interpretability logics.  These
logics are related to or connected with the provability logic GL, the
normal modal logic obtained from the smallest normal modal logic K by
adding Lob's axiom $\Box (\Box p \supset p) \supset \Box p$.  The
name ``provability logic'' derives from Solovay's completeness
theorem.  He proved that GL is complete for the formal provability
interpretation in Peano arithmetic PA.  So, GL has been considered as
one of the most important modal logics.

FPL as well as interpretability logics also have a formal provability
interpretation.  FPL is the propositional logic embedded into GL by
Godel's translation $\tau$.  Interpretability logics are modal logics
with a binary modal operator $\rhd$ including GL.  We treat these two
kinds of logics with this motivation in mind.

The normal modal logic K4 is a sublogic of GL, which is obtained from
K by adding the transitivity axiom $\Box p \supset \Box \Box p$.  As
is expected by the additional axioms of K4 and GL, the transitivity
axiom and Lob's axiom, K4 is much easier to deal with than GL.  So, as
was stated by C. Smorynski, knowledge of K4 is useful for the
discussion of GL.  Here we also treat Visser's propositional logic
(VPL), the propositional logic embedded into K4 by $\tau$, before
treating FPL, and the sublogic of the smallest interpretability logic
IL whose $\rhd$-free fragment is K4, before IL.  We consider the
consequence relation of VPL and a property of Lob's axiom on VPL.  To
give cut-free sequent systems is one of the issues here.  We first
give such systems for VPL and the sublogic of IL, and then, using a
property of Lob's axiom, for FPL and IL.

The remaining one among the logics treated here is the intuitionistic
modal logic called propositional lax logic (PLL) by M. Fairtlough and
M. Mendler.  PLL is not a logic for provability.  However, PLL has
other interesting interpretations.  For example, it corresponds to the
computational typed lambda calculus introduced by E. Moggi by the
Curry-Howard isomorphism.  Here we discuss Diego's theorem in PLL, and
elucidate the structure of sets of disjunction free formulas with only
finitely many propositional variables.