Closed fragments of provability logics of constructive theories. (English) Zbl 1165.03049

Visser, Albert

J. Symb. Log. 73, No. 3, 1081-1096 (2008).

H. Friedman stated in [J. Symb. Log. 40, 113–129 (1975; Zbl 0318.02002)] as 35th problem to give a decision procedure for the closed fragment of the provability logic of Peano Arithmetic. It was indepedently solved by J. van Benthem (in his doctoral thesis, 1974, Amsterdam), G. Boolos [J. Symb. Log. 41, 779–781 (1976; Zbl 0359.02050)], and C. Bernardi and F. Montagna (unpublished). The situation changes dramatically, when we go on to consider the provability logics of constructive theories. A. Visser gave characterizations and corresponding decision procedures for the closed fragments of Heyting arithmetic, first in 1985 [Log. Group Prep. Series 4, Utrecht]. But he was not happy with its presentation and the result was finally published in [Ann. Pure Appl. Logic 114, No. 1–3, 227–271 (2002; Zbl 1009.03029)]. In the paper under review, a new proof of the characterizations of the closed fragments of the provability logic of Heyting arithmetic is given. It is formalized in a Smoryński-style Kripke-model argument. Also given is a characterization of the closed fragment of the provability logic of Heyting arithmetic plus Markov’s principle and Heyting arithmetic plus primitive recursive Markov’s principle.

Reviewer: Mladen Vuković (Zagreb)

MSC:

03F45	Provability logics and related algebras (e.g., diagonalizable algebras)
03F30	First-order arithmetic and fragments
03F50	Metamathematics of constructive systems

Keywords:

provability logic; Heyting arithmetic; constructive arithmetic

Citations:

Zbl 0318.02002; Zbl 0359.02050; Zbl 1009.03029

References:

[1]	Embeddings of Heyting algebras pp 187–
[2]	One hundred and two problems in mathematical logic 40 pp 113– (1975)
[3]	The logic of provability (1993)
[4]	On deciding the truth of certain statements involving the notion of consistency 41 pp 779– (1976)
[5]	Predicate logics of constructive arithmetical theories 71 pp 1311– (2006) · Zbl 1116.03055
[6]	DOI: 10.1016/S0168-0072(01)00081-1 · Zbl 1009.03029 · doi:10.1016/S0168-0072(01)00081-1
[7]	Propositional combinations of {\(\Sigma\)}-sentences in Heyting’s Arithmetic (1994)
[8]	Evaluation, provably deductive equivalence in Heyting’s Arithmetic of substitution instances of propositional formulas (1985)
[9]	DOI: 10.1016/0003-4843(82)90024-9 · Zbl 0505.03026 · doi:10.1016/0003-4843(82)90024-9
[10]	Constructivism in mathematics, vol 1 121 (1988) · Zbl 0653.03040
[11]	Self-reference and modal logic (1985) · Zbl 0596.03001
[12]	Metamathematical investigations of intuitionistic arithmetic and analysis (1973)
[13]	Metamathematical investigations of intuitionistic arithmetic and analysis pp 324– (1973)
[14]	Categories for the working mathematician (1971) · Zbl 0232.18001
[15]	Logic: from foundations to applications (1996)
[16]	DOI: 10.1007/BF00370383 · Zbl 0742.03003 · doi:10.1007/BF00370383