Logic of proofs and provability Original Research Article

In the paper the joint Logic of Proofs and Provability View the MathML source is presented that incorporates both the modality □ for provability (Israel J. Math. 25 (1976) 287–304) and the proof operator 〚t〛F representing the proof predicate “t is a proof of F” (Technical Report No. CFIS 95-29, Cornell University, 1995). The obtained system View the MathML source naturally includes both the modal logic of provability GL and Artemovʹs Logic of Proofs View the MathML source. The presence of the modality □ requires two new operations on proofs that together with operations of View the MathML source allow to realize all the invariant operations on proofs admitting description in the modal propositional language. Logic View the MathML source is proved to be decidable and complete with the intended provability semantics.