We deal here with two modal logics, GL and Grz, that are known to have interesting arithmetical interpretations connected with the notion of provability. GL is the extensiom of K (or K4) by the schema □(□ A → A) → □ A, and Grz is the extension of S4 by □(□(A → □A) →A) → □A. GL is also known to be sound and complete with respect to the class of all Kripke models that are transitive, irreflexive and well founded. Grz bears the same relation to the corresponding reflexive models. We refer the reader to [1] for a full exposition of the subject. (See also [4], [2], [6].)

In §I we develop a sequential calculus for both GL and Grz and give a semantical proof that both systems admit cut-elimination. (Incidentally, this provides an easy proof of the semantical completeness of the two systems.) With respect to GL this yields a correction of an error in [2].

In §II we show that cut-elimination fails for QGL (the extension of GL to a language with quantifiers). We further show that, despite this failure, QGL still has some of GL's interesting properties (e.g., the disjunction property). We also show, using fixed-point techniques, that similar properties obtain if we take as semantics for QGL the arithmetical interpretation extended in the obvious way.

We want to thank Professor H. Gaifman for his help while working on the subject.

The concepts “classical valuation” and “supervaluation” were introduced by van Fraassen around 1966, to provide a semantic analysis of the then extant axiomatic systems of free logic. Consider an atomic sentence

and a “partial” model which fails to interpret c. Then (1) has no truth value in , nor does

While the valuelessness of (1) was found intuitively acceptable, that of (2) was not. Indeed, (2) and all other tautologies are theorems of free logic.

Van Fraassen found a way to accommodate both intuitions. He interprets the unproblematic atomic sentences as usual, while “interpreting” those like (1) by simply assigning them a truth-value in arbitrary fashion. Then a truth-value for every sentence can be defined in the usual way; the result van Fraassen calls a “classical valuation” of the language. The arbitrary element in any given classical valuation is then eliminated by passage to the “supervaluation” over , which agrees with the classical valuations where they agree among themselves, and otherwise is undefined. In the supervaluation over , (1) is valueless but (2) true (since true on all classical valuations), as was required.

There is a slight, but crucial oversimplification in the preceding account. Evaluation of the sentence

requires prior evaluation of the open formula

But here mere assignment of truth-value is not enough; a whole set must be arbitrarily assigned as extension. The quantification over classical valuations involved in passage to the supervaluation thus involves an implicit quantification over subsets of the domain of : supervaluations are second order.

The recursively unsolvable halting problem for Turing machines is reduced to the problem of the existence or not of an algorithm for deciding whether a field is finite. The latter problem is further reduced to the decision problem of each of properties

for recursive sets Σ of equations of strong algebraic languages with infinitely many operation symbols.

Decision problems concerning properties of sets of equations were first raised by Tarski [9] and subsequently examined by Perkins [6], McKenzie [4], McNulty [5] and Pigozzi [7]. Perkins is the only one who studied recursive sets; the others investigated finite sets. Since the undecidability of properties Pi for recursive sets of equations does not imply any answer to the corresponding decision problems for finite sets, the latter problems remain open.

The work presented here is part of my Ph.D. thesis [2]. I thank Wilfrid Hodges, who supervised it.

An algebraic language is a first-order language with equality but without relation symbols. It is here denoted by , where Qi is an operation symbol and cj, is a constant symbol.

If M ⊨ PA (= Peano Arithmetic), we set AM = {N ⊂eM: N ⊨ PA} and study this family.

Ziegler studies in [2] the expressive power of (Lωω)t for T3 topological spaces. He defines for every natural number n the set of n-types by induction: . If A is a T3 space, the n-type of a ∈ A is defined inductively by: : in every neighborhood of a there is an a′ ≠ a with tn(a′, A) = α}. These types are (Lωω)t-definable. Then, it is shown that two T3 spaces are (Lωω)t-equivalent precisely if for every n-type α they have the same number of points with n-type α (cf. [2]).

In order to study the expressability of (Lω1ω)t, for T3 spaces, we introduce in this paper the notion of accessible set. Looking at the behaviour of convergence by means of this notion, we refine Ziegler's notion of n-type and introduce a new set Sn of n-types, which are (Lω1ω)t-definable. Then, we prove a characterization of (Lω1ω)t-equivalence for a wide class of T3 spaces. A T3 space A belongs to this class if there is a κ ∈ ω such that, for every n ∈ ω, there are at most κ n-types in Sn which are satisfiable in A. Such a space is said to be of a-finite type. Some relations between these spaces and the spaces of finite type in the sense of [2] are shown in the last section.

The contents of the present paper are treated in more detail in [3].