Kolmogorov and Gödel’s approach to intuitionistic logic, and investigations in this direction in the last decade. (English. Russian original) Zbl 1074.03029

Russ. Math. Surv. 59, No. 2, 203-229 (2004); translation from Usp. Mat. Nauk 59, No. 2, 9-36 (2004).
This is a survey of work (mainly, but not only) by the author and his students on the properties and extensions of the propositional system LP (logic of proofs) introduced by the author. The idea is to get a more manageable system than a standard modal logic GL of provability by using an explicit proof construction \(t:F\) (\(t\) is a proof of \(F\)) instead of \(\square F\) interpreted as “\(F\) is provable”. The intended interpretation of \(t:F\) is “\(t\) is a derivation and \(F\) is one of the formulas in this derivation”, but an arithmetical completeness theorem holds for some combination of this standard predicate with a proof search construction for the logic LP itself. The system complete for the standard predicate is obtained by adding to LP a schema \(\neg (t_1:A_1(t_2)\wedge t_2:A_2(t_3)\wedge\dots\wedge t_n:A_n(t_1))\), where \(t_i\) occurs in \(A(t_i)\). Among the results not mentioned in the author’s previous survey [Bull. Symb. Log. 7, No. 1, 1–36 (2001; Zbl 0980.03059)] are Kripke models for LP (M. Fitting), an upper bound \(\Sigma^p_2\) for the complexity of LP and NP bound for the modalized fragment, and interpolation theorem (in a slightly weakened form). Quantified extensions of LP are non-axiomatizable.


03F55 Intuitionistic mathematics
03B20 Subsystems of classical logic (including intuitionistic logic)
03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations


Zbl 0980.03059
Full Text: DOI