A field K in a ring language $\mathcal {L}$ is finitely undecidable if $\mbox {Cons}(T)$ is undecidable for every nonempty finite $T \subseteq {\mathtt{Th}}(K; \mathcal {L})$. We extend a construction of Ziegler and (among other results) use a first-order classification of Anscombe and Jahnke to prove every NIP henselian nontrivially valued field is finitely undecidable. We conclude (assuming the NIP Fields Conjecture) that every NIP field is finitely undecidable. This work is drawn from the author’s PhD (...) thesis [48, Chapter 3]. (shrink)

n 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 configurationns of Prisoner’s Dilemma strategies will take the form of such cellular automata. (shrink)

For many, the two key thinkers about science in the twentieth century are Thomas Kuhn and Karl Popper, and one of the key questions in contemplating science is how to make sense of theory change. In Creatively Undecided, philosopher Menachem Fisch defends a new way to make sense of the rationality of scientific revolutions. He argues, loosely following Kuhn, for a strong notion of the framework dependency of all scientific practice, while at the same time he shows how such frameworks (...) can be deemed the possible outcomes of keen rational deliberation along Popperian lines. Fisch's innovation is to call attention to the importance of ambiguity and indecision in scientific change and advancement. Specifically, he backs the problem up, looking not at how we might communicate rationally across an already existing divide but at the rational incentive to create an alternative framework in the first place. Creatively Undecided will be essential reading for philosophers of science, and its vivid case study in Victorian mathematics will draw in historians. (shrink)

The recent, short debate over the alethic undecidability of a Liar Sentence between Stephen Barker and Mark Jago is revisited. It is argued that Jago’s objections succeed in refuting Barker’s alethic undecidability solution to the Liar Paradox, but that, nevertheless, this approach may be revived as the alethic indeterminacy solution to the Liar Paradox. According to the alethic indeterminacy solution, there is genuine metaphysical indeterminacy as to whether a Liar Sentence bears an alethic property, whether truth or falsity. While the (...) alethic indeterminacy solution is presented here, and some revenge cases are considered and addressed, the primary aim of this paper is to revive and defend this underexplored and auspicious approach to solving the Liar Paradox. (shrink)

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.

Stephen Barker presents a novel approach to solving semantic paradoxes, including the Liar and its variants and Curry’s paradox. His approach is based around the concept of alethic undecidability. His approach, if successful, renders futile all attempts to assign semantic properties to the paradoxical sentences, whilst leaving classical logic fully intact. And, according to Barker, even the T-scheme remains valid, for validity is not undermined by undecidable instances. Barker’s approach is innovative and worthy of further consideration, particularly by those (...) of us who aim to find a solution without logical revisionism. As it stands, however, the approach is unsuccessful, as I shall demonstrate below. (shrink)

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.

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)

This book is well known for its proof that many mathematical systems - including lattice theory and closure algebras - are undecidable. It consists of three treatises from one of the greatest logicians of all time: "A General Method in Proofs of Undecidability," "Undecidability and Essential Undecidability in Mathematics," and "Undecidability of the Elementary Theory of Groups.".

"A valuable collection both for original source material as well as historical formulations of current problems."-- The Review of Metaphysics "Much more than a mere collection of papers . . . a valuable addition to the literature."-- Mathematics of Computation An anthology of fundamental papers on undecidability and unsolvability by major figures in the field, this classic reference opens with Godel's landmark 1931 paper demonstrating that systems of logic cannot admit proofs of all true assertions of arithmetic. Subsequent papers by (...) Godel, Church, Turing, and Post single out the class of recursive functions as computable by finite algorithms. Additional papers by Church, Turing, and Post cover unsolvable problems from the theory of abstract computing machines, mathematical logic, and algebra, and material by Kleene and Post includes initiation of the classification theory of unsolvable problems. Suitable for graduate and undergraduate courses. 1965 ed. (shrink)

According to Thomasson’s Easy Ontology, all existential questions have straightforward answers and are solvable by conceptual and empirical work. So there is no need for traditional metaphysics to solve them. First, I give some counterexamples to this thesis from incomplete and undecidable theories. Then I discuss some possible responses, I consider a wider sense of conceptual analysis and argue that even in this sense Easy ontology is not able to resolve the problem and must sacrifice either easiness or answerability. (...) Finally, I will argue that although traditional metaphysics does not make the undecidable sentences answerable, it can still make sense of them and helps us to understand why there are unanswerable questions at all. (shrink)

We argue that it is fundamentally impossible to recover information about quantum superpositions when a quantum system has interacted with a sufficiently large number of degrees of freedom of the environment. This is due to the fact that gravity imposes fundamental limitations on how accurate measurements can be. This leads to the notion of undecidability: there is no way to tell, due to fundamental limitations, if a quantum system evolved unitarily or suffered wavefunction collapse. This in turn provides a solution (...) to the problem of outcomes in quantum measurement by providing a sharp criterion for defining when an event has taken place. We analyze in detail in examples two situations in which in principle one could recover information about quantum coherence: a) “revivals” of coherence in the interaction of a system with the measurement apparatus and the environment and b) the measurement of global observables of the system plus apparatus plus environment. We show in the examples that the fundamental limitations due to gravity and quantum mechanics in measurement prevent both revivals from occurring and the measurement of global observables. It can therefore be argued that the emerging picture provides a complete resolution to the measurement problem in quantum mechanics. (shrink)

This chapter explores some fundamental consequences of the correspondence between physical process and computations. Most physical questions may be answerable only through irreducible amounts of computation. Those that concern idealized limits of infinite time, volume, or numerical precision can require arbitrarily long computations, and so be considered formally undecidable. The behavior of a physical system may always be calculated by simulating explicitly each step in its evolution. Much of theoretical physics has, however, been concerned with devising shorter methods of (...) calculation that reproduce the outcome without tracing each step. Computational irreducibility is common among the systems investigated in mathematics and computation theory, but it may well be the exception rather than the rule, since most physical questions may be answerable only through irreducible amounts of computation. (shrink)

We argue that it is fundamentally impossible to recover information about quantum superpositions when a quantum system has interacted with a sufficiently large number of degrees of freedom of the environment. This is due to the fact that gravity imposes fundamental limitations on how accurate measurements can be. This leads to the notion of undecidability: there is no way to tell, due to fundamental limitations, if a quantum system evolved unitarily or suffered wavefunction collapse. This in turn provides a solution (...) to the problem of outcomes in quantum measurement by providing a sharp criterion for defining when an event has taken place. We analyze in detail in examples two situations in which in principle one could recover information about quantum coherence: (a) “revivals” of coherence in the interaction of a system with the measurement apparatus and the environment and (b) the measurement of global observables of the system plus apparatus plus environment. We show in the examples that the fundamental limitations due to gravity and quantum mechanics in measurement prevent both revivals from occurring and the measurement of global observables. It can therefore be argued that the emerging picture provides a complete resolution to the measurement problem in quantum mechanics. (shrink)

We construct an existentially undecidable complete discretely valued field of mixed characteristic with existentially decidable residue field and decidable algebraic part, answering a question by Anscombe–Fehm in a strong way. Along the way, we construct an existentially decidable field of positive characteristic with an existentially undecidable finite extension, modifying a construction due to Kesavan Thanagopal.

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 present paper the well-known Gödels – Churchs argument concerning the undecidability of logic (of the first order functional calculus) is exhibited in a way which seems to be philosophically interestingfi The natural numbers are not used. (Neither Chinese Theorem nor other specifically mathematical tricks are applied.) Only elementary logic and very simple set-theoretical constructions are put into the proof. Instead of the arithmetization I use the theory of concatenation (formalized by Alfred Tarski). This theory proves to be an (...) appropriate tool. The decidability is defined directly as the property of graphical discernibility of formulas. (shrink)

The famous theory of undecidable sentences created by Kurt Godel in 1931 is presented as clearly and as rigorously as possible. Introductory explanations beginning with the necessary facts of arithmetic of integers and progressing to the theory of representability of arithmetical functions and relations in the system (S) prepare the reader for the systematic exposition of the theory of Godel which is taken up in the final chapter and the appendix.

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.

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)

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 undecidability of the first-order theory of diagonalizable algebras is shown here.

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)

The present paper has three objectives: Presenting an actualization of a proof of the decidability of monadic predicates logic in the contemporary model theory context; Show examples of decidable and undecidable fragments inside First order logic, offering an original proof of the following theorem: Any formula of First of order logic is decidable if its prenex normal form is in the following form: ∀x1,…,∀xn∃y1,…,∃ymφ; Presenting a theorem that characterizes the validity of First order logic by the tautologicity of Propositional (...) logic, said result is interesting since immediately arises the doubt of how to conciliate said characterization with Alonzo Church’s Undecidability Theorem for First Order Logic. (shrink)

Let S be a signature of operations and relations definable in relation algebra, let R be the class of all S-structures isomorphic to concrete algebras of binary relations with concrete interpretations for symbols in S, and let F be the class of S-structures isomorphic to concrete algebras of binary relations over a finite base. To prove that membership of R or F for finite S-structures is undecidable, we reduce from a known undecidable problem—here we use the tiling problem, (...) the partial group embedding problem and the partial group finite embedding problem to prove undecidability of finite membership of R or F for various signatures S. It follows that the equational theory of R is undecidable whenever S includes the boolean operators and composition. We give an exposition of the reduction from the tiling problem and the reduction from the group embedding problem, and summarize what we know about the undecidability of finite membership of R and of F for different signatures S. (shrink)

We obtain an effective embedding of the classical predicate logic into the logic of partial quasiary predicates. The embedding has the property that an image of a non-theorem of the classical logic is refutable in a model of the logic of partial quasiary predicates that has the same cardinality as the classical countermodel of the non-theorem. Therefore, we also obtain an embedding of the classical predicate logic of finite models into the logic of partial quasiary predicates over finite structures. As (...) a consequence, we prove that the logic of partial quasiary predicates is undecidable—more precisely, $\varSigma ^0_1$-complete—over arbitrary structures and not recursively enumerable—more precisely, $\varPi ^0_1$-complete—over finite structures. (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 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 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.

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)

For an arbitrary finite algebra $\g A = (A, f, 0, 1)$ one defines a double sequence $a(i,j)$ by $a(i,0)\!=\!a(0,j)\! =\! 1$ and $a(i,j) \!= \!f( a(i, j-1) , a(i-1,j) )$.The problem if such recurrent double sequences are ultimately zero is undecidable, even if we restrict it to the class of commutative finite algebras.

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)

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)

Church's Undecidability Theorem is one of the meta-theoretical results of the mid-third decade of the last century, which along with other limiting theorems such as those of Gödel and Tarski have generated endless reflections and analyzes, both within the framework of the formal sciences, that is, mathematics, logic and theoretical computation, as well as outside them, especially the philosophy of mathematics, philosophy of logic and philosophy of mind. We propose, as a general purpose of this article, to formulate Church's Undecidability (...) Theorem and present the main ideas of its demonstration. In order to carry out the first objective, we need to introduce and explain the notions of recursive function and numbering used by Gödel, which will allow to formally and rigorously enunciate Church's Theorem. After we enunciate Church's Theorem of Unspeakability in a formal and rigorous manner, we will present the main ideas of the proof of Church's Undecidability Theorem for First Order Logic, which uses Robinson's axiomatic system for arithmetic and four facts about himself: In Robinson's system for arithmetic recursive functions are representable Robinson's system is undecidable, The number of axioms proper to the Robinson system is finite and The logical calculation of the Robinson system is equal to the calculation of the first-order logic. (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 this article I will consider John D. Caputo’s ‘radical hermeneutics’, with ‘undecidability’ as its major theme, in conversation with Martin Heidegger’s notion of ‘anticipatory resoluteness’. Through an examination of the positions of Caputo and Heidegger I argue that Heidegger’s notion of ‘anticipatory resoluteness’ reaches far beyond the claims of ‘radical hermeneutics’, and that it assumes a reconstructive process which carries within its scope the overtones of deconstruction, the experience of repetition and authenticity and also the implications of Gelassenheit. Further, (...) I am arguing that Caputo’s ‘radical hermeneutics’ is problematic and even erroneous when it comes to criticize Heidegger’s thought portraying it as being founded on ‘the myth of the early Greeks’. (shrink)

In vol. 2 of Grundlagen der Mathematik Hilbert and Bernays carry out their undecid- ability proof of predicate logic basing it on their undecidability proof of the arithmeti- cal systemZ00. In this paper, the latter proof is reconstructed and summarized within a formal derivation schema. Formalizing the proof makes the presumed use of a meta language explicit by employing formal predicates as propositional functions, with ex- pressions as their arguments. In the final section of the paper, the proof is analyzed (...) critically by applying Wittgenstein’s view on meta language, which does not lead to a questioning of the assumptions on which the proof is based but of its presumed use of meta language. Finally, it will be argued that determining if it is the undecidability proof or Wittgenstein’s analysis of meta language that is right depends on whether a decision procedure for a predicate that undecidability proofs have seemingly proven undecidable can nonetheless be defined. Thus serious attempts to define a procedure for such a predicate should not be ruled out without studying them. (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)

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)

Ambos-Spies, K. and R.A. Shore, Undecidability and 1-types in the recursively enumerable degrees, Annals of Pure and Applied Logic 63 3–37. We show that the theory of the partial ordering of recursively enumerable Turing degrees is undecidable and has uncountably many 1-types. In contrast to the original proof of the former which used a very complicated O''' argument our proof proceeds by a much simpler infinite injury argument. Moreover, it combines with the permitting technique to get similar results for (...) any ideal of the r.e. degrees. (shrink)

In this work we study the decidability of a class of global modal logics arising from Kripke frames evaluated over certain residuated lattices, known in the literature as modal many-valued logics. We exhibit a large family of these modal logics which are undecidable, in contrast with classical modal logic and propositional logics defined over the same classes of algebras. This family includes the global modal logics arising from Kripke frames evaluated over the standard Łukasiewicz and Product algebras. We later (...) refine the previous result, and prove that global modal Łukasiewicz and Product logics are not even recursively axiomatizable. We conclude by closing negatively the open question of whether each global modal logic coincides with its local modal logic closed under the unrestricted necessitation rule. (shrink)

It is often supposed that, unlike typical axioms of mathematics, the Continuum Hypothesis (CH) is indeterminate. This position is normally defended on the ground that the CH is undecidable in a way that typical axioms are not. Call this kind of undecidability “absolute undecidability”. In this paper, I seek to understand what absolute undecidability could be such that one might hope to establish that (a) CH is absolutely undecidable, (b) typical axioms are not absolutely undecidable, and (c) (...) if a mathematical hypothesis is absolutely undecidable, then it is indeterminate. I shall argue that on no understanding of absolute undecidability could one hope to establish all of (a)–(c). However, I will identify one understanding of absolute undecidability on which one might hope to establish both (a) and (c) to the exclusion of (b). This suggests that a new style of mathematical antirealism deserves attention—one that does not depend on familiar epistemological or ontological concerns. The key idea behind this view is that typical mathematical hypotheses are indeterminate because they are relevantly similar to CH. (shrink)

Let S be a deductive system such that S-derivability (⊦s) is arithmetic and sound with respect to structures of class K. From simple conditions on K and ⊦s, it follows constructively that the K-completeness of ⊦s implies MP(S), a form of Markov's Principle. If ⊦s is undecidable then MP(S) is independent of first-order Heyting arithmetic. Also, if ⊦s is undecidable and the S proof relation is decidable, then MP(S) is independent of second-order Heyting arithmetic, HAS. Lastly, when ⊦s (...) is many-one complete, MP(S) implies the usual Markov's Principle MP. An immediate corollary is that the Tarski, Beth and Kripke weak completeness theorems for the negative fragment of intuitionistic predicate logic are unobtainable in HAS. Second, each of these: weak completeness for classical predicate logic, weak completeness for the negative fragment of intuitionistic predicate logic and strong completeness for sentential logic implies MP. Beth and Kripke completeness for intuitionistic predicate or sentential logic also entail MP. These results give extensions of the theorem of Gödel and Kreisel (in [4]) that completeness for pure intuitionistic predicate logic requires MP. The assumptions of Godel and Kreisel's original proof included the Axiom of Dependent Choice and Herbrand's Theorem, no use of which is explicit in the present article. (shrink)

This paper considers undecidability in the imitation game, the so-called Turing Test. In the Turing Test, a human, a machine, and an interrogator are the players of the game. In our model of the Turing Test, the machine and the interrogator are formalized as Turing machines, allowing us to derive several impossibility results concerning the capabilities of the interrogator. The key issue is that the validity of the Turing test is not attributed to the capability of human or machine, but (...) rather to the capability of the interrogator. In particular, it is shown that no Turing machine can be a perfect interrogator. We also discuss meta-imitation game and imitation game with analog interfaces where both the imitator and the interrogator are mimicked by continuous dynamical systems. (shrink)