佐々木克巳(南山大, 非古典論理), Provability and interpretability logics
------------------------------------------------------------
Provability logic GL is one of the normal modal logics, which is obtained
from the
smallest normal modal logic K by adding L\"ob's axiom. The name ``provability
logic''
derives from Solovay's 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.
Interpretability logics were introduced by Albert Visser in 1990 as
extensions of
the provability logic GL with a binary modality \rhd. The arithmetic realization
of
A \rhd B in a theory T will be that T plus the realization of B is interpretable
in T
plus the realization of A (T+A interprets T+B). More precisely, there exists
a function
f(the relative interpretation) on the formulas of the language of T such
that T+B \vdash C
implies T+A \vdash f(C).
Here, we describe some results on these logics in a recent few years.
--------------------------------------------------------------