zbMATH — the first resource for mathematics

Admissible and derivable rules in intuitionistic logic. (English) Zbl 0797.03001
The paper considers admissible and derivable inference rules in intuitionistic propositional logic. A finite set \(\Gamma\) of formulas is said to have the same admissible and derivable consequences if, for every formula \(C\), intuitionistic logic is closed under the rule \(\Gamma/C\) iff \(\Gamma\lvdash C\). \(\Gamma\) has the disjunction property for admissibility of admissibility of the rule \(\Gamma/C\lor D\) implies \(\Gamma\lvdash C\) or \(\Gamma\lvdash D\). It is proved that Harrop formulas and anti-Harrop formulas (which are equivalent to conjunctions of formulas \(p\to A\), where \(p\) is a propositional variable) have the same admissible and derivable consequences and the disjunction property for admissibility.

03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI
[1] Troelsta, Studies in Logic and the Foundations of Mathematics 121 (1988)
[2] Rybakov, Izv. Akad. Nauf. SSSR, ser. Mat 50 (1986)
[3] DOI: 10.1007/BF01978706 · Zbl 0598.03014 · doi:10.1007/BF01978706
[4] DOI: 10.2307/2271891 · Zbl 0318.02002 · doi:10.2307/2271891
[5] Rozière, Règies admissibles en calcul propositionnel intuitionniste (1991)
[6] Mints, Zap. Nauchn. Sem. Leningrad. Otdel. Mat. Inst. Steklov. (LOMI) 32 pp 85– (1972)
[7] DOI: 10.1007/BF01982031 · Zbl 0598.03013 · doi:10.1007/BF01982031
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.