Advertisement

Observations on a recent generalization of completeness theorems due to Schütte

  • G. Kreisel
Conference paper
  • 190 Downloads
Part of the Lecture Notes in Mathematics book series (LNM, volume 500)

Abstract

The generalization in question is contained in [15] which will be referred to as [KMS]. It concerns the language of ordinary predicate logic without function symbols or =, (i) two kinds of valuations ρ, namely ‘total’ ones (defined for all formulas of the language considered), and ‘semi-valuations’ in the sense of Schütte's article [22], (ii) the complexityC of the valuations used, that is, validity (of a formula) for valuations ∈C is considered provided C satisfies some simple closure conditions depending on the exact choice of data determining the valuations of the kind in question—and not only ‘logical’ validity, that is, validity for the class of arbitrary valuations, and (iii) instead of finite (derivation) trees, socalled C-founded trees are used, built up according to suitable rules Rρ; in particular, rules with cut correspond to the total valuations mentioned in (i) and rules without cut correspond to semi-valuations. As in [KMS] the familiar completeness theorems, for finite (well-founded) trees built up by use of the finitary rules Rρ and logical validity (for valuations ρ), are generalized to C-founded trees and ρ-valuations of complexity C resp. The generalization also applies to ω-logic. These generalizations suggest a reappraisal of some work in the fifties on ‘constructive’ models by Mostowski [18] and Vaught [24], in which the complexity of a model is measured by its valuation on the atomic formulas.—The significance of the differencebetweenruleswithandwithoutcut is analyzed in ‘extensional’ terms by showing that, for C of suitably low complexity, for example, for recursive C, there are formulas which are true for all total valuations ∈C, but not for all such semi-valuations.

The observations fall into 3 groups. The most controversial ones concern defectsoftraditionalviews, for example, (i) of the restriction to finite, and, in particular, formal derivation trees (which would make the use of infinite C-founded trees teratological, if not ‘illegitimate’) and (ii) of so-called operational semantics which provided—in effect, if not in intention—the only permanent, not merely heuristic, significance for cut free rules: this semantics can now be compared to the usual model theoretical interpretation refined by ‘definability’ requirements C. Only slightly less controversial are the related historicalobservations; ‘related’ because earlier work was presumably influenced by, and certainly formulated in terms proper to, traditional views. The least controversial observations are about openproblems stated by essential use of the concepts involved in the generalization. Some of these problems are new, some are more precise versions or questions scattered in [KMS].

It is certainly possible to read this article with very little previous knowledge of the subject provided one simply ignores the issues arising from the literature specifically cited. But the principal aim is to serve the needs of those readers who have a detailed knowledge of our (venerable) subject which goes back >100 years; readers who wish to test to what extent this detailed work agrees with the expectations they—or, for that matter, its founders—have had of our subject. In short, the article is intended to have pedagogic use for the so to speak logically over privileged (with genuine problems of their own); a class which is created by progress, and therefore liable to be neglected by those who follow uncritically (once) ‘reasonable’ pedagogic traditions.

Keywords

Operational Semantic Atomic Formula Predicate Logic Kripke Model Natural Deduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    E. W. Beth, La crise de la raison et de la logique, Collection de logique math. A, No. 12, 1957; rev. JSL 23 (1958) 35–37.Google Scholar
  2. [2]
    J. Y. Girard, Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types, pp. 63–92 in: Proc. Sec. Scand. Logic Symposium, ed. Fenstad, Amsterdam 1971.Google Scholar
  3. [3]
    J. Y. Girard, Quelques résultats sur les interprétations fonctionnelles, pp. 232–252 in: Springer Lecture Notes 337 (1973).Google Scholar
  4. [4]
    J. Y. Girard, Three valued logic and cut elimination: the actual meaning of Takeuti's conjecture, Dissertationes math. (to appear).Google Scholar
  5. [5]
    L. Harrington, Recursively presentable prime models, JSL 39 (1974) 305–309.MathSciNetzbMATHGoogle Scholar
  6. [6]
    G. Hasenjäger, Eine Bemerkung zu Henkins Beweis fur die Vollständigkeit des Prädikatenkalkuls der ersten Stufe, JSL 18 (1953) 42–48.Google Scholar
  7. [7]
    G. C. Jockusch, П10-classes and boolean combinations of recursively enumerable sets, JSL 39 (1974) 95–96. See also recent numbers of: Algebra and Logic.MathSciNetzbMATHGoogle Scholar
  8. [8]
    S. C. Kleene, Introduction to metamathematics, Amsterdam, 1952.Google Scholar
  9. [9]
    H. J. Keisler, Model theory for infinitary logic; logic with countable conjunctions and finite quantifiers, Amsterdam, 1971.Google Scholar
  10. [10]
    G. Kreisel, Note on arithmetic models for consistent formulae of predicate calculus, FM 37 (1950) 265–285 and Part II, Proc. XI Int. Congress of Philosophy, 14 (1953) 39–39.MathSciNetzbMATHGoogle Scholar
  11. [11]
    -, A variant to Hilbert's theory of the foundations of arithmetic, Brit. J. Phil. Sc. 4 (1953) 107–127.MathSciNetCrossRefGoogle Scholar
  12. [12]
    G. Kreisel, Church's thesis: a kind of reducibility axiom for constructive mathematics, pp. 121–150 in: Intuitionism and Proof Theory, ed. Myhill et al., Amsterdam, 1970.Google Scholar
  13. [13]
    G. Kreisel, A survey of proof theory II, pp. 109–170 in: Proc. Sec. Scand. Logic Symposium, ed. Fenstad, Amsterdam, 1971.Google Scholar
  14. [14]
    G. Kreisel and J. L. Krivine, Modelltheorie, Springer Hochschultext 1972.Google Scholar
  15. [15]
    G. Kreisel, G. E. Mints and S. G. Simpson, The use of abstract language in elementary metamathematics; some pedagogic examples, pp. 38–131 in: Proc. 1973 Boston Logic Colloquium, ed. Parikh, Springer Lecture Notes 453; Vgl. PPS.Google Scholar
  16. [16]
    G. Kreisel and G. Takeuti, Formally self-referential propositions for cut-free classical analysis and related systems, Dissertationes math. 118 (1974) 4–50.MathSciNetzbMATHGoogle Scholar
  17. [17]
    G. E. Mints, On E-theorems, Zapiski 40 (1974) 101–118; siehe auch PPS.Google Scholar
  18. [18]
    A. Mostowski, On recursive models of formalized arithmetic, Bull Ac. Pol. Sc., cl. III 5 (1957), 705–710.MathSciNetzbMATHGoogle Scholar
  19. [19]
    A. J. Pljuškevičene, A sequential variant of R. M. Robinson's arithmetic system not containing cut rules, Proc. Steklov Inst. Math. 121 (1972) 121–150.zbMATHGoogle Scholar
  20. [20]
    D. Prawitz, Some results for intuitionistic logic with second order quantification rules, pp. 259–269 in: Intuitionism and Proof Theory, ed. Myhill et al., Amsterdam, 1970.Google Scholar
  21. [21]
    M. G. Rogava, Sequential variants of applied predicate calculus without structural deductive rules, Proc. Steklov. Inst. Math. 121 (1972).Google Scholar
  22. [22]
    K. Schutte, Syntactical and semantical properties of simple type theory, JSL 25 (1960) 305–326.MathSciNetzbMATHGoogle Scholar
  23. [23]
    R. Statman, Structural complexity of proofs, Dissertation, Stanford, 1974.Google Scholar
  24. [24]
    R. L. Vaugh, Sentences true in all constructive models, JSL 25 (1960) 39–53.MathSciNetGoogle Scholar
  25. [25]
    E. Zermelo, Grundlagen einer allgemeinen Theorie der mathematischen Satzsysteme, FM 25 (1935) 136–146.zbMATHGoogle Scholar
  26. [26]
    J. Zucker, Cut-elimination and normalization, Annals of Math. Logic 7 (1974) 1–112.MathSciNetCrossRefzbMATHGoogle Scholar
  27. [27]
    E. G. K. Lopez-Escobar and W. Veldman, Intuitionistic completeness of a restricted second-order logic, this volume.Google Scholar
  28. [28]
    D. Prawitz, Comments on Gentzen-type procedures and the classical notion of truth, this volume.Google Scholar

Copyright information

© Springer-Verlag 1975

Authors and Affiliations

  • G. Kreisel

There are no affiliations available

Personalised recommendations