zbMATH — the first resource for mathematics

Numerically correct provability logics. (English. Russian original) Zbl 0621.03038
Sov. Math., Dokl. 34, 384-387 (1987); translation from Dokl. Akad. Nauk SSSR 290, 1289-1292 (1986).
The paper shows that the usual definition of the predicate provability logic leads to numerically incorrect logics, that is, to logics that essentially depend on the choice of the recursively enumerable arithmetic formula that numerically expresses the fixed system of axioms of the given theory. The logics \(QL^ A\) are defined that desribe all the true (in standard model of arithmetic) provability laws in the recursively enumerable extension A of arithmetic. It is proved that \(QL^ A\) and \(QL^{A+ConsisA}\) are different for any consistent theory A. As shown in the author’s paper in Dokl. Akad. Nauk SSSR 284, 270-271 (1985; Zbl 0605.03007), none of the logics \(QL^ A\) (A true) is an arithmetic set.

03F30 First-order arithmetic and fragments
03F07 Structure of proofs
03B45 Modal logic (including the logic of norms)