It is a well known fact that Zermelo's Axiom of Choice and Zorn's Lemma are equivalent logical assumptions. However, an investigation from the viewpoint of the hierarchy of types reveals a complication in the nature of this equivalence. In a type-theoretical formalism both postulates enter as spectra (ZAα) and (ZLα) of formulas, where ZAα is Zermelo's Axiom and ZLα is Zorn's Lemma stated for variables of a fixed type α. The complication has its origin in the fact that, although the formula ZAα implies ZLα, in order to deduce ZAα it seems to be necessary to assert Zorn's Lemma ZLβ for a type β which is higher than α. In other words, we don't know a proof assuring the equivalence of the two formulas ZAα and ZLα. Therefore the equivalence of Zermelo's Axiom and Zorn's Lemma has to be understood in the sense that the assertion of the formulas ZAα for all types α implies every one of the formulas ZLβ and conversely the assertion of the spectrum of formulas (ZLα) implies every one of the formulas ZAβ.

In § 3 we shall indicate a type β which makes the deduction of ZAα from ZLβ possible. For this purpose a proof by G. Birkhoff [3] is translated into type-theoretical language.

In § 2 it is shown that ZAα implies ZLα. In this proof no use is made of the notion of well-ordering. Specifically, we do not first deduce the Well-Ordering Theorem as it is usually done in proving Zorn's Lemma from Zermelo's Axiom. However, the method is suggested by Zermelo's second proof of the Well-Ordering Theorem [2].

In [2] we constructed an infinite set of natural numbers containing no subset of higher (Turing) degree. Since it is well known that there are nonrecursive sets (e.g. sets of minimal degree) containing no nonrecursive subset of lower degree, it is natural to suppose that these arguments may be combined, but this is false. We prove that every infinite set must contain a nonrecursive subset of either higher or lower degree.

Throughout this paper denotes a nonprincipal ultrafilter and ℐ denotes the dual ideal. ℙ(ℐ) is the poset of all partial functions p: ω → 2 such that dom(p) ∈ ℐ. In [2], Grigorieff proved that ω1 is preserved in the corresponding generic extension if and only if is a P-point. Later, when Shelah introduced the notion of a proper poset, many people observed that if is a P-point, then ℙ(ℐ) is proper. One way of proving this is to show that player II has a winning strategy in the game for ℙ(ℐ) (see [3, p. 91].)

The notion of an Axiom A poset was introduced by Baumgartner [1]. If a poset satisfies Axiom A, then player II has a winning strategy in the game for ℙ, and thus, ℙ is proper. Indeed most of the naturally occurring proper posets satisfy Axiom A (e.g., Mathias's poset and Laver's poset). Thus, it is natural to ask whether or not ℙ(ℐ) satisfies Axiom A. The main result of this paper is a negative answer to this question. We will prove this by introducing another game and showing that is a P-point if and only if the corresponding game is undetermined. We will then show that if ℙ(ℐ) satisfied Axiom A, then player II would have a winning strategy in the corresponding game .

We let [X]<ω = {s ⊆ X∣ ∣s∣ < ω}. We let Seq(X) denote the set of finite sequences of elements of X. If s = 〈x0, …, xn〉 ∈ Seq(X) and y ∈ X, then s * 〈y〉 = 〈x0,…,xn,y〉 ∈ Seq(X).

In this note we sketch a decision procedure for S3.51 based on reduction to conjunctive normal form. Using the following theorem of S3.5: and its dual for M over a conjunction, any formula can be reduced by standard methods (as in S52) to a conjunction of disjunctions of the form where Í is (p ⊃ p), 0 is ∼(p ⊃ p) and α — λ are all PC-wffs (i.e. they contain no modal operators).

The aim of this paper is to present a decision procedure which seems to be as easy to use as other available procedures in quantification theory, but which is considerably stronger than the others, providing a mechanical test for a sub-species of polyadic validity which is very much broader than monadic validity. Of course, a test for polyadic validity in general is out of the question, but the present test's limits, short of polyadic validity, are not known. That is, of all the polyadically valid schemata which have been tested, ncne has failed to yield decisions under this method. The material thus examined includes schemata corresponding to the cases of all absolute metatheorems in ML's Chapters II and III, and five polyadic samples from MeL. The handiness of this test is illustrated by sample applications in § 3 below.

Using a technique developed by Coquand and Hofmann [3] we verify that adding the analytical form MP1: $\forall \alpha (\neg \neg \exists {\rm{x}}\alpha ({\rm{x}}) = 0 \to \exists {\rm{x}}\alpha ({\rm{x}}) = 0)$ of Markov’s Principle does not increase the class of ${\rm{\Pi }}_2^0$ formulas provable in Kleene and Vesley’s formal system for intuitionistic analysis, or in subsystems obtained by omitting or restricting various axiom schemas in specified ways.

We show that a solution to Hilbert's Tenth Problem in the rings of algebraic integers and bigger subrings of number fields where it is currently not known, is equivalent to a problem of bounding archimedean valuations over non-real number fields.

We present sharpened lower bounds on the size of cut free proofs for first-order logic. Prior lower bounds for eliminating cuts from a proof established superexponential lower bounds as a stack of exponentials, with the height of the stack proportional to the maximum depth d of the formulas in the original proof. Our results remove the constant of proportionality, giving an exponential stack of height equal to d − O(1). The proof method is based on more efficiently expressing the Gentzen–Solovay cut formulas as low depth formulas.