S. N. Artemov, T. Yavorskaya, “On first order logic of proofs”, Mosc. Math. J., 2001, Volume 1, Number 4,Pages <nobr>475

This article is cited in 15 papers

On first order logic of proofs

S. N. Artemov^a, T. Yavorskaya^b

^a City University of New York, Graduate Center
^b M. V. Lomonosov Moscow State University, Faculty of Mechanics and Mathematics

Abstract: The Logic of Proofs LP solved long standing Gödel's problem concerning his provability calculus (cf. [1]). It also opened new lines of research in proof theory, modal logic, typed programming languages, knowledge representation, etc. The propositional logic of proofs is decidable and admits a complete axiomatization. In this paper we show that the first order logic of proofs is not recursively axiomatizable.

Key words and phrases: Logic of proofs, provability, recursive axiomatizability.

MSC: Primary 03F45; Secondary 03F30, 03F50

Received: July 7, 2001; in revised form January 9, 2002

Language: English

DOI: 10.17323/1609-4514-2001-1-4-475-490