Let T be an ω1-Souslin tree. We show the property of forcing notions; “is {ω1}-semi-proper and preserves T” is preserved by a new kind of revised countable support iteration of arbitrary length. As an application we have a forcing axiom which is compatible with the existence of an ω1 -Souslin tree for preorders as wide as possible.

This paper concerns automorphisms of the computably enumerable sets. We prove two results relating semilow sets and prompt degrees via automorphisms, one of which is complementary to a recent result of Downey and Harrington. We also show that the property of effective simplicity is not invariant under automorphism, and that in fact every promptly simple set is automorphic to an effectively simple set. A major technique used in these proofs is a modification of the Harrington-Soare version of the method of Harrington-Soare and Cholak for constructing Δ30 automorphisms; this modification takes advantage of a recent result of Soare on the extension of “restricted” automorphisms to full automorphisms.

The present report is a, somewhat lengthy, addendum to [4], where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.

The main novelty here is the observation that this type-distinction is not essential: we can allow classical sequent derivations to use any combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of tq-reductions.

We give a detailed description of the simulation of tq-reductions by means of reductions of the interpretation of any given classical proof as a proof net of PN2 (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of one type, e.g., multiplicative.

We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are independent: it is not possible to simulate them internally, i.e.. by only one specific combination, and structural rules.

A propositional system of modal logic is second-order if it contains quantifiers ∀p and ∃p which, in the standard interpretation, are construed as ranging over sets of possible worlds (propositions). Most second-order systems of modal logic are highly intractable; for instance, when augmented with propositional quantifiers, K, B, T, K4 and S4 all become effectively equivalent to full second-order logic. An exception is S5, which, being interpretable in monadic second-order logic, is decidable.

In this paper we generalize this framework by allowing multiple modalities. While this does not affect the undecidability of K, B, T, K4 and S4, poly-modal second-order S5 is dramatically more expressive than its mono-modal counterpart. As an example, we establish the definability of the transitive closure of finitely many modal operators. We also take up the decidability issue, and, using a novel encoding of sets of unordered pairs by partitions of the leaves of certain graphs, we show that the second-order propositional logic of two S5 modalitities is also equivalent to full second-order logic.

We confirm a conjecture, about neat embeddings of cylindric algebras, made in 1969 by J. D. Monk, and a later conjecture by Maddux about relation algebras obtained from cylindric algebras. These results in algebraic logic have the following consequence for predicate logic: for every finite cardinal α ≥ 3 there is a logically valid sentence X, in a first-order language ℒ with equality and exactly one nonlogical binary relation symbol E, such that X contains only 3 variables (each of which may occur arbitrarily many times), X has a proof containing exactly α + 1 variables, but X has no proof containing only α variables. This solves a problem posed by Tarski and Givant in 1987.

We define a property R(A0, A1) in the partial order of computably enumerable sets under inclusion, and prove that R implies that A0 is noncomputable and incomplete. Moreover, the property is nonvacuous. and the A0 and A1 which we build satisfying R form a Friedberg splitting of their union A, with A1 prompt and A promptly simple. We conclude that A0 and A1 lie in distinct orbits under automorphisms of , yielding a strong answer to a question previously explored by Downey, Stob, and Soare about whether halves of Friedberg splittings must lie in the same orbit.

Say that (a, d) is an isolation pair if a is a c.e. degree, d is a d.c.e. degree, a < d and a bounds all c.e. degrees below d. We prove that there are an isolation pair (a, d) and a c.e. degree c such that c is incomparable with a, d, and c cups d to o′, caps a to o. Thus, {o, c, d, o′} is a diamond embedding, which was first proved by Downey in [9]. Furthermore, combined with Harrington-Soare continuity of capping degrees, our result gives an alternative proof of N5 embedding.

We study the class of elementary submodels of a large superstable homogeneous model. We introduce a rank which is bounded in the superstable case, and use it to define a dependence relation which shares many (but not all) of the properties of forking in the first order case. The main difference is that we do not have extension over all sets. We also present an example of Shelah showing that extension over all sets may not hold for any dependence relation for superstable homogeneous models.

We give some new examples of possible degree spectra of invariant relations on Δ20-categorical computable structures, which demonstrate that such spectra can be fairly complicated. On the other hand, we show that there are nontrivial restrictions on the sets of degrees that can be realized as degree spectra of such relations. In particular, we give a sufficient condition for a relation to have infinite degree spectrum that implies that every invariant computable relation on a Δ20-categorical computable structure is either intrinsically computable or has infinite degree spectrum. This condition also allows us to use the proof of a result of Moses [23] to establish the same result for computable relations on computable linear orderings.

We also place our results in the context of the study of what types of degree-theoretic constructions can be carried out within the degree spectrum of a relation on a computable structure, given some restrictions on the relation or the structure. From this point of view we consider the cases of Δ20-categorical structures, linear orderings, and 1-decidable structures, in the last case using the proof of a result of Ash and Nerode [3] to extend results of Harizanov [14].

If T is a model complete theory with the strict order property, then the theory of the models of T with an automorphism has no model companion.

The Logic of Partial Terms LPT is a strict negative free logic that provides an economical framework for developing many traditional mathematical theories having partial functions. In these traditional theories, all functions and predicates are strict. For example, if a unary function (predicate) is applied to an undefined argument, the result is undefined (respectively, false). On the other hand, every practical programming language incorporates at least one nonstrict or lazy construct, such as the if-then-else, but nonstrict functions cannot be either primitive or introduced in definitional extensions in LPT. Consequently, lazy programming language constructs do not fit the traditional mathematical mold inherent in LPT. A nonstrict (positive free) logic is required to handle nonstrict functions and predicates.

Previously developed nonstrict logics are not fully satisfactory because they are verbose in describing strict functions (which predominate in many programming languages), and some logicians find their semantics philosophically unpalatable. The newly developed Lazy Logic of Partial Terms LL is as concise as LPT in describing strict functions and predicates, and strict and nonstrict functions and predicates can be introduced in definitional extensions of traditional mathematical theories. LL is “built on top of” LPT. and, like LPT, admits only one domain in the semantics. In the semantics, for the case of a nonstrict unary function h in an LL theory T, we have ⊨Th(⊥) = y ↔ ∀x(h(x) = y), where ⊥ is a canonical undefined term. Correspondingly, in the axiomatization, the “indifference” (to the value of the argument) axiom h(⊥) = y ↔ ∀x(h(x) = y) guarantees a proper fit with the semantics. The price paid for LL's naturalness is that it is tailored for describing a specific area of computer science, program specification and verification, possibly limiting its role in explicating classical mathematical and philosophical subjects.

A general strategy for proving completeness theorems for quantified modal logics is provided. Starting from free quantified modal logic K. with or without identity, extensions obtained either by adding the principle of universal instantiation or the converse of the Barcan formula or the Barcan formula are considered and proved complete in a uniform way. Completeness theorems are also shown for systems with the extended Barcan rule as well as for some quantified extensions of the modal logic B. The incompleteness of Q°.B + BF is also proved.

We show, within the framework of Bishop's constructive mathematics, that (sequential) completeness of the locally convex space (ℝ) of test functions is equivalent to the principle BD-ℕ which holds in classical mathemtatics, Brouwer's intuitionism and Markov's constructive recursive mathematics, but does not hold in Bishop's constructivism.

We analyze the two cardinal properties of definable sets in homogeneous graphs.

In this paper we shall repair some errors and fill some gaps in the inner model theory of [2]. The problems we shall address affect some quite basic definitions and proofs.

We shall be concerned with condensation properties of canonical inner models constructed from coherent sequences of extenders as in [2]. Condensation results have the general form: if x is definable in a certain way over a level , then either x ∈ , or else from x we can reconstruct in a simple way.

The first condensation property considered in [2] is the initial segment condition, or ISC. In section 1 we show that the version of this condition described in [2] is too strong, in that no coherent in which the extenders are indexed in the manner of [2], and which is such that L[] satisfies the mild large cardinal hypothesis that there is a cardinal which is strong past a measurable, can satisfy the full ISC of [2]. It follows that the coherent sequences constructed in [2] do not satisfy the ISC of [2]. We shall describe the weaker ISC which these sequences do satisfy, and indicate the small changes in the arguments of [2] this new condition requires.

For X ⊆ ω, let [X]n denote the class of all n-element subsets of X. An infinite set A ⊆ ω is called n-r-cohesive if for each computable function f: [ω]n → {0, 1} there is a finite set F such that f is constant on [A − F]n. We show that for each n > 2 there is no Πn0 set A ⊆ ω which is n-r-cohesive. For n = 2 this refutes a result previously claimed by the authors, and for n ≥ 3 it answers a question raised by the authors.

We point out that a certain complex compact manifold constructed by Lieberman has the dimensional order property, and has U-rank different from Morley rank. We also give a sufficient condition for a Kähler manifold to be totally degenerate (that is, to be an indiscernible set, in its canonical language) and point out that there are K3 surfaces which satisfy these conditions.

In this note we show:

Theorem 1.1. Let G be a Polish group and X a Polish G-space with the induced orbit equivalence relation EG Borel as a subset of X × X. Then exactly one of the following:

(I) There is a countable languageℒand a Borel function

such that for all x1, x2 ∈ X

or

(II) there is a turbulent Polish G-space Y and a continuous G-embedding

There are various bows and ribbons which can be woven into these statements. We can strengthen (I) by asking that θ also admit a Borel orbit inverse, that is to say some Borel function

for some Borel set B ⊂ Mod(ℒ), such that for all x ∈ X

and then after having passed to this strengthened version of (I) we still obtain the exact same dichotomy theorem, and hence the conclusion that the two competing versions of (I) are equivalent. Similarly (II) can be relaxed to just asking that τ be a Borel G-embedding, or even simply a Borel reduction of the relevant orbit equivalence relations. It is in fact a consequence of 1.1 that all the plausible weakenings and strengthenings of (I) and (II) are respectively equivalent to one another.

I will not closely examine these possible variations here. The equivalences alluded to above follow from our main theorem and the results of [3]. That monograph had previously shown that (I) and (II) are incompatible, and proved a barbaric forerunner of 1.1, and gone on to conjecture the dichotomy result above.

In [9] we introduced a new framework for asymptotic probabilities, in which a σ-additive measure is defined on the sample space of all sequences of finite models, where the universe of , is {1,2,…,n}. In this framework we investigated the strong 0-1 law for sentences, which states that each sentence either holds in eventually almost surely or fails in eventually almost surely.

In this paper we define the strong convergence law for formulas, which carries over the ideas of the strong 0-1 law to formulas with free variables, and roughly states that for each formula ϕ(x), the fraction of tuples a in , which satisfy the formula ϕ(x), almost surely has a limit as n tends to infinity.

We show that the infinitary logic with finitely many variables has the strong convergence law for formulas for the uniform measure, and further characterize the measures on random graphs for which the strong convergence law holds.

We prove that every n-modal logic between Kn and S5n is undecidable, whenever n ≥ 3. We also show that each of these logics is non-finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic. These results answer several questions of Gabbay and Shehtman. The proofs combine the modal logic technique of Yankov–Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, and give a reduction of the (undecidable) representation problem of finite relation algebras.