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{MLP}$ naturally includes both Solovay's provability logic GL and Artemov's operational modal logic $\mathcal{LP}$. All finite extensions of the basic system $\mathcal{MLP}_{0}$ are proved to be decidable and arithmetically complete. It is shown that $\mathcal{LP}$ realizes all operations over proofs admitting description in the modal propositional language.

All articles are published in Russian.

Main page Contents of the journal News Search

Location: http://mech.math.msu.su/~fpm/eng/97/974/97418t.htm
Last modified: January 27, 2000