Using possibly infinite computations on universal monotone Turing machines, we prove Martin-Löf randomness in ∅′ of the probability that the output be in some set under complexity assumptions about .

We explore the interaction between Lebesgue measure and dominating functions. We show, via both a priority construction and a forcing construction, that there is a function of incomplete degree that dominates almost all degrees. This answers a question of Dobrinen and Simpson, who showed that such functions are related to the proof-theoretic strength of the regularity of Lebesgue measure for Gδ sets. Our constructions essentially settle the reverse mathematical classification of this principle.

We consider some natural deduction systems for quantification theory whose only quantificational rules involve elimination of quantifiers. By imposing certain restrictions on the rules, we obtain a system which we term Analytic Natural Deduction; it has the property that the only formulas used in the proof of a given formula X are either subformulas of X, or negations of subformulas of X. By imposing further restrictions, we obtain a canonical procedure which is bound to terminate, if the formula being tested is valid. The procedure (ultimately in the spirit of Herbrand [1]) can be thought of as a partial linearization of the method of semantical tableaux [2], [3]. A further linearization leads to a variant of Gentzen's system which we shall study in a sequel.

The completeness theorem for semantical tableaux rests essentially on König's lemma on infinite graphs [4]. Our completeness theorem for natural deduction uses as a counterpart to König's lemma, a lemma on infinite “nest structures”, as they are to be defined. These structures can be looked at as the underlying combinatorial basis of a wide variety of natural deduction systems.

In § 1 we study these nest structures in complete abstraction from quantification theory; the results of this section are of a purely combinatorial nature. The applications to quantification theory are given in § 2.

We provide a general framework for studying the expansion of strongly minimal sets by adding additional relations in the style of Hrushovski. We introduce a notion of separation of quantifiers which is a condition on the class of expansions of finitely generated models for the expanded theory to have a countable ω-saturated model. We apply these results to construct for each sufficiently fast growing finite-to-one function μ from ‘primitive extensions’ to the natural numbers a theory Tμ of an expansion of an algebraically closed field which has Morley rank 2. Finally, we show that if μ is not finite-to-one the theory may not be ω-stable.

Lachlan [5] has shown that it is not possible to embed the diamond lattice in the r.e. Turing degrees while preserving least and greatest elements; that is, there do not exist incomparable r.e. Turing degrees a and b such that a ∧ b = 0 and a ∨ b = 0′. Cooper [3] has compared the r.e. Turing degrees to the enumeration degrees below 0e′ and has asked if the two structures are elementarily equivalent.

In this paper we show that such an embedding is possible in the Σ2enumeration degrees, which implies a negative answer to Cooper's question.

Theorem. There are low enumeration degreesaandbsuch thata ∧ b = 0eanda ∨ b = 0e′.

Lower case italic letters denote elements of ω while upper case italic letters denote subsets of ω. D, E and F are reserved for finite sets, and K for ′. If D = {x0, x1, …, xn} then the canonical index of D is , and the canonical index of is ∅. Dx denotes the set with canonical index x. {Wi}i∈ω is any fixed standard listing of the r.e. sets, and <·, ·> is any fixed recursive bijection from ω × ω to ω.

Intuitively, A is enumeration reducible to B if there is an effective algorithm for producing an enumeration of A from any enumeration of B. There is a natural one-to-one correspondence between all such algorithms and the r.e. sets.

We show that the structure (C, +, ·) has no proper non locally modular reducts which contain +. In other words, if X ⊂ Cn is constructible and not definable in the module structure (C, +, λa)a Є C (where λa denotes multiplication by a) then multiplication is definable in (C, +, X).

Combinations of capital letters (e.g., G, EVEN) will be used as names of formulas of Peano arithmetic, x, y, z will be variables. Let be a model for Peano arithmetic. The names of formulas with a bar (e.g., G−, EVEN−(x)) will denote the relations defined by the formulas in . The elements of are called numbers.

By a finite sequence of numbers 〈a0, …, an〉 we mean a number . Note that n Pi's and ai's can be nonstandard elements and therefore “finite,” and all concepts which will use it are not absolute but relative to .

In [5] it was shown that to complete Herbrand's argument for his Fundamental Theorem (see [6]) a weak analyzing function for certain applications of the rules of passage is needed. The following theorem describes such a function. (We use the terminology and notation of [5] except that, for each schema S and each p ≧ 1, we shall write D(S,p) rather than DSp for the domain of order p generated by S. In addition, we shall say that an element of D(S, p) is of order k, 1 ≦ k ≦ p, if it belongs to D(S, k) but not to D(S,k—1).)

According to Sobociński's recollection, the consistency of Mereology was proved by Leśniewski by means of an appropriate interpretation within the framework of the theory of real numbers. His proof was never published, but in a recent paper R. E. Clay has succeeded in reconstructing a version of it.1 Clay's result amounts to showing that if Lesniewski's Ontology expanded by the addition of the axioms for the real numbers is consistent then Mereology is consistent. Without casting any doubts on the validity of the proof one can hardly fail to note that here we have a case where the consistency of a conceptually simple theory is made to depend on the consistency of a theory which from the point of view of intuition is far from being obvious.

We prove that the set of all recursive functions cannot be inferred using first-order queries in the query language containing extra symbols [+ , <]. The proof of this theorem involves a new decidability result about Presburger arithmetic which is of independent interest. Using our machinery, we show that the set of all primitive recursive functions cannot be inferred with a bounded number of mind changes, again using queries in [+, <]. Additionally, we resolve an open question in [7] about passive versus active learning.

Emil Post has shown that the word problem for Thue systems is unsolvable. A Thue system is a system of strings of letters x1, x2, …, xr, where a string or word is either void or a succession of letters a1a2 … at with each ai some xi. We are given a finite number of pairs of strings Ai, Bii = 1, …, m. Operations in the Thue system consist of the replacements or “productions.”

An explanation is given of why, after adding to a model M of ZFC first a Solovay real r and next a Cohen real c, in M[r] [c] a Cohen real over M[c] is produced. It is also shown that a Solovay algebra iterated with a Cohen algebra can be embedded into a Cohen algebra iterated with a Solovay algebra.

In this paper we devise some technical tools for dealing with problems connected with the philosophical view usually called mathematical instrumentalism. These tools are interesting in their own right, independently of their philosophical consequences. For example, we show that even though the fragment of Peanos Arithmetic known as IΣ1 is a conservative extension of the equational theory of Primitive Recursive Arithmetic (PRA). IΣ1 has a super-exponential speed-up over PRA. On the other hand, theories studied in the Program of Reverse Mathematics that formalize powerful mathematical principles have only polynomial speed-up over IΣ1.

Frege's conception of reference has been interpreted as calling for a completely extensional language, on the grounds that according to it the reference of a complex expression is a function of the references of its parts. To meet this demand and still allow for oblique contexts, one uses Frege's idea that in an oblique context an expression has as reference what is ordinarily its sense.

A purely extensional formalized intensional logic was constructed in the 1940s by Alonzo Church: his logic of sense and denotation [2], [3]. The ambiguity of the “direct” and “oblique” reference of an expression is avoided. For each denoting expression A there is an expression A denoting its sense, which then replaces A in “oblique” contexts. A consequence of this approach is that for each natural number n, in a context with n-fold embedding of intensional operators A is paraphrased by the result of iterating the operation à n times, so that A is treated as if it were infinitely ambiguous. Church's underlying logic is a simple theory of types, in fact just an expansion of the extensional typed λ-calculus so as to contain ωth-order predicate logic.

In this paper we study a variant of Church's logic that admits a possible-worlds semantics, i.e. a version of Church's Alternative (2) [3, pp. 4–5], [4]. This type of logic has been perspicuously formulated by David Kaplan [11], [12], and we follow his version.

In §1 we formulate Kaplan's logic L-Church-O with two alterations: the typed λ-calculus is replaced by combinators, and unlike Kaplan (but like Church) we allow concepts (that is, senses) that are not concepts of anything.

A statement X in the lower predicate calculus is said to be persistent with respect to the set of statements K ([2], [3]), if whenever X holds in a model M of K then X holds also in all extensions of M which are models of K. If X is persistent with respect to the empty set, then it may be said to be absolutely persistent.

A statement X is called existential, if it is in prenex normal form and does not contain any universal quantifiers. This includes the possibility that X does not contain any quantifiers at all.

Let E be the class of all existential statements. Then it is not difficult to see that E is quasi-disjunctive. That is to say, given statements Y1, Y2 in E, there exists a statement Y in E such that

is provable.

L. Henkin [1] has raised the question how to characterise the statements X which are persistent with respect to a given set K (e.g. a set of axioms for a field or a group) by a syntactical condition. He has shown that, in order that a statement X be absolutely persistent, it is necessary and sufficient that there exist a statement Y ϵ E such that

is provable.

We study computable Polish spaces and Polish groups up to homeomorphism. We prove a natural effective analogy of Stone duality, and we also develop an effective definability technique which works up to homeomorphism. As an application, we show that there is a $\Delta ^0_2$ Polish space not homeomorphic to a computable one. We apply our techniques to build, for any computable ordinal $\alpha $, an effectively closed set not homeomorphic to any $0^{(\alpha )}$-computable Polish space; this answers a question of Nies. We also prove analogous results for compact Polish groups and locally path-connected spaces.

Hirsch and Hodkinson proved, for $3 \le m < \omega $ and any $k < \omega $, that the class $SNr_m {\bf{CA}}_{m + k + 1} $ is strictly contained in $SNr_m {\bf{CA}}_{m + k} $ and if $k \ge 1$ then the former class cannot be defined by any finite set offirst-order formulas, within the latter class. We generalize this result to thefollowing algebras of m-ary relations for which the neat reductoperator $_m $ is meaningful: polyadic algebras with or without equality andsubstitution algebras. We also generalize this result to allow the case wherem is an infinite ordinal, using quasipolyadic algebras inplace of polyadic algebras (with or without equality).

We investigate the relation between intermediate predicate logics based on countable linear Kripke frames with constant domains and Gödel logics. We show that for any such Kripke frame there is a Gödel logic which coincides with the logic defined by this Kripke frame on constant domains and vice versa. This allows us to transfer several recent results on Gödel logics to logics based on countable linear Kripke frames with constant domains: We obtain a complete characterisation of axiomatisability of logics based on countable linear Kripke frames with constant domains. Furthermore, we obtain that the total number of logics defined by countable linear Kripke frames on constant domains is countable.

The Fraenkel-Mostowski method has been widely used to prove independence results among weak versions of the axiom of choice. In this paper it is shown that certain statements cannot be proved by this method. More specifically it is shown that in all Fraenkel-Mostowski models the following hold:

1. The axiom of choice for sets of finite sets implies the axiom of choice for sets of well-orderable sets.

2. The Boolean prime ideal theorem implies a weakened form of Sikorski's theorem.