zbMATH — the first resource for mathematics

Criteria for admissibility of rules of inference with parameters in the intuitionistic propositional calculus. (English. Russian original) Zbl 0743.03037
Math. USSR, Izv. 37, No. 3, 693-703 (1991); translation from Izv. Akad. Nauk SSSR, Ser. Mat. 54, No. 6, 1331-1341 (1990).
This is a refinement of the author’s solution of a problem raised by H. Friedman: admissibility of rules with parameters in the intuitionistic propositional calculus is decidable. The rule \(A(x;p)/B(x;p)\) with parameters \(p\), where \(x=x_ 1,\dots,x_ m\), \(p=p_ 1,\dots,p_ n\), is admissible if for any formulas \(F_ 1,\dots,F_ m=F\), derivability of \(A(F;p)\) implies derivability of \(B(F;p)\). If \(B\)=false, the rule is inadmissible exactly when the “logical equation” \(A(x;p)\) is solvable for \(x\). The proof uses reduction to finite intuitionistic Kripke models without detour via modal logic [the author, Algebra Logika 25, No. 2, 172-204 (1986; Zbl 0624.03007) and Ann. Pure Appl. Logic 50, No. 1, 71- 106 (1990; Zbl 0709.03009)].
Reviewer: G.Mints (Stanford)
03F50 Metamathematics of constructive systems
Full Text: DOI