On Logic of Formal Provability and Explicit Proofs

arXiv1405.2559MaRDI QIDQ6251440FDOQ6251440

Publication date: 11 May 2014

Abstract: In 1933, G"odel considered two modal approaches to describing provability. One captured formal provability and resulted in the logic GL and Solovay's Completeness Theorem. The other was based on the modal logic S4 and led to Artemov's Logic of Proofs LP. In this paper, we study introduced by the author logic GLA, which is a fusion of GL and LP in the union of their languages. GLA is supplied with a Kripke-style semantics and the corresponding completeness theorem. Soundness and completeness of GLA with respect to the arithmetical provability semantics is established.

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Modal logic (including the logic of norms) (03B45) Proof theory in general (including proof-theoretic semantics) (03F03) First-order arithmetic and fragments (03F30) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

This page was built for publication: On Logic of Formal Provability and Explicit Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6251440)