We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.

Die Verbandstheorie ist bekanntlich von Dedekind an Hand seiner idealtheoretischen Untersuchungen begründet worden. Es hat sich in letzter Zeit herausgestellt, daß die wesentliche Eigenschaft des Dedekind'schen Idealsystems darin liegt, daß die Ideale einen Halbverband (§1) bilden. Die Idealtheorie führt so auf die Frage nach alien Halbverbänden über einer beliebigen halbgeordneten Menge M. Die einfache Antwort enthält §2. Ebenso einfach ist die Frage nach alien distributiven Verbänden uber M zu beantworten. In beiden Fällen ist unter den Halbverbänden bzw. distributiven Verbänden über M einer dadurch ausgezeichnet, daß alle anderen homomorph zu ihm sind. Diesen ausgezeichneten Halbverband bzw. distributiven Verband nennen wir den freien Halbverband bzw. freien distributiven Verband über M.

Zu neuen Fragen kommt man bei der Untersuchung speziellerer Halbverbände über M. Es ist z.B. bekannt, daß M stets zu einem vollständigen Boole'schen Verband erweitert werden kann. Gibt es unter diesen Erweiterungen stets den freien vollständigen Boole'schen Verband über M, der dadurch ausgezeichnet ist, daß alle anderen zu ihm homomorph sind ?

In §3 wird zunächst die Existenz des freien orthokomplementären Halbverbandes über M bewiesen. Mit Hilfe der hier benutzten Methode läßt sich auch der Existenzbeweis für den freien abzählbar-vollständigen Boole'schen Verband über M führen.

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.

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.

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.

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.

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.

§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.

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.

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.

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.

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 ∈ ℐ).

We generalize the Bolzano-Weierstrass theorem (that every bounded sequence of reals admits a convergent subsequence) on ideal convergence. We show examples of ideals with and without the Bolzano-Weierstrass property, and give characterizations of BW property in terms of submeasures and extendability to a maximal P-ideal. We show applications to Rudin-Keisler and Rudin-Blass orderings of ideals and quotient Boolean algebras. In particular we show that an ideal does not have BW property if and only if its quotient Boolean algebra has a countably splitting family.

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∞ω.

The modern problem of infinity was first raised by Aristotle who held (at least on the popular interpretation) that infinite sets exist potentially (i.e. one more number can always be counted, one more division can always be made in a line segment) but not actually (i.e. the numbers or divisions cannot all exist at one time). In fact, Aristotle not only held that completed infinities never actually exist, but also that they are impossible, that is, that the assumption that they do exist leads to contradictions. To see this, consider Aristotle's view that mathematical entities depend for their existence on the existence of primary substance in which they inhere, coupled with his view that there can be no infinite body. From these it follows that if there were actual completed infinities, infinite bodies would both exist and not exist. The details here are not so important as the idea that if a completed infinite is assumed to exist a contradiction follows.

This negative attitude towards completed infinities flourished for centuries. By the mid-1500's, the German mathematician Stifel (who apparently also invented Pascal's triangle) was moved to condemn irrational numbers simply by their association with the completed infinite:

About a hundred years later, Galileo further discredited the completed infinite by pointing out that line segments of different lengths can be brought into one-to-one correspondence by projection, as can the natural numbers and the perfect squares by assigning each number to its square.

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].

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 be a relational system whereby D is a nonempty set and P1 is an m1-ary relation on D. With we associate the (weak) monadic second-order theory consisting of the first-order predicate calculus with individual variables ranging over D; monadic predicate variables ranging over (finite) subsets of D; monadic predicate quantifiers; and constants corresponding to P1, P2, …. We will often use ambiguously to mean also the set of true sentences of .