zbMATH — the first resource for mathematics

Rules of inference with parameters for intuitionistic logic. (English) Zbl 0788.03007
Let \(A(x_ 1,\dots,x_ n,p_ 1,\dots,p_ m)\) and \(B(x_ 1,\dots,x_ n,p_ 1, \dots,p_ m)\) be formulas of the intuitionistic propositional calculus in variables \(x_ i\), \(p_ j\). The rule \(A/B\) with parameters \(p_ j\) is admissible, if for all \(n\)-tuples of formulas \(B_ 1,\dots,B_ n\) derivability of \(A(B_ 1,\dots,B_ n,p_ 1,\dots,p_ m)\) implies derivability of \(B(B_ 1,\dots,B_ n,p_ 1,\dots,p_ m)\). An algorithm for deciding admissibility with parameters is given here by testing the rule on certain finite sets of finite Kripke models. In particular this decides existence of formulas \(B_ 1,\dots,B_ n\) such that \(A(B_ 1,\dots,B_ n,p_ 1,\dots,p_ n)\) is derivable: this is equivalent to the nonadmissibility of the rule \(A/\)false.
Reviewer: G.Mints (Stanford)

03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI
[1] Doklady Akademii Nauk SSSR 287 pp 554– (1986)
[2] Izvestiya Akademii Nauk SSSR Seriya Matematicheskaya 50 pp 598– (1986)
[3] Algebra i Logika 23 pp 546– (1984)
[4] Zapiski Nauchnykh Seminarov L0M1 32 pp 85– (1972)
[5] Matematicheskie Zametki 37 pp 797– (1985)
[6] One hundred and two problems in mathematical logic 40 pp 113– (1975)
[7] Vollst√§ndige Systeme modaler und intuitionistischer Logik 42 (1968) · Zbl 0157.01602
[8] Doklady Akademii Nauk SSSR 241 pp 1288– (1978)
[9] Matematicheskiń≠ Sbornik 102 pp 314– (1977)
[10] Logical notebook: unsolved questions of mathematical logic (1986)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.