We investigate the provability or nonprovability of certain ordinary mathematical theorems within certain weak subsystems of second order arithmetic. Specifically, we consider the Cauchy/Peano existence theorem for solutions of ordinary differential equations, in the context of the formal system RCA0 whose principal axioms are comprehension and induction. Our main result is that, over RCA0, the Cauchy/Peano Theorem is provably equivalent to weak König's lemma, i.e. the statement that every infinite {0, 1}-tree has a path. We also show that, over RCA0, the Ascoli lemma is provably equivalent to arithmetical comprehension, as is Osgood's theorem on the existence of maximum solutions. At the end of the paper we digress to relate our results to degrees of unsolvability and to computable analysis.

In this paper we show that the propositional logics E of entailment, R of relevant implication and T of ticket entailment are undecidable. The decision problem is also shown to be unsolvable in an extensive class of related logics. The main tool used in establishing these results is an adaptation of the von Neumann coordinatization theorem for modular lattices.

Interest in the decision problem for these systems dates from the late 1950s. The earliest result was obtained by Anderson and Belnap who proved that the first degree fragment of all these logics is decidable. Kripke [11] proved that the pure implicational fragments R→ and E→ of R and E are decidable. His methods were extended by Belnap and Wallace to the implication-negation fragments of these systems [3]; Kripke's methods also extend easily to include the implication-conjunction fragments of R and E. Meyer in his thesis [14] extended the result for R to include a primitive necessity operator. He also proved decidable the system R-mingle, an extension of R, and ortho-R (OR), the logic obtained from R by omitting the distribution axiom. Various weak relevant logics are also known to be decidable by model-theoretic proofs of the finite model property (see Fine [5]). Finally, S. Giambrone [7] has solved the decision problem for various logics obtained by the omission of the contraction axiom (A → ⦁ A → B) → ⦁ A → B, including R+ − W (R+ minus contraction). It is worth noting that even where positive results were obtained, the decision methods were usually of a complexity considerably greater than in the case of other nonclassical logics such as intuitionistic logic or modal logic, a fact which already indicates the difficulty of the decision problem.

In [3] a definition of negation was presented for the system K′ of extended basic logic [1], but it has since been shown by Peter Päppinghaus (personal communication) that this definition fails to give rise to the law of double negation as I claimed it did. The purpose of this note is to revise this defective definition in such a way that it clearly does give rise to the law of double negation, as well as to the other negation rules of K′.

Although Päppinghaus's original letter to me was dated September 19, 1972, the matter has remained unresolved all this time. Only recently have I seen that there is a simple way to correct the definition. I am of course very grateful to Päppinghaus for pointing out my error in claiming to be able to derive the rule of double negation from the original form of the definition.

The corrected definition will, as before, use fixed-point operators to give the effect of the required kind of transfinite induction, but this time a double transfinite induction will be used, somewhat like the double transfinite induction used in [5] to define simultaneously the theorems and antitheorems of system CΓ.

In this note it is shown that the property of orthomodularity of the lattice of orthoclosed subspaces of a pre-Hilbert space is not determined by any first-order properties of the relation ⊥ of orthogonality between vectors in . Implications for the study of quantum logic are discussed at the end of the paper.

The key to this result is the following:

Ifis a separable Hilbert space, andis an infinite-dimensional pre-Hilbert subspace of, then (, ⊥) and (, ⊥) are elementarily equivalent in the first-order languageL2of a single binary relation.

Choosing to be a pre-Hilbert space whose lattice of orthoclosed subspaces is not orthomodular, we obtain our desired conclusion. In this regard we may note the demonstration by Amemiya and Araki [1] that orthomodularity of the lattice of orthoclosed subspaces is necessary and sufficient for a pre-Hilbert space to be metrically complete, and hence be a Hilbert space. Metric completeness being a notoriously nonelementary property, our result is only to be expected (note also the parallel with the elementary L2-equivalence of the natural order (Q, <) of the rationals and its metric completion to the reals (R, <)).

To derive (1), something stronger is proved, viz. that (, ⊥) is an elementary substructure of (, ⊥).

Un espace ultramétrique est un ensemble muni d'une distance à valeurs dans un ordre total avec premier élément et pour laquelle tout triangle est isocèle avex deux grands côtés égaux. Les deux cas importants d'espaces ultramétriques sont:

(1) les corps valués lorsqu'on ne considère que leur structure métrique, et

(2) les ensembles Aλ, où λ est un ensemble bien ordonné, munis de la distance d(α, β) = inf {γ ∈ λ; α(γ) ≠ β(γ)} si α ≠ β et d(α, β) = 0 sinon; distance à valeurs dans l'ordre inverse de λ enrichi d'un premier élément 0.

Nous étudions ces structures dans un langage comportant un seul type de variables, les points de l'espace, et un prédicat à quatre places traduisant l'ordre sur les distances

Nous définissons la notion d'espace riche, qui est la modèle-complétion relative à un ensemble des distances fixé: un espace est riche si et seulement s'il est existentiellement clos dans toute extension qui n'ajoute pas de nouvelle distance. Les deux exemples précédemment donnés, espaces Aλ et corps valués, fournissent des espaces riches. La suite de l'article s'attache à la description des espaces riches.

This paper contributes to the question of under which conditions recursively enumerable sets with isomorphic lattices of recursively enumerable-supersets are automorphic in the lattice of all recursively enumerable sets. We show that hyperhypersimple sets (i.e. sets where the recursively enumerable supersets form a Boolean algebra) are automorphic if there is a -definable isomorphism between their lattices of supersets. Lerman, Shore and Soare have shown that this is not true if one replaces by .

Cette note est consacrée à quelques compléments à mon article [6], que le lecteur est supposé avoir sous les yeux, et qui traite de la propriété de recouvrement fini, de Keisler. Je rappelle seulement ici que:

a) La définition originale est la suivante: une théorie complète T n'a pas la p.r.f. si à toute formule f(x, ȳ) de son langage est associé un entier n, de sorte que tout ensemble (fini!) {f(x, ā1), …, f(x, ās)}, où les āi; sont des paramètres extraits d'un modèle M de T, soit consistant dès que ses parties à n éléments le sont. Une théorie sans p.r.f. satisfait done un renforcement du théorème de compacité; elle est en ce sens plus simple qu'une théorie avec p.r.f.

b) T n'a pas la p.r.f. si et seulement si elle est stable (i.e. tout type sur un modèle M de T est définissable; à toute formule f(x, ȳ) est associée une formule g(ȳ, ā) à paramètres dans M, telle que les de M pour lesquels f(x, ) est dans le type en question soient précisément ceux qui vérifient g(ȳ, ā)), et si en outre on peut exprimer par une formule sur le paramètre ā que g(ȳ, ā) définit un f-type consistant: à f1(x, ȳ), …, fs(x, ȳ), g1(ȳ, ), …, gs(ȳ, ) est associé une formule h(), telle que pour tout ā de tout modèle M de T, ā satisfasse h si et seulement si l'ensemble de tous les fi(x, ), où est dans M et satisfait gi(ȳ, ā), est consistant.

E. Specker has proved that the axiom of choice (AC) is false in NF [6]. Since AC is stratified, one can, according to another famous result of Specker [7], prove directly ¬AC in type theory (TT) plus some finite set of ambiguity axioms, i.e. sentences of the form φ ↔ φ+, where φ+ results from φ by adding one to its type indices.

We shall in §2 of this paper give a disproof of AC directly in TT plus some axioms of ambiguity. The argument will be split into two parts. The first one (contained in Proposition 2) concerns cardinal arithmetic and has nothing to do with typical ambiguity. Though carried out in TT, it could have been done in other set theories such as Zermelo's Z or ZF. The second part is an application of this to the cardinals of the universes at different types. This is made possible through the introduction of an appropriate definition of 2α in §1 enabling one to express shifting sentences as “typed properties” of the universe, in Boffa's sense. The disproof of AC is then completed in TT plus two extra ambiguity axioms. In §3, we show that this is in a sense the best possible result: that means that every single ambiguity axiom is consistent with TT plus AC, thus giving a positive solution to a conjecture of Specker [7, p. 119].

J. Barbanel [1] characterized the class of cardinals fixed by an elementary embedding induced by a normal ultrafilter on Pκλ assuming that κ is supercompact. In this paper we shall prove the same results from the weaker hypothesis that κ is strongly compact and the ultrafilter is fine.

We work in ZFC throughout. Our set-theoretic notation is quite standard. In particular, if X is a set, ∣X∣ denotes the cardinality of X and P(X) denotes the power set of X. Greek letters will denote ordinals. In particular γ, κ, η and γ will denote cardinals. If κ and λ are cardinals, then λ<κ is defined to be supγ<κγγ. Cardinal exponentiation is always associated from the top. Thus, for example, 2λ<κ means 2(λ<κ). V denotes the universe of all sets. If M is an inner model of ZFC, ∣X∣M and P(X)M denote the cardinality of X in M and the power set of X in M respectively.

We review the basic facts on fine ultrafilters and the corresponding elementary embeddings. (For detail, see [2].)

Definition. Assume κ and λ are cardinals with κ ≤ λ. Then, Pκλ = {X ⊂ λ∣∣X∣ < κ}.

It is important to note that ∣Pκλ∣ = λ< κ.

Let PA be the theory of first order Peano arithmetic, in the language L with binary operation symbols + and ·. Let N be the theory of the standard model of PA. We consider countable models M of PA such that the universe ∣M∣ is ω. The degree of such a model M, denoted by deg(M), is the (Turing) degree of the atomic diagram of M. The results of this paper concern the degrees of models of N, but here in the Introduction, we shall give a brief survey of results about degrees of models of PA.

Let D0 denote the set of degrees d such that there is a nonstandard model of M of PA with deg(M) = d. Here are some of the more easily stated results about D0.

(1) There is no recursive nonstandard model of PA; i.e., 0 ∈ D0.

This is a result of Tennenbaum [T].

(2) There existsd ∈ D0such thatd ≤ 0′.

This follows from the standard Henkin argument.

(3) There existsd ∈ D0such thatd < 0′.

Shoenfield [Sh1] proved this, using the Kreisel-Shoenfield basis theorem.

(4) There existsd ∈ D0such thatd′ = 0′.

Jockusch and Soare [JS] improved the Kreisel-Shoenfield basis theorem and obtained (4).

(5) D0 = Dc = De, where Dc denotes the set of degrees of completions of PA and De the set of degrees d such that d separates a pair of effectively inseparable r.e. sets.

Solovay noted (5) in a letter to Soare in which in answer to a question posed in [JS] he showed that Dc is upward closed.

This paper is the sequel of “a functorial construction of the Veblen hierarchy” [GV]: it was announced in it.

We define the notion of garden (Definition I.1.6), that is a functorial version of a Bachmann collection: in a garden Jy, at each ordinal x ≤ y, of cofinality Ω, is associated an Ω-flower (Definition I.1.1); we define also the notion of a function compatible with a garden (Definition I.3.3). We construct a hierarchy of functors from Ω to Ω (for each x ≤ y and x ∈ Jy) and for each function (f ∈ I(x, y) compatible with Jy a natural transformation T(f) from to ; we show that, if the garden is Gε Ω + 1 (Definition I.2.1), then, for each ordinal x ≤ εΩ + 1, the hierarchy of functions coincides exactly with the usual hierarchy ψx constructed using the usual Bachmann collection of height εΩ + 1, and founded on composition (that is, ψx + 1 = ψx ˚ ψ1; then, (0) is the usual Howard ordinal. We show also, that for eac x ≤ y, φx is an Ω-flower, and so we can use this hierarchy of functors for ordinal notations: see Chapter II of -logic [G].

The construction made in this article corresponds, essentially, to Chapter V of -logic [G]: the exact connections between these two works will be the matter of a subsequent article.

We say that the Boolean algebra B is λ-compact, where λ is a cardinal number, if for every family Z ⊆ B∖{0} of power at most λ, if inf Z = 0 then for some finite subfamily Z0 ⊆ Z we have inf Z0 = 0.

On the set of all finite subsets of a cardinal number κ, which is denoted [κ]<ω, the sets of the form for any p Є [κ]<ω generate the filter Tκ.

This filter is a standard example of a κ-regular filter (see [2]). Because of the importance of κ-regular filters in studying the saturatedness of ultraproducts and reduced products by model-theoretic methods, the question of compactness of the algebra Bκ = P([κ]<ω/Tκ was natural. This question in the most optimistical way was formulated by M. Benda [1, Problem 5c]: is the algebra Bκω-compact for every uncountable κ?

In this paper we show that for most of the cardinal numbers which are greater or equal to 2ω the algebra Bκ is not ω-compact. Hence, in view of obtained results, the following question appears: does there exist an uncountable κ such that the algebra Bκ is κ-compact?

We use standard set-theoretical notations. CH denotes the Continuum Hypothesis, GCH denotes the General Continuum Hypothesis and MA denotes Martin's Axiom.

An ideal I defined on a group G is called idempotent if for every A ∈ I, {g ∈ G:Ag−1 ∉ ∈ I} ∈ I. We show that a countably complete idempotent ideal on an abelian group cannot be prime but may have strong saturation properties.

In an earlier paper we proved that a universal Horn class generated by finitely many finite structures has a model companion. If the language has only finitely many fundamental operations then the theory of the model companion admits a primitive recursive elimination of quantifiers and is primitive recursive. The theory of the model companion is ℵ0-categorical iff it is complete iff the universal Horn class has the joint embedding property iff the universal Horn class is generated by a single finite structure. In the last section we look at structure theorems for the model companions of universal Horn classes generated by functionally complete algebras, in particular for the cases of rings and groups.

The question of the limits of recursive enumerability was first formulated by Sacks (1980) and investigated further in Sacks (198?). E-recursion or “set recursion”, as a natural generalization of Kleene recursion in normal objects of finite type, was introduced by Normann (1978) in order to facilitate the study of the degrees of functionals. We shall extend the work of Sacks on the question of how definable is the E-closure of an ordinal α (written E(α)). We write gc(κ) to denote the largest τ < κ such that Lκ ⊨ “τ is a cardinal” and cf (τ) for τ ∈ ON to denote the cofinality of τ.

In §1 we give the basic definitions and state the results of Silver and Friedman (1980) used by Sacks to show that if E(α) = Lκ and is not Σ1-admissible and

then P(gc(κ)) ∩ Lκ is indexical on Lκ and hence RE. We show in this case first that P(gc(κ)) ∩ Lκ indexical implies that Lκ is indexical (and hence RE).

In §2 we introduce the notion of a “nonstandard stage comparison” and use it to extend the definability result of §1 to show that this Lκ is in fact REC. Finally we remark that E(α) is indexical if and only if E(α) is RE.

In [O1], we gave algebraic characterizations of elementary equivalence for finitely generated finite-by-abelian groups, i.e. finitely generated FC-groups. We also provided several examples of finitely generated finite-by-abelian groups which are elementarily equivalent without being isomorphic.

In this paper, we shall use our previous results to describe precisely the models of the theories of finitely generated finite-by-abelian groups and the elementary embeddings between these models.