The Martin-Steel coarse inner model theory is employed in obtaining new results in descriptive set theory. determinacy implies that for every thin equivalence relation there is a real, N, over which every equivalence class is generic—and hence there is a good (N#) wellordering of the equivalence classes. Analogous results are obtained for and quasilinear orderings and determinacy is shown to imply that every prewellorder has rank less than .

Martin's axiom is equivalent to the statement that the universe is absolute under ccc forcing extensions for Σ1 sentences with a subset of κ, , as a parameter.

Applying the seed concept to Prikry tree forcing ℙμ, I investigate how well ℙμ preserves the maximality property of ordinary Prikry forcing and prove that ℙμ, Prikry sequences are maximal exactly when μ admits no non-canonical seeds via a finite iteration. In particular, I conclude that if μ is a strongly normal supercompactness measure, then ℙμ Prikry sequences are maximal, thereby proving, for a large class of measures, a conjecture of W. Hugh Woodin's.

We investigate the algebraic structure of the upper semi-lattice formed by the recursively enumerable Turing degrees. The following strong generalization of Lachlan's Nonsplitting Theorem is proved: Given n ≥ 1, there exists an r.e. degree d such that the interval [d, 0′] ⊂ R admits an embedding of the n-atom Boolean algebra preserving (least and) greatest element, but also such that there is no (n + 1 )-tuple of pairwise incomparable r.e. degrees above d which pairwise join to 0′ (and hence, the interval [d, 0′] ⊂ R does not admit a greatest-element-preserving embedding of any lattice which has n + 1 co-atoms, including ). This theorem is the dual of a theorem of Ambos-Spies and Soare, and yields an alternative proof of their result that the theory of R has infinitely many one-types.

Let DO denote the principle: Every infinite set has a dense linear ordering. DO is compared to other ordering principles such as O, the Linear Ordering principle, KW, the Kinna-Wagner Principle, and PI, the Prime Ideal Theorem, in ZF, Zermelo-Fraenkel set theory without AC, the Axiom of Choice.

The main result is:

Theorem. AC ⇒ KW ⇒ DO ⇒ O, and none of the implications is reversible in ZF + PI.

The first and third implications and their irreversibilities were known. The middle one is new. Along the way other results of interest are established. O, while not quite implying DO, does imply that every set differs finitely from a densely ordered set. The independence result for ZF is reduced to one for Fraenkel-Mostowski models by showing that DO falls into two of the known classes of statements automatically transferable from Fraenkel-Mostowski to ZF models. Finally, the proof of PI in the Fraenkel-Mostowski model leads naturally to versions of the Ramsey and Ehrenfeucht-Mostowski theorems involving sets that are both ordered and colored.

A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a sequent with a cut-free proof (or with a proof with cut-formulas of restricted form; in particular, with only analytic cuts) with k inferences has an interpolant whose circuit-size is at most k. We give a new proof of the interpolation theorem based on a communication complexity approach which allows a similar estimate for a larger class of proofs. We derive from it several corollaries:

1. (1) Feasible interpolation theorems for the following proof systems:

   1. (a) resolution

   2. (b) a subsystem of LK corresponding to the bounded arithmetic theory (α)

   3. (c) linear equational calculus

   4. (d) cutting planes.

2. (2) New proofs of the exponential lower bounds (for new formulas)

   1. (a) for resolution ([15])

   2. (b) for the cutting planes proof system with coefficients written in unary ([4]).

3. (3) An alternative proof of the independence result of [43] concerning the provability of circuit-size lower bounds in the bounded arithmetic theory (α).

In the other direction we show that a depth 2 subsystem of LK does not admit feasible monotone interpolation theorem (the so called Lyndon theorem), and that a feasible monotone interpolation theorem for the depth 1 subsystem of LK would yield new exponential lower bounds for resolution proofs of the weak pigeonhole principle.

In this paper we develop some basic features of Galois cohomology, specifically the connection between first Galois cohomology groups and principal homogeneous spaces, in a model-theoretic context. “Descent theory” also fits into our approach.

The model theory involved is elementary, and the reader is referred to [2]. It should be said that we make crucial use of Meq in our analysis. The reader is also referred to Poizat's seminal paper “Une theorie de Galois imaginaire” ([6]). Although our results do not depend on Poizat's work, it is in his paper that the model-theoretic context is suggested for a generalised treatment of Galois theory.

Nothing in this paper is particularly deep. We are concerned mainly with translating between the Galois cohomological language and the language of definable sets and definable families of definable sets. We will introduce (in a suitable context) the notion of a definable cocycle (from an automorphism group to a definable group G). The (classical) situation of profinite and continuous cocycles will be a special case. Kolchin's theory of constrained cohomology will be another special case, and our results yield a substantially simpler proof of his Theorem 5 from Chapter VII of [4]. In any case model-theorists will see that definable cocycles correspond to objects with which they are already quite familiar—commuting families of definable bijections.

The role played by real-valued functions in functional analysis is fundamental. One often considers metrics, or seminorms, or linear functionals, to mention some important examples.

We introduce the notion of definable real-valued function in functional analysis: a real-valued function f defined on a structure of functional analysis is definable if it can be “approximated” by formulas which do not involve f. We characterize definability of real-valued functions in terms of a purely topological condition which does not involve logic.

Gentzen's sequential system LJ of intuitionistic logic has two symbols of implication. One is the logical symbol → and the other is the metalogical symbol ⇒ in sequents

Considering the logical system LJ as a mathematical object, we understand that the logical symbols ∧, ∨, →, ¬, ∀, ∃ are operators on formulas, and ⇒ is a relation. That is, φ ⇒ Ψ is a metalogical sentence which is true or false, on the understanding that our metalogic is a classical logic. In other words, we discuss the logical system LJ in the classical set theory ZFC, in which φ ⇒ Ψ is a sentence.

The aim of this paper is to formulate an intuitionistic set theory together with its metatheory. In Takeuti and Titani [6], we formulated an intuitionistic set theory together with its metatheory based on intuitionistic logic. In this paper we postulate that the metatheory is based on classical logic.

Let Ω be a cHa. Ω can be a truth value set of a model of LJ. Then the logical symbols ∧, ∨, →, ¬, ∀x, ∃x are interpreted as operators on Ω, and the sentence φ ⇒ Ψ is interpreted as 1 (true) or 0 (false). This means that the metalogical symbol ⇒ also can be expressed as a logical operators such that φ ⇒ Ψ is interpreted as 1 or 0.

We define a propositionally quantified intuitionistic logic Hπ+ by a natural extension of Kripke's semantics for propositional intuitionistic logic. We then show that Hπ+ is recursively isomorphic to full second order classical logic. Hπ+ is the intuitionistic analogue of the modal systems S5π+, S4π+, S4.2π+, K4π+, Tπ+, Kπ+ and Bπ+, studied by Fine.

We here examine the expressive power of first order logic with generalized quantifiers over finite ordered structures. In particular, we address the following problem: Given a family Q of generalized quantifiers expressing a complexity class C, what is the expressive power of first order logic FO(Q) extended by the quantifiers in Q? From previously studied examples, one would expect that FO(Q) captures LC, i.e., logarithmic space relativized to an oracle in C. We show that this is not always true. However, after studying the problem from a general point of view, we derive sufficient conditions on C such that FO(Q) captures LC. These conditions are fulfilled by a large number of relevant complexity classes, in particular, for example, by NP. As an application of this result, it follows that first order logic extended by Henkin quantifiers captures LNP. This answers a question raised by Blass and Gurevich [Ann. Pure Appl. Logic, vol. 32, 1986]. Furthermore we show that for many families Q of generalized quantifiers (including the family of Henkin quantifiers), each FO(Q)-formula can be replaced by an equivalent FO(Q)-formula with only two occurrences of generalized quantifiers. This generalizes and extends an earlier normal-form result by I. A. Stewart [Fundamenta Inform, vol. 18, 1993].

In this paper we study (self-)applicative theories of operations and binary words in the context of polynomial time computability. We propose a first order theory PTO which allows full self-application and whose provably total functions on = {0, 1}* are exactly the polynomial time computable functions. Our treatment of PTO is proof-theoretic and very much in the spirit of reductive proof theory.

We give positive answers to two open questions from [15]. (1) For every set C countably determined over , if C is then it must be over , and (2) every Borel subset of the product of two internal sets X and Y all of whose vertical sections are can be represented as an intersection (union) of Borel sets with vertical sections of lower Borel rank. We in fact show that (2) is a consequence of the analogous result in the case when X is a measurable space and Y a complete separable metric space (Polish space) which was proved by A. Louveau and that (1) is equivalent to the property shared by the inverse standard part map in Polish spaces of preserving almost all levels of the Borel hierarchy.

Let be the infinitary language obtained from the first-order language of graphs by closure under conjunctions and disjunctions of arbitrary sets of formulas, provided only finitely many distinct variables occur among the formulas. Let p(n) be the edge probability of the random graph on n vertices. It is shown that if p(n) ≪ n−1 satisfies certain simple conditions on its growth rate, then for every , the probability that σ holds for the random graph on n vertices converges. In fact, if p(n) = n−α, α > 1, then the probability is either smaller than for some d > 0, or it is asymptotic to cn−d for some c > 0, d ≥ 0. Results on the difficulty of computing the asymptotic probability are given.

We consider total well-founded orderings on monadic terms satisfying the replacement and full invariance properties. We show that any such ordering on monadic terms in one variable and two unary function symbols must have order type ω, ω2 or ωω. We show that a familiar construction gives rise to continuum many such orderings of order type ω. We construct a new family of such orderings of order type ω2, and show that there are continuum many of these. We show that there are only four such orderings of order type ωω, the two familiar recursive path orderings and two closely related orderings. We consider also total well-founded orderings on Nn which are preserved under vector addition. We show that any such ordering must have order type ωk for some 1 ≤ k ≤ n. We show that if k < n there are continuum many such orderings, and if k = n there are only n!, the n! lexicographic orderings.

Cartesian closed categories (CCCs) have played and continue to play an important role in the study of the semantics of programming languages. An axiomatization of the isomorphisms which hold in all Cartesian closed categories discovered independently by Soloviev and Bruce, Di Cosmo and Longo leads to seven equalities. We show that the unification problem for this theory is undecidable, thus settling an open question. We also show that an important subcase, namely unification modulo the linear isomorphisms, is NP-complete. Furthermore, the problem of matching in CCCs is NP-complete when the subject term is irreducible.

CCC-matching and unification form the basis for an elegant and practical solution to the problem of retrieving functions from a library indexed by types investigated by Rittri. It also has potential applications to the problem of polymorphic type inference and polymorphic higher-order unification, which in turn is relevant to theorem proving and logic programming.

In this paper we prove the Chomsky Conjecture (all languages recognized by the Lambek calculus are context-free) for both the full Lambek calculus and its product-free fragment. For the latter case we present a construction of context-free grammars involving only product-free types.

We show that no formula of first order logic using linear ordering and the logical relation y = 2x can define the property that the size of a finite model is divisible by 3. This answers a long-standing question which may be of relevance to certain open problems in circuit complexity.