Disjunction and existence under implication in elementary intuitionistic formalisms
S. C. Kleene · Journal of Symbolic Logic · 1962
Let Pp, Pd, and N be the intuitionistic formal systems of prepositional calculus, predicate calculus, and elementary number theory, respectively.1 Consider the following six propositions.8 (1) ├A V B only if ├A or ├B. (2) ├∋xA(x) only if ├Ã(t) for some formula Ã(x) congruent to A(x) and some term t free for x in Ã(x).