Although Kurt Gödel does not figure prominently in the history of computabilty theory, he exerted a significant influence on some of the founders of the field, both through his published work and through personal interaction. In particular, Gödel’s 1931 paper on incompleteness and the methods developed therein were important for the early development of recursive function theory and the lambda calculus at the hands of Church, Kleene, and Rosser. Church and his students studied Gödel 1931, and Gödel taught a seminar (...) at Princeton in 1934. Seen in the historical context, Gödel was an important catalyst for the emergence of computability theory in the mid 1930s. (shrink)

The period from 1900 to 1935 was particularly fruitful and important for the development of logic and logical metatheory. This survey is organized along eight "itineraries" concentrating on historically and conceptually linked strands in this development. Itinerary I deals with the evolution of conceptions of axiomatics. Itinerary II centers on the logical work of Bertrand Russell. Itinerary III presents the development of set theory from Zermelo onward. Itinerary IV discusses the contributions of the algebra of logic tradition, in particular, Löwenheim (...) and Skolem. Itinerary V surveys the work in logic connected to the Hilbert school, and itinerary V deals specifically with consistency proofs and metamathematics, including the incompleteness theorems. Itinerary VII traces the development of intuitionistic and many-valued logics. Itinerary VIII surveys the development of semantical notions from the early work on axiomatics up to Tarski's work on truth. (shrink)

The connections between forms of code and coding and the many crises that currently afflict the contemporary world run deep. Code and crisis in our time mutually define, and seemingly prolong, each other in ‘infinite branching graphs’ of decision problems. There is a growing academic literature that investigates digital code and software from a wide range of perspectives –power, subjectivity, governmentality, urban life, surveillance and control, biopolitics or neoliberal capitalism. The various strands in this literature are reflected in the papers (...) that comprise this special issue. They address topics ranging from social networks, mass media, financial markets and academic plagiarism to highway engineering in relation to the dynamics and diversity of crises. Against this backdrop, the purpose of this essay is to highlight and explore some of the underlying themes connecting codes and codings and the production and apprehension of ‘crisis’. We analyse how the ever-increasing intermediation of contemporary life by codes of various kinds has been closely shadowed by a proliferation of crises. We discuss three related aspects of the coupling of code and crisis (signification, performativity and excess) running across these seemingly diverse topics. We and the other contributors in this special issue seek to go beyond the restricted (and often restricting) understanding of code as the language of machines. Rather, we view code qua programs and algorithms as epitomizing a much broader phenomenon. The codes that we live, and that we live by, also tell us about the ways in which the ‘will to power’ and the 'will to knowledge' tend to be enacted in the contemporary world. (shrink)

Es wird gezeigt, dass Wittgenstein in seiner Frühphilosophie ein nicht-axiomatisches Beweisverständnis entwickelt, für das sich das Problem der Begründung der Axiome nicht stellt. Nach Wittgensteins Beweisverständnis besteht der Beweis einer formalen Eigenschaft einer Formel – z.B. der logischen Wahrheit einer prädikatenlogischen Formel oder der Gleichheit zweier arithmetischer Ausdrücke – in der Transformation der Formel in eine andere Notation, an deren Eigenschaften sich entscheiden lässt, ob die zu beweisende formale Eigenschaft besteht oder nicht besteht. Dieses Verständnis grenzt Wittgenstein gegenüber einem axiomatischen (...) Beweisverständnis ab. Sein Beweisverständnis bedingt ein Programm der Grundlegung der Mathematik, das eine Alternative zu den Ansätzen des Logizismus, Formalismus und Konstruktivismus darstellt. Wittgensteins Ansatz steht im Widerspruch zu den Ergebnissen der Metamathematik, da er die Möglichkeit der Formulierung von Entscheidungsverfahren in der Prädikatenlogik und Arithmetik voraussetzt. Um seinem Ansatz gegenüber der traditionellen Metamathematik Recht zu geben, müsste gezeigt werden, dass sein Beweisverständnis im Bereich der Logik und Arithmetik – der traditionellen Metamathematik zum Trotz – realisierbar ist. (shrink)

Provides a comprehensive overview and introduction to the Routledge Handbook of Propositions.

This paper extends the investigations into logical properties of the quantified argument calculus (Quarc) by suggesting a series of proper subsystems which, although retaining the entire vocabulary of Quarc, restrict quantification in such a way as to make the result decidable. The proof of decidability is via a procedure that prunes the infinite branches of a derivation tree in what is a syntactic counterpart of semantic filtration. We demonstrate an application of one of these systems by showing that Aristotle’s assertoric (...) syllogistic is embeddable within, thus also providing another method of showing its decidability. (shrink)

In the early 1960s, to prove undecidability of monadic fragments of sublogics of the predicate modal logic $$\textbf{QS5}$$ QS 5 that include the classical predicate logic $$\textbf{QCl}$$ QCl, Saul Kripke showed how a classical atomic formula with a binary predicate letter can be simulated by a monadic modal formula. We consider adaptations of Kripke’s simulation, which we call the Kripke trick, to various modal and superintuitionistic predicate logics not considered by Kripke. We also discuss settings where the Kripke trick does (...) not work and where, as a result, decidability of monadic modal predicate logics can be obtained. (shrink)

The book’s core argument is that an artificial intelligence that could equal or exceed human intelligence—sometimes called artificial general intelligence (AGI)—is for mathematical reasons impossible. It offers two specific reasons for this claim: Human intelligence is a capability of a complex dynamic system—the human brain and central nervous system. Systems of this sort cannot be modelled mathematically in a way that allows them to operate inside a computer. In supporting their claim, the authors, Jobst Landgrebe and Barry Smith, marshal evidence (...) from mathematics, physics, computer science, philosophy, linguistics, and biology, setting up their book around three central questions: What are the essential marks of human intelligence? What is it that researchers try to do when they attempt to achieve "artificial intelligence" (AI)? And why, after more than 50 years, are our most common interactions with AI, for example with our bank’s computers, still so unsatisfactory? Landgrebe and Smith show how a widespread fear about AI’s potential to bring about radical changes in the nature of human beings and in the human social order is founded on an error. There is still, as they demonstrate in a final chapter, a great deal that AI can achieve which will benefit humanity. But these benefits will be achieved without the aid of systems that are more powerful than humans, which are as impossible as AI systems that are intrinsically "evil" or able to "will" a takeover of human society. (shrink)

O presente volume se trata de uma coletânea de artigos que reúne alguns dos trabalhos propostos para o evento “III International Colloquium of Analytic Epistemology and VII Conference of Social Epistemology”, realizado entre os dias 27 e 30 de Novembro de 2018, na Universidade Federal de Santa Maria. O “III International Colloquium of Analytic Epistemology and VII Conference of Social Epistemology” é um dos principais eventos de Epistemologia analítica da América Latina e reúne especialistas do Brasil e do exterior para (...) promover debates de alto nível sobre temas que fazem parte da agenda contemporânea no que se refere ao debate analítico contemporâneo acerca da Epistemologia. (shrink)

Esta enciclopédia abrange, de uma forma introdutória mas desejavelmente rigorosa, uma diversidade de conceitos, temas, problemas, argumentos e teorias localizados numa área relativamente recente de estudos, os quais tem sido habitual qualificar como «estudos lógico-filosóficos». De uma forma apropriadamente genérica, e apesar de o território teórico abrangido ser extenso e de contornos por vezes difusos, podemos dizer que na área se investiga um conjunto de questões fundamentais acerca da natureza da linguagem, da mente, da cognição e do raciocínio humanos, bem (...) como questões acerca das conexões destes com a realidade não mental e extralinguística. A razão daquela qualificação é a seguinte: por um lado, a investigação em questão é qualificada como filosófica em virtude do elevado grau de generalidade e abstracção das questões examinadas (entre outras coisas); por outro, a investigação é qualificada como lógica em virtude de ser uma investigação logicamente disciplinada, no sentido de nela se fazer um uso intenso de conceitos, técnicas e métodos provenientes da disciplina de lógica. O agregado de tópicos que constitui a área de estudos lógico-filosóficos é já visível, pelo menos em parte, no Tractatus Logico-Philosophicus de Ludwig Wittgenstein, uma obra publicada em 1921. E uma boa maneira de ter uma ideia sinóptica do território disciplinar abrangido por esta enciclopédia, ou pelo menos de uma porção substancial dele, é extrair do Tractatus uma lista dos tópicos mais salientes aí discutidos; a lista incluirá certamente tópicos do seguinte género, muitos dos quais se podem encontrar ao longo desta enciclopédia: factos e estados de coisas; objectos; representação; crenças e estados mentais; pensamentos; a proposição; nomes próprios; valores de verdade e bivalência; quantificação; funções de verdade; verdade lógica; identidade; tautologia; o raciocínio matemático; a natureza da inferência; o cepticismo e o solipsismo; a indução; as constantes lógicas; a negação; a forma lógica; as leis da ciência; o número. (shrink)

Textbook on Gödel’s incompleteness theorems and computability theory, based on the Open Logic Project. Covers recursive function theory, arithmetization of syntax, the first and second incompleteness theorem, models of arithmetic, second-order logic, and the lambda calculus.

An introductory textbook on metalogic. It covers naive set theory, first-order logic, sequent calculus and natural deduction, the completeness, compactness, and Löwenheim-Skolem theorems, Turing machines, and the undecidability of the halting problem and of first-order logic. The audience is undergraduate students with some background in formal logic.

This book attempts to explicate and expand upon Frank Ramsey's notion of the realistic spirit. In so doing, it provides a systematic reading of his work, and demonstrates the extent of Ramsey's genius as evinced by both his responses to the Tractatus Logico-Philosophicus , and the impact he had on Wittgenstein's later philosophical insights.

Heinrich Behmann (1891-1970) obtained his Habilitation under David Hilbert in Göttingen in 1921 with a thesis on the decision problem. In his thesis, he solved - independently of Löwenheim and Skolem's earlier work - the decision problem for monadic second-order logic in a framework that combined elements of the algebra of logic and the newer axiomatic approach to logic then being developed in Göttingen. In a talk given in 1921, he outlined this solution, but also presented important programmatic remarks on (...) the significance of the decision problem and of decision procedures more generally. The text of this talk as well as a partial English translation are included. (shrink)

There are various ways of achieving an enlarged understanding of a concept of interest. One way is by giving its proper definition. Another is by giving something else a proper definition and then using it to model or formally represent the original concept. Between the two we find varying shades of grey. We might open up a concept by a direct lexical definition of the predicate that expresses it, or by a theory whose theorems define it implicitly. At the other (...) end of the spectrum, the modelling-this-as-that option also admits of like variation, ranging from models rooted in formal representability theorems to models conceived of as having only heuristic value. There exist on both sides of this divide further differences still. In one of them, both the definiendum and definiens of a definition are words or phrases of some common natural language. In others, the item of interest is a natural language expression and its representation is furnished by the artificial linguistic system that models it. The modern history of these approaches is both very large and growing. Much of this evolution has given too short a shrift to the history of the demotion of ‘intuitive’ concepts in favour of the artificially contrived ones intended to model them. A working assumption of this article is that in the absence of a good understanding of what motivated the modelling-turn in the foundations of mathematics and the intuitive theory of truth, the whole notion of formal representability will have been inadequately understood. In the interests of space, I will concentrate on seminal issues in set theory as dealt with by Russell and Frege, and in the theory of truth in natural languages as dealt with by Tarski. The nub of the present focus is the representational role of model theory in the logics of formalized languages. (shrink)

The paper examines Andrei A. Markov’s critical attitude towards L.E.J. Brouwer’s intuitionism, as is expressed in his endnotes to the Russian translation of Heyting’s Intuitionism, published in Moscow in 1965. It is argued that Markov’s algorithmic approach was shaped under the impact of the mathematical style and values prevailing in the Petersburg mathematical school, which is characterized by the proclaimed primacy of applications and the search for rigor and effective solutions.

This paper studies intersection and union type assignment for the calculus , a proof-term syntax for Gentzen’s classical sequent calculus, with the aim of defining a type-based semantics, via setting up a system that is closed under conversion. We will start by investigating what the minimal requirements are for a system, for to be complete ; this coincides with System , the notion defined in Dougherty et al. [18]; however, we show that this system is not sound , so our (...) goal cannot be achieved. We will then show that System is also not complete, but can recover from this by presenting System as an extension of and showing that it satisfies completeness; it still lacks soundness. We show how to restrict so that it satisfies soundness as well by limiting the applicability of certain type assignment rules, but only when limiting reduction to call-by-name or call-by-value reduction; in restricting the system this way, we sacrifice completeness. These results when combined show that, with respect to full reduction, it is not possible to define a sound and complete intersection and union type assignment system for. (shrink)

We describe how finite colimits can be described using the internal lanuage, also known as the Mitchell-Benabou language, of a topos, provided the topos admits countably infinite colimits. This description is based on the set theoretic definitions of colimits and coequalisers, however the translation is not direct due to the differences between set theory and the internal language, these differences are described as internal versus external. Solutions to the hurdles which thus arise are given.

This is Part I of a two-part study of the foundations of mathematics through the lenses of (i) apriority and analyticity, and (ii) the resources supplied by Core Logic. Here we explain what is meant by apriority, as the notion applies to knowledge and possibly also to truths in general. We distinguish grounds for knowledge from grounds of truth, in light of our recent work on truthmakers. We then examine the role of apriority in the realism/anti-realism debate. We raise a (...) hitherto unnoticed problem for any Orthodox Realist who attempts to explain the a priori. (shrink)

This article presents Tarski's Address at the Princeton Bicentennial Conference on Problems of Mathematics, together with a separate summary. Two accounts of the discussion which followed are also included. The central topic of the Address and of the discussion is decision problems. The introductory note gives information about the Conference, about the background of the subjects discussed in the Address, and about subsequent developments to these subjects.

This article presents Tarski's Address at the Princeton Bicentennial Conference on Problems of Mathematics, together with a separate summary. Two accounts of the discussion which followed are also included. The central topic of the Address and of the discussion is decision problems. The introductory note gives information about the Conference, about the background of the subjects discussed in the Address, and about subsequent developments to these subjects.

We begin with the history of the discovery of computability in the 1930’s, the roles of Gödel, Church, and Turing, and the formalisms of recursive functions and Turing automatic machines . To whom did Gödel credit the definition of a computable function? We present Turing’s notion [1939, §4] of an oracle machine and Post’s development of it in [1944, §11], [1948], and finally Kleene-Post [1954] into its present form. A number of topics arose from Turing functionals including continuous functionals on (...) Cantor space and online computations. Almost all the results in theoretical computability use relative reducibility and o-machines rather than a-machines and most computing processes in the real world are potentially online or interactive. Therefore, we argue that Turing o-machines, relative computability, and online computing are the most important concepts in the subject, more so than Turing a-machines and standard computable functions since they are special cases of the former and are presented first only for pedagogical clarity to beginning students. At the end in §10–§13 we consider three displacements in computability theory, and the historical reasons they occurred. Several brief conclusions are drawn in §14. (shrink)

We consider the informal concept of "computability" or "effective calculability" and two of the formalisms commonly used to define it, "(Turing) computability" and "(general) recursiveness". We consider their origin, exact technical definition, concepts, history, general English meanings, how they became fixed in their present roles, how they were first and are now used, their impact on nonspecialists, how their use will affect the future content of the subject of computability theory, and its connection to other related areas. After a careful (...) historical and conceptual analysis of computability and recursion we make several recommendations in section §7 about preserving the intensional differences between the concepts of "computability" and "recursion." Specifically we recommend that: the term "recursive" should no longer carry the additional meaning of "computable" or "decidable;" functions defined using Turing machines, register machines, or their variants should be called "computable" rather than "recursive;" we should distinguish the intensional difference between Church's Thesis and Turing's Thesis, and use the latter particularly in dealing with mechanistic questions; the name of the subject should be "Computability Theory" or simply Computability rather than "Recursive Function Theory.". (shrink)

Alonzo Church's mathematical work on computability and undecidability is well-known indeed, and we seem to have an excellent understanding of the context in which it arose. The approach Church took to the underlying conceptual issues, by contrast, is less well understood. Why, for example, was "Church's Thesis" put forward publicly only in April 1935, when it had been formulated already in February/March 1934? Why did Church choose to formulate it then in terms of Gödel's general recursiveness, not his own λ (...) -definability as he had done in 1934? A number of letters were exchanged between Church and Paul Bernays during the period from December 1934 to August 1937; they throw light on critical developments in Princeton during that period and reveal novel aspects of Church's distinctive contribution to the analysis of the informal notion of effective calculability. In particular, they allow me to give informed, though still tentative answers to the questions I raised; the character of my answers is reflected by an alternative title for this paper, Why Church needed Gödel's recursiveness for his Thesis. In Section 5, I contrast Church's analysis with that of Alan Turing and explore, in the very last section, an analogy with Dedekind's investigation of continuity. (shrink)

This paper challenges two orthodox theses: (a) that computational processes must be algorithmic; and (b) that all computed functions must be Turing-computable. Section 2 advances the claim that the works in computability theory, including Turing's analysis of the effective computable functions, do not substantiate the two theses. It is then shown (Section 3) that we can describe a system that computes a number-theoretic function which is not Turing-computable. The argument against the first thesis proceeds in two stages. It is first (...) shown (Section 4) that whether a process is algorithmic depends on the way we describe the process. It is then argued (Section 5) that systems compute even if their processes are not described as algorithmic. The paper concludes with a suggestion for a semantic approach to computation. (shrink)

We describe a possible physical device that computes a function that cannot be computed by a Turing machine. The device is physical in the sense that it is compatible with General Relativity. We discuss some objections, focusing on those which deny that the device is either a computer or computes a function that is not Turing computable. Finally, we argue that the existence of the device does not refute the Church–Turing thesis, but nevertheless may be a counterexample to Gandy's thesis.

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

In this paper, the predicate counterparts, defined both axiomatically and semantically by means of Kripke frames, of the modal propositional logics $\textbf {GL}$, $\textbf {Grz}$, $\textbf {wGrz}$ and their extensions are considered. It is proved that the set of semantical consequences on Kripke frames of every logic between $\textbf {QwGrz}$ and $\textbf {QGL.3}$ or between $\textbf {QwGrz}$ and $\textbf {QGrz.3}$ is $\Pi ^1_1$-hard even in languages with three (sometimes, two) individual variables, two (sometimes, one) unary predicate letters, and a single (...) proposition letter. As a corollary, it is proved that infinite families of modal predicate axiomatic systems, based on the classical first-order logic and the modal propositional logics $\textbf {GL}$, $\textbf {Grz}$, $\textbf {wGrz}$ are not Kripke complete. Both $\Pi ^1_1$-hardness and Kripke incompleteness results of the paper do not depend on whether the logics contain the Barcan formula. (shrink)

The article investigates the mathematical and philosophical backdrop of the digital ocean as contemporary model, moving from the digitalized ocean of Georg Cantor’s set theory to that of Alan Turing’s computation theory. It examines in Cantor what is arguably the most rigorous historical attempt to think the structural essence of the continuum, in order to clarify what disappears from the computational paradigm once Turing begins to advocate for the structural irrelevance of this ancient ground.

There is an intensive discussion nowadays about the meaning of effective computability, with implications to the status and provability of the Church–Turing Thesis (CTT). I begin by reviewing what has become the dominant account of the way Turing and Church viewed, in 1936, effective computability. According to this account, to which I refer as the Gandy–Sieg account, Turing and Church aimed to characterize the functions that can be computed by a human computer. In addition, Turing provided a highly convincing argument (...) for CTT by analyzing the processes carried out by a human computer. I then contend that if the Gandy–Sieg account is correct, then the notion of effective computability has changed after 1936. Today computer scientists view effective computability in terms of finite machine computation. My contention is supported by the current formulations of CTT, which always refer to machine computation, and by the current argumentation for CTT, which is different from the main arguments advanced by Turing and Church. I finally turn to discuss Robin Gandy's characterization of machine computation. I suggest that there is an ambiguity regarding the types of machines Gandy was postulating. I offer three interpretations, which differ in their scope and limitations, and conclude that none provides the basis for claiming that Gandy characterized finite machine computation. (shrink)

Decidability of monadic first-order classical logic was established by Löwenheim in 1915. The proof made use of a semantic argument, but a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3-style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the (...) modal logic T. (shrink)

The notion of computation has changed the world more than any previous expressions of knowledge. However, as know-how in its particular algorithmic embodiment, computation is closed to meaning. Therefore, computer-based data processing can only mimic life’s creative aspects, without being creative itself. AI’s current record of accomplishments shows that it automates tasks associated with intelligence, without being intelligent itself. Mistaking the abstract for the concrete has led to the religion of “everything is an output of computation”—even the humankind that conceived (...) the computer. The hypostatized role of computers explains the increased dependence on them. The convergence machine called deep learning is only the most recent form through which the deterministic theology of the machine claims more than what it actually is: extremely effective data processing. A proper understanding of complexity, as well as the need to distinguish between the reactive nature of the artificial and the anticipatory nature of the living are suggested as practical responses to the challenges posed by machine theology. (shrink)