An old conjecture of modal logics states that every splitting of the major systems K4, S4, G and Grz has the finite model property. In this paper we will prove that all iterated splittings of G have fmp, whereas in the other cases we will give explicit counterexamples. We also introduce a proof technique which will give a positive answer for large classes of splitting frames. The proof works by establishing a rather strong property of these splitting frames namely that they preserve the finite model property in the following sense. Whenever an extension Λ has fmp so does the splitting Λ/f of Λ by f. Although we will also see that this method has its limitations because there are frames lacking this property, it has several desirable side effects. For example, properties such as compactness, decidability and others can be shown to be preserved in a similar way and effective bounds for the size of models can be given. Moreover, all methods and proofs are constructive.

One way to construct a contraction operator for a theory (belief set) is to assign to it a base (belief base) and an operator of partial meet contraction for that base. Axiomatic characterizations are given of the theory contractions that are generated in this way by (various types of) partial meet base contractions.

We investigate the connection between -stability for random and Cohen forcing notions and the measurability and categoricity of the -sets. We show that Shelah's model for -measurability and categoricity satisfies -random-stability while it does not satisfy -Cohen-stability. This gives an example of measure-category asymmetry. We also present a result concerning finite support iterations of Suslin forcing.

We show that -Amoeba-absoluteness implies that and, hence, measurability. This answers a question of Haim Judah (private communication).

If two models of a first-order theory are isomorphic, then they remain isomorphic in any forcing extension of the universe of sets. In general however, such a forcing extension may create new isomorphisms. For example, any forcing that collapses cardinals may easily make formerly nonisomorphic models isomorphic. However, if we place restrictions on the partially-ordered set to ensure that the forcing extension preserves certain invariants, then the ability to force nonisomorphic models of some theory T to be isomorphic implies that the invariants are not sufficient to characterize the models of T.

A countable first-order theory is said to be classifiable if it is superstable and does not have either the dimensional order property (DOP) or the omitting types order property (OTOP). If T is not classifiable, Shelah has shown in [5] that sentences in L∞,λ do not characterize models of T of power λ. By contrast, in [8] Shelah showed that if a theory T is classifiable, then each model of cardinality λ is described by a sentence of L∞,λ. In fact, this sentence can be chosen in the . ( is the result of enriching the language by adding for each μ < λ a quantifier saying the dimension of a dependence structure is greater than μ) Further work ([3], [2]) shows that ⊐+ can be replaced by ℵ1.

In this note, we give a necessary and sufficient condition for a BCK-formula to have the unique normal form proof.

We call implicational propositional formulas formulas for short. BCK-formulas are the formulas which are derivable from axioms B = (a → b) → (c → a) → c → b, C = (a→b→c)→b→a→c, and K = a→b→a by substitution and modus ponens. It is known that the property of being a BCK-formula is decidable (Jaskowski [11, Theorem 6.5], Ben-Yelles [3, Chapter 3, Theorem 3.22], Komori [12, Corollary 6]). The set of BCK-formulas is identical to the set of provable formulas in the natural deduction system with the following two inference rules.

Here γ occurs at most once in (→I). By the formulae-as-types correspondence [10], this set is identical to the set of type-schemes of closed BCK-λ-terms. (See [5].) A BCK-λ-term is a λ-term in which no variable occurs twice. Basic notion concerning the type assignment system can be found [4]. Uniqueness of normal form proofs has been known for balanced formulas. (See [2,14].) It is related to the coherence theorem in cartesian closed categories. A formula is balanced when no variable occurs more than twice in it. It was shown in [8] that the proofs of balanced formulas are BCK-proofs. Relevantly balanced formulas were defined in [9], and it was proved that such formulas have unique normal form proofs. Balanced formulas are included in the set of relevantly balanced formulas.

One of the main theorems of the paper states the following. Let R-K-M be finite extensions of a rational one variable function field R over a finite field of constants. Let S be a finite set of valuations of K. Then the ring of elements of K having no poles outside S has a Diophantine definition over its integral closure in M.

We consider reducts of the structure ℛ = 〈ℝ, +, ·, <〉 and other real closed fields. We compete the proof that there exists a unique reduct between 〈ℝ, +, <,λa〉a ∈ ℝ and ℛ, and we demonstrate how to recover the definition of multiplication in more general contexts than the semialgebraic one. We then conclude a similar result for reducts between 〈ℝ, ·, <〉 and ℛ and for general real closed fields.

We consider the question of when, given a subset A of M, the setwise stabilizer of the group of automorphisms induces a closed subgroup on Sym(A). We define s-homogeneity to be the analogue of homogeneity relative to strong embeddings and show that any subset of a countable, s-homogeneous, ω-stable structure induces a closed subgroup and contrast this with a number of negative results. We also show that for ω-stable structures s-homogeneity is preserved under naming countably many constants, but under slightly weaker conditions it can be lost by naming a single point.

‘How can we recognize, given axioms and inference rules of a calculus, whether the calculus has such-and-such property?’ A question of this kind arises whenever we deal with a new logic system. For large families of logics, this question may be considered as an algorithmic problem, and a property is called decidable in a given family if there exists an algorithm which is capable of deciding, for a finite axiomatics of a calculus in the family, whether or not it has the property.

In the class of intermediate propositional logics, for instance, nontrivial properties such as the tabularity, pretabularity, and interpolation property (Maksimova [1972, 1977]) are decidable. However, for many other important properties—decidability, finite model property, disjunction property, Halldén-completeness, etc.—effective criteria were not found in spite of considerable efforts.

In this paper we show that the difficulties in investigating these properties in the classes of intermediate logics and normal modal logics containing S4 are of principal nature, since all of them turn out to be algorithmically undecidable. In other words, there are no algorithms which, given a finite set of axioms of an intermediate or modal calculus, can recognize whether or not it is decidable, Halldén-complete, has the finite model or disjunction property.

The first results concerning the undecidability of properties of calculi seem to have been obtained by Linial and Post [1949], who proved the undecidability of the problem of equivalence to classical calculus in the class of all propositional calculi with the same language as the classical one and the two inference rules: modus ponens and substitution. Kuznetsov [1963] generalized this result having proved the undecidability of the problem of equivalence to any fixed intermediate calculus (for instance, to intuitionistic calculus or even the inconsistent one). However, these results will not hold if we confine ourselves only to the class of intermediate logics, though the problem of equivalence to the undecidable intermediate calculus of Shehtman [1978] is clearly undecidable in this class as well.

A first-order sentence Φ is Σ2 if there is a quantifier-free formula Θ such that Φ has the form . The Σ2-theory of a structure for a language ℒ is the set of Σ2-sentences of ℒ true in . It was shown independently by Lerman and Shore (see [Le, Theorem VII.4.4]) that the Σ2-theory of the structure = 〈D, ≤ 〉 is decidable, where D is the set of degrees of unsolvability and ≤ is the standard ordering of D. This result is optimal in the sense that the Σ3-theory of is undecidable, a result due to J. Schmerl. (For a proof, see [Le, Theorem VII.4.5]. As Lerman has pointed out, this proof should be corrected by defining θσ to be ∀xσ1(x) rather than ∀x(ψ(x)→ σ1(x)).) Nonetheless, in this paper we extend the decidability result of Lerman and Shore by showing that the Σ2-theory of is decidable, where ⋃ is the least upper bound operator and 0 is the least degree. Of course ⋃ is definable in , but many interesting degree-theoretic results are expressible as Σ2-sentences in the language of ∪ but not as Σ2-sentences in the language of . For instance, Simpson observed that the Posner-Robinson cupping theorem could be used to show that for any nonzero degrees a, b, there is a degree g such that b ≤ a ⋃ g, and b ⋠ g (see [PR, Corollary 6]). However, the Posner-Robinson technique does not seem to suffice to decide the Σ2-theory of ∪. We introduce instead a new method for coding a set into the join of two other sets and use it to decide this theory.

The main result of this paper is to show that for every recursive ordinal α ≠ 0 and for every nonrecursive r.e. degree d there is a r.e. set of rank α and degree d.

Let us call an integer part of an ordered field any subring such that every element of the field lies at distance less than I from a unique element of the ring. We show that every real closed field has an integer part.

If ZFC is consistent, then each of the following is consistent with :

(1) X ⊆ ℝ is of strong measure zero iff ∣X∣ ≤ ℵ1 + there is a generalized Sierpinski set.

(2) The union of ℵ many strong measure zero sets is a strong measure zero set + there is a strong measure zero set of size ℵ2 + there is no Cohen real over L.

We discuss a ‘negative’ way of defining frame classes in (multi)modal logic, and address the question of whether these classes can be axiomatized by derivation rules, the ‘non-ξ rules’, styled after Gabbay's Irreflexivity Rule. The main result of this paper is a metatheorem on completeness, of the following kind: If ⋀ is a derivation system having a set of axioms that are special Sahlqvist formulas and ⋀+ is the extension of ⋀ with a set of non-ξ rules, then ⋀+ is strongly sound and complete with respect to the class of frames determined by the axioms and the rules.

For a ring with unit R, which need not be associative, denote the group of upper unitriangular 3 × 3 matrices over R by UT3(R). Let e1 = (1,0,0), e2 = (0,1,0), where (α, β, γ) denotes the matrix

Denote the expanded group (UT3(R), e1, e2) by (R). A. 1. Mal′cev [M] gave an algebraic characterization of the expanded groups of the form (R) as follows. Let h1, h2 be elements of a group H; then (H, h1, h2) is isomorphic to (R), for some R, if and only if

(i) H is 2-step nilpotent;

(ii) CH(hi) are abelian, i = 1,2;

(iii) CH(h1) ∩ CH(h2) = Z(H);

(iv) [CH(h1),h2] = [h1, CH(h2)] = Z(H);

(v) Z(H) is a direct summand in both CH(hi).

(In [M] condition (v) is a bit stronger; the version above is presented in [B2].)

A pair (h1, h2) of elements of a group H is said to be a base if (H, h1, h2) satisfies the conditions (i)–(iv). A. I. Mal′cev [M] found a uniform way of first order interpreting a ring Ring(H, h1, h2) in any group with a base (H, h1, h2); in particular, Ring((R)) ≃ R.

The notions of forcing and generic set were introduced by Cohen in 1963 to prove the independence of the Axiom of Choice and the Continuum Hypothesis in set theory. Let ω be the set of natural numbers, i.e., {0,1,2,3,…}. A string is a mapping from an initial segment of ω into {0,1}. We identify a set A ⊆ ω to with its characteristic function.

We now consider a set generic over the arithmetic sets. A set A ⊆ ω is called n-generic if it is Cohen-generic for n-quantifier arithmetic. This is equivalent to saying that for every -set of strings S, there is a σ ⊂ A such that σ ∈ S or (∀v ≥ σ)(v ∉ S). By degree we mean Turing degree (of unsolvability). We call a degree n-generic if it has an n-generic representative. For a degree a, let D(≤a) denote the set of degrees which are recursive in a.

Before Cohen's work, there was a precursor of the notion of forcing in recursion theory. Friedberg showed that for every degree b above the complete degree 0', i.e., the degree of a complete r.e. set, there is a degree a such that a′ = a ⋃ 0′ = b. He actually proved this result by using the notion of forcing for statements.

It is a well-known fact that the notion of an archimedean order cannot be formalized in the first-order calculus. In [12] and [18], A. Robinson and E. Zakon characterized the elementary class generated by all the archimedean, totally-ordered abelian groups (o-groups) in the language 〈+,<〉, calling it the class of regularly ordered or generalized archimedean abelian groups. Since difference (−) and 0 are definable in that language, it is immediate that in the expanded language 〈 +, −, 0, < 〉 the definable expansion of the class of regular groups is also the elementary class generated by the archimedean ones. In the more general context of lattice-ordered groups (l-groups), the notion of being archimedean splits into two different notions: a strong one (being hyperarchimedean) and a weak one (being archimedean). Using the representation theorem of K. Keimel for hyperarchimedean l-groups, we extend in this paper the Robinson and Zakon characterization to the elementary class generated by the prime-projectable, hyperarchimedean l-groups. This characterization is also extended here to the elementary class generated by the prime-projectable and projectable archimedean l-groups (including all complete l-groups). Finally, transferring a result of A. Touraille on the model theory of Boolean algebras with distinguished ideals, we give the classification up to elementary equivalence of the characterized class.

We recall that a lattice-ordered group, l-group for short, is a structure

We consider an infinite two-person game. The second player has a winning perfect information strategy; we show that this player has a winning strategy which depends on substantially less information. The game studied here is a variation on a game of Gale.

This is a continuation of [N2]. We find a Borel definition of Q-isolation. We pursue a topological and Scott analysis of pseudotypes on S(Q).