 Heyting pointed out that these explanations for disjunction and negation, taken together, are an immediate argument against the acceptability of PEM, for which a general method would be needed that, applied to any given proposition \(p\), produces either a proof of \(p\) or a proof of \(\neg p\). What Heyting did not do here was to generalize this explanation of negation to one for implication. Also, note that the procedure does not operate on proofs of \(p\), but starts from merely the assumption that \(p\), which in general gives less information. Both points were taken care of shortly afterward. In a letter to Freudenthal dated October 25, 1930, shortly after the Königsberg lecture, Heyting wrote: