 In 1960a Schütte developed a semantic equivalent to the (syntactic) fundamental conjecture using partial or semi-valuations. He employed the method of search trees (or deduction chains) to show that a formula F that cannot be deduced in the cut-free system has a deduction chain without axioms which then gives rise to a partial valuation V assigning the value “false” to F. From the latter he inferred that the completeness of the cut-free  system[20]  is equivalent to the semantic property that every partial valuation can be extended to a total valuation (basically a Henkin model of STT). In 1966 Tait succeeded in proving cut-elimination for second order logic using Schütte’s semantic equivalent for that fragment. Soon afterwards, Takahashi (1967) and Prawitz (1968) independently proved for full classical simple type that every partial valuation extends to a total one, thereby establishing Takeuti’s fundamental conjecture. These results, though, were somewhat disappointing as they were obtained by highly non-constructive methods that provided no concrete method for eliminating cuts in a derivation. However, Girard showed in 1971 that simple type theory not only allows cut-elimination but that there is also a terminating normalization  procedure.[21]  These are clearly very interesting results, but as far as instilling trust in the consistency of \(\bZ_2\) or SST is concerned, the cut elimination or termination proofs are just circular since they blatantly use the very comprehension principles formalized in these theories (and a bit more). To quote Takeuti: 