A class of decidable intermediate propositional logics
Craig Graham McKay · Journal of Symbolic Logic · 1971
For the terminology and motivation of this note, my earlier paper [3] should be consulted. Here I make a slight change by requiring the Intuitionist Propositional Logic H to be given in terms of axiom schemata rather than axioms. Definition. An axiom schema F is essentially negative iff each schematic letter appearing in F is negated. Thus the schemata (¬P ∨ ¬¬P), (¬¬(¬P ∨ ¬Q)→(¬P ∨ ¬Q)) are essentially negative, whereas (¬P ∨ P) and (¬¬P→P) are not. Lemma. Let F be an essentially negative axiom schema. Then F yields at most finitely many intuitionistically nonequivalent axioms whose atoms are chosen from a fixed finite set.