By a theory is meant an applied first-order predicate calculus with at least one predicate symbol and perhaps some individual constants and function symbols and a specified set of axioms. In addition to the terms defined by means of the individual variables, constants, and function symbols a theory may also include among its terms those constructed by means of operators such as the epsilon or iota operators; that is, expressions like (εχΡ) or (οχΡ), where P is a well formed formula (wff) of the theory, may also be terms. A constant term of a theory F is then a term in which no variable occurs free. We are interested only in theories which have at least one constant term so that if a theory doesn't have any individual constants it must necessarily admit as terms expressions constructed by means of operators. A sentence of a theory F is a closed wff.

We show that the first order theory of the lattice <ω(S) of finite dimensional closed subsets of any nontrivial infinite dimensional Steinitz Exhange System S has logical complexity at least that of first order number theory and that the first order theory of the lattice (S∞) of computably enumerable closed subsets of any nontrivial infinite dimensional computable Steinitz Exchange System S∞ has logical complexity exactly that of first order number theory. Thus, for example, the lattice of finite dimensional subspaces of a standard copy of ⊕ωQ interprets first order arithmetic and is therefore as complicated as possible. In particular, our results show that the first order theories of the lattice (V∞) of c.e. subspaces of a fully effective ℵ0-dimensional vector space V∞ and the lattice of c.e. algebraically closed subfields of a fully effective algebraically closed field F∞ of countably infinite transcendence degree each have logical complexity that of first order number theory.

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.

It is shown that a stable division ring with positive characteristic has finite dimension over its centre. This is then extended to simple division rings.

Embeddings into initial segments of (the lattice of ideals of r.e. degrees) are relevant for the investigation of decidability of (fragments of) the theory of (with constant-symbols denoting principal ideals). Interest in this investigation stems from open problems concerning decidability of fragments of the theory of R (the usl of r.e. degrees) and embeddings into R. Ambos-Spies and Lerman established comprehensive nonembeddability [AS/LR1] and embeddability [AS/LR2] conditions, but their complementarity is open. (For background on embeddings and decidability consult Lerman [LR1] and Lerman and Shore [LR/SH].) The first systematic investigation of embeddings into is in Calhoun [CL], where the existence of uniform bounds, in the case of embeddings into , on the number of “join traces” arising with nondistributive lattices is shown to remove “obstructions” to lattice-embeddings into R (such as typified in the nonembeddable lattice S8, see [LA/SR], [AS/LR1/). The analysis to follow extends this, by showing that it also removes the “obstruction” to lattice-embeddings into initial segments of R, arising with Lachlan's M5, which embeds into R, but not into every nontrivial initial segment R[0, a], by a result of Downey [DW]. The techniques are Lachlan's [LA], as adapted in Lerman's “pinball machine model” [LR1, LR2], combined with Fejer's “meet-trick” [FJ] as used by Downey [DW] in the proof that every distributive lattice is embeddable into every nontrivial initial segment of r.e. degrees R[0, a], a > 0. We present a sufficient condition, “allowing evasion” [Definition 4.2] for lattice embeddability into every [0, a], a > 0.

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.