This work results from an attempt to give the vague notion of relevance a concrete semantical interpretation. The idea is that propositions may be divided into different “domains of relevance”. Each “domain” has its own “T” and “F” values, and propositions “belonging” to one domain can never entail propositions “belonging” to another, unconnected one.

The semantics we have developed were found to correspond to an already known system, which we call here RMI⥲. Its axioms are the implication-negation axioms of the system RM ([1, Chapter 5]). However, as Meyer has shown, RM is not a conservative extension of RMI⥲, since RMI⥲ has the sharing-of-variables property ([5], and [1, pp. 148–149[), which the implication-negation fragment of RM has not.

RMI⥲ has four advantages in comparison to its more famous sister R⥲ (the pure intentional fragment of the system R; see [1]):

a) It has a very natural (from a relevance point of view) many-valued semantics, the simple form of which we describe here.

b) RMI⥲, ⊢ A1 → [A2 → (… → (An → A) …)] iff there is a proof of A from the set {A1, …, An} that actually uses all the members of this set. In R⥲, this holds only if we talk about “sequences” instead of “sets”. This is somewhat less intuitive (see [1, pp. 394–395]).

c) RMI⥲ is a maximal “natural” relevance logic, in the sense that every proper extension of it limits the number of “domains of relevance” (§III).

In this paper we show that any countable upper semilattice with zero can be embedded as an initial segment of the degrees of unsolvability. This provides a characterization of the order types of the countable initial segments of the degrees since any such initial segment is trivially an initial segment of a countable upper semilattice. Let a segment S of the degrees be a set of degrees such that, if a, b Є S and a < c < b, then c Є S. One may readily observe that our result also characterizes the order types of all countable segments of the degrees of unsolvability.

We consider the problem of finding and classifying representations in algebraic logic. This is approached by letting two players build a representation using a game. Homogeneous and universal representations are characterized according to the outcome of certain games. The Lyndon conditions defining representable relation algebras (for the finite case) and a similar schema for cylindric algebras are derived. Finte relation algebras with homogeneous representations are characterized by first order formulas. Equivalence games are defined, and are used to establish whether an algebra is ω-categorical. We have a simple proof that the perfect extension of a representable relation algebra is completely representable.

An important open problem from algebraic logic is addressed by devising another two-player game, and using it to derive equational axiomatisations for the classes of all representable relation algebras and representable cylindric algebras.

Other instances of this approach are looked at, and include the step by step method.

We have come to believe that propositional modal logic (with the usual relational semantics) must be understood as a rather strong fragment of classical second-order predicate logic. (The interpretation of propositional modal logic in second-order predicate logic is well known; see e.g. [2, §1].) “Strong” refers of course to the expressive power of the languages, not to the deductive power of formal systems. By “rather strong” we mean sufficiently strong that theorems about first-order logic which fail for second-order logic usually fail even for propositional modal logic. Some evidence for this belief is contained in [2] and [3]. In the former is exhibited a finitely axiomatized consistent tense logic having no relational models, and the latter presents a finitely axiomatized modal logic between T and S4, such that □p → □2p is valid in all relational models of the logic but is not a thesis of the logic. The result of [2] is strong evidence that bimodal logic is essentially second-order, but that of [3] does not eliminate the possibility that unimodal logic only appears to be incomplete because we have not adopted sufficiently powerful rules of inference. In the present paper we present stronger evidence of the essentially second-order nature of unimodal logic.

We consider structural completeness in modal logics. The main result is the necessary and sufficient condition for modal logics over K4 to be hereditarily structurally complete: a modal logic λ is hereditarily structurally complete iff λ is not included in any logic from the list of twenty special tabular logics. Hence there are exactly twenty maximal structurally incomplete modal logics above K4 and they are all tabular.

I solve here some problems left open in “T-convexity and Tame Extensions” [9]. Familiarity with [9] is assumed, and I will freely use its notations. In particular, T will denote a complete o-minimal theory extending RCF, the theory of real closed fields. Let (, V) ⊨ Tconvex, let = V/m(V) be the residue field, with residue class map x ↦ : V ↦ , and let υ: → Γ be the associated valuation. “Definable” will mean “definable with parameters”. The main goal of this article is to determine the structure induced by (, V) on its residue fieldand on its value group Γ. In [9] we expanded the ordered field to a model of T as follows. Take a tame elementary substructure ′ of such that R′ ⊆ V and R′ maps bijectively onto under the residue class map, and make this bijection into an isomorphism ′ ≌ of T-models. (We showed such ′ exists, and that this gives an expansion of to a T-model that is independent of the choice of ′.).

The notion of a “partition relation”, as it has been studied in the context of set theory for the past several years, was inspired by the following theorem of F. P. Ramsey [14]:

Theorem 0.1. Let n be a positive integer and let {A, B} be a partition of those subsets of the nonnegative integers containing exactly n elements. Then there exists an infinite subset x of the nonnegative integers all of whose n-element subsets are contained in only one of A or B. (Any such set x is said to be “homogeneous” for the partition.)

We present a formal theory of propositions and combinator terms, and in this theory we give an interpretation of Martin-Löf's type theory. The construction of the interpretation is inspired by the semantics for type theory, but it can also be viewed as a formalized realizability interpretation.

The basic setting of nonstandard analysis consists of a set-theoretical structure together with a map * from into another structure * of the same sort. The function * is taken to be an elementary embedding (in an appropriate sense) and is generally assumed to make * into an enlargement of [13]. The structures and * may be type-hierarchies as in [11] and [13] or they may be cumulative structures with ω levels as in [14]. The assumption that * is an enlargement of has been found to be the weakest hypothesis which allows for the familiar applications of nonstandard analysis in calculus, elementary topology, etc. Indeed, practice has shown that a smooth and useful theory can be achieved only by assuming also that * has some stronger properties such as the saturation properties first introduced in nonstandard analysis by Luxemburg [11].

This paper concerns an entirely new family of properties, stronger than the saturation properties. For each cardinal number κ, * satisfies the κ-isomorphism property (as an enlargement of ) if the following condition holds:

For each first order language L with fewer than κ nonlogical symbols, if and are elementarily equivalent structures for L whose domains, relations and functions are all internal (relative to * and ), then and are isomorphic.

The main purpose of this note is to prove (theorem 11, § 5) that, in any interpretation of the formalisation of Aristotelian syllogistic given by Łukasiewicz [4], it is always possible to associate with each element a a non-null sub-class φ(a) of some ‘universal’ class V in such a way that ‘Aab’ (all a are b), ‘Iab’ (some a are b) are equivalent respectively to ‘φ(a) is contained in φ(b)’, ‘φ(a) has a non-null intersection with φ(b)’. Similarly (theorem 6, §4) we show that in Wedberg's system [14] with primitives ‘Aab’, ‘a’ (not a), it is possible to find a mapping a → φ(a) as above such that ‘Aab’ is equivalent to ‘φ(a) is contained in φ(b)’ and φ(a‘ is equal to φ(a)’, the complement of φ(a) with respect to V. Thus, if we make the preliminary step of identifying elements a, b such that Aab and Aba both hold (i.e. taking equivalence classes with respect to the relation Aab & Aba), we are left with essentially only one kind of interpretation for these systems, namely the ‘normal’ interpretation by classes. Slupecki [11], [12] has proved that Łukasiewicz's system is a complete and decidable theory of the relations of inclusion and intersection of non-null classes, and Wedberg [14] has proved that his system is a complete and decidable theory of the relation of inclusion and the operation of complementation for nonnull, non-universal classes. Using the above-mentioned embedding theorem, we are able to obtain (theorems 9, 6, §§ 5, 4) very simple proofs of these results.

In 1984. Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidabie in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004. the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime. thus 2-ExpTime-complete. We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted on tree structures.

We review briefly the attempts to define random sequences (§0). These attempts suggest two theorems: one concerning the number of subsequence selection procedures that transform a random sequence into a random sequence (§§1–3 and 5); the other concerning the relationship between definitions of randomness based on subsequence selection and those based on statistical tests (§4).

It is consistent that for many cardinals λ there is a family of at least λ+ unbounded subsets of λ which have uniformization properties. In particular if it is consistent that a supercompact cardinal exists, then it is consistent that ℵω has such a family. We have applications to point set topology, Whitehead groups and reconstructing separable abelian p-groups from their socles.

We present two finitely axiomatized modal propositional logics, one between T and S4 and the other an extension of S4, which are incomplete with respect to the neighbourhood or Scott-Montague semantics.

Throughout this paper we are referring to logics which contain all the classical connectives and only one modal connective □ (unary), no propositional constants, all classical tautologies, and which are closed under the rules of modus ponens (MP), substitution, and the rule RE (from A ↔ B infer αA ↔ □B). Such logics are called classical by Segerberg [6]. Classical logics which contain the formula □p ∧ □q → □(p ∧ q) (denoted by K) and its “converse,” □{p ∧ q)→ □p ∧ □q (denoted by R) are called regular; regular logics which are closed under the rule of necessitation, RN (from A infer □A), are called normal. The logics that we are particularly concerned with are all normal, although some of our results will be true for all regular or all classical logics. It is well known that K and R and closure under RN imply closure under RE and also that normal logics are also those logics closed under RN and containing □{p → q) → {□p → □q).

We consider here the pure functional calculus of first order as formulated by Church.

Church, l.c., p. 79, gives the definition of the validity of a formula in a given set I of individuals and shows that a formula is provable in if and only if it is valid in every non-empty set I. The definition of validity is preceded by the definition of a value of a formula; the notion of a value is the basic “semantical” notion in terms of which all other semantical notions are definable.

The notion of a value of a formula retains its meaning also in the case when the set I is empty. We have only to remember that if I is empty, then an m-ary propositional function (i.e. a function from the m-th cartesian power Im to the set {f, t}) is the empty set. It then follows easily that the value of each well-formed formula with free individual variables is the empty set. The values of wffs without free variables are on the contrary either f or t. Indeed, if B has the unique free variable c and ϕ is the value of B, then the value of (c)B according to the definition given by Church is the propositional constant f or t according as ϕ(j) is f for at least one j in I or not. Since, however, there is no j in I, the condition ϕ(j) = t for all j in I is vacuously satisfied and hence the value of (c)B is t.

We analyse here the monadic theory of the rational order, the monadic theory of the real line with quantification over “small” subsets and models of these theories. We prove that the results are in some sense the best possible.

We study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count.

To this end an isomorphism preserving (‘generic’) model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation of the relational vs. the arithmetical side of the algorithms involved.

In parallel, we study the relations of Fixed-Point+Counting with the infinitary logics and the corresponding pebble games.

The main result, however, involves the concept of an arithmetical invariant. By this we mean a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. In particular its values are linearly ordered structures. We establish the existence of a family of arithmetical invariants with the following properties:

• The invariants themselves can be evaluated in polynomial time.

• A class of finite relational structures is definable in Fixed-Point+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants.

• The invariant r classifies all finite relational structures exactly up to equivalence with respect to the logic

We also give a characterization of Fixed-Point+Counting in terms of sequences of formulae in the : It corresponds exactly to the polynomial time computable families (φn)n ∈ ω in these logics.

Towards a positive assessment of the expressive power of Fixed-Point+Counting, it is shown that the natural extension of fixed-point logic by Lindström quantifiers, which capture all the PTime computable properties of cardinalities of definable predicates, is strictly weaker than what we get here. This implies in particular that every extension of fixed-point logic by means of monadic Lindström quantifiers, which stays within PTime, must be strictly contained in Fixed-Point+Counting.

In this paper we mainly study preservation theorems for two fragments of the infinitary languages Lκκ, with κ regular, without the equality symbol: the universal Horn fragment and the universal strict Horn fragment. In particular, when κ is ω, we obtain the corresponding theorems for the first-order case.

The universal Horn fragment of first-order logic (with equality) has been extensively studied; for references see [10], [7] and [8]. But the universal Horn fragment without equality, used frequently in logic programming, has received much less attention from the model theoretic point of view. At least to our knowledge, the problem of obtaining preservation results for it has not been studied before by model theorists. In spite of this, in the field of abstract algebraic logic we find a theorem which, properly translated, is a preservation result for the strict universal Horn fragment of infinitary languages without equality which, apart from function symbols, have only a unary relation symbol. This theorem is due to J. Czelakowski; see [5], Theorem 6.1, and [6], Theorem 5.1. A. Torrens [12] also has an unpublished result dealing with matrices of sequent calculi which, properly translated, is a preservation result for the strict universal Horn fragment of a first-order language. And in [2] of W. J. Blok and D. Pigozzi we find Corollary 6.3 which properly translated corresponds to our Corollary 19, but for the case of a first-order language that apart from its function symbols has only one κ-ary relation symbol, and for strict universal Horn sentences. The study of these results is the basis for the present work. In the last part of the paper, Section 4, we will make these connections clear and obtain some of these results from our theorems. In this way we hope to make clear two things: (1) The field of abstract algebraic logic can be seen, in part, as a disguised study of universal Horn logic without equality and so has an added interest. (2) A general study of universal Horn logic without equality from a model theoretic point of view can be of help in the field of abstract algebraic logic.

c.c.c. posets are characterised in terms of -generic conditions. This characterisation can be applied to get simple proofs of many facts about c.c.c. forcing including Con(MA + ┐CH).

We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [37]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia theorem and the theory of modal companions to systems of multiple-conclusion rules or (unitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property.