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. |