  The third major development came when Specker (in [1958] and [1962]) placed the narrative in Quine [1937a] recounted above on a firm mathematical footing. (For an illustrated translation, with commentary, of Specker [1958], see Forster [2000], in the Other Internet Resources section below.) We’ve seen that \(\Phi^+\) is the result of raising all the type subscripts on all variables in \(\Phi\) by one. Then \(\Phi \leftrightarrow \Phi^+\) is an axiom of typical ambiguity. Specker established that the consistency of NF is equivalent to the consistency of TST + the scheme of all axioms of typical ambiguity. This reduction of the consistency question of NF to the consistency of TST + the axiom scheme of typical ambiguity clarifies matters but doesn’t actually solve anything, since the axioms of typical ambiguity turn out to be quite strong – as are their analogues in other languages (such as geometry) that admit endomorphisms. Notice that the mere fact that if \(\phi\) is provable then so is \(\phi^+\) is not enough to ensure that \(\phi \rightarrow \phi^+\) is provable, so the axioms of typical ambiguity are prima facie nontrivial and we should not be surprised that they turn out to be strong.