On Logic of Formal Provability and Explicit Proofs

TL;DR

This paper introduces the logic GLA, combining provability and explicit proof modalities, with a Kripke semantics and completeness results, bridging G"odel's provability logic and Artemov's Logic of Proofs.

Contribution

The paper presents GLA, a novel fusion of GL and LP logics, along with a Kripke semantics and a completeness theorem, extending the understanding of formal provability and explicit proofs.

Findings

GLA is sound and complete with respect to arithmetical provability semantics.

The logic GLA successfully combines features of GL and LP.

Kripke-style semantics for GLA is established.

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.