The logic of proofs, semantically
type: Item
instance of: scholarly article
title: The logic of proofs, semantically
zbMATH Open document ID: 1066.03059
author: Melvin Fitting
published in: Annals of Pure and Applied Logic
publication date: 2005-01-11T00:00:00Z
review text: 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.
reviewed by: Osamu Sonobe
Mathematics Subject Classification ID: 03F45
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03B42
zbMATH DE Number: 2126475
zbMATH Keywords: logic of proofs
zbMATH Keywords: explicit knowledge
zbMATH Keywords: arithmetical provability interpretation
zbMATH Keywords: modal logic S4
zbMATH Keywords: proof polynomial
zbMATH Keywords: Kripke-type semantics
zbMATH Keywords: intuitionistic logic
MaRDI profile type: Publication
full work available at URL: j.apal.2004.04.009
OpenAlex ID: W2045237008
cites work: Explicit provability and constructive semantics
cites work: Q2753686
cites work: Q4376067
cites work: Q5560258
DOI: 10.1016/J.APAL.2004.04.009
description: scientific article; zbMATH DE number 2126475