The real elements in a consistency proof for simple type theory I

  • Horst Luckhardt
Conference paper
Part of the Lecture Notes in Mathematics book series (LNM, volume 500)


This is the first of two papers on the questions: What does consistency of simple type theory mean, and how can it be achieved by interpretation, the strongest constructive method today. Concerning the first question the following results are proved.
  1. (1)

    Simple type theory can be reduced to arithmetic over the primitive recursive functionals plus the quantifierfree rule of extensionality plus one comprehension over a special Λ-property on objects of type ≠ O.

  2. (2)

    Consistency is fully describable by the notion “continuity indicator”, a generalization of the modulus of continuity with respect to types and extensionality. Especially:

  3. (3)

    A necessary condition for consistency is that the theory T of the primitive recursive functionals contains no continuity indicator for type O(Oα) at definable points.

    The μ-operator based on continuity gives no proof-theoretic strengthening; it rather leads to the negations of the above mentioned comprehension instances and to continuity indicators. Therefore a consistency proof has to make very fine distinctions.

  4. (4)

    ω-rules for types greater than zero cannot be added consistently to theories of classical and intuitionistic analysis of a certain strength. Moreover Markov's principle (MP) and Kreisel-Troelstra's Λα⌝⌝Va·α=a imply intuitionistically that the existence of a non-recursive constructive function is not absurd. From this it follows that ω-rules for lawlike objects of type O are intuitionistically incompatible with (MP) and Λα⌝⌝Va·α=a.


The second paper makes the failure of the functional interpretation of higher comprehensions-even with functionals which have only a description by intuitionistic means-explicit. Significant results on the second question above are obtained by pursuing Hilbert's fundamental concept of the real elements, which was developed in full for arithmetic and analysis by the author in a previous paper on the basis of functional interpretation.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [0]
    Kleene, S.C.: Introduction to Metamathematics. Amsterdam 1962.Google Scholar
  2. [1]
    Kleene, S.C. and Vesley, R.E.: The Foundations of Intuitionistic Mathematics. Amsterdam 1965.Google Scholar
  3. [2]
    Kreisel, G.: On weak completeness of intuitionistic predicate logic. J. symb. logic 27 (1962), 139–158.MathSciNetCrossRefzbMATHGoogle Scholar
  4. [3]
    Luckhardt, H.: Extensional Gödel Functional Interpretation. A Consistency Proof of Classical Analysis. Lecture Notes in Mathematics 306, Springer 1973.Google Scholar
  5. [4]
    Luckhardt, H.: Über Hilbert's reale and ideale Elemente. Archiv für mathematische Logik und Grundlagenforschung, to appear.Google Scholar
  6. [5]
    Kreisel, G. und Troelstra, A.S.: Formal systems for some branches of intuitionistic analysis. Annals math. logic 1 (1970), 229–387.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag 1975

Authors and Affiliations

  • Horst Luckhardt

There are no affiliations available

Personalised recommendations