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

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 complexity C 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 difference between rules with and without cut 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 defects of traditional views, 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 historical observations; ‘related’ because earlier work was presumably influenced by, and certainly formulated in terms proper to, traditional views. The least controversial observations are about open problems 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.