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)

By a classical result of Kotlarski, Krajewski and Lachlan, pathological satisfaction classes can be constructed for countable, recursively saturated models of Peano arithmetic. In this paper we consider the question of whether the pathology can be eliminated; we ask in effect what generalities involving the notion of truth can be obtained in a deflationary truth theory (a theory of truth which is conservative over its base). It is shown that the answer depends on the notion of pathology we adopt. It (...) turns out in particular that a certain natural closure condition imposed on a satisfaction class—namely, closure of truth under sentential proofs—generates a nonconservative extension of a syntactic base theory (Peano arithmetic). (shrink)

In this paper, we investigate the phenomenon ofspeed-upin the context of theories of truth. We focus on axiomatic theories of truth extending Peano arithmetic. We are particularly interested on whether conservative extensions of PA have speed-up and on how this relates to a deflationist account. We show that disquotational theories have no significant speed-up, in contrast to some compositional theories, and we briefly assess the philosophical implications of these results.

This paper develops a proof theory for logical forms of proofs in the case of monadic languages. Among the consequences are different kinds of generalization of proofs in various schematic proof systems. The results use suitable relations between logical properties of partial proof data and algebraic properties of corresponding sets of linear diophantine equations.

Around 1989, a striking letter written in March 1956 from Kurt Gödel to John von Neumann came to light. It poses some problems about the complexity of algorithms; in particular, it asks a question that can be seen as the first formulation of the P=?NP question. This paper discusses some of the background to this letter, including von Neumann's own ideas on complexity theory. Von Neumann had already raised explicit questions about the complexity of Tarski's decision procedure for elementary algebra (...) and geometry in a letter of 1949 to J. C. C. McKinsey. The paper concludes with a discussion of why theoretical computer science did not emerge as a separate discipline until the 1960s. (shrink)

The affirmative answer to the title question is justified in two ways: logical and empirical. The logical justification is due to Gödel’s discovery that in any axiomatic formalized theory, having at least the expressive power of PA, at any stage of development there must appear unsolvable problems. However, some of them become solvable in a further development of the theory in question, owing to subsequent investigations. These lead to new concepts, expressed with additional axioms or rules. Owing to the so-amplified (...) axiomatic basis, new routine procedures like algorithms, can be reached. Those, in turn, help to gain new insights which lead to still more powerful axioms, and consequently again to ampler algorithmic resources. Thus scientific progress proceeds to an ever higher scope of solvability. The existence of such feedback cycles –in a formal way rendered with Turing’s systems of logic based on ordinal – gets empirically supported by the history of mathematics and other exact sciences. An instructive instance of such a process is found in the history of the number zero. Without that insight due to some ancient Hindu mathematicians there could not arise such an axiomatic theory as PA. It defines the algorithms of arithmetical operations, which in turn help intuitions; those, inturn, give rise to algorithmic routines, not available in any of the previous phases of the process in question. While the logical substantiation of the point of this essay is a well-established result of logico-semantic inquiries, its empiricalclaim, based on historical evidences, remains open for discussion. Hence the author’s intention to address philosophers and historians of science, and to encourage their critical responses. (shrink)

The following inference is valid: There are exactly 101 dalmatians, There are exactly 100 food bowls, Each dalmatian uses exactly one food bowl Hence, at least two dalmatians use the same food bowl. Here, “there are at least 101 dalmatians” is nominalized as, "x1"x2…."x100$y(Dy & y ¹ x1 & y ¹ x2 & … & y ¹ x100) and “there are exactly 101 dalmatians” is nominalized as, "x1"x2…."x100$y(Dy & y ¹ x1 & y ¹ x2 & … & y ¹ (...) x100) & Ø"x1"x2…."x101$y(Dy & y ¹ x1 & y ¹ x2 & … & y ¹ x101). This is abbreviated $101xDx. The validity of the above inference corresponds to the valid formula, PHP(100): [$101xDx & $100xFx & "x(Dx ® Ff(x))] ® $x1$x2(Dx1 & Dx2 & x1 ¹ x2 & f(x1) = f(x2)). More generally, for variable n, the formula PHP(n) is PHP(n): [$n+1xDx & $nxFx & "x(Dx ® Ff(x))] ® $x1$x2(Dx1 & Dx2 & x1 ¹ x2 & f(x1) = f(x2)). A mathematical proof that PHP(n) is valid, for all n > 0, is quite short (less than a page), but refers to numbers, functions and sets. It uses the Pigeonhole Principle. This explains why PHP(n) is valid, for all n>0. However, I estimate that a predicate calculus derivation of PHP(100), using natural deduction, say, would require around 107 symbols. Unfeasibility Problem: nominalism is the radical anti-realist view that there are no numbers, functions or sets. So, how could a nominalist know that PHP(100) is valid, without directly performing the rather long derivation? Can the nominalist “ride piggyback” on the standard mathematical proof? If so, how is this justified? (shrink)

In ‘The varieties of indispensability arguments’ Marco Panza and Andrea Sereni argue that, for any clear notion of indispensability, either there is no conclusive argument for the thesis that mathematics is indispensable to science, or the notion of indispensability at hand does not support mathematical realism. In this paper, I shall not object to this main thesis directly. I shall instead try to assess in a naturalistic spirit a family of objections the authors make along the way to the use (...) of indispensability premises in indispensability arguments. (shrink)

Ranging from Alan Turing’s seminal 1936 paper to the latest work on Kolmogorov complexity and linear logic, this comprehensive new work clarifies the relationship between computability on the one hand and constructivity on the other. The authors argue that even though constructivists have largely shed Brouwer’s solipsistic attitude to logic, there remain points of disagreement to this day. Focusing on the growing pains computability experienced as it was forced to address the demands of rapidly expanding applications, the content maps the (...) developments following Turing’s ground-breaking linkage of computation and the machine, the resulting birth of complexity theory, the innovations of Kolmogorov complexity and resolving the dissonances between proof theoretical semantics and canonical proof feasibility. Finally, it explores one of the most fundamental questions concerning the interface between constructivity and computability: whether the theory of recursive functions is needed for a rigorous development of constructive mathematics. This volume contributes to the unity of science by overcoming disunities rather than offering an overarching framework. It posits that computability’s adoption of a classical, ontological point of view kept these imperatives separated. In studying the relationship between the two, it is a vital step forward in overcoming the disagreements and misunderstandings which stand in the way of a unifying view of logic. (shrink)