This paper concerns Alan Turing’s ideas about machines, mathematical methods of proof, and intelligence. By the late 1930s, Kurt Gödel and other logicians, including Turing himself, had shown that no finite set of rules could be used to generate all true mathematical statements. Yet according to Turing, there was no upper bound to the number of mathematical truths provable by intelligent human beings, for they could invent new rules and methods of proof. So, the output of a human mathematician, for (...) Turing, was not a computable sequence (i.e., one that could be generated by a Turing machine). Since computers only contained a finite number of instructions (or programs), one might argue, they could not reproduce human intelligence. Turing called this the “mathematical
objection” to his view that machines can think. Logico-mathematical reasons, stemming from his own work, helped to convince Turing that it should be possible to reproduce human intelligence, and eventually compete with it, by developing the appropriate kind of digital computer. He felt it
should be possible to program a computer so that it could learn or discover new rules, overcoming the limitations imposed by the incompleteness and undecidability results in the same way that human
mathematicians presumably do. (shrink)

In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert's programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert's epsilon-substitution method. There was, however, a second approach which was not reflected in the publications of the Hilbert school in the 1920s, and which is a direct precursor of Hilbert's first epsilon theorem and a certain "general consistency result" due to Bernays. An analysis of the form of this so-called "failed proof" (...) sheds further light on an interpretation of Hilbert's programme as an instrumentalist enterprise with the aim of showing that whenever a "real" proposition can be proved by ?ideal? means, it can also be proved by "real", finitary means. (shrink)

This article presents an historical and conceptual overview on different approaches to logical abstraction. Two main trends concerning abstraction in the history of logic are highlighted, starting from the logical notions of concept and function. This analysis strictly relates to the philosophical discussion on the nature of abstract objects. I develop this issue further with respect to the procedure of abstraction involved by (typed) λ-systems, focusing on the crucial change about meaning and predicability. In particular, the analysis of the nature (...) of logical types in the context of Constructive Type Theory allows elucidation of the role of the previously introduced notions. Finally, the connection to the analysis of abstraction in computer science is drawn, and the methodological contribution provided by the notion of information is considered, showing its conceptual and technical relevance. Future research shall focus on the notion of information in distributed systems, analysing the paradigm of information hiding in dependent type theories. (shrink)

A comparison is given between two conditions used to define logical constants: Belnap's uniqueness and Hacking's deducibility of identicals. It is shown that, in spite of some surface similarities, there is a deep difference between them. On the one hand, deducibility of identicals turns out to be a weaker and less demanding condition than uniqueness. On the other hand, deducibility of identicals is shown to be more faithful to the inferentialist perspective, permitting definition of genuinely proof-theoretical concepts. This kind of (...) analysis is driven by exploiting the Curry–Howard correspondence. In particular, deducibility of identicals is shown to correspond to the computational property of eta expansion, which is essential in the characterization of propositional identity. (shrink)

By supplying propositional calculus with a probability semantics we showed, in our 1996, that finite stochastic problems can be treated by logic-theoretic means equally as well as by the usual set-theoretic ones. In the present paper we continue the investigation to further the use of logical notions in probability theory. It is shown that quantifier logic, when supplied with a probability semantics, is capable of treating stochastic problems involving countably many trials.

The terms of a mathematical problem become precise and concise if they are expressed in an appropriate notation, therefore notations are useful to mathematics. But are notations only useful, or also essential? According to prevailing view, they are not essential. Contrary to this view, this paper argues that notations are essential to mathematics, because they may play a crucial role in mathematical discovery. Specifically, since notations may consist of symbolic notations, diagrammatic notations, or a mix of symbolic and diagrammatic notations, (...) notations may play a crucial role in mathematical discovery in different ways. Some examples are given to illustrate these ways. (shrink)

In the early 1920s, the German mathematician David Hilbert (1862–1943) put forward a new proposal for the foundation of classical mathematics which has come to be known as Hilbert's Program. It calls for a formalization of all of mathematics in axiomatic form, together with a proof that this axiomatization of mathematics is consistent. The consistency proof itself was to be carried out using only what Hilbert called “finitary” methods. The special epistemological character of finitary reasoning then yields the required justification (...) of classical mathematics. Although Hilbert proposed his program in this form only in 1921, various facets of it are rooted in foundational work of his going back until around 1900, when he first pointed out the necessity of giving a direct consistency proof of analysis. Work on the program progressed significantly in the 1920s with contributions from logicians such as Paul Bernays, Wilhelm Ackermann, John von Neumann, and Jacques Herbrand. It was also a great influence on Kurt Gödel, whose work on the incompleteness theorems were motivated by Hilbert's Program. Gödel's work is generally taken to show that Hilbert's Program cannot be carried out. It has nevertheless continued to be an influential position in the philosophy of mathematics, and, starting with the work of Gerhard Gentzen in the 1930s, work on so-called Relativized Hilbert Programs have been central to the development of proof theory. (shrink)