Abstract:
K. G. Niebergall suggested a simple example of a non-gödelean arithmetical
theory $\mathrm{NA}$, in which a natural formalization of its consistency
is derivable. In the present paper we consider the provability logic
of $\mathrm{NA}$ with respect to Peano arithmetic. We describe the class of its
finite Kripke frames and establish the corresponding completeness theorem.
For a conservative extension of this logic in the language with an additional
propositional constant, we obtain a finite axiomatization. We also consider
the truth provability logic of $\mathrm{NA}$ and the provability logic of
$\mathrm{NA}$ with respect to $\mathrm{NA}$ itself. We describe the classes of Kripke
models with respect to which these logics are complete. We establish
$\mathrm{PSpace}$-completeness of the derivability problem in these logics
and describe their variable free fragments. We also prove that
the provability logic of $\mathrm{NA}$ with respect to Peano arithmetic
does not have the Craig interpolation property.
Keywords:the logic of provability, Kripke semantics.