We show that there is a finite set of tiles which can tile the plane but not in any recursive way. This answers a natural sequel to Hao Wang's problem of the existence of a finite set of tiles which can tile the plane but not in any periodic way. In the proof, an elaboration of Robinson's method of transforming origin-constrained problems into unconstrained problems is applied to Hanf's origin-constrained tiling of Part I. We will assume familiarity with §§2, 3, and 7 of [3].

Following Robinson, we will mark the edges of our tiles with symbols and configurations of arrow heads and tails as well as with colors. The matching condition for abutting tiles will be that the symbols on adjacent edges must be identical, every arrow head must match with a tail, every tail with a head, and the colors must be the same. This is, of course, mathematically equivalent to the original condition which involved only colors. A tiling of the plane by a set of tiles is a covering of the plane with translated copies of the tiles such that adjacent edges of abutting tiles satisfy the above matching condition. A set of tiles is consistent if the plane can be tiled by the set. A set of tiles with a designated origin tile is origin-consistent if there is a tiling of the plane with the origin tile at the center.

A square block of tiles is a tiling if every pair of abutting tiles satisfies the above matching condition. If an origin tile has been designated, a block of tiles is an origin-constrained tiling if it is a tiling with the origin tile at the center. Two blocks have the “same” center row if the blocks are of the same size and have identical center rows or if the smaller block's center row is a centered segment of the larger block's center row.

The problem of treating the semantics of intuitionistic logic within the framework of intuitionistic mathematics was first attacked by E. W. Beth [1]. However, the completeness theorem he thought to have obtained, was not true, as was shown in detail in a report by V. H. Dyson and G. Kreisel [2]. Some vague remarks of Beth's, for instance in his book, The foundations of mathematics , show that he sustained the hope of restoring his proof. But arguments by K. Gödel and G. Kreisel gave people the feeling that an intuitionistic completeness theorem would be impossible [3]. (A (strong) completeness theorem would imply

for any primitive recursive predicate A of natural numbers, and one has no reason to believe this for the usual intuitionistic interpretation.) Nevertheless, the following contains a correct intuitionistic completeness theorem for intuitionistic predicate logic. So the old arguments by Godel and Kreisel should not work for the proposed semantical construction of intuitionistic logic. They do not, indeed. The reason is, loosely speaking, that negation is treated positively.

Although Beth's semantical construction for intuitionistic logic was not satisfying from an intuitionistic point of view, it proved to be useful for the development of classical semantics for intuitionistic logic. A related and essentially equivalent classical semantics for intuitionistic logic was found by S. Kripke [4].

The paper considers the set of first-order polymodal formulas the modal operators in which can be applied to subformulas of at most one free variable. Using a mosaic technique, we prove a general satisfiability criterion for formulas in , which reduces the modal satisfiability to the classical one. The criterion is then used to single out a number of new, in a sense optimal, decidable fragments of various modal predicate logics.

Our ultimate purpose is to give an axiomatic treatment of recursion theory sufficient to develop the priority method. The direct or abstract approach is to keep in mind as clearly as possible the methods actually used in recursion theory, and then to formulate them explicitly. The indirect or experimental approach is to look first for other mathematical theories which seem similar to recursion theory, to formulate the analogies precisely, and then to search for an axiomatic treatment which covers not only recursion theory but also the analogous theories as particular cases.

The first approach is more general because it does not depend on the existence of (familiar) analogues. A concrete mathematical theory, it seems, need have no such analogues and still be important, as e.g. classical number theory. In such a case, an axiomatic treatment may still be useful for exhibiting the mathematical structure of the theory considered and the assumptions on which it rests. However, it will lack one of the most heavily advertised advantages of the axiomatic method, namely, the “economy of thought” which results from an uniform theory for several different and interesting cases: we cannot hope for this if, by hypothesis, we know of only one particular case. In contrast, the second approach, if successful at all, is bound to achieve such “economy” because we start out with several interesting particular cases. Another possible virtue of the second approach is that of field work over insight: the abstract pattern that we are looking for and hoping to formalize in axioms, may not be evident in any one mathematical theory, but may spring to the eye if one happens to look simultaneously at several theories which happen to realize the pattern.

We use models of set theory described in [2] and [3] to prove the consistency of several combinatorial principles, for example:

If ℱ is any filter on N containing all the cofinite sets, then there is a finite-to-one function f: N → N such that f(ℱ) is either the filter of cofinite sets or an ultrafilter.

As a consequence of our combinatorial principles, we also obtain the consistency of:

The partial ordering P of slenderness classes of abelian groups, denned and studied in [4], is a four-element chain.

In the remainder of this Introduction, we shall define our terminology and state the combinatorial principles to be considered. In §2, we shall establish some implications between these principles. In §3, we shall prove our consistency results by showing that the strongest of our principles holds in models of set theory constructed in [2] and [3].

A filter on N will always mean a proper filter containing all cofinite sets; in particular, an ultrafilter will necessarily be nonprincipal. We write N ↗ N for the set of nondecreasing functions from the set N of positive integers into itself. A subset ℐ of N ↗ N is called an ideal if it is closed downward (if f(n) ≤ g(n) for all n and if g ∈ ℐ, then f ∈ ℐ) and closed under binary maximum (if f(n) = max(g(n), h(n)) for all n and if g, h ∈ ℐ then f ∈ ℐ).

The two results of this paper (a theorem and an example) are applications of a device described in section 1. Our notation is that of [4], with which we assume familiarity. It may be worth while to mention in particular the function Φ(n, x) which recursively enumerates the partial recursive functions of one variable, the Cantor enumerating functions J(x, y), K(x), L(x), and the classes F and Q of r.e. (recursively enumerable) and finite sets respectively.

It is possible to “give” a finite set in a way which conveys the maximum amount of information; this may be called “giving explicitly”, and it requires that in addition to an effective enumeration or decision procedure for the set we give its cardinal number. It is sometimes desired to enumerate effectively an infinite class of finite sets, each given explicitly (e.g., [4] p. 360, or Dekker [1] p. 497), and we suggest here a device for doing this.

We set up an effective one-to-one correspondence between the finite sets of non-negative integers and these integers themselves: the integer , corresponds to the set αi, = {a1, a2, …, an} and inversely. α0 is the empty set. Clearly i can be effectively computed from the elements of αi and its cardinal number.

This paper is concerned with questions of the following kind: let L be a language of the form Lαω and let be a class of modules over a fixed ring or a class of rings; is it possible to define in L? We will be mainly interested in the cases where L is Lωω or L∞ω and is a familiar class in homologic algebra or ring theory.

In Part I we characterize the rings Λ such that the class of free (respectively projective, respectively flat) left Λ-modules is elementary. In [12] we solved the corresponding problems for injective modules; here we show that the class of injective Λ-modules is definable in L∞ω if and only if it is elementary. Moreover we identify the right noetherian rings Λ such that the class of projective (respectively free) left Λ-modules is definable in L∞ω.

In the course of a recent paper on modal' extensions of the intuitionist propositional calculus, [1], I made some suggestions as to the relationships between the system MIPC, the intuitionist predicate calculus, and the question of producing a genuine intuitionist concept of modality. This paper may be regarded as a clarification of those rather inaccurate ideas in the light of Kripke's outstanding analysis of the intuitionist predicate calculus, [2]. (I use Kripke's notation and terminology here without explanation — this work is intended to be read in conjunction with [2].) In particular, I shall adapt his interpretation of his modelling to give an account of MIPC in terms of differing mathematical intuitions.

Can one extend crisp Peano arithmetic PA by a possibly many-valued predicate Tr(x) saying “x is true” and satisfying the “dequotation schema” for all sentences φ? This problem is investigated in the frame of Łukasiewicz infinitely valued logic.

It is well known that equality is definable in type theory. Thus, in the language of [2], the equality relation between elements of type α is definable as , i.e., xα = yα iff every set which contains xα also contains yα. However, in a nonstandard model of type theory, the sets may be so sparse that the wff above does not denote the true equality relation. We shall use this observation to construct a general model in the sense of [2] in which the Axiom of Extensionality is not valid. Thus Theorem 2 of [2] is technically incorrect. However, it is easy to remedy the situation by slightly modifying the definition of general model.

Our construction will show that the Axiom Schema of Extensionality is independent even if one takes as an axiom schema.

We shall assume familiarity with, and use the notation of, [2] and §§2–3 of [1].

The set of equations which use only one variable and hold in all representable relation algebras cannot be derived from any finite set of equations true in all representable relation algebras. Similar results hold for cylindric algebras and for logic with finitely many variables. The main tools are a construction of nonrepresentable one-generated relation algebras, a method for obtaining cylindric algebras from relation algebras, and the use of relation algebras in defining algebraic semantics for first-order logic.

A minimal pair of recursively enumerable (r.e.) degrees is a pair of degrees a, b of nonrecursive r.e. sets with the property that if c ≤ a and c ≤ b then c = 0. Lachlan [2] and Yates [4] independently proved the existence of minimal pairs. It was natural to ask whether for an arbitrary nonzero r.e. degree c there is a minimal pair a, b with a ≤ c and b ≤ c. In 1971 Lachlan and Ladner proved that a minimal pair below c cannot be obtained in a uniformly effective way from c for r.e. c ≠ 0. but the result was never published. More recently Cooper [1] showed that if c is r.e. and c′ = 0″ then there is a minimal pair below c.

In this paper we prove two results:

Theorem 1. There exists a nonzero r.e. degree with no minimal pair below it.

Theorem 2. There exists a nonzero r.e. degree c such that, if d is r.e. and 0 < d ≤ c, then there is a minimal pair below d.

The second theorem is a straightforward variation on the original minimal pair construction, but the proof of the first theorem has some novel features. After some preliminaries in §1, the first theorem is proved in §2 and the second in §3.

I am grateful to Richard Ladner who collaborated with me during the first phase of work on this paper as witnessed by our joint abstract [3]. The many discussions we had about the construction required in Theorem 1 were of great help to me.

Let Γ be the unique (up to isomorphism) countable graph with the following property: (*) Given any two finite disjoint subsets U and V of Γ, there exists a vertex z ∈ Γ joined to every vertex in U and to none in V.

Thus Γ is the countable, universal, homogeneous graph; also known as the random graph. In this paper, we shall study the reducts of Γ Here a reduct of Γ is defined to be a permutation group (G, Γ) such that:

(i) Aut(Γ) ≤ G; and

(ii) G is a closed subgroup of Sym(Γ).

Equivalently, there exists a structure for some language L such that:

(iii) has universe Γ;

(iv) for each R ∈ L, is definable without parameters in Γ; and

(v) G = Aut().

We will give a simple philosophical “proof” of the negation of Cantor's continuum hypothesis (CH). (A formal proof for or against CH from the axioms of ZFC is impossible; see Cohen [1].) We will assume the axioms of ZFC together with intuitively clear axioms which are based on some intuition of Stuart Davidson and an old theorem of Sierpiński and are justified by the symmetry in a thought experiment throwing darts at the real number line. We will in fact show why there must be an infinity of cardinalities between the integers and the reals. We will also show why Martin's Axiom must be false, and we will prove the extension of Fubini's Theorem for Lebesgue measure where joint measurability is not assumed. Following the philosophy—if you reject CH you are only two steps away from rejecting the axiom of choice (AC)—we will point out along the way some extensions of our intuition which contradict AC.

Let P0, …,Pq be predicates, of which at least one has two or more places. By a formula in P0, …, Pq (or simply a formula, when the list P0, …, Pq is fixed, as in this section) is meant any formula whose only symbols, other than sentential connectives, quantifiers, and (individual) variables, are among P0, …, Pq. A realization (or possible model) of such a formula is a system where A is a non-empty set and each Pk is a relation among the elements of A, having the same number of places as Pk.

§0. Introduction. Ask a beginning philosophy of mathematics student why we believe the theorems of mathematics and you are likely to hear, “because we have proofs!” The more sophisticated might add that those proofs are based on true axioms, and that our rules of inference preserve truth. The next question, naturally, is why we believe the axioms, and here the response will usually be that they are “obvious”, or “self-evident”, that to deny them is “to contradict oneself” or “to commit a crime against the intellect”. Again, the more sophisticated might prefer to say that the axioms are “laws of logic” or “implicit definitions” or “conceptual truths” or some such thing.

Unfortunately, heartwarming answers along these lines are no longer tenable (if they ever were). On the one hand, assumptions once thought to be self-evident have turned out to be debatable, like the law of the excluded middle, or outright false, like the idea that every property determines a set. Conversely, the axiomatization of set theory has led to the consideration of axiom candidates that no one finds obvious, not even their staunchest supporters. In such cases, we find the methodology has more in common with the natural scientist's hypotheses formation and testing than the caricature of the mathematician writing down a few obvious truths and preceeding to draw logical consequences.

The central problem in the philosophy of natural science is when and why the sorts of facts scientists cite as evidence really are evidence. The same is true in the case of mathematics. Historically, philosophers have given considerable attention to the question of when and why various forms of logical inference are truth-preserving. The companion question of when and why the assumption of various axioms is justified has received less attention, perhaps because versions of the “self-evidence” view live on, and perhaps because of a complacent if-thenism.

In this paper, following an idea of Christophe Chalons, I propose a new kind of forcing axiom, the Maximality Principle, which asserts that any sentence φ holding in some forcing extension Vℙ and all subsequent extensions Vℙ*ℚ holds already in V. It follows, in fact, that such sentences must also hold in all forcing extensions of V. In modal terms, therefore, the Maximality Principle is expressed by the scheme (◊ □ φ) ⇒ □ φ, and is equivalent to the modal theory S5. In this article, I prove that the Maximality Principle is relatively consistent with ZFC. A boldface version of the Maximality Principle, obtained by allowing real parameters to appear in φ, is equiconsistent with the scheme asserting that Vδ ≺ V for an inaccessible cardinal δ, which in turn is equiconsistent with the scheme asserting that ORD is Mahlo. The strongest principle along these lines is □ , which asserts that holds in V and all forcing extensions. From this, it follows that 0# exists, that x# exists for every set x, that projective truth is invariant by forcing, that Woodin cardinals are consistent and much more. Many open questions remain.

A set A of vertices of a graph G is called d-scattered in G if no two d-neighborhoods of (distinct) vertices of A intersect. In other words, A is d-scattered if no two distinct vertices of A have distance at most 2d. This notion was isolated in the context of finite model theory by Ajtai and Gurevich and recently it played a prominent role in the study of homomorphism preservation theorems for special classes of structures (such as minor closed classes). This in turn led to the notions of wide, almost wide and quasi-wide classes of graphs. It has been proved previously that minor closed classes and classes of graphs with locally forbidden minors are examples of such classes and thus (relativized) homomorphism preservation theorem holds for them. In this paper we show that (more general) classes with bounded expansion and (newly defined) classes with bounded local expansion and even (very general) nowhere dense classes are quasi wide. This not only strictly generalizes the previous results but it also provides new proofs and algorithms for some of the old results. It appears that bounded expansion and nowhere dense classes are perhaps a proper setting for investigation of wide-type classes as in several instances we obtain a structural characterization. This also puts classes of bounded expansion in the new context. Our motivation stems from finite dualities. As a corollary we obtain that any homomorphism closed first order definable property restricted to a bounded expansion class is a restricted duality.

One of the standard ways of proving the consistency of additional hypotheses with the basic axioms of an axiom system is by the construction of what may be described as ‘inner models.’ By starting with a domain of individuals assumed to satisfy the basic axioms an inner model is constructed whose domain of individuals is a certain subset of the original individual domain. If such an inner model can be constructed which satisfies not only the basic axioms but also the particular additional hypothesis under consideration, then this affords a proof that if the basic axiom system is consistent then so is the system obtained by adding to this system the new hypothesis. This method has been applied to axiom systems for set theory by many authors, including v. Neumann (4), Mostowski (5), and more recently Gödel (1), who has shown by this method that if the basic axioms of a certain axiomatic system of set theory are consistent then so is the system obtained by adding to these axioms a strong form of the axiom of choice and the generalised continuum hypothesis. Having been shown in this striking way the power of this method it is natural to inquire whether it has any limitations or whether by the construction of a sufficiently ingenious inner model one might hope to decide other outstanding consistency questions, such as the consistency of the negations of the axiom of choice and continuum hypothesis. In this and two following papers we prove some general theorems concerning inner models for a certain axiomatic system of set theory which lead to the result that as far as a fairly large family of inner models are concerned this method of proving consistency has been exhausted, that no essentially new consistency results can be obtained by the use of this kind of model.

The complexity of a computable function can be measured by considering the time or space required to compute its values. Particular notions of time and space arising from variants of Turing machines have been investigated by R. W. Ritchie [14], Hartmanis and Stearns [8], and Arbib and Blum [1], among others. General properties of such complexity measures have been characterized axiomatically by Rabin [12], Blum [2], Young [16], [17], and McCreight and Meyer [10].

In this paper the speed-up and super-speed-up theorems of Blum [2] are generalized to speed-up by arbitrary total effective operators. The significance of such theorems is that one cannot equate the complexity of a computable function with the running time of its fastest program, for the simple reason that there are computable functions which in a very strong sense have no fastest programs.

Let φi be the ith partial recursive function of one variable in a standard Gödel numbering of partial recursive functions. A family Φ0, Φ1, … of functions of one variable is called a Blum measure on computation providing

(1) domain (φi) = domain (Φi), and

(2) the predicate [Φi(x) = m] is recursive in i, x and m.

Typical interpretations of Φi(x) are the number of steps required by the ith Turing machine (in a standard enumeration of Turing machines) to converge on input x, the space or number of tape squares required by the ith Turing machine to converge on input x (with the convention that Φi(x) is undefined even if the machine fails to halt in a finite loop), and the length of the shortest derivation of the value of φi(x) from the ith set of recursive equations.