The logic of proofs, semantically (Q703832): Difference between revisions

Artemov introduced the logic of proofs, called LP, and established its arithmetical provability completeness as well as the realization of modal logic S4 in LP, which answers a long-standing question about the provability semantics for S4, posed by Gödel, and hence for intuitionistic propositional logic. The logic LP is featured by its language extending the standard propositional one with proof polynomial terms, which are built up from constants and variables by three fundmantal functions, ``application'', ``proof checker'', and ``sum'', and then operate on formulas resulting in those of the form \(t:F\), to be read as ``\(t\) is a proof of \(F\)'', where \(t\) is a proof polynomial term and \(F\) is a formula. In this paper the author presents a new semantics for LP based on the intuition that it is a logic of explicit knowledge; the formula \(t:F\) is here intended to mean ``I know \(F\) for reason \(t\)'', so that a proof may be considered as a kind of explicit knowledge. The semantics is established by supplying S4 Kripke frames with suitably designed machinery to cover the role of proof polynomials, and is used to give new proofs of several basic results concerning LP, among which, in particular, the author examines the realizability of S4 in LP in detail and explicates the role of ``sum'' on proof polynomials. It is also shown that a parallel argument can be developed for the fragment of LP without ``sum''. The semantics thus provided is, from a general view point, quite flexible not only in itself but also in considering several variations. The author suggests the application to LP-type logics obtained by replacing the S4 modal characteristics of LP with those of other fundamental modal logics such as K, T, and K4.