This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic, group announcement logic, and coalition announcement logic. In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents all of which are simultaneously making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that (...) group may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics. (shrink)

This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic, group announcement logic, and coalition announcement logic. In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents all of which are simultaneously making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that (...) group may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics. (shrink)

In dynamic epistemic logic and other fields, it is natural to consider relativization as an operator taking sentences to sentences. When using the ideas and methods of dynamic logic, one would like to iterate operators. This leads to iterated relativization. We are also concerned with the transitive closure operation, due to its connection to common knowledge. We show that for three fragments of the logic of iterated relativization and transitive closure, the satisfiability problems are fi1 11–complete. Two of these (...) fragments do not include transitive closure. We also show that the question of whether a sentence in these fragments has a finite (tree) model is fi0 01–complete. These results go via reduction to problems concerning domino systems. (shrink)

The first-order theory of the lattice of recursively enumerable closed subsets of an effective topological space is proved undecidable using the undecidability of the first-order theory of the lattice of recursively enumerable sets. In particular, the first-order theory of the lattice of recursively enumerable closed subsets of Euclidean n -space, for all n , is undecidable. A more direct proof of the undecidability of the lattice of recursively enumerable closed subsets of Euclidean n -space, n ⩾ 2, is (...) provided using the method of reduction and the recursive inseparability of the set of all formulae satisfiable in every model of the theory of SIBs and the set of all formulae refutable in some finite model of the theory of SIBs. (shrink)

With each projective geometry we can associate a Lyndon algebra. Such an algebra always satisfies Tarski's axioms for relation algebras and Lyndon algebras thus form an interesting connection between the fields of projective geometry and algebraic logic. In this paper we prove that if G is a class of projective geometries which contains an infinite projective geometry of dimension at least three, then the class L(G) of Lyndon algebras associated with projective geometries in G has an undecidable equational theory. In (...) our proof we develop and use a connection between projective geometries and diagonal-free cylindric algebras. (shrink)

With each projective geometry we can associate a Lyndon algebra. Such an algebra always satisfies Tarski's axioms for relation algebras and Lyndon algebras thus form an interesting connection between the fields of projective geometry and algebraic logic. In this paper we prove that if G is a class of projective geometries which contains an infinite projective geometry of dimension at least three, then the class L of Lyndon algebras associated with projective geometries in G has an undecidable equational theory. In (...) our proof we develop and use a connection between projective geometries and diagonal-free cylindric algebras. (shrink)

It is a classical result of Mortimer that $L^2$ , first-order logic with two variables, is decidable for satisfiability. We show that going beyond $L^2$ by adding any one of the following leads to an undecidable logic:– very weak forms of recursion, viz.¶(i) transitive closure operations¶(ii) (restricted) monadic fixed-point operations¶– weak access to cardinalities, through the Härtig (or equicardinality) quantifier¶– a choice construct known as Hilbert's $\epsilon$ -operator.In fact all these extensions of $L^2$ prove to be undecidable both for (...) satisfiability, and for satisfiability in finite structures. Moreover most of them are hard for $\Sigma^1_1$ , the first level of the analytical hierachy, and thus have a much higher degree of undecidability than first-order logic. (shrink)

In this article the theoretic evolution and the empirical-experimental efforts that have led to the affirmation of the bounded/procedural rationality paradigm are discussed. Moreover, the debate on supporters of the "optimization" approach and supporters of the "bounded/procedural rationality" approach is traced, highlighting the irreconcilability of these two approaches and, in retort, a solid defense against a merely "reductionist" attempt of the innovative context of the Simonian theory. Critically going over the debate on decision dynamics, it becomes clear how, due to (...) the uncertain nature of rational processes, it is impossible to establish the decision-making best way. The imperfect character of individual choice is explained by how the decider identifies a solution that appears satisfying in that moment due to cognitive and temporal limits. (shrink)

We investigate the first-order theory of closed subspaces of complex Hilbert spaces in the signature \\), where ‘\’ is the orthogonality relation. Our main result is that already its quasi-identities are undecidable: there is no algorithm to decide whether an implication between equations and orthogonality relations implies another equation. This is a corollary of a recent result of Slofstra in combinatorial group theory. It follows upon reinterpreting that result in terms of the hypergraph approach to quantum contextuality, for which it (...) constitutes a proof of the inverse sandwich conjecture. It can also be interpreted as stating that a certain quantum satisfiability problem is undecidable. (shrink)

Deductive inference is usually regarded as being “tautological” or “analytical”: the information conveyed by the conclusion is contained in the information conveyed by the premises. This idea, however, clashes with the undecidability of first-order logic and with the (likely) intractability of Boolean logic. In this article, we address the problem both from the semantic and the proof-theoretical point of view. We propose a hierarchy of propositional logics that are all tractable (i.e. decidable in polynomial time), although by means of (...) growing computational resources, and converge towards classical propositional logic. The underlying claim is that this hierarchy can be used to represent increasing levels of “depth” or “informativeness” of Boolean reasoning. Special attention is paid to the most basic logic in this hierarchy, the pure “intelim logic”, which satisfies all the requirements of a natural deduction system (allowing both introduction and elimination rules for each logical operator) while admitting of a feasible (quadratic) decision procedure. We argue that this logic is “analytic” in a particularly strict sense, in that it rules out any use of “virtual information”, which is chiefly responsible for the combinatorial explosion of standard classical systems. As a result, analyticity and tractability are reconciled and growing degrees of computational complexity are associated with the depth at which the use of virtual information is allowed. (shrink)

It is shown that both classical and intuitionistic propositional logics of an associative binary modality are undecidable. The proof is based on the deduction theorem for these logics.

We sketch proofs of the theorems of Church-Turing and Trachtenbrot using a semi-monomorphic axiomatization.

Buss, S.R., The undecidability of k-provability, Annals of Pure and Applied Logic 53 75-102. The k-provability problem is, given a first-order formula ø and an integer k, to determine if ø has a proof consisting of k or fewer lines . This paper shows that the k-provability problem for the sequent calculus is undecidable. Indeed, for every r.e. set X there is a formula ø and an integer k such that for all n,ø has a proof of k sequents (...) if and only if n ε X. (shrink)

We investigate a contractionless naive set theory, due to Grisin [11]. We prove that the theory is undecidable.

We investigate a contractionless naive set theory, due to Grisin [11]. We prove that the theory is undecidable.

One of the earliest discussions of the so-called 'bad company' objection to Neo-Fregeanism, I show that the consistency of an arbitrary second-order 'contextual definition' (nowadays known as an 'abstraction principle' is recursively undecidable. I go on to suggest that an acceptable such principle should satisfy a condition nowadays known as 'stablity'.

Feature logics are the logical basis for so-called unification grammars studied in computational linguistics. We investigate the expressivity of feature terms with negation and the functional uncertainty construct needed for the description of long-distance dependencies and obtain the following results: satisfiability of feature terms is undecidable, sort equations can be internalized, consistency of sort equations is decidable if there is at least one atom, and consistency of sort equations is undecidable if there is no atom.

The undecidability of the first-order theory of diagonalizable algebras is shown here.

By a fragment of a natural language we mean a subset of thatlanguage equipped with semantics which translate its sentences intosome formal system such as first-order logic. The familiar conceptsof satisfiability and entailment can be defined for anysuch fragment in a natural way. The question therefore arises, for anygiven fragment of a natural language, as to the computational complexityof determining satisfiability and entailment within that fragment. Wepresent a series of fragments of English for which the satisfiabilityproblem is polynomial, (...) NP-complete, EXPTIME-complete,NEXPTIME-complete and undecidable. Thus, this paper represents a casestudy in how to approach the problem of determining the logicalcomplexity of various natural language constructions. In addition, wedraw some general conclusions about the relationship between naturallanguage and formal logic. (shrink)

We give a new proof of the following result : it is undecidable whether a given calculus, that is a finite set of propositional formulas together with the rules of modus ponens and substitution, axiomatizes the classical logic. Moreover, we prove the same for every superintuitionistic calculus. As a corollary, it is undecidable whether a given calculus is consistent, whether it is superintuitionistic, whether two given calculi have the same theorems, whether a given formula is derivable in a given calculus. (...) The proof is by reduction from the undecidable halting problem for the so-called tag systems introduced by Post. We also give a historical survey of related results. (shrink)

We prove that the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also show that the two-variable fragment of a quantified modal logic L with expanding first-order domains is undecidable whenever there is a Kripke frame for L with a point having infinitely many successors (such are, in particular, the first-order extensions of practically all standard modal logics like K, K4, GL, S4, S5, K4.1, S4.2, GL.3, etc.). For many quantified modal logics, including those (...) in the standard nomenclature above, even the monadic two-variable fragments turn out to be undecidable. (shrink)

We prove that the second order predicate unification problem is undecidable by reducing the second order term unification problem to it.

The product of two |$\textbf {Alt}$| logics possesses the polynomial product finite model property and its membership problem is |$\textbf {coNP}$|-complete. Using a reduction from an undecidable domino-tiling problem, we prove that its admissibility problem is undecidable.

We show that true first-order arithmetic of the positive integers is interpretable over the real-algebraic structure of Scott's topological model for intuitionistic analysis. From this the undecidability of the structure follows.

The results of Cubitt et al. on the spectral gap problem add a new chapter to the issue of undecidability in physics, as they show that it is impossible to decide whether the Hamiltonian of a quantum many-body system is gapped or gapless. This implies, amongst other things, that a reductionist viewpoint would be untenable. In this paper, we examine their proof and a few philosophical implications, in particular ones regarding models and limitative results. In more detail, we examine (...) the way these theorems model many-body quantum systems, and we question what, if anything, is the physical counterpart of the models used by Cubitt et al. We argue that these models are non-representational and that, even if they are so artificial that it is hard to imagine a physical system arising from them, they nonetheless offer an opportunity to learn about the world and the relation between mathematics and reality. On this basis, we draw the conclusion that their results do not undermine the reductionist viewpoint in a strong sense but leave the question open in a weak sense. (shrink)

The unreduced solution to the arbitrary interaction problem, absent in the standard theory framework, reveals many equally real and mutually incompatible system configurations, or "realizations". This is the essence of universal dynamic undecidability, or multivaluedness, and the ensuing causal randomness (unpredictability), non-computability, irreversible time flow (evolution, emergence), and dynamic complexity of every real system, object, or process. This creative undecidability of real-world dynamics provides causal explanations for "quantum mysteries", relativity postulates, cosmological problems, and the huge efficiency of high-complexity (...) phenomena, such as life, intelligence, and consciousness, giving rise to extended applications, far beyond the critical limits of usual science paradigm. (shrink)

We investigate and classify the notion of final derivability of two basic inconsistency-adaptive logics. Specifically, the maximal complexity of the set of final consequences of decidable sets of premises formulated in the language of propositional logic is described. Our results show that taking the consequences of a decidable propositional theory is a complicated operation. The set of final consequences according to either the Reliability Calculus or the Minimal Abnormality Calculus of a decidable propositional premise set is in general undecidable, and (...) can be -complete. These classifications are exact. For first order theories even finite sets of premises can generate such consequence sets in either calculus. (shrink)

We prove that the positive fragment of first-order intuitionistic logic in the language with two individual variables and a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals \ and \, where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser’s basic and formal logics, (...) respectively. We also show that, for most “natural” first-order modal logics, the two-variable fragment with a single monadic predicate letter, without functional symbols, constants, and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz—among them, QK, QT, QKB, QD, QK4, and QS4. (shrink)

We show that true first-order arithmetic is interpretable over the real-algebraic structure of models of intuitionistic analysis built upon a certain class of complete Heyting algebras. From this the undecidability of the structures follows. We also show that Scott's model is equivalent to true second-order arithmetic. In the appendix we argue that undecidability on the language of ordered rings follows from intuitionistically plausible properties of the real numbers.

We show the undecidability of the equational theories of some classes of BAOs with a non-associative, residuated binary extra-Boolean operator. These results solve problems in Jipsen [9], Pratt [21] and Roorda [22], [23]. This paper complements Andréka-Kurucz-Németi-Sain-Simon [3] where the emphasis is on BAOs with an associative binary operator.

In this paper, I consider the contribution of Geoffrey Bennington's book, _Scatter 1_, to the ongoing discussion of the political dimension of deconstruction. Focusing on the resonances between Bennington's "politics of politics" and the notion of infrapolitics, I suggest that Bennington's major contribution revolves around the introduction of undecidability into political action and thought.

Propositional logic has been recognized throughout the centuries as one of the cornerstones of reasoning in philosophy and mathematics. Over time, its formalization into Boolean algebra was accompanied by the recognition that a wide range of combinatorial problems can be expressed as propositional satisfiability (SAT) problems. Because of this dual role, SAT developed into a mature, multi-faceted scientific discipline, and from the earliest days of computing a search was underway to discover how to solve SAT problems in an automated (...) fashion. This book, the Handbook of Satisfiability, is the second, updated and revised edition of the book first published in 2009 under the same name. The handbook aims to capture the full breadth and depth of SAT and to bring together significant progress and advances in automated solving. Topics covered span practical and theoretical research on SAT and its applications and include search algorithms, heuristics, analysis of algorithms, hard instances, randomized formulae, problem encodings, industrial applications, solvers, simplifiers, tools, case studies and empirical results. SAT is interpreted in a broad sense, so as well as propositional satisfiability, there are chapters covering the domain of quantified Boolean formulae (QBF), constraints programming techniques (CSP) for word-level problems and their propositional encoding, and satisfiability modulo theories (SMT). An extensive bibliography completes each chapter. This second edition of the handbook will be of interest to researchers, graduate students, final-year undergraduates, and practitioners using or contributing to SAT, and will provide both an inspiration and a rich resource for their work. Edmund Clarke, 2007 ACM Turing Award Recipient: "SAT solving is a key technology for 21st century computer science." Donald Knuth, 1974 ACM Turing Award Recipient: "SAT is evidently a killer app, because it is key to the solution of so many other problems." Stephen Cook, 1982 ACM Turing Award Recipient: "The SAT problem is at the core of arguably the most fundamental question in computer science: What makes a problem hard?". (shrink)

Using a result of Gurevich and Lewis on the word problem for finite semigroups, we give short proofs that the following theories are hereditarily undecidable: (1) finite graphs of vertex-degree at most 3; (2) finite nonvoid sets with two distinguished permutations; (3) finite-dimensional vector spaces over a finite field with two distinguished endomorphisms.

In the spatialized Prisoner's Dilemma, players compete against their immediate neighbors and adopt a neighbor's strategy should it prove locally superior. Fields of strategies evolve in the manner of cellular automata (Nowak and May, 1993; Mar and St. Denis, 1993a,b; Grim 1995, 1996). Often a question arises as to what the eventual outcome of an initial spatial configuration of strategies will be: Will a single strategy prove triumphant in the sense of progressively conquering more and more territory without opposition, or (...) will an equilibrium of some small number of strategies emerge? Here it is shown, for finite configurations of Prisoner's Dilemma strategies embedded in a given infinite background, that such questions are formally undecidable: there is no algorithm or effective procedure which, given a specification of a finite configuration, will in all cases tell us whether that configuration will or will not result in progressive conquest by a single strategy when embedded in the given field. The proof introduces undecidability into decision theory in three steps: by (1) outlining a class of abstract machines with familiar undecidability results, by (2) modelling these machines within a particular family of cellular automata, carrying over undecidability results for these, and finally by (3) showing that spatial configurations of Prisoner's Dilemma strategies will take the form of such cellular automata. (shrink)

For arbitrary finite group $G$ and countable Dedekind domain $R$ such that the residue field $R/P$ is finite for every maximal $R$ -ideal $P$ , we show that the localizations at every maximal ideal of two $RG$ -lattices are isomorphic if and only if the two lattices satisfy the same first order sentences. Then we investigate generalizations of the above results to arbitrary $R$ -torsion-free $RG$ -modules and we apply the previous results to show the decidability of the theory of (...) ${\vec Z}C(2)^2$ -lattices. Eventually, we show that ${\vec Z} [i] C(2)^2$ -lattices have undecidable theory. (shrink)

We show that the Π 4 -theory of the partial order of recursively enumerable weak truth-table degrees is undecidable, and give a new proof of the similar fact for r.e. T-degrees. This is accomplished by introducing a new coding scheme which consists in defining the class of finite bipartite graphs with parameters.

We show that the $\Pi_4$-theory of the partial order of recursively enumerable weak truth-table degrees is undecidable, and give a new proof of the similar fact for r.e. T-degrees. This is accomplished by introducing a new coding scheme which consists in defining the class of finite bipartite graphs with parameters.