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/97418h.htm
Last modified: January 27, 2000