Proof of the independence of the primitive symbols of Heyting's calculus of propositions
J. C. C. McKinsey · Journal of Symbolic Logic · 1939
In this paper I shall show that no one of the four primitive symbols of Heyting's calculus of propositions is definable in terms of the other three. So as to make the paper self-contained, I begin by stating the rules and primitive sentences given by Heyting. The primitive symbols of the calculus are “⅂”, “∨”, “∧”, and “⊃”, which may be read, respectively, as “not,” “either…or,” “and,” and “if…then.” The symbol “⊃⊂”, which may be read “if and only if,” is defined in terms of these as follows: The rule of substitution is assumed, and the rule that S2 follows from S1 and S1⊃S2; in addition it is assumed that S1∧S2 follows from S1 and S2. The primitive sentences are as follows: