We investigate the question “To what extent can random reals be used as a tool to establish number theoretic facts?” Let 2-RAN be the principle that for every real X there is a real R which is 2-random relative to X. In Section 2, we observe that the arguments of Csima and Mileti [3] can be implemented in the base theory RCA0 and so RCA0 + 2-RAN implies the Rainbow Ramsey Theorem. In Section 3, we show that the Rainbow Ramsey Theorem is not conservative over RCA0 for arithmetic sentences. Thus, from the Csima–Mileti fact that the existence of random reals has infinitary-combinatorial consequences we can conclude that 2-RAN has non-trivial arithmetic consequences. In Section 4, we show that 2-RAN is conservative over RCA0 + BΣ2 for -sentences. Thus, the set of first-order consequences of 2-RAN is strictly stronger than P− + IΣ1 and no stronger than P− + BΣ2.

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$, the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all $m \ge 1$. We show that, for $m \ge 2$, this subfragment forces $\left\lfloor {m/2} \right\rfloor$-tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$-NExpTime-hard. We further establish that, for $m \ge 3$, any satisfiable ${\cal F}{{\cal L}^m}$-formula has a model of at most ($m - 2$)-tuply exponential size, whence the satisfiability (= finite satisfiability) problem for this fragment is in ($m - 2$)-NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for ${\cal F}{{\cal L}^m}$ for all $m \le 4$.

Fix an integer $r \ge 3$. We consider metric spaces on n points such that the distance between any two points lies in $\left\{ {1, \ldots ,r} \right\}$. Our main result describes their approximate structure for large n. As a consequence, we show that the number of these metric spaces is $\left\lceil {{{r + 1} \over 2}} \right\rceil ^{\left( {\matrix{ n \cr 2 \cr } } \right) + o\left( {n^2 } \right)} .$

Related results in the continuous setting have recently been proved by Kozma, Meyerovitch, Peled, and Samotij [34]. When r is even, our structural characterization is more precise and implies that almost all such metric spaces have all distances at least $r/2$. As an easy consequence, when r is even, we improve the error term above from $o\left( {n^2 } \right)$ to $o\left( 1 \right)$, and also show a labeled first-order 0-1 law in the language ${\cal L}_r $, consisting of r binary relations, one for each element of $[r]$ . In particular, we show the almost sure theory T is the theory of the Fraïssé limit of the class of all finite simple complete edge-colored graphs with edge colors in $\left\{ {r/2, \ldots ,r} \right\}$.

Our work can be viewed as an extension of a long line of research in extremal combinatorics to the colored setting, as well as an addition to the collection of known structures that admit logical 0-1 laws.

In 1970, Kenneth Kunen showed that there is no non-trivial elementary embedding of the universe V into itself [2] using the axiom of choice. Kunen remarked in his paper that the result can be formalized in Morse-Kelley theory of sets and classes. In this paper, we will work within ZF, Zermelo-Fraenkel axioms, and deal with embeddings definable with a formula and a parameter.

In ZF, a “class” is usually synonymous with “property”, that is a class definable with a parameter, C = {x: φ(x,p)}, where φ is a formula in the language [∈}. Using this convention, let j be a class. Then “j is an elementary embedding of V into V” is not a single statement but a schema of statements “j preserves ψ” for each formula ψ. We prove that this schema is expressible in the language {∈} by a single formula:

Lemma. An embedding j: V → V is elementary iff j preservesψ.

Here ψ(α, ψ, a) is the property “a is an ordinal, φ is a formula and Vα.”

The lemma is of course a schema of lemmas, one for each formula denning j and for each ψ to be preserved.

Using this we prove our theorem in ZF (again, a schema of theorems.):

Theorem 1.1. There is no nontrivial definable elementary embedding j: V → V.

Many symbols and their definitions follow those used by Drake's book [1]. The formula Sat expresses the satisfaction relation . The formula Fmla(u) expresses that u is the Gödel-set for a formula.

When the axioms of infinity and choice are added to the system of logic of the second edition of Whitehead and Russell's Principia mathematica, and when, as in the second edition, the axiom of reducibility is omitted (so that the ramified nature of Russell's theory of types, especially his distinction between “orders,” is not in effect obliterated), the resulting system will hereafter be referred to as “the ramified Principia.” It will be shown that a certain system S, slightly stronger than the ramified Principia, is consistent, so that the ramified Principia itself is consistent. From Gödel's theorem it will then follow that the sort of mathematical induction employed in the consistency proof of S cannot be adequately handled within S or within the ramified Principia.

The method of proving the consistency of S will be roughly as follows: A consistent non-constructive system S′ will be defined by means of induction with respect to a serial well-ordering of all the propositions of S. It will then be shown that every true proposition of S is a true proposition of S′, so that S must also be consistent.

1. Preliminary conventions.

1.1. Definition. By a “symbol” is to be understood any typographical expression which does not consist of a horizontal collinear sequence of expressions. Expressions formed by adding indices to either of the two upper or two lower corners of a symbol will also be considered symbols.

The correspondence decision problem was first formulated and shown to be recursively unsolvable in Post (1946). The method of proof was to reduce the known unsolvable decision problem for the class of normal systems on a, b to the correspondence decision problem. In the present paper the concept of a standard Post normal system is used so as to obtain some equivalence reductions of combinatorial systems. In particular the following main result is obtained.

An open U ⊆ ℝ is produced such that (ℝ, +, ·, U) defines a Borel isomorph of (ℝ, +, ·, ℕ) but does not define ℕ. It follows that (ℝ, +, ·, U) defines sets in every level of the projective hierarchy but does not define all projective sets. This result is elaborated in various ways that involve geometric measure theory and working over o-minimal expansions of (ℝ, +, ·). In particular, there is a Cantor set E ⊆ ℝ such that (ℝ, +, ·, ℕ) defines a Borel isomorph of (ℝ, +, ·, ℕ) and, for every exponentially bounded o-minimal expansion of (ℝ, +, ·), every subset of ℝ definable in (, E) either has interior or is Hausdorff null.

Let $ \le _c $ be computable the reducibility on computably enumerable equivalence relations (or ceers). We show that for every ceer R with infinitely many equivalence classes, the index sets $\left\{ {i:R_i \le _c R} \right\}$ (with R nonuniversal), $\left\{ {i:R_i \ge _c R} \right\}$, and $\left\{ {i:R_i \equiv _c R} \right\}$ are ${\rm{\Sigma }}_3^0$ complete, whereas in case R has only finitely many equivalence classes, we have that $\left\{ {i:R_i \le _c R} \right\}$ is ${\rm{\Pi }}_2^0$ complete, and $\left\{ {i:R \ge _c R} \right\}$ (with R having at least two distinct equivalence classes) is ${\rm{\Sigma }}_2^0$ complete. Next, solving an open problem from [1], we prove that the index set of the effectively inseparable ceers is ${\rm{\Pi }}_4^0$ complete. Finally, we prove that the 1-reducibility preordering on c.e. sets is a ${\rm{\Sigma }}_3^0$ complete preordering relation, a fact that is used to show that the preordering relation $ \le _c $ on ceers is a ${\rm{\Sigma }}_3^0$ complete preordering relation.

Strengthening known instances of Vaught Conjecture, we prove the Glimm-Effros dichotomy theorems for countable linear orderings and for simple trees. Corollaries of the theorems answer some open questions of Friedman and Stanley in an Lω1ω-interpretability theory. We also give a survey of this theory.

Ackermann proved termination for a special order of reductions in Hilbert's epsilon substitution method for the first order arithmetic. We establish termination for arbitrary order of reductions.

We study partitions of Fraïssé limits of classes of finite relational structures where the partitions are encoded by infinite binary strings which are random in the sense of Kolmogorov-Chaitin.

In [A1]–[A4] there is an abstract description, in terms of “α-systems”, of the object of a nested priority construction, and there is a metatheorem listing conditions which guarantee the success of the construction. The metatheorem has different versions, with later versions becoming simpler and more general. The information needed to meet the requirements is enumerated by a function, where α is an arbitrary recursive ordinal. All other objects associated with the α-system are r.e. In the basic metatheorem, the requirements must all be at level α, although there is a special result, for limit α, which allows one requirement at each level in an increasing sequence with limit α. There are other abstract descriptions of nested priority arguments in [K1], [K2], [K3], and [L-L].

A typical use of α-systems is that in [B], where it is shown that, for a relation R on a recursive structure , under suitable assumptions, if R does not have a “recursive Σα” definition in , then there is a recursive isomorphic copy of in which the image of R is not . There is no difficulty in generalizing this to make each of infinitely many relations not , when the assumptions are uniformly satisfied and each relation has no recursive Σα definition. However, the metatheorems for α-systems do not apply to the situation where we have several (even two) relations Ri, which do not have recursive Σβi definitions and whose images we wish to make not for distinct βi. An even more basic problem is to construct a recursive copy of a recursive structure via an isomorphism whose restriction to various sets Ui, is not If βi, = α for all i, then we can use an (α + 1)-system; otherwise, the old metatheorems do not apply.

This paper compares the roles classical and intuitionistic logic play in restricting the free use of truth principles in arithmetic. We consider fifteen of the most commonly used axiomatic principles of truth and classify every subset of them as either consistent or inconsistent over a weak purely intuitionistic theory of truth.

We introduce the concept of a locally finite abstract elementary class and develop the theory of disjoint$\left( { \le \lambda ,k} \right)$-amalgamation) for such classes. From this we find a family of complete ${L_{{\omega _1},\omega }}$ sentences ${\phi _r}$ that a) homogeneously characterizes ${\aleph _r}$ (improving results of Hjorth [11] and Laskowski–Shelah [13] and answering a question of [21]), while b) the ${\phi _r}$ provide the first examples of a class of models of a complete sentence in ${L_{{\omega _1},\omega }}$ where the spectrum of cardinals in which amalgamation holds is other that none or all.

In this paper, we investigate connections between structures present in every generic extension of the universe V and computability theory. We introduce the notion of generic Muchnik reducibility that can be used to compare the complexity of uncountable structures; we establish basic properties of this reducibility, and study it in the context of generic presentability, the existence of a copy of the structure in every extension by a given forcing. We show that every forcing notion making ω2 countable generically presents some countable structure with no copy in the ground model; and that every structure generically presentable by a forcing notion that does not make ω2 countable has a copy in the ground model. We also show that any countable structure ${\cal A}$ that is generically presentable by a forcing notion not collapsing ω1 has a countable copy in V, as does any structure ${\cal B}$ generically Muchnik reducible to a structure ${\cal A}$ of cardinality ℵ1. The former positive result yields a new proof of Harrington’s result that counterexamples to Vaught’s conjecture have models of power ℵ1 with Scott rank arbitrarily high below ω2. Finally, we show that a rigid structure with copies in all generic extensions by a given forcing has a copy already in the ground model.

In Handbook of Philosophical Logic M. Dunn formulated a problem of describing pretabular extensions of relevant logics (cf. M. Dunn [1984], p. 211; M. Dunn, G. Restall [2002], p. 79). The main result of this paper is described in the title.

In 1959 M. Dummett [3] introduced the logic LC obtained by adding the axiom ACpqCqp to the formalization of the intuitionistic prepositional calculus having modus ponens and substitution as its rules of inference. Later on R. A. Bull [1] showed, by quite a roundabout way, that the implicational theses of LC were precisely the theses of the implicational calculus obtained by adding the axiom CCCpqrCCCqprr to the system of positive implication. In 1964 Bull [2] gave another proof, this time using results of Birkhoff concerning subdirectly reducible algebras.

The aim of this short note is to emphasize that the use of Gentzen's natural deduction systems (see Prawitz [4]) allows us to give a much more direct proof.

In [2] we described an arithmetic theory of constructions (ATC) and showed that first-order intuitionistic arithmetic (HA) could be interpreted in it. In [3] we went on to show that the interpretation of HA in ATC is faithful. The purpose of the present paper is to apply these ideas to intuitionistic arithmetic in all finite types. Tait has shown [6] that a conservative extension of HA is obtained by adding the Gödel functionals with intuitionistic logic and intensional identity in all finite types. Below we show that this extension remains conservative on the addition of certain axioms of choice which are evident on the intended interpretation of the intuitionistic logical connectives. This theorem (Corollary 6.2 below) was first obtained by a more complicated argument in our dissertation [1]. Some of its implications are discussed in Goodman and Myhill [4].

We assume that the reader is familiar with [2] and [3].

Shoenfield [6] constructed a hierarchy for any type two object F in which 2E is recursive by generalizing the hyperarithmetical hierarchy, using a jump operation jF defined by

(A similar hierarchy was constructed independently by Hinman [3].) In order to construct a hierarchy for an arbitrary type two F we must first associate with F an operator which, on one hand will always be recursive in F, and on the other hand will generate all the functions recursive in F when iterated over a simultaneously generated set of ordinal notations OF. Clearly the use of 2E in the above definition of jF(f) can be avoided if, instead of diagonalizing F over all functions recursive in f, we only diagonalize F over, say, the functions primitive recursive in f. If furthermore we code in a function which enumerates all functions primitive recursive in f then the resulting operation will certainly generate a primitive recursively expanding hierarchy of functions recursive in F. The problem that remains is whether this hierarchy will exhaust the 1-section of F. But this reduces to an effectiyized version of the following problem: If g is recursive in some level of the hierarchy, is g primitive recursive in some higher level ? An affirmative answer is suggested by the completeness results of Feferman [2], and our main theorem below will be proved by combining his ideas with those of Shoenfield [6]. The result is a hierarchy which applies to all type two objects, and which replaces the notion of recursion in F by the simpler notion of primitive recursion in certain functions generated by F. Unfortunately, in contrast with the Shoenfield hierarchy, the hierarchy developed here cannot always be expected to have the uniqueness property (even w.r.t. ≤T), and for this reason the proof of our main theorem is rather more complicated than the corresponding proof in [6].