Аннотация:Propositional Provability Logic was axiomatized by Solovay in 1976. This logic describes the behaviour of the arithmetical operator “y is provable”. The aim of the current paper is to provide propositional axiomatizations of the predicate “x is a proof of y” by means of modal logic, with the intention of meeting some of the needs of computer science.