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.

We show that the 0-1 law does not hold for the class (∀∃∀ without = ) by finding a sentence in this class which almost surely expresses parity. We also show that every recursive real in the unit interval is the asymptotic probability of a sentence in this class. This expands a result by Lidia Tendera, who in 1994 proved that every rational number in the unit interval is the asymptotic probability of a sentence in the class ∀∃∀ with equality.

An infinite set X is given. D. Gale, in correspondence with J. Mycielski, described the following game in which players one and two play an inning per positive integer: In the nth inning one chooses a finite subset Xn of X, and two chooses a point xn from (X1∪ … ∪Xn)\{x1,…,xn−1}. A play

is won by two if . Gale asked whether two could have a winning strategy which depends for each n on knowledge of only the contents of the set

In mathematical terms, is there a function F defined on the collection of finite subsets of X such that:

for every sequence X1, x1, …, Xn, xn,…. where each Xn is a finite subset

of X and for each n

we have

We shall call a strategy of this sort a remainder strategy for two. If there is some finite subset U of X such that F(U) ∉ U, then F cannot be a winning remainder strategy for two, because one can defeat F by choosing U each inning. So, when studying remainder strategies for two we may as well assume that for each finite set U ⊂ X, F(U) ∈ U.

Let X be an infinite but separable metric space. An open cover of X is said to be large if for each x ϵ X the set {U ϵ : x ϵ U} is infinite. The symbol Λ denotes the collection of large open covers of X. An open cover of X is said to be an ω-cover if for each finite subset F of X there is a U ϵ such that F ⊆ U, and X is not a member of , X is said to have Rothberger's property if there is for every sequence (n : n = 1,2,3,…) of open covers of X a sequence (Un : n = 1,2,3,…) such that:

(1) for each n, Un is a member of n, and

(2) {Un: n = 1,2,3,…} is a cover of X.

Rothberger introduced this property in his paper [2]. For convenience we let denote the collection of all open covers of X.

In [3] it was shown that X has Rothberger's property if, and only if, the following partition relation is true for large open covers of X:

This partition relation means:

for every large cover of X, for every coloring

such that for each U ϵ and each large cover there is an i with a large cover of X,

either there is a large cover such that f({A, B}) = 0 whenever {A,B} ϵ ,

or else there is a which is not point–finite such that f{{A, B}) = 1 whenever {A, B} ϵ .

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.

We analyze Zorn's Lemma and some of its consequences for Boolean algebras in a constructive setting. We show that Zorn's Lemma is persistent in the sense that, if it holds in the underlying set theory, in a properly stated form it continues to hold in all intuitionistic type theories of a certain natural kind. (Observe that the axiom of choice cannot be persistent in this sense since it implies the law of excluded middle.) We also establish the persistence of some familiar results in the theory of (complete) Boolean algebras—notably, the proposition that every complete Boolean algebra is an absolute subretract. This (almost) resolves a question of Banaschewski and Bhutani as to whether the Sikorski extension theorem for Boolean algebras is persistent.

We prove an exponential lower bound on the length of cutting plane proofs. The proof uses an extension of a lower bound for monotone circuits to circuits which compute with real numbers and use nondecreasing functions as gates. The latter result is of independent interest, since, in particular, it implies an exponential lower bound for some arithmetic circuits.

We prove that the class of trees with no branches of cardinality ≤ κ is not RPC definable in L∞κ when κ is regular. Earlier such a result was known for under the assumption κ<κ = κ. Our main result is actually proved in a stronger form which covers also L∞κ (and makes sense there) for every strong limit cardinal λ < κ of cofinality κ.

Let k and l be two multiplicatively independent integers, and let L ⊆ ℕn be a l-recognizable set which is not definable in 〈ℕ; +〉. We prove that the elementary theory of 〈ℕ; +, Vk, L〉, where Vk(x) denotes the greatest power of k dividing x, is undecidable. This result leads to a new proof of the Cobham-Semënov theorem.

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.

The Kleene-Kreisel continuous functionals [6, 7] have been given several alternative characterisations: using Kuratowski's limit spaces (Scarpellini [20]), using their generalisation, filter spaces (Hyland [4]), via hyperfinite functionals (Normann [11]) and perhaps most elegantly using Scott-Ershov domains (Ershov [3], later generalised by Berger [1]). We propose to add yet another characterisation to this list, which may be called model-theoretic in contrast to the others, but which is in fact closely related to Ershov's approach.

We use the notion of logically presented domains developed in Palmgren and Stoltenberg-Hansen [17] (originating in the work of [15]). Certain logical types, i.e., finitely consistent sets of formulas, over the full type structure built from ℕ correspond to the continuous functionals in the sense of Kreisel, or to Kleene's associates, while the elements realising the types correspond to functionals having associates (cf. [6]). To define these—the total types—we make a nonstandard extension of the full type structure. The set of nonstandard elements is sufficiently rich to single out the total types. The nonstandard extension also makes it possible to relate the logical presentation to Ershov's approach. The logical form of the domain constructions allows us to use a (generalised) Fréchet power as a nonstandard extension. This extension is constructive, in the sense that it avoids the axiom of choice, as distinguished from the one employed in [11].

In the present paper we are interested in simple forcing notions and Forcing Axioms. A starting point for our investigations was the article [4] in which several problems were posed. We answer some of those problems here.

In the first section we deal with the problem of adding Cohen reals by simple forcing notions. Here we interpret simple as of small size. We try to establish as weak as possible versions of Martin Axiom sufficient to conclude that some forcing notions of size less than the continuum add a Cohen real. For example we show that MA(σ-centered) is enough to cause that every small σ-linked forcing notion adds a Cohen real (see Theorem 1.2) and MA(Cohen) implies that every small forcing notion adding an unbounded real adds a Cohen real (see Theorem 1.6). A new almost ωω-bounding σ-centered forcing notion ℚ⊚ appears naturally here. This forcing notion is responsible for adding unbounded reals in this sense, that MA(ℚ⊚) implies that every small forcing notion adding a new real adds an unbounded real (see Theorem 1.13).

In the second section we are interested in Anti-Martin Axioms for simple forcing notions. Here we interpret simple as nicely definable. Our aim is to show the consistency of AMA for as large as possible class of ccc forcing notions with large continuum. It has been known that AMA(ccc) implies CH, but it has been (rightly) expected that restrictions to regular (simple) forcing notions might help.

In this paper we give a constructive proof of the pointfree version of Tychonoff's theorem within formal topology, using ideas from Coquand's proof in [7]. To deal with pointfree topology Coquand uses Johnstone's coverages. Because of the representation theorem in [3], from a mathematical viewpoint these structures are equivalent to formal topologies but there is an essential difference also. Namely, formal topologies have been developed within Martin Löf's constructive type theory (cf. [16]), which thus gives a direct way of formalizing them (cf. [4]).

The most important aspect of our proof is that it is based on an inductive definition of the topological product of formal topologies. This fact allows us to transform Coquand's proof into a proof by structural induction on the last rule applied in a derivation of a cover. The inductive generation of a cover, together with a modification of the inductive property proposed by Coquand, makes it possible to formulate our proof of Tychonoff s theorem in constructive type theory. There is thus a clear difference to earlier localic proofs of Tychonoff's theorem known in the literature (cf. [9, 10, 12, 14, 27]). Indeed we not only avoid to use the axiom of choice, but reach constructiveness in a very strong sense. Namely, our proof of Tychonoff's theorem supplies an algorithm which, given a cover of the product space, computes a finite subcover, provided that there exists a similar algorithm for each component space.