 Heyting’s formalization comprised intuitionistic propositional and predicate logic, arithmetic, and analysis, all together in one big system (with only variables for arbitrary objects). The part concerned with analysis was, not only in its intended interpretation (involving choice sequences) but also formally, no subsystem of its classical counterpart; this explains why it sparked no general interest at the time. (A consequence we noted above is that Brouwer’s strong counterexamples never affected the debate.) Therefore this part of Heyting’s formalization was left out of consideration by the other participants in the Foundational  Debate.[25]  This was different for the parts concerned with logic and arithmetic. Formally speaking and disregarding their intended interpretations, from these one could distill subsystems of their classical counterparts, from which only PEM (or double negation elimination) is missing. No doubt this encouraged many to accord to these systems a definitive character, which, as Heyting had remarked at the beginning of his paper, on the intuitionistic conception of logic they cannot have: