01162nas a2200109 4500008004100000245003000041210003000071260002300101520087100124100001900995856003801014 1994 eng d00aThe basic logic of proofs0 aThe basic logic of proofs bUniversity of Bern3 aPropositional 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.1 aStrassen, Tyko uhttp://www.strassen.us/thesis.pdf