Generalization of a lemma of G. F. Rose
I. L. Gál, J. Barkley Rosser, D. Scott · Journal of Symbolic Logic · 1958
In attempting to reconstruct Rose's proof of Lemma 3.2 of [1], the present authors found what is apparently a different and simpler method, which moreover leads to a far stronger conclusion. We are operating in the Heyting prepositional calculus as formulated on p. 3 of [1] or on pp. 82 and 101 of [2], and shall make use of relevant theorems on pp. 90, 113–119 of [2]. We shall use a, b, c, w, x, y, z as propositional variables. We say that a conjunction is simple if each factor has one of the forms: (i) a, (ii) ¬a, (iii) a⊃b, (iv) a⊃(b∨c), (v) (a&b)⊃c, (vi) (a⊃b)⊃c.