Criteria for admissibility of rules of inference with parameters in the intuitionistic propositional calculus. (English. Russian original) Zbl 0743.03037

Rybakov, V. V.

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)

MSC:

03F50

Metamathematics of constructive systems

Keywords:

admissibility of rules; intuitionistic propositional calculus; Kripke models