By theword problemfor some class of algebraic structures we mean the problem of determining, given a finite setEof equations between words and an additional equationx=y, whetherx=ymust hold in all structures satisfying each member ofE. In 1947 Post [P] showed the word problem for semigroups to be undecidable. This result was strengthened in 1950 by Turing, who showed the word problem to be undecidable forcancellation semigroups,i.e. semigroups satisfying thecancellation propertyNovikov [N] eventually showed the word problem for groups to be undecidable.In 1966 (...) Gurevich [G] showed the word problem to be undecidable forfinitesemigroups. However, this result on finite structures has not been extended to cancellation semigroups or groups; indeed it is easy to see that a finite cancellation semigroup is a group, so both questions are the same. We do not here settle the word problem for finite groups, but we do show that the word problem is undecidable for finite semigroups with zero satisfying an approximation to the cancellation property. (shrink)

It is well known that for all recursively enumerable sets X 1 , X 2 there are disjoint recursively enumerable sets Y 1 , Y 2 such that $Y_1 \subseteq X_1, Y_2 \subseteq X_2$ and Y 1 ∪ Y 2 = X 1 ∪ X 2 . Alistair Lachlan called distributive lattices satisfying this property separated. He proved that the first-order theory of finite separated distributive lattices is decidable. We prove here that the first-order theory of all separated distributive lattices (...) is undecidable. (shrink)

The set of all words in the alphabet {l, r} forms the full binary tree T. If x ∈ T then xl and xr are the left and the right successors of x respectively. We consider the monadic second-order language of the full binary tree with the two successor relations. This language allows quantification over elements of T and over arbitrary subsets of T. We prove that there is no monadic second-order formula φ * (X, y) such that for every (...) nonempty subset X of T there is a unique y ∈ X that satisfies φ * (X, y) in T. (shrink)

I am an historian in a country in which it is not only impossible to say what the future will be, but in which the past itself—as someone put it—is susceptible to change. This country is currently going through an unprecedented crisis that has turned both its material and political as well as spiritual life upside-down. The crisis, the roots of which stretch back over decades, has made life virtually unbearable for many of its citizens. Yet for the historian, and (...) for the philosopher and sociologist, this crisis affords an unusual opportunity. As a result of the earthquakes that have shaken the former Soviet Union, formerly hidden layers of history—and the forces that underpin them—have been revealed. Such cases do not often arise. To a scholar endeavoring to discover the secret springs of unfolding events, Russia represents a gigantic and unique “laboratory.” Although it is easier to judge the extent of a cataclysm, to comprehend its deeper import, after the event, this does not relieve the contemporary—who participates in historical events—of the duty of trying to understand, to the extent possible, the nature of the changes taking place. (shrink)

Church's Thesis asserts that the only numeric functions that can be calculated by effective means are the recursive ones, which are the same, extensionally, as the Turing-computable numeric functions. The Abstract State Machine Theorem states that every classical algorithm is behaviorally equivalent to an abstract state machine. This theorem presupposes three natural postulates about algorithmic computation. Here, we show that augmenting those postulates with an additional requirement regarding basic operations gives a natural axiomatization of computability and a proof of Church's (...) Thesis, as Gödel and others suggested may be possible. In a similar way, but with a different set of basic operations, one can prove Turing's Thesis, characterizing the effective string functions, and--in particular--the effectively-computable functions on string representations of numbers. (shrink)

We start with a simple proof of Leivant's normal form theorem for ∑11 formulas over finite successor structures. Then we use that normal form to prove the following:1. over all finite structures, every ∑21 formula is equivalent to a ∑21 formula whose first-order part is a Boolean combination of existential formulas, and2. over finite successor structures, the Kolaitis-Thakur hierarchy of minimization problems collapses completely and the Kolaitis-Thakur hierarchy of maximization problems collapses partially.The normal form theorem for ∑21 fails if ∑21 (...) is replaced with ∑11 or if infinite structures are allowed. (shrink)

Assume ZFC + "There is a weakly compact cardinal" is consistent. Then: For every $S \subseteq \omega, \mathrm{ZFC} +$ "S and the monadic theory of ω 2 are recursive each in the other" is consistent; and ZFC + "The full second-order theory of ω 2 is interpretable in the monadic theory of ω 2 " is consistent.

People usually regard algorithms as more abstract than the programs that implement them. The natural way to formalize this idea is that algorithms are equivalence classes of programs with respect to a suitable equivalence relation. We argue that no such equivalence relation exists.

This paper is a reaction to the following remark by grzegorczyk: "the compound sentences are not a product of experiment. they arise from reasoning. this concerns also negations; we see that the lemon is yellow, we do not see that it is not blue." generally, in science the truth is ascertained as indirectly as falsehood. an example: a litmus-paper is used to verify the sentence "the solution is acid." this approach gives rise to a (very intuitionistic indeed) conservative extension of (...) the heyting logic satisfying natural duality laws. (shrink)

This paper is motivated by the question whether there exists a logic capturing polynomial time computation over unordered structures. We consider several algorithmic problems near the border of the known, logically defined complexity classes contained in polynomial time. We show that fixpoint logic plus counting is stronger than might be expected, in that it can express the existence of a complete matching in a bipartite graph. We revisit the known examples that separate polynomial time from fixpoint plus counting. We show (...) that the examples in a paper of Cai, Fürer, and Immerman, when suitably padded, are in choiceless polynomial time yet not in fixpoint plus counting. Without padding, they remain in polynomial time but appear not to be in choiceless polynomial time plus counting. Similar results hold for the multipede examples of Gurevich and Shelah, except that their final version of multipedes is, in a sense, already suitably padded. Finally, we describe another possible candidate, involving determinants, for the task of separating polynomial time from choiceless polynomial time plus counting. (shrink)

We consider fixed point logics, i.e., extensions of first order predicate logic with operators defining fixed points. A number of such operators, generalizing inductive definitions, have been studied in the context of finite model theory, including nondeterministic and alternating operators. We review results established in finite model theory, and also consider the expressive power of the resulting logics on infinite structures. In particular, we establish the relationship between inflationary and nondeterministic fixed point logics and second order logic, and we consider (...) questions related to the determinacy of games associated with alternating fixed points. (shrink)

Primal infon logic was introduced in 2009 in connection with access control. In addition to traditional logic constructs, it contains unary connectives p said indispensable in the intended access control applications. Propositional primal infon logic is decidable in linear time, yet suffices for many common access control scenarios. The most obvious limitation on its expressivity is the failure of the transitivity law for implication: \$$ \to \$$ and \$$ \to \$$ do not necessarily yield \$$ \to \$$. Here we introduce (...) and investigate equiexpressive extensions TPIL and TPIL* of propositional primal infon logic as well as their quote-free fragments TPIL0 and TPIL0* respectively. We prove the subformula property for TPIL0* and a similar property for TPIL*; we define Kripke models for the four logics and prove the corresponding soundness-and-completeness theorems; we show that, in all these logics, satisfiable formulas have small models; but our main result is a quadratic-time derivation algorithm for TPIL*. (shrink)

Turing machines define polynomial time on strings but cannot deal with structures like graphs directly, and there is no known, easily computable string encoding of isomorphism classes of structures. Is there a computation model whose machines do not distinguish between isomorphic structures and compute exactly PTime properties? This question can be recast as follows: Does there exist a logic that captures polynomial time ? Earlier, one of us conjectured a negative answer. The problem motivated a quest for stronger and stronger (...) PTime logics. All these logics avoid arbitrary choice. Here we attempt to capture the choiceless fragment of PTime. Our computation model is a version of abstract state machines . The idea is to replace arbitrary choice with parallel execution. The resulting logic expresses all properties expressible in any other PTime logic in the literature. A more difficult theorem shows that the logic does not capture all of PTime. (shrink)

Ch. 1. Filosofskoe osmyslenie kulʹtury -- ch. 2. Problemy mnozhestvennosti kulʹtur.

This article is based on a conversation between the President of the Society for the Anthropology of Consciousness and the Editor‐in‐Chief of its journal. The aim of this conversation is threefold: (1) to engage a broader audience within the field of the anthropology of consciousness, (2) to discuss the recent history of the organization and its current direction, and (3) to recognize why concrete efforts toward a practice of decolonization is essential to maintaining the relevance of an anthropology of consciousness.

The choice construct (choose x: φ(x)) is useful in software specifications. We study extensions of first-order logic with the choice construct. We prove some results about Hilbert's ε operator, but in the main part of the paper we consider the case when all choices are independent.

I felt happy but a little apprehensive when I received the suggestion from the editors of Science in Context to write a comment on my book Categories of Medieval Culture quite a few years after its first publication and translation. It is always difficult to comment on one's own work, for in such a case there is seldom the necessary degree of “distance” between the author and the commentator. I offer this paper rather as a short account of the direction (...) of my thoughts. (shrink)

Pollution is currently responsible for 16% of premature deaths worldwide and poses the greatest long-term threat to public health due to the effects of climate change. The current framework of publ...

The theory of trees with additional unary predicates and quantification over nodes and branches embraces a rich branching time logic. This theory was reduced in the companion paper to the first-order theory of binary, bounded, well-founded trees with additional unary predicates. Here we prove the decidability of the latter theory.

Under a weak set-theoretic assumption we interpret second-order logic in the monadic theory of order.

The main result of this paper is a probabilistic construction of finite rigid structures. It yields a finitely axiomatizable class of finite rigid structures where no L ω ∞,ω formula with counting quantifiers defines a linear order.

This is the first part of a two part work on the monadic theory of short orders (embedding neither ω 1 nor ω 1 * ). This part provides the technical groundwork for decidability results. Other applications are possible.

Assume ZFC + "There is a weakly compact cardinal" is consistent. Then: (i) For every $S \subseteq \omega, \mathrm{ZFC} +$ "S and the monadic theory of ω 2 are recursive each in the other" is consistent; and (ii) ZFC + "The full second-order theory of ω 2 is interpretable in the monadic theory of ω 2 " is consistent.

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.

Each relational structure X has an associated Gaifman graph, which endows X with the properties of a graph. If x is an element of X, let $B_n (x)$ be the ball of radius n around x. Suppose that X is infinite, connected and of bounded degree. A first-order sentence ϕ in the language of X is almost surely true (resp. a. s. false) for finite substructures of X if for every x ∈ X, the fraction of substructures of $B_n (x)$ (...) satisfying ϕ approaches 1 (resp. 0) as n approaches infinity. Suppose further that, for every finite substructure, X has a disjoint isomorphic substructure. Then every ϕ is a. s. true or a. s. false for finite substructures of X. This is one form of the geometric zero-one law. We formulate it also in a form that does not mention the ambient infinite structure. In addition, we investigate various questions related to the geometric zero-one law. (shrink)