⊨ISILC Proof Theory Symposion pp 164-181 | Cite as

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

- 190 Downloads

## 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## Preview

Unable to display preview. Download preview PDF.

## References

- [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]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]J. Y. Girard, Quelques résultats sur les interprétations fonctionnelles, pp. 232–252 in: Springer Lecture Notes 337 (1973).Google Scholar
- [4]J. Y. Girard, Three valued logic and cut elimination: the actual meaning of Takeuti's conjecture, Dissertationes math. (to appear).Google Scholar
- [5]L. Harrington, Recursively presentable prime models, JSL 39 (1974) 305–309.MathSciNetzbMATHGoogle Scholar
- [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]G. C. Jockusch, П
_{1}^{0}-classes and boolean combinations of recursively enumerable sets, JSL 39 (1974) 95–96. See also recent numbers of: Algebra and Logic.MathSciNetzbMATHGoogle Scholar - [8]S. C. Kleene, Introduction to metamathematics, Amsterdam, 1952.Google Scholar
- [9]H. J. Keisler, Model theory for infinitary logic; logic with countable conjunctions and finite quantifiers, Amsterdam, 1971.Google Scholar
- [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]-, A variant to Hilbert's theory of the foundations of arithmetic, Brit. J. Phil. Sc. 4 (1953) 107–127.MathSciNetCrossRefGoogle Scholar
- [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]G. Kreisel, A survey of proof theory II, pp. 109–170 in: Proc. Sec. Scand. Logic Symposium, ed. Fenstad, Amsterdam, 1971.Google Scholar
- [14]G. Kreisel and J. L. Krivine, Modelltheorie, Springer Hochschultext 1972.Google Scholar
- [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]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]G. E. Mints, On E-theorems, Zapiski 40 (1974) 101–118; siehe auch PPS.Google Scholar
- [18]A. Mostowski, On recursive models of formalized arithmetic, Bull Ac. Pol. Sc., cl. III 5 (1957), 705–710.MathSciNetzbMATHGoogle Scholar
- [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]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]M. G. Rogava, Sequential variants of applied predicate calculus without structural deductive rules, Proc. Steklov. Inst. Math. 121 (1972).Google Scholar
- [22]K. Schutte, Syntactical and semantical properties of simple type theory, JSL 25 (1960) 305–326.MathSciNetzbMATHGoogle Scholar
- [23]R. Statman, Structural complexity of proofs, Dissertation, Stanford, 1974.Google Scholar
- [24]R. L. Vaugh, Sentences true in all constructive models, JSL 25 (1960) 39–53.MathSciNetGoogle Scholar
- [25]E. Zermelo, Grundlagen einer allgemeinen Theorie der mathematischen Satzsysteme, FM 25 (1935) 136–146.zbMATHGoogle Scholar
- [26]J. Zucker, Cut-elimination and normalization, Annals of Math. Logic 7 (1974) 1–112.MathSciNetCrossRefzbMATHGoogle Scholar
- [27]E. G. K. Lopez-Escobar and W. Veldman, Intuitionistic completeness of a restricted second-order logic, this volume.Google Scholar
- [28]D. Prawitz, Comments on Gentzen-type procedures and the classical notion of truth, this volume.Google Scholar