We present two different types of models where, for certain singular cardinals λ of uncountable cofinality, λ → (λ, ω + 1)2, although λ is not a strong limit cardinal, We announce, here, and will present in a subsequent paper, [7], that, for example, consistently, and consistently, .

The logical system P-W is an implicational non-commutative intuitionistic logic denned by axiom schemes B − (b → c) → (a → b) → a → c. B′ = (a → b) → (b → c) → a → c. I - a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α - β holds if α → β and β → α are both provable in P-W. The answer is affirmative. The first to prove this was E. P. Martin by a semantical method.

In this paper, we give the first proof of Martin's theorem based on the theory of simply typed λ-calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin's Theorem, that any closed hereditary right-maximal linear (HRML) λ-term of type α → α is βη-reducible to λxx. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style.

It is known that there exists a first-order sentence that holds in a finite group if and only if the group is soluble. Here it is shown that the corresponding statements with ‘solubility’ replaced by ‘nilpotence’ and ‘perfectness’, among others, are false.

These facts present difficulties for the study of pseudofinite groups. However, a very weak form of Frattini’s theorem on the nilpotence of the Frattini subgroup of a finite group is proved for pseudofinite groups.

We establish a course-of-values induction principle for K-finite sets in intuitionistic type theory. Using this principle, we prove a pigeonhole principle conjectured by Bénabou and Loiseau. We also comment on some variants of this pigeonhole principle.

The aim of this paper is to give a new proof for the decidability and finite model property of first-order logic with two variables (without function symbols), using a combinatorial theorem due to Herwig. The results are proved in the framework of polyadic equality set algebras of dimension two (Pse2). The new proof also shows the known results that the universal theory of Pse2 is decidable and that every finite Pse2 can be represented on a finite base. Since the class Cs2 of cylindric set algebras of dimension 2 forms a reduct of Pse2, these results extend to Cs2 as well.

Profinite algebras are exactly those that are isomorphic to inverse limits of finite algebras. Such algebras are naturally equipped with Boolean topologies. A variety ${\cal V}$ is standard if every Boolean topological algebra with the algebraic reduct in ${\cal V}$ is profinite.

We show that there is no algorithm which takes as input a finite algebra A of a finite type and decide whether the variety $V\left( {\bf{A}} \right)$ generated by A is standard. We also show the undecidability of some related properties. In particular, we solve a problem posed by Clark, Davey, Freese, and Jackson.

We accomplish this by combining two results. The first one is Moore’s theorem saying that there is no algorithm which takes as input a finite algebra A of a finite type and decides whether $V\left( {\bf{A}} \right)$ has definable principal subcongruences. The second is our result saying that possessing definable principal subcongruences yields possessing finitely determined syntactic congruences for varieties. The latter property is known to yield standardness.

We show that any simple group of Morley rank 4 must be a bad group with no proper definable subgroups of rank larger than 1. We also give an application to groups acting on sets of Morley rank 2.

Theorem. Suppose that k = (K, $$\prec_k$$) is an ℵ0-presentable abstract elementary class with Löwenheim–Skolem number ℵ0, satisfying the joint embedding and amalgamation properties in ℵ0. If K has only countably many models in ℵ1, then all are small. If, in addition, k is almost Galois ω-stable then k is Galois ω-stable. Suppose that k = (K, $$\prec_k$$) is an ℵ0-presented almost Galois ω-stable AEC satisfying amalgamation for countable models, and having a model of cardinality ℵ1. The assertion that K is ℵ1-categorical is then absolute.

We analyze the strength of the existence of idempotent ultrafilters in higher-order reverse mathematics.

Let $\left( {{{\cal U}_{{\rm{idem}}}}} \right)$ be the statement that an idempotent ultrafilter on ℕ exists. We show that over $ACA_0^\omega$, the higher-order extension of ACA0, the statement $\left( {{{\cal U}_{{\rm{idem}}}}} \right)$ implies the iterated Hindman’s theorem (IHT) and we show that $ACA_0^\omega + \left( {{{\cal U}_{{\rm{idem}}}}} \right)$ is ${\rm{\Pi }}_2^1$-conservative over $ACA_0^\omega + IHT$ and thus over $ACA_0^ +$.

Let W0, W1 … be one of the usual enumerations of recursively enumerable (r.e.) subsets of the set N of nonnegative integers. (Background information will be given later.) Suggestions of Anil Nerode led to the following

Definitions. Let B be a subset of N and let ψ be a partial recursive function.

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 show that true first-order arithmetic is interpretable over the real-algebraic structure of models of intuitionistic analysis built upon a certain class of complete Heyting algebras. From this the undecidability of the structures follows. We also show that Scott's model is equivalent to true second-order arithmetic. In the appendix we argue that undecidability on the language of ordered rings follows from intuitionistically plausible properties of the real numbers.

The nonrecursiveness of an arithmetical set can be measured in at least two ways. One way is to consider the level of the set in the arithmetical hierarchy. Another is to consider the degree of unsolvability of the set; more precisely to look at the set of degrees recursive in the degree of the set. The Hierarchy Theorem [1] indicates a correspondence between these two ways of considering the nonrecursiveness of an arithmetical set. The results below indicate some of the contrasts between these two points of view. (It should perhaps be mentioned that, although the results are stated in terms of degrees and levels in the arithmetical hierarchy, they can also be stated, in view of the Hierarchy Theorem, strictly in terms of degrees.)

It is well known that if σ is a strongly compact cardinal and λ a regular cardinal ≥ σ, then for every stationary subset X of {α < λ: cof (α) = ω} there is some β < λ such that X ⋂ β is stationary in β. In fact the existence of a uniform, countably complete ultrafilter over λ is sufficient to prove the same conclusion about stationary subsets of {α < λ: cof (α) = ω}. See [13] or [10]. By analyzing the proof of this theorem as presented in [10], we realized the same conclusion will follow from the existence of a certain ideal, not necessarily prime, on . Throughout we will assume that σ is a regular uncountable cardinal and use the word “ideal” to mean fine ideal.