Feasible operations on proofs: the logic of proofs for bounded arithmetic
type: Item
instance of: scholarly article
title: Feasible operations on proofs: the logic of proofs for bounded arithmetic
zbMATH Open document ID: 1144.03038
author: Evan Goris
published in: Theory of Computing Systems
publication date: 2008-06-17T00:00:00Z
review text: The logic of proofs (LP), introduced by \textit{S. Artemov} [Technical Report MSI 95-29, Cornell University (1995)], is a constructive variant of provability logic which has explicit proof terms instead of the provability operator. It has found applications in epistemic logics, where proof terms can be reinterpreted as terms providing explicit justification for knowledge of a formula. In this paper, the author adapts Artemov's arithmetical completeness proof for LP to show completeness with respect to arithmetical interpretations in Buss's bounded arithmetical theory \(S^1_2\). In particular, LP is complete with respect to semantics where proof terms represent feasible (polynomial-time computable) functions.
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F45
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03B42
zbMATH DE Number: 5288692
zbMATH Keywords: logic of proofs
zbMATH Keywords: bounded arithmetic
zbMATH Keywords: arithmetical completeness
MaRDI profile type: Publication
full work available at URL: s00224-007-9058-x
OpenAlex ID: W1991386049
cites work: Justified and Common Knowledge: Limited Conservativity
cites work: Explicit provability and constructive semantics
cites work: Logical Omniscience Via Proof Complexity
cites work: Introducing Justification into Epistemic Logic
cites work: On the provability logic of bounded arithmetic
cites work: Q3794177
cites work: Reasoning with Justifications
cites work: Q4856172
cites work: Existence and feasibility in arithmetic
cites work: Provability interpretations of modal logic
DOI: 10.1007/S00224-007-9058-X
description: scientific article; zbMATH DE number 5288692