If a formal theory T is able to reason about its own syntax, then the diagonalizable algebra of T is defined as its Lindenbaum sentence algebra endowed with a unary operator □ which sends a sentence φ to the sentence □φ asserting the provability of φ in T. We prove that the first order theories of diagonalizable algebras of a wide class of theories are undecidable and establish some related results.

The main concern of this paper is the design of a noetherian and confluent normalization for LK2 (that is, classical second order predicate logic presented as a sequent calculus).

The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of ‘programming-with-proofs’ ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making.

A comparison of our method to that of embedding LK into LJ (intuitionistic sequent calculus) brings to the fore the latter's defects for these ‘deconstructive purposes’.

In the twenties Brouwer established the well-known continuity theorem “every real function is locally uniformly continuous,” [3, 2, 5]. From this theorem one immediately concludes that the continuum is indecomposable (unzerlegbar), i.e., if ℝ = A ∪ B and A ∩ B = ∅ (denoted by ℝ = A + B), then ℝ = A or ℝ = B.

Brouwer deduced the indecomposability directly from the fan theorem (cf. the 1927 Berline Lectures, [7, p. 49]).

The theorem was published for the first time in [6], it was used to refute the principle of the excluded middle: ¬∀x ∈ ℝ (x ∈ ℚ ∨ ¬x ∈ ℚ).

The indecomposability of ℝ is a peculiar feature of constructive universa, it shows that ℝ is much more closely knit in constructive mathematics, than in classically mathematics. The classically comparable fact is the topological connectedness of ℝ. In a way this characterizes the position of ℝ: the only (classically) connected subsets of ℝ are the various kinds of segments. In intuitionistic mathematics the situation is different; the continuum has, as it were, a syrupy nature, one cannot simply take away one point. In the classical continuum one can, thanks to the principle of the excluded third, do so. To put it picturesquely, the classical continuum is the frozen intuitionistic continuum. If one removes one point from the intuitionistic continuum, there still are all those points for which it is unknown whether or not they belong to the remaining part.

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.

Let κ be an uncountable cardinal and the edges of a complete graph with κ vertices be colored with ℵ0 colors. For the Erdős-Rado theorem implies that there is an infinite monochromatic subgraph. However, if , then it may be impossible to find a monochromatic triangle. This paper is concerned with the latter situation. We consider the types of colorings of finite subgraphs that must occur when . In particular, we are concerned with the case ℵ1 ≤ κ ≤ ℵω.

The study of these color patterns (known as identities) has a history that involves the existence of compactness theorems for two cardinal models [4]. When the graph being colored has size ℵ1, the identities that must occur ((ℵ1)) have been classified by Shelah [6]. If the graph has size greater than or equal to ℵω the identities that must occur ((ℵω)) have also been classified in [5]. This leaves open the question of how the sets (ℵm) (2 ≤ m < ω) fit between (ℵ1) and ⊆ (ℵω). Some progress in this direction has been made in the paper [2]. It is there shown that if ZFC is consistent then so is for each m < ω. The number of colors is fixed at ℵ0 as it is the natural place to start and the results here can be generalized to more colors. We first give some definitions and establish some notation.

It is well known that if σ is a strongly compact cardinal and λ a regular cardinal ≥ σ, then for every stationary subset X of {α < λ: cof (α) = ω} there is some β < λ such that X ⋂ β is stationary in β. In fact the existence of a uniform, countably complete ultrafilter over λ is sufficient to prove the same conclusion about stationary subsets of {α < λ: cof (α) = ω}. See [13] or [10]. By analyzing the proof of this theorem as presented in [10], we realized the same conclusion will follow from the existence of a certain ideal, not necessarily prime, on . Throughout we will assume that σ is a regular uncountable cardinal and use the word “ideal” to mean fine ideal.

In this paper we prove Jensen's Coding Theorem, assuming ˜ 0#, via a proof that makes no use of the fine structure theory. We do need to quote Jensen's Covering Theorem, whose proof uses fine-structural ideas, but make no direct use of these ideas. The key to our proof is the use of “coding delays.”

Coding Theorem (Jensen). Suppose 〈M,A〉 is a model of ZFC + O#does not exist. Then there is an 〈M, A〉-definable class forcing P such that if G ⊆ P is P-generic over 〈M, A〉:

(a) 〈M[G],A,G〉 ⊨ NZFC.

(b) M[G] ⊨ V = L[R], R ⊆ ωand 〈M[G], A, G〉 ⊨ A,G are definable from the parameter R.

In the above statement when we say “〈M, A〉 ⊨ ZFC” we mean that M ⊨ ZFC and in addition M satisfies replacement for formulas that mention A as a predicate. And “P-generic over 〈M, A〉” means that all 〈M, A〉-definable dense classes are met.

The consequence of ˜ O# that we need follows directly from the Covering Theorem.

We show here that the first order theory of the positive integers equipped with multiplication remains decidable when one adds to the language the usual order restricted to the prime numbers. We see moreover that the complexity of the latter theory is a tower of exponentials, of height O(n).

A boolean algebra is shown to be completely representable if and only if it is atomic, whereas it is shown that neither the class of completely representable relation algebras nor the class of completely representable cylindric algebras of any fixed dimension (at least 3) are elementary.

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.

The main result of this note is showing that if γ and μ are regular uncountable cardinals with γ ≤ μ then the non-stationary ideal (henceforth the NS ideal) on can be precipitous. This strengthens a result of [1] showing, under the same hypotheses, that a restriction of this ideal can be precipitous. See [1, Theorem 29, p. 36]. In fact, we show that even the strongly NS ideal on is precipitous in our model (since the former ideal is a restriction of the latter, the latter's being precipitous is a stronger assertion).

More precisely, by starting with a model of “ZFC + ‘κ is a supercompact cardinal’ + ‘μ < κ is a regular uncountable cardinal’ ”, we generate a model of ZFC where all cardinals below and including μ are not collapsed and where the NS and strongly NS ideals on Pγμ are precipitous, for all regular uncountable γ which are less than or equal to μ.

As far as consistency strength, we can obtain the same result even if κ is only Woodin in the ground model. However, the proof of this result is more complicated than in the case when κ is a supercompact cardinal. Furthermore, there are essentially no new ideas in adapting the proof relative to a supercompact cardinal to that relative to a Woodin cardinal beyond what appears in, e.g., [2]. We therefore give the complete proof relative to the existence of a supercompact cardinal and then briefly sketch the proof relative to the existence of a Woodin cardinal, using [2] as a reference.

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 prove that no restriction of the sine function to any (open and nonempty) interval is definable in 〈R, +, ·, ×, <, exp, constants〉, and that no restriction of the exponential function to an (open and nonempty) interval is definable in 〈R, +, ·, <, sin0, constants〉, where sin0(x) = sin(x) for x ∈ [—π, π], and sin0(x) = 0 for all x ∉ [—π, π].

Gurevich and Shelah have shown that Peano Arithmetic cannot be interpreted in the monadic second-order theory of short chains (hence, in the monadic second-order theory of the real line). We will show here that it is consistent that the monadic second-order theory of no chain interprets Peano Arithmetic.

Tense logics formulated in the bimodal propositional language are investigated with respect to Kripke-completeness (completeness) and decidability. It is proved that all minimal tense extensions of modal logics of finite width (in the sense of K. Kine) as well as all minimal tense extensions of cofinal subframe logics (in the sense of M. Zakharyaschev) are complete. The decidability of all finitely axiomatizable minimal tense extensions of cofinal subframe logics is shown. A number of variations and extensions of these results are also presented.

In 1965, during the first All-Union Symposium on Group Theory, Kargapolov presented the following two problems: (a) describe the universal theory of free nilpotent groups of class m; (b) describe the universal theory of free groups (see [18, 1.28 and 1.27]). The first of these problems is still open and it is known [25] that a positive solution of this problem for an m ≤ 2 should imply the decidability of the universal theory of the field of the rationals (this last problem is equivalent to Hilbert's tenth problem for the field of the rationals which is a difficult open problem; see [17] and [20] for discussions on this problem). Regarding the second problem, Makanin proved in 1985 that a free group has a decidable universal theory (see [15] for stronger results), however, the problem of deriving an explicit description of the universal theory of free groups is open. To try to solve this problem Remeslennikov gave different characterization of finitely generated groups with the same universal theory as a noncyclic free group (see [21] and [22] and also [11]). Recently, the author proved in [8] that a free metabelian group has a decidable universal theory, but the proof of [8] does not give an explicit description of the universal theory of free metabelian groups.

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.

There are inequalities between cardinal characteristics of the continuum that are true in any model of ZFC, but without a Borel morphism proving the inequality. We answer some questions from Blass [1].

The model theoretic ‘back and forth’ construction of isomorphisms and automorphisms is based on the proof by Cantor that the theory of dense linear orderings without endpoints is ℵ0-categorical. However, Cantor's method is slightly different and for many other structures it yields an injection which is not surjective. The purpose here is to examine Cantor's method (here called ‘going forth’) and to determine when it works and when it fails. Partial answers to this question are found, extending those earlier given by Cameron. We also give fuller characterisations of when forth suffices for model theoretic classes such as structures containing Jordan sets for the automorphism group, and ℵ0-categorical ω-stable structures. The work is based on the author's Ph.D. thesis.