The Basic Logic of Proofs. Strassen, T. Ph.D. Thesis, University of Bern, April, 1994.
Propositional Provability Logic was axiomatized by R.~M.~Solovay in~1976. This modal logic describes the behavior of the arithmetical operator $A$~is provable''. The aim of these investigations is to provide propositional axiomatizations of the predicates $p$~is a proof of~$A$'', $p$~is a proof which contains~$A$'' and $p$~is a program which computes~$A$'' using the same semantics. The presented systems, called the Basic Logic of Proofs, are first proved to be sound and complete with respect to arithmetical interpretations. Decidability is a consequence of a semantical cut elimination theorem. Moreover, appropriate syntactical models for the Basic Logic of Proofs are defined, which are closely related to canonical models. Finally, some general principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.
@PhdThesis{str94,
Author         = {Strassen, Tyko},
Title          = {The Basic Logic of Proofs},
School         = {University of Bern},
abstract       = {Propositional Provability Logic was axiomatized by
R.~M.~Solovay in~1976. This modal logic describes the
behavior of the arithmetical operator $A$~is
provable''. The aim of these investigations is to
provide propositional axiomatizations of the predicates
$p$~is a proof of~$A$'', $p$~is a proof which
contains~$A$'' and $p$~is a program which
computes~$A$'' using the same semantics. The presented
systems, called the Basic Logic of Proofs, are first
proved to be sound and complete with respect to
arithmetical interpretations. Decidability is a
consequence of a semantical cut elimination theorem.
Moreover, appropriate syntactical models for the Basic
Logic of Proofs are defined, which are closely related
to canonical models. Finally, some general principles
of the Basic Logic of Proofs, mainly concerning fixed
points, are investigated.},
month          = apr,
url            = {http://www.strassen.us/thesis.pdf},
year           = 1994
}