We prove that it is decidable of a finite algebra whether it has a near-unanimity term operation, which settles a ten-year-old problem. As a consequence, it is decidable of a finite algebra in a congruence distributive variety whether it admits a natural duality.

It has long been known that every free associative algebra can be embedded in a skew field [11]; in fact there are many different embeddings, all obtainable by specialization from the ‘universal field of fractions’ of the free algebra (cf. [5, Chapter 7]). This makes it reasonable to call the latter the free field; see §2 for precise definitions. The existence of this free field was first established by Amitsur [1], but his proof is rather indirect and does not provide anything like a normal form for the elements of the field. Actually one cannot expect to find such a normal form, since it does not even exist in the field of fractions of a commutative integral domain, but at least one can raise the word problem for free fields: Does there exist an algorithm for deciding whether a given expression for an element of the free field represents zero?

Now some recent work has revealed a more direct way of constructing free fields ([4], [5], [6]), and it is the object of this note to show how this method can be used to solve the word problem for free fields over infinite ground fields. In this connexion it is of interest to note that A. Macintyre [9] has shown that the word problem for skew fields is recursively unsolvable. Of course, every finitely generated commutative field has a solvable word problem (see e.g. [12]).

The construction of universal fields of fractions in terms of full matrices is briefly recalled in §2, and it is shown quite generally for a ring R with a field of fractions inverting all full matrices, that if the set of full matrices over R is recursive, then the universal field has a solvable word problem. This holds more generally if the precise set of matrices over R inverted over the field is recursive, but it seems difficult to exploit this more general statement.

Péter Gács showed (Gács 1974) that for every n there exists a bit string x of length n whose plain complexity C(x) has almost maximal conditional complexity relative to x, i.e., $C\left( {C\left( x \right)|x} \right) \ge {\rm{log}}n - {\rm{log}}^{\left( 2 \right)} n - O\left( 1 \right)$ (Here ${\rm{log}}^{\left( 2 \right)} i = {\rm{loglog}}i$.) Following Elena Kalinina (Kalinina 2011), we provide a simple game-based proof of this result; modifying her argument, we get a better (and tight) bound ${\rm{log}}n - O\left( 1 \right)$ We also show the same bound for prefix-free complexity.

Robert Solovay showed (Solovay 1975) that infinitely many strings x have maximal plain complexity but not maximal prefix complexity (among the strings of the same length): for some c there exist infinitely many x such that $|x| - C\left( x \right) \le c$ and $|x| + K\left( {|x|} \right) - K\left( x \right) \ge {\rm{log}}^{\left( 2 \right)} |x| - c{\rm{log}}^{\left( 3 \right)} |x|$ In fact, the results of Solovay and Gács are closely related. Using the result above, we provide a short proof for Solovay’s result. We also generalize it by showing that for some c and for all n there are strings x of length n with $n - C\left( x \right) \le c$ and $n + K\left( n \right) - K\left( x \right) \ge K\left( {K\left( n \right)|n} \right) - 3K\left( {K\left( {K\left( n \right)|n} \right)|n} \right) - c.$ We also prove a close upper bound $K\left( {K\left( n \right)|n} \right) + O\left( 1 \right)$

Finally, we provide a direct game proof for Joseph Miller’s generalization (Miller 2006) of the same Solovay’s theorem: if a co-enumerable set (a set with c.e. complement) contains for every length a string of this length, then it contains infinitely many strings x such that$|x| + K\left( {|x|} \right) - K\left( x \right) \ge {\rm{log}}^{\left( 2 \right)} |x| - O\left( {{\rm{log}}^{\left( 3 \right)} |x|} \right).$

In this paper we analyze some aspects of the question of using methods from model theory to study structures of functional analysis.

By a well known result of P. Lindström, one cannot extend the expressive power of first order logic and yet preserve its most outstanding model theoretic characteristics (e.g., compactness and the Löwenheim-Skolem theorem). However, one may consider extending the scope of first order in a different sense, specifically, by expanding the class of structures that are regarded as models (e.g., including Banach algebras or other structures of functional analysis), and ask whether the resulting extensions of first order model theory preserve some of its desirable characteristics.

A formal framework for the study of structures based on Banach spaces from the perspective of model theory was first introduced by C. W. Henson in [8] and [6]. Notions of syntax and semantics for these structures were defined, and it was shown that using them one obtains a model theoretic apparatus that satisfies many of the fundamental properties of first order model theory. For instance, one has compactness, Löwenheim-Skolem, and omitting types theorems. Further aspects of the theory, namely, the fundamentals of stability and forking, were first introduced in [10] and [9].

The classes of mathematical structures formally encompassed by this framework are normed linear spaces, possibly expanded with additional structure, e.g., operations, real-valued relations, and constants. This notion subsumes wide classes of structures from functional analysis. However, the restriction that the universe of a structure be a normed space is not necessary. (This restriction has a historical, rather than technical origin; specifically, the development of the theory was originally motivated by questions in Banach space geometry.) Analogous techniques can be applied if the universe is a metric space. Now, when the underlying metric topology is discrete, the resulting model theory coincides with first order model theory, so this logic extends first order in the sense described above. Furthermore, without any cost in the mathematical complexity, one can also work in multi-sorted contexts, so, for instance, one sort could be an operator algebra while another is. say, a metric space.

We summarize the known methods of producing a non-supercompact strongly compact cardinal and describe some new variants. Our Main Theorem shows how to apply these methods to many cardinals simultaneously and exactly control which cardinals are supercompact and which are only strongly compact in a forcing extension. Depending upon the method, the surviving non-supercompact strongly compact cardinals can be strong cardinals, have trivial Mitchell rank or even contain a club disjoint from the set of measurable cardinals. These results improve and unify Theorems 1 and 2 of [5], due to the first author.

We show there is a non-recursive r.e. set A such that if W is any low r.e. set. then the join W ⊕ A is also low. That is. A is “almost deep”. This answers a question of Joekusch. The almost deep degrees form an definable ideal in the r.e. degrees (with jump.)

We show that the structure of recursively enumerable degrees is not a Σ1-elementary substructure of , where (n > 1) is the structure of n-r.e. degrees in the Ershov hierarchy.

1. The theory of classes presented in this paper is a simplification of that presented by J. von Neumann in his paper Die Axiomatisierung der Mengenlehre. However, this paper is written so that it can be read independently of von Neumann's. The principal modifications of his system are the following.

(1) The idea of ordered pair is defined in terms of the other primitive concepts of the system. (See Axiom 4.3 below.)

(2) A much simpler proof of the well-ordering theorem, based on von Neumann's equivalence axiom (Axiom 2.2 below) is given. (More exactly, the theory of ordinal numbers, on which the proof of the well-ordering theorem is based, is simplified—see §8.)

(3) Functions are not assumed to be defined for all arguments. In place of “ = A” we have “is undefined.” This makes possible a constructive interpretation of the system. (See §2.)

2. We wish first to give a rough picture of the system which we are trying to construct. Suppose that we have the idea “class,” but no material from which to construct classes. Nevertheless, we can construct the class 0 having no elements. And then the class 1 having 0 as its only element. And then the classes {1}, and {0, 1}, etc., using always the previously constructed classes as elements. To extend this method to infinite classes, we must give rules telling what elements are to be included. Since the nature of the rules which we can use is not altogether clear, we try to formalize the whole system; that is, to set up a system of axioms which seems to characterize this system of classes. Now in this set of axioms we find it necessary to use the idea of function (in the “Axiom of Replacement”).

A variety V (equational class of algebras) satisfies a strong Malcev condition ∃f1,…, ∃fnθ(f1, …, fn, x1, …, xm) where θ is a conjunction of equations in the function variables f1, …, fn and the individual variables x1, …, xm, if there are polynomial symbols p1, …, pn in the language of V such that ∀x1, …, xmθ(p1 …, pn, x1, …, xm) is a law of V. Thus a strong Malcev condition involves restricted second order quantification of a strange sort. The quantification is restricted to functions which are “polynomially definable”. This notion was introduced by Malcev [6] who used it to describe those varieties all of whose members have permutable congruence relations. The general formal definition of Malcev conditions is due to Grätzer [1]. Since then and especially since Jónsson's [3] characterization of varieties with distributive congruences there has been extensive study of strong Malcev conditions and the related concepts: Malcev conditions and weak Malcev conditions.

In [9], Taylor gives necessary and sufficient semantic conditions for a class of varieties to be defined by a (strong) Malcev condition. A key to the proof is the translation of the restricted second order concepts into first order concepts in a certain many sorted language. In this paper we show that, given this translation, Taylor's theorem is an easy consequence of a result of Tarski [8] and the standard preservation theorems of first order logic.

In this paper we are going to consider experimental logics introduced by Jeroslow [4] as models of human reasoning proceeding by trial and error, i.e. admitting changes of axioms in time (some axioms are deleted, some new ones accepted). Jeroslow's notion is based on the idea that events which may cause changes in axioms and rules of reasoning are mechanical. Suppose a finite alphabet Γ to be fixed and let Γ* be the set of words in the alphabet Γ. N denotes the set of natural numbers.

0.1. Definition. An experimental logic is a recursive relation H ⊆ N × Γ*; H(t, φ) is read “the expression is accepted at the point of time t”. φ is recurring w.r.t. H (notation: RecH(φ)) if H(t, φ) holds for infinitely many t; is stable w.r.t. H (notation: StblH(φ)) if H(t,φ) holds for all but finitely many t. In symbols:

H is convergent if every recurring expression is stable.

0.2. We have the following facts: Let X ∈ Γ*. (1) X ∈ iff there is an experimental logic H such that X = {φ; RecH(φ)}- (2) X ∈ iff there is an experimental logic H such that X = {φ; StblH(φ)}. (3) X ∈ iff there is a convergent experimental logic H such that X is the set of all expressions recurring ( = stable) w.r.t. H. (See [4], [3], [7]; cf. also [5].)

In the predicate calculus, variables provide a flexible indexing service which selects the actual arguments to a predicate letter from among possible arguments that precede the predicate letter (in the parse of the formula). In the process of selection, the possible arguments can be permuted, repeated (used more than once), and skipped. If this service is withheld, so that arguments must be the immediately preceding ones, taken in the order in which they occur, the formula is said to be fluted. Quine showed that if a fluted formula contains only homogeneous conjunction (conjoins only subformulas of equal arity), then the satisfiability of the formula is decidable. It remained an open question whether the satisfiability of a fluted formula without this restriction is decidable. This paper answers that question.

This addendum supplies details of the proof in 3.6 of our paper Disjunction and existence under implication in elementary intuition-istic formalisms in this Journal, vol. 27 (1962), pp. 11–18, as promised in Footnote 8 of that paper (p. 16 lines 11 and 16, for “├” read “|”).

A congruence-substitution (or free substitution with change of bound variables) on a formula E with result F consists in, simultaneously, substituting for each of the free variables of E in all its free occurrences a respective term and replacing each bound occurrence of a variable in E by a respective variable, so that (a) each image in F of a free occurrence of a variable in E is free (IM p. 410) and (b) each image in F of a bound occurrence of a variable in E is bound by the corresponding quantifier (i.e. if the j-th quantifier in E binds the original occurrence, then the j-th quantifier in F binds the image).

Morley rank and Lascar rank are equal on generic types of definable groups in differentially closed fields with finitely many commuting derivations.

Let Th be a formal theory extending number theory. Call an ordinal ξ provable in Th if there is a primitive recursive ordering which can be proved in Th to be a wellordering and whose order type is > ξ. One may define the ordinal ∣ Th ∣ of Th to be the least ordinal which is not provable in Th. By [3] and [12] we get , where IDN is the formal theory for N-times iterated inductive definitions. We will generalize this result not only to the case of transfinite iterations but also to a more general notion of ‘the ordinal of a theory’.

For an X-positive arithmetic formula [X,x] there is a natural norm ∣x∣: = μξ (x ∈ Iξ), where Iξ is defined as {x: [∪μ<ξIμ, x]} by recursion on ξ (cf. [7], [17]). By P we denote the least fixed point of [X,x]. Then P = ∪ξξ holds. If Th allows the formation of P, we get the canonical definitions ∥Th()∥ = sup{∣x∣ + 1: Th ⊢ x ∈ P} and ∥Th∥ = sup{∥Th()∥: P is definable in Th} (cf. [17]). If ≺ is any primitive recursive ordering define Q≺[X,x] as the formula ∀y(y ≺ x → y ∈ X) and ∣x∣≺:= ∣x∣O≺. Then ∣x∣≺ turns out to be the order type of the ≺ -predecessors of x and P is the accessible part of ≺. So Th ⊢ x ∈ P implies the provability of ∣x∣≺ in Th.

Dynamic Topological Logic () is a multimodal system for reasoning about dynamical systems. It is defined semantically and, as such, most of the work done in the field has been model-theoretic. In particular, the problem of finding a complete axiomatization for the full language of over the class of all dynamical systems has proven to be quite elusive.

Here we propose to enrich the language to include a polyadic topological modality, originally introduced by Dawar and Otto in a different context. We then provide a sound axiomatization for over this extended language, and prove that it is complete. The polyadic modality is used in an essential way in our proof.

Tense logics formulated in the bimodal propositional language are investigated with respect to Kripke-completeness (completeness) and decidability. It is proved that all minimal tense extensions of modal logics of finite width (in the sense of K. Kine) as well as all minimal tense extensions of cofinal subframe logics (in the sense of M. Zakharyaschev) are complete. The decidability of all finitely axiomatizable minimal tense extensions of cofinal subframe logics is shown. A number of variations and extensions of these results are also presented.

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 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.

In the literature, a type Γ is a set of formulas ϕ(ν0) in the one free variable ν0. A model M realizes Γ if there is an element a of M such that

M ╞ ϕ [a] for all ϕ ∈ Γ.

A model M omits Γ if no element of M realizes Γ. Evidently, the two statements:

(*) M realizes Γ

and

(**) M omits Γ

In this paper we continue the study of the structure of the lattice of recursively enumerable (r.e.) open subsets of a topological space. Work in this approach to effective topology began in Kalantari and Retzlaff [5] and continued in Kalantari [2], Kalantari and Leggett [3] and Kalantari and Remmel [4]. Studies in effectiveness of results in structures other than integers began with the work of Specker [17] and Lacombe [8] on effective analysis.

The renewed activity in the study of the effective content of mathematical structures owes much to Nerode's program and Metakides' and Nerode's [11], [12] work on vector spaces and fields. These studies have been extended by Kalantari, Remmel, Retzlaff, Shore and Smith. Similar studies on the effective content of other mathematical structures have been conducted. These include work on topological vector spaces, boolean algebras, linear orderings etc.

Kalantari and Retzlaff [5] began a study of effective topological spaces by considering a topological space with a countable basis ⊿ for the topology. The space X is to be fully effective; that is, the basis elements are coded into ω and the operations of intersection of basis elements and the relation of inclusion among them are both computable. An r.e. open subset of X is then represented as the union of basic open sets whose codes lie in an r.e. subset of ω.