Schnorr randomness is a notion of algorithmic randomness for real numbers closely related to Martin-Löf randomness. After its initial development in the 1970s the notion received considerably less attention than Martin-Löf randomness, but recently interest has increased in a range of randomness concepts. In this article, we explore the properties of Schnorr random reals, and in particular the c.e. Schnorr random reals. We show that there are c.e. reals that are Schnorr random but not Martin-Löf random, and provide a new characterization of Schnorr random real numbers in terms of prefix-free machines. We prove that unlike Martin-Löf random c.e. reals, not all Schnorr random c.e. reals are Turing complete, though all are in high Turing degrees. We use the machine characterization to define a notion of “Schnorr reducibility” which allows us to calibrate the Schnorr complexity of reals. We define the class of “Schnorr trivial” reals, which are ones whose initial segment complexity is identical with the computable reals, and demonstrate that this class has non-computable members.

In a paper in this Journal [1], McKinsey used as a criterion for the independence (non-definability) of a connective F in a propositional calculus L, the existence of a matrix for L in which the functions corresponding to all the connectives other than F are class-closing over some subset S of the elements, while the function corresponding to F is not class-closing over S (i.e., for a certain choice of arguments in S its value is not in S).

This paper concerns certain relationships between the ordering of degrees of unsolvability and the jump operation. It is shown that every minimal degree a < 0′ satisfies a″ = 0″. To restate this result in more suggestive language and compare it with related results, we shall use notation based on the now standard terminology of “high” and “low” degrees. Let Hn be the class of degrees a < 0′ such that a(n) = 0(n+1), and let Ln be the class of degrees a ≤ 0′ such that an = 0n. (Observe that Hi ⊆ Lj and Li ⊆ Lj, whenever i ≤ j, and Hi ∩ Lj = ∅ for all i andj.) The result mentioned above may now be restated in the form that every minimal degree a ≤ 0′ is in L2. This extends an earlier result of S. B. Cooper ([1], see also [4]) that no minimal degree a < 0′ is in H1. In the other direction, Sasso, Epstein, and Cooper ([10], [15]) have shown that there is a minimal degree a < 0′ which is not in L1. Also, C.E.M. Yates [14, Corollary 11.14], showed the existence of a minimal degree a < 0′ in L1. Thus each minimal degree a < 0′ lies in exactly one of the two classes L1L2 – L1 and each of the classes contains minimal degrees.

Our results are not restricted to the degrees below 0′. We show in fact that every minimal degree a satisfies a″ = (a ∪ 0′)′. To restate this result and discuss extensions of it, we extend the “high-low” classification of degrees from the degrees below 0′ to degrees in general. There are a number of fairly plausible ways of doing this, but we choose the one way we know of doing so which leads to interesting results. Let GHn be the class of degrees a such that a(n) = (a ∪ 0′)(n), and let GLn be the class of degrees a such that a(n) = (a ∪ 0′)(n−1).

The so-called Curry-Howard interpretation (Curry [1934], Curry and Feys [1958], Howard [1969], Tait [1965]) is known to provide a rather neat term-functional account of intuitionistic implication. Could one refine the interpretation to obtain an almost as good account of other neighbouring implications, including the so-called ‘resource’ implications (e.g. linear, relevant, etc.)?

We answer this question positively by demonstrating that just by working with side conditions on the rule of assertability conditions for the connective representing implication (‘→’) one can characterise those ‘resource’ logics. The idea stems from the realisation that whereas the elimination rule for conditionals (of which implication is a particular case) remains virtually unchanged no matter what kind of conditional one has (i.e. linear, relevant, intuitionistic, classical, etc., all have modus ponens), the corresponding introduction rule carries an element of vagueness which can be explored in the characterisation of several sorts of conditionals. The rule of →-introduction is classified as an ‘improper’ inference rule, to use a terminology from Prawitz [1965]. Now, the so-called improper rules leave room for manoeuvre as to how a particular logic can be obtained just by imposing conditions on the discharge of assumptions that would correspond to the particular logical discipline one is adopting (linear, relevant, ticket entailment, intuitionistic, classical, etc.). The side conditions can be ‘naturally’ imposed, given that a degree of ‘vagueness’ is introduced by the presentation of those improper inference rules, such as the rule of →-introduction:

which says: starting from assumption ‘A’, and arriving at ‘B’ via an unspecified number of steps, one can discharge the assumption and conclude that ‘A’ implies ‘B’.

Introduction. In setting up his definition of analyticity, Carnap uses various non-constructive rules, of which we shall be concerned with only one. This one we shall call simply “Carnap's rule.” It can be roughly stated thus: If f(0), f(1), f(2), … are all provable, then (x)f(x) shall be provable.

In this paper will be briefly considered the logics got by starting with the system of Principia plus Peano's axioms and allowing one, two, …, ω, ω+l, and so on up to, but not including ω uses of Carnap's rule (interspersed with uses of the ordinary rules), as well as the system which includes Principia and Peano's axioms and is closed under application of Carnap's rule and the ordinary rules. Under suitable assumptions as to consistency, it is shown that in each of these logics there occur undecidable propositions and that a formula which states the consistency of the logic exists in the logic but is not provable in the logic. An interesting side result is that the logic got by allowing co applications of Carnap's rule is not closed under Carnap's rule.

The paper establishes the general structure of the inconsistent models of arithmetic of [7]. It is shown that such models are constituted by a sequence of nuclei. The nuclei fall into three segments: the first contains improper nuclei: the second contains proper nuclei with linear chromosomes: the third contains proper nuclei with cyclical chromosomes. The nuclei have periods which are inherited up the ordering. It is also shown that the improper nuclei can have the order type of any ordinal, of the rationals, or of any other order type that can be embedded in the rationals in a certain way.

Davis, Matijasevic, and Robinson, in their admirable survey article [D-M-R], interpret the negative solution of Hilbert's Tenth Problem as a resounding positive statement about the versatility of Diophantine equations (that any listable set can be coded as the set of parameter values for which a suitable polynomial possesses integral solutions).

One can also view the Matijasevic result as implying that there are families of Diophantine equations parametrized by a variable t, which have integral solutions for some integral values t = a > 0, and yet there is no computable function of t which provides an upper bound for the smallest integral solution for these values a. The smallest integral solutions of the Diophantine equation for these values are, at least sporadically, too large to be bounded by any computable function. This is somewhat difficult to visualize, since there is quite an array of computable functions. But let us take an explicit example. Consider the function

Matijasevic's result guarantees the existence of parametrized families of Diophantine equations such that even this function fails to yield an upper bound for its smallest integral solutions (for all values of the parameter t for which there are integral solutions).

Families of Diophantine equations in a parameter t, whose integral solutions for t = 1, 2, 3,… exhibit a certain arythmia in terms of their size, have fascinated mathematicians for centuries, and this phenomenon (the size of smallest integral solution varying wildly with the parameter-value) is surprising, even when the equations are perfectly “decidable”.

A completeness theorem is established for logics with congruence endowed with general semantics (in the style of general frames). As a corollary, completeness is shown to be preserved by fibring logics with congruence provided that congruence is retained in the resulting logic. The class of logics with equivalence is shown to be closed under fibring and to be included in the class of logics with congruence. Thus, completeness is shown to be preserved by fibring logics with equivalence and general semantics. An example is provided showing that completeness is not always preserved by fibring ligics endowed with standard (non general) semantics. A categorial characterization of fibring is provided using coproducts and cocartesian liftings.

Tarski's writings on the concepts of truth and logical consequence rank among the most influential works in both logic and philosophy of the twentieth century. Because of this, it would be impossible to give a careful and accurate account of how far that influence reaches and of the complex route by which it spread. In logic, Tarski's methods of defining satisfaction and truth, as well as his work pioneering general model-theoretic techniques, have been entirely absorbed into the way the subject is presently done; they have become part of the fabric of contemporary logic, material presented in the initial pages of every modern textbook on the subject. In philosophy, the influence has been equally pervasive, extending not only to work in semantics and the philosophies of logic and language, but to less obviously allied areas such as epistemology and the philosophy of science as well.

Rather than try to chart the wide-ranging influence of these writings or catalog the important research they have inspired, I will concentrate on various confusions and misunderstandings that continue to surround this work. For in spite of the extensive attention the work has received in the past fifty years, especially in the philosophical literature, misunderstandings of both conceptual and historical sorts are still remarkably widespread. Indeed in the philosophical community, recent reactions to Tarski's work on truth range from Karl Popper's “intense joy and relief” at Tarski's “legitimation” of the notion [1974, p. 399], to Hilary Putnam's assessment that “as a philosophical account of truth, Tarski's theory fails as badly as it is possible for an account to fail” [1985, p. 64]. Opinions have not exactly converged.

According to Gödel's completeness theorem, every consistent theory1 has a model whose domain is a set of natural numbers. The objects of the model corresponding to the predicate symbols of the theory are then predicates of natural numbers. Kleene [5] p. 398 showed that, if the theory is axiomatizable,2 then the model can be chosen so that these predicates are in both two-quantifier forms, i.e., they can be expressed in both the forms (x)(Ey)R and (Ex)(y)S with R and S recursive. An alternative proof has been given by Hasen jaeger [3].

The modal logic GL has been found by Solovay [13] to formalize the provable propositional properties of the provability-predicate for Peano's Arithmetic PA (cf. §1 below). We give several sequential calculi for GL, compare their merits, and use one calculus to syntactically derive several metamathematical results about GL.

Some of our results have been proved model theoretically, and similar proofs are fairly straightforward for several of the remaining ones (G. Boolos and the referee have provided such proofs for 4.1, 4.3 and 5.1 below). However, our syntactic techniques often yield more concise and obviously constructive proofs, they offer additional insight into the nature of the systems considered, and are easily adaptable to systems for which semantical analysis is problematic.

I am indebted to G. Boolos and to the referee for their valuable advice. The referee has suggested the rule GL of §3 below as an axiomatization of GL; the resulting sequential calculus has allowed a definite improvement of our original presentation.

Several extensions of the basic modal language are characterized in terms of interpolation. Our main results are of the following form: Language L′ is the least expressive extension of L with interpolation. For instance, let ℳ(D) be the extension of the basic modal language with a difference operator [7], First-order logic is the least expressive extension of ℳ(D) with interpolation. These characterizations are subsequently used to derive new results about hybrid logic, relation algebra and the guarded fragment.

During the past several decades, linguists have developed and applied widely techniques which enable them, to a considerable extent, to determine and state the structure of natural languages without semantic reference. It is of interest to inquire seriously into the formality of linguistic method and the adequacy of whatever part of it can be made purely formal, and to examine the possibilities of applying it, as has occasionally been suggested, to a wider range of problems. In order to pursue these aims it is first necessary to reconstruct carefully the set of procedures by which the linguist derives the statements of a linguistic grammar from the behaviour of language users, distinguishing clearly between formal and experimental in such a way that grammatical notions, appearing as definienda in a constructional system, will be formally derivable for any language from a fixed sample of linguistic material upon which the primitives of the system are experimentally defined. The present paper will be an attempt to formalize a certain part of the linguist's generalized syntax language.

From another point of view, this paper is an attempt to develop an adequate notion of syntactic category within an inscriptional nominalistic framework. The inscriptional approach seems natural for linguistics, particularly in view of the fact that an adequate extension of the results of this paper will have to deal with the problem of homonymity, i.e., with a statement of the conditions under which tokens of the same type must be assigned to different syntactic classes.

A previously unexplored method, combining logical and mathematical elements, is shown to yield substantial numerical improvements in the area of Diophantine approximations. Kreisel illustrated the method abstractly by noting that effective bounds on the number of elements are ensured if Herbrand terms from ineffective proofs of Σ2-finiteness theorems satisfy certain simple growth conditions. Here several efficient growth conditions for the same purpose are presented that are actually satisfied in practice, in particular, by the proofs of Roth's theorem due to Roth himself and to Esnault and Viehweg. The analysis of the former yields an exponential bound of order exp(70ε−2d2) in place of exp(285ε−2d2) given by Davenport and Roth in 1955, where α is (real) algebraic of degree d ≥ 2 and ∣α − pq−1∣ < q−2−ε. (Thus the new bound is less than the fourth root of the old one.) The new bounds extracted from the other proof are polynomial of low degree (in ε−1 and log d). Corollaries: Apart from a new bound for the number of solutions of the corresponding Diophantine equations and inequalities (among them Thue's inequality), log log qν, < Cα, εν5/6+ε, where qν are the denominators of the convergents to the continued fraction of α.

There are a number of open problems involving the concepts of decidability and essential undecidability. This paper will present solutions to some of these problems. Specifically:

(1) Can a decidable theory have an essentially undecidable, axiomatizable extension (with the same constants)?

(2) Are all the complete extensions of an undecidable theory ever decidable?

We shall show that the answer to both questions is in the affirmative. In answering question (1), the decidable theory for which an essentially undecidable axiomatizable extension will be constructed is the theory of the successor function and a single one-place predicate. It will also be shown that the decidability of this theory is a “best possible” result in the following direction: the theory of either of the common diadic arithmetic functions and a one-place predicate; i.e., of addition and a one-place predicate, or of multiplication and a one-place predicate, is undecidable.

Before establishing the main result, it is convenient to give a simple proof that a decidable theory can have an axiomatizable (simply) undecidable extension. This is, of course, an immediate consequence of the main result; but the proof is simple and illustrates the methods that we are going to use in this paper.

1. This paper grew out of an attempt to answer a question raised in [4]. Let a logic L containing “numerals” z1, z2, … and a certain statement N(x) (intended to express the proposition that x is a natural number) be called ω-inconsistent if there is a statement such that ⊦ F(zk) for k = 1, 2, …, and ⊦ ∼(x)·N(x) ⊃ F(x); then it is evident that L cannot have a model in which N(x) is satisfied by the images of the numerals and nothing else if L is ω-inconsistent.

Question: If L is ω-consistent, i.e. not ω-inconsistent, must there be such a model? Calling a model of the kind just described a special model, we ask for necessary and sufficient conditions on L to insure the existence of a special model. We give several sets of such conditions, applicable to a certain very inclusive class of logics, in Theorem 1 and Theorems 3 and 4. Theorem 2 shows that a logic may be ω-consistent but still not have a special model.

This paper was close to completion when [3] appeared. For systems with only denumerably many symbols our results include Henkin's, for, by adjoining a new predicate N(x) to each of the systems considered in [3] which have only a denumerable number of constant symbols and then adding as an axiom (x)N(x), these systems become special cases of the systems we consider. It is easily seen that Henkin's Theorem 7 essentially proves the equivalence of conditions (2) and (3) in our Theorem 1, and Theorem 3 of [3] corresponds to our Theorem 2. Incidentally, our argument of Theorem 2 could also serve to prove Henkin's Theorem 6.

This paper contains some results concerning the completeness of a first-order system of infinite valued logic

There are under consideration two distinct notions of completeness corresponding to the two notions of validity (see Definition 3) and strong validity (see Definition 4). Both notions of validity, whether based on the unit interval [0, 1] or based on linearly ordered MV-algebras, use the element 1 as the designated truth value. Originally, it was thought by many investigators in the field that one should be able to prove that the set of valid sentences is recursively enumerable. It was first proved by Rutledge in [9] that the set of valid sentences in the monadic first-order infinite valued logic is recursively enumerable.

Let ℜ be an expansion of a dense linear order (R, <) without endpoints having the intermediate value property, that is, for all a, b ∈ R, every continuous (parametrically) definable function f: [a, b] → R takes on all values in R between f(a) and f(b). Every expansion of the real line (ℝ, <), as well as every o-minimal expansion of (R, <), has the intermediate value property. Conversely, some nice properties, often associated with expansions of (ℝ, <) or with o-minimal structures, hold for sets and functions definable in ℜ. For example, images of closed bounded definable sets under continuous definable maps are closed and bounded (Proposition 1.10).

Of particular interest is the case that ℜ expands an ordered group, that is, ℜ defines a binary operation * such that (R, <, *) is an ordered group. Then (R, *) is abelian and divisible (Proposition 2.2). Continuous nontrivial definable endo-morphisms of (R, *) are surjective and strictly monotone, and monotone nontrivial definable endomorphisms of (R, *) are strictly monotone, continuous and surjective (Proposition 2.4). There is a generalization of the familiar result that every proper noncyclic subgroup of (ℝ, +) is dense and codense in ℝ: If G is a proper nontrivial subgroup of (R, *) definable in ℜ, then either G is dense and codense in R, or G contains an element u such that (R, <, *, e, u, G) is elementarily equivalent to (ℚ, <, +, 0, 1, ℤ), where e denotes the identity element of (R, *) (Theorem 2.3).

Here is an outline of this paper. First, we deal with some basic topological results. We then assume that ℜ expands an ordered group and establish the results mentioned in the preceding paragraph. Some examples are then given, followed by a brief discussion of analytic results and possible limitations. In an appendix, an explicit axiomatization (used in the proof of Theorem 2.3) is given for the complete theory of the structure (ℚ, <, +, 0, 1, ℤ).

It has been proved by S. C. Kleene and David Nelson that the formula

is intuitionistically non-deducible, i.e., non-deducible within the intuitionistic functional calculus.

The aim of this note is to outline a general method which permits us to establish the intuitionistic non-deducibility of many formulas and in particular of the formula (1).