FUNDAMENTALNAYA I PRIKLADNAYA MATEMATIKA

(FUNDAMENTAL AND APPLIED MATHEMATICS)

1997, VOLUME 3, NUMBER 4, PAGES 1173-1197

## Provability logic with operations over proofs

T. L. Sidon

Abstract

View as HTML     View as gif image    View as LaTeX source

We present a natural axiomatization for propositional logic with modal operator for formal provability (Solovay, [5]) and labeled modalities for individual proofs with operations over them (Artemov, [2]). For this purpose the language is extended by two new operations. The obtained system $\mathcal\left\{MLP\right\}$ naturally includes both Solovay's provability logic GL and Artemov's operational modal logic $\mathcal\left\{LP\right\}$. All finite extensions of the basic system $\mathcal\left\{MLP\right\}_\left\{0\right\}$ are proved to be decidable and arithmetically complete. It is shown that $\mathcal\left\{LP\right\}$ realizes all operations over proofs admitting description in the modal propositional language.

All articles are published in Russian.

Location: http://mech.math.msu.su/~fpm/eng/97/974/97418h.htm