The Basic Logic of Proofs. Strassen, T. Ph.D. Thesis, University of Bern, April, 1994.
The Basic Logic of Proofs [pdf]Paper  abstract   bibtex   
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
}
Downloads: 0