Let Th be a formal theory extending number theory. Call an ordinal ξ provable in Th if there is a primitive recursive ordering which can be proved in Th to be a wellordering and whose order type is > ξ. One may define the ordinal ∣ Th ∣ of Th to be the least ordinal which is not provable in Th. By [3] and [12] we get , where IDN is the formal theory for N-times iterated inductive definitions. We will generalize this result not only to the case of transfinite iterations but also to a more general notion of ‘the ordinal of a theory’.

For an X-positive arithmetic formula [X,x] there is a natural norm ∣x∣: = μξ (x ∈ Iξ), where Iξ is defined as {x: [∪μ<ξIμ, x]} by recursion on ξ (cf. [7], [17]). By P we denote the least fixed point of [X,x]. Then P = ∪ξξ holds. If Th allows the formation of P, we get the canonical definitions ∥Th()∥ = sup{∣x∣ + 1: Th ⊢ x ∈ P} and ∥Th∥ = sup{∥Th()∥: P is definable in Th} (cf. [17]). If ≺ is any primitive recursive ordering define Q≺[X,x] as the formula ∀y(y ≺ x → y ∈ X) and ∣x∣≺:= ∣x∣O≺. Then ∣x∣≺ turns out to be the order type of the ≺ -predecessors of x and P is the accessible part of ≺. So Th ⊢ x ∈ P implies the provability of ∣x∣≺ in Th.

One of the most significant by-products of the study of admissible sets with urelements is the emphasis it has given to recursively saturated models. As suggested in [Schlipf, 1977], countable recursively saturated models (for finite languages) possess many of the desirable properties of saturated and special models. The notion of resplendency was introduced to isolate some of these desirable properties. In §§1 and 2 of this paper we study these parallels, showing how they can be exploited to give new proofs of some traditional model theoretic theorems. This yields both pedagogical and philosophical advantages: pedagogical since countable recursively saturated models are easier to build and manipulate than saturated and special models; philosophical since it shows that uncountable models — which the downward Lowenheim–Skolem theorem tells us are in some sense not basic in the study of countable theories — are not needed in model theoretic proofs of these theorems. In §3 we apply our local results to get results about resplendent models of ZF set theory and PA (Peano arithmetic). In §4 we shall examine certain analogous results for admissible languages, most similar to, and seemingly generally slightly weaker than, already known results. (The Chang–Makkai sort of result, however, is new.)

Although this paper is an outgrowth of work with admissible sets with urelements, I have tried to keep it as accessible as possible to those with a background only in finitary model theory. Thus §§1,2, and 3 should not involve any work with admissible sets. §4, however, is concerned with some admissible analogues to results in §2 and necessarily uses certain technical results of §11 5 of [Schlipf, 1977].

It has been shown that, for all rational numbers r such that 0≤ r ≤ 1, the ℵ0-valued Łukasiewicz propositional calculus whose designated truth-values are those truth-values x such that r ≤ x ≤ 1 may be formalised completely by means of finitely many axiom schemes and primitive rules of procedure. We shall consider now the case where r is rational, 0≥r≤1 and the designated truth-values are those truth-values x such that r≤x≤1.

We note that, in the subcase of the previous case where r = 1, a complete formalisation is given by the following four axiom schemes together with the rule of modus ponens (with respect to C),

the functor A being defined in the usual way. The functors B, K, L will also be considered to be defined in the usual way. Let us consider now the functor Dαβ such that if P, Dαβ take the truth-values x, dαβ(x) respectively, α, β are relatively prime integers and r = α/β then

It follows at once from a theorem of McNaughton that the functor Dαβ is definable in terms of C and N in an effective way. If r = 0 we make the definition

We note first that if x ≤ α/β then dαβ(x)≤(β + 1)α/β − α = α/β. Hence

Let us now define the functions dnαβ(x) (n = 0,1,…) by

Since

it follows easily that

and that

Thus, if x is designated, x − α/β > 0 and, if n > − log(x − α/β)/log(β + 1), then (β + 1)n(x−α/β) > 1.

Fine [1] and Thomason [4] have recently shown that the familiar relational semantics of Kripke [2] is inadequate for certain normal extensions of T and S4. It is here shown that the more general semantics developed by Kripke in [3] to handle nonnormal modal logics is likewise inadequate for certain of those logics.

The interest of incompleteness results, such as those of Fine and Thomason, is of course a function of one's expectations. Define a “normal” logic too broadly and it is not surprising that a given semantics is not adequate for all normal logics. In the case of relational semantics, for example, one would want to require at least that a normal logic contain T, the logic determined by the class of all normal frames, and that it be closed under certain (though perhaps not all) rules of inference which are validity preserving in such frames. The adequacy of that semantics will otherwise be ruled out at the outset.

For Kripke a logic is normal if it contains all tautologies, □p→p and □ (p → q)→(□p → □q), and is closed under the rules of substitution, modus ponens and necessitation (from A infer □A). T is the smallest normal logic, and this fact, together with the “naturalness” of the definition and the enormous number of normal logics which have been shown to be complete, made it plausible to suppose that Kripke's original semantics was adequate for all normal logics. That it is not is indeed surprising and would seem to reveal a genuine shortcoming.

In 1930, A. Heyting first specified a formal system for part of intuitionistic mathematics. Although his rules were presumably motivated by the “intended interpretation” or meaning of the logical symbols, over the years a number of other possible interpretations have been discovered for which the rules are also valid. In particular, one might mention the realizablity interpretation of Kleene, the (Dialectica) interpretation of Gödel, and various semantic interpretations, such as Kripke models. (Each of these has several variants or close relatives.) Each such interpretation can be regarded as defining precisely a certain “notion of constructivity”, the study of which may illuminate the still rather vague notions which underlie the intended interpretation; or, if one doubts that there is a single interpretation “intended” by all constructivist mathematicians, the study of precisely defined interpretations may help to delineate and distinguish the possibilities.

In the last few years, Heyting's systems have been vastly extended, in order to encompass the large and growing body of constructive mathematics. Several kinds of new systems have been put forward and studied. The present author has extended the various realizability interpretations to several of these systems [B1], [B2] and drawn a number of interesting applications. The mathematical content of the present paper is an interpretation in the style of Godel's Dialectica interpretation, but applicable to the new systems put forward by Feferman [Fl]. The original motivation for this work was to obtain certain metamathematical applications: roughly speaking, Markov's rule and its variants.

This paper is devoted to the general question, which assertions φ have the property,

if φ is provable classically, then φ is

(*) provable constructively.

More generally, we consider the question, what is the “constructive content” of a given classical proof? Our aim is to formulate rules in a form applicable to mathematical practice. Often a mathematician has the feeling that there will be no difficulty constructivizing a certain proof, only a number of routine details; although it can be quite laborious to set them all out. We believe that most such situations will come quite easily under the scope of the rules given here; the metamathematical machinery will then take care of the details.

This basic idea is not new; it has been discussed by Gödel and by Kreisel. Kreisel's investigations [Kr] were based on Herbrand's theorem; in unpublished memoranda he has also used Gödel's methods on some examples. These methods of Gödel (the double-negation and Dialectica interpretations) lie at the root of our work here. Previous work, however, has been limited to traditional formal systems of number theory and analysis. It is only recently that formal systems adequate to formalize constructive mathematics as a whole have been developed. Thus, for the first time we are in a position to formulate logical theorems which are easily applicable to mathematical practice. It is this program which we here carry out.

Now that the work has been placed in some historical context, let us return to the main question: which φ have the property (*)? Upon first considering the problem, one might guess that any φ which makes no existential assertions (including disjunctions) should have the property (*).

This note shows that the argument used in the proof of the inconsistency of Curry's system (see [1]) can also be applied to Fitch's system QD (see [3, Chapter 6]). As one vital rule of is not present in QD this argument does not lead to an actual contradiction, but it does lead to a theorem which is not a proposition if the system is consistent.

The method used below is that of [2], which is simpler than that of [1].

The axioms and rules of QD that we require are also present in [1] and [2] provided that Fitch's D is replaced by H. These axioms and rules are the following:

DD int: ⊦ D(Da),

m p: If ⊦ a ⊃ b2 and ⊦ a then ⊦ b, and

res imp int: If a ⊦ b then Da ⊦ a ⊃ b.

Let a be arbitrary and let G be [x](Dx ⊃ (x ⊃ a)). Then let X be BWBG(BWBG). We then have the following proof:

Thus, we have ⊦ X. Now suppose we also had ⊦ DX. Then by the method of the innermost subproof in the above proof, we would have ⊦ a, and since a is

arbitrary the system would be inconsistent. Hence, if QD is consistent, we do not have ⊦ DX, and so X is a theorem which is not a proposition.

Let n ≥ 3. The following theorems are proved.

Theorem. The theory of the class of strictly upper triangular n × n matrix rings over fields is finitely axiomatizable.

Theorem. If R is a strictly upper triangular n × n matrix ring over a field K, then there is a recursive map σ from sentences in the language of rings with constants for K into sentences in the language of rings with constants for R such that K ⊨ φ if and only if R φ σ(φ).

Theorem. The theory of a strictly upper triangular n × n matrix ring over an algebraically closed field is ℵ1-categorical.

Let V∞ be a fixed, fully effective, infinite dimensional vector space. Let be the lattice consisting of the recursively enumerable (r.e.) subspaces of V∞, under the operations of intersection and weak sum (see §1 for precise definitions). In this article we examine the algebraic properties of .

Early research on recursively enumerable algebraic structures was done by Rabin [14], Frölich and Shepherdson [5], Dekker [3], Hamilton [7], and Guhl [6]. Our results are based upon the more recent work concerning vector spaces of Metakides and Nerode [12], Crossley and Nerode [2], Remmel [15], [16], and Kalantari [8].

In the main theorem below, we extend a result of Lachlan from the lattice of r.e. sets to . We define hyperhypersimple vector spaces, discuss some of their properties and show if A, B ∈ , and A is a hyperhypersimple subspace of B then there is a recursive space C such that A + C = B. It will be proven that if V ∈ and the lattice of superspaces of V is a complemented modular lattice then V is hyperhypersimple. The final section contains a summary of related results concerning maximality and simplicity.

Several new features arise in the generalization of recursion theory on ω to recursion theory on admissible ordinals α, thus making α-recursion theory an interesting theory. One of these is the appearance of irregular sets. A subset A of α is called regular (over α), if we have for all β < α that A ∩ B ∈ Lα, otherwise A is called irregular (over α). So in the special case of ordinary recursion theory (α = ω) every subset of α is regular, but if α is not a cardinal of L we find constructible sets A ⊆ α which are irregular. The notion of regularity becomes essential, if we deal with α-recursively enumerable (α-r.e.) sets in priority constructions (α-r.e. is defined as Σ1 over Lα). The typical situation occurring there is that an α-r.e. set A is enumerated during some construction in which one tries to satisfy certain requirements. Often this construction succeeds only if we can insure that every initial segment A ∩ β of A is completely enumerated at some stage before α. This calls for making sure that A is regular because due to the admissibility of α an α-r.e. set A is regular iff for every (or equivalently for one) enumeration f of A (f is an enumeration of A iff f: α → A is α-recursive, total, 1-1 and onto) we have that is the image of the set σ under f).

We present two theorems whose applications are to eliminate diagonalization arguments from a variety of constructions of degrees of unsolvability.

All definitions and notations come from [1, Chapter 1]. We give a brief resumé of them here.

We identify a set with its characteristic function. (A(x)= 1 if x ∈ A and A (x) = 0 if x ∉ A.) A string σ is the restriction of a characteristic function to a finite initial segment of natural numbers, lh(σ) = length of σ = n + 1 if σ = A[n] for some set A. (A [n] is the restriction of A to {m: m ≤ n}.) If i = 0 or 1, σ * i is defined as the string of length lh(σ) + 1 such that σ * i ⊇ σ and σ * i(lh(σ)) = i. We write σ ∣ τ if σ ⊉ τ and τ ⊉ σ.

{Φn} is a listing of the partial recursive functionals. We write “A ≤TB” (“A is Turing reducible to B”) if ∃n∀xΦn(B)(x) = A(x).

A partial function, T, from strings to strings is a tree if T is order preserving and for all strings, σ, if one of T(σ * 0), T(σ * 1) is defined then T(σ), T(σ * 0), T(σ * 1) are all defined and T(σ * 0)∣(σ * 1).

Let us consider the following infinite game between two players, Empty and Nonempty. We are given a large set S. Empty opens the game by choosing a large subset S0 of S; then Nonempty chooses a large set S1 ⊆ S0; then Empty chooses large S2 ⊆ S, etc. The game is over after ω moves. If ⋂n=0xSn is empty then Empty wins, and if ⋂n=0∞Sn is nonempty then Nonempty wins.

If “large” means “infinite”, then Empty can beat Nonempty rather easily: he chooses So countable, S0 = {a0, a1,…, an,…}, and then he chooses S2 such that a0 ∉ S2, S4 such that a1, ∉ S4 and so on.

Next we assume that S is a set of uncountable cardinality, and that “large” means “of cardinality ∣S∣”. Then still Empty can win, but his winning strategy is somewhat more sophisticated: Let us identify S with a cardinal number κ. Thus each subset of S of size κ is a set of ordinals below κ. For each X ⊆ κ of size κ, let fx be the unique order-preserving mapping of X onto κ, and let F(X) = {x ϵ X: f(x) is a successor ordinal}. Empty's strategy is to play S0 = F(K), and when Nonempty plays S2k − 1, let S2k = F(S2k − 1).

The main point of this paper is a further development of some aspects of the recent theory of recursively enumerable (r.e.) algebraic structures. Initial work in this area is due to Frölich and Shepherdson [4] and Rabin [10]. Here we are only concerned with vector space structure. The previous work on r.e. vector spaces is due to Dekker [2], [3], Metakides and Nerode [8], Remmel [11], Retzlaff [13], and the author [5].

Our object of study is V∞ a countably infinite dimensional fully effective vector space over a countable recursive field . By fully effective we mean that V∞. under a fixed Godel numbering has the following properties:

(i) Operations of vector addition and scalar multiplication on V∞ are presented by partial recursive functions on the Gödel numbers of elements of V∞.

(ii) V∞ has a dependence algorithm, i.e., there is a uniform effective procedure which applied to any n vectors of V∞ determines whether or not they are linearly independent.

We also study , the lattice of r.e. subspaces of V∞ (under the operations of intersection, ⋂ and (weak) sum, +). We note that if is not distributive and is merely modular (see [1]). This fact indicates the essential difference between the lattice of r.e. sets and .

It is the purpose of this paper to investigate the model theory of logic with a generalized quantifier; in particular the logic L(Q1) where Q1xφ(x) has the intended meaning “there exist uncountably many x such that φ(x)”. We do this from the point of view that the best way to study what happens in the so-called “ω1-standard” models of L(Q1) is to examine the countable ideal models of L(Q) that satisfy all of the axioms for L(Q1) (see definitions of ω1-standard and ideal models in §1). We believe that this study can be as fruitful for L(Q1) as the study of countable models of ZF has been for set theory.

A major problem is formulating an adequate definition of submodel for countable ideal models that is compatible with that for ω1-standard models. Thus we begin the paper by discussing several possible definitions of the notion of submodel. We then adopt a particular definition of submodel and investigate model-completeness in L(Q). We define model-completeness both for ω1-standard models and for countable ideal models and compare the two notions. We also examine elimination of quantifiers, as well as investigating formulas preserved under submodels, again both for ω1-standar d and countable ideal models.

Ever since Post [4] the structure of recursively enumerable sets and their classification has been an important area in recursion theory. It is also intimately connected with the study of the lattices and of r.e. sets and r.e. sets modulo finite sets respectively. (This lattice theoretic viewpoint was introduced by Myhill [3].) Key roles in both areas have been played by the lattice of r.e. supersets, , of an r.e. set A (along with the corresponding modulo finite sets) and more recently by the group of automorphisms of and . Thus for example we have Lachlan's deep result [1] that Post's notion of A being hyperhypersimple is equivalent to (or ) being a Boolean algebra. Indeed Lachlan even tells us which Boolean algebras appear as —precisely those with Σ3 representations. There are also many other simpler but still illuminating connections between the older typology of r.e. sets and their roles in the lattice . (r-maximal sets for example are just those with completely uncomplemented.) On the other hand, work on automorphisms by Martin and by Soare [8], [9] has shown that most other Post type conditions on r.e. sets such as hypersimplicity or creativeness which are not obviously lattice theoretic are in fact not invariant properties of .

In general the program of analyzing and classifying r.e. sets has been directed at the simple sets. Thus the subtypes of simple sets studied abound — between ten and fifteen are mentioned in [5] and there are others — but there seems to be much less known about the nonsimple sets. The typologies introduced for the nonsimple sets begin with Post's notion of creativeness and add on a few variations. (See [5, §8.7] and the related exercises for some examples.) Although there is a classification scheme for r.e. sets along the simple to creative line (see [5, §8.7]) it is admitted to be somewhat artificial and arbitrary. Moreover there does not seem to have been much recent work on the nonsimple sets.

Let L be a countable language including the unary relation symbol U. Let and be L-structures such that is a proper elementary U-extension of ; i.e., , and . Under what conditions will have a proper elementary U-extension? In [2], it was shown that this is not always the case, even if and are countable. However, the examples given are completely artificial, and it still seems that in most cases will have a proper elementary U-extension.

Lascar asked whether will necessarily have a proper elementary U-extension whenever it contains an infinite set of indiscernibles over . This paper gives a counterexample for Lascar's question. The example is produced by modifying one of the examples in [2], using an idea of Marcus [5].

Models containing an infinite set of indiscernibles can often be “stretched” to produce larger models that share some desired nonelementary property with the original [1], [6]. However, the mere presence of indiscernibles in a model does not guarantee that it can be used in this way.

If the model is not completely determined by the indiscernibles, the nonelementary property may not carry over to larger models. An example of this is given in [3]. The example for Lascar's question is further evidence that models with indiscernibles need not be “elastic”.

In his celebrated paper of 1931 [7], Kurt Gödel proved the existence of sentences undecidable in the axiomatized theory of numbers. Gödel's proof is constructive and such a sentence may actually be written out. Of course, if we follow Gödel's original procedure the formula will be of enormous length.

Forty-five years have passed since the appearance of Gödel's pioneering work. During this time enormous progress has been made in mathematical logic and recursive function theory. Many different mathematical problems have been proved recursively unsolvable. Theoretically each such result is capable of producing an explicit undecidable number theoretic predicate. We have only to carry out a suitable arithmetization. Until recently, however, techniques were not available for carrying out these arithmetizations with sufficient efficiency.

In this article we construct an explicit undecidable arithmetical formula, F(x, n), in prenex normal form. The formula is explicit in the sense that it is written out in its entirety with no abbreviations. The formula is undecidable in the recursive sense that there exists no algorithm to decide, for given values of n, whether or not F(n, n) is true or false. Moreover F(n, n) is undecidable in the formal (axiomatic) sense of Gödel [7]. Given any of the usual axiomatic theories to which Gödel's Incompleteness Theorem applies, there exists a value of n such that F(n, n) is unprovable and irrefutable. Thus Gödel's Incompleteness Theorem can be “focused” into the formula F(n, n). Thus some substitution instance of F(n, n) is undecidable in Peano arithmetic, ZF set theory, etc.