Hilbert arithmetic in a wide sense, including Hilbert arithmetic in a narrow sense consisting by two dual and anti-isometric Peano arithmetics, on the one hand, and the qubit Hilbert space (originating for the standard separable complex Hilbert space of quantum mechanics), on the other hand, allows for an arithmetic version of Gentzen’s cut elimination and quantum measurement to be described uniformy as two processes occurring accordingly in those two branches. A philosophical reflection also justifying that unity by quantum neo-Pythagoreanism links (...) it to the opposition of propositional logic, to which Gentzen’s cut rule refers immediately, on the one hand, and the linguistic and mathematical theory of metaphor therefore sharing the same structure borrowed from Hilbert arithmetic in a wide sense. An example by hermeneutical circle modeled as a dual pair of a syllogism (accomplishable also by a Turing machine) and a relevant metaphor (being a formal and logical mistake and thus fundamentally inaccessible to any Turing machine) visualizes human understanding corresponding also to Gentzen’s cut elimination and the Gödel dichotomy about the relation of arithmetic to set theory: either incompleteness or contradiction. The metaphor as the complementing “half” of any understanding of hermeneutical circle is what allows for that Gödel-like incompleteness to be overcome in human thought. (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)

Information can be considered as the most fundamental, philosophical, physical and mathematical concept originating from the totality by means of physical and mathematical transcendentalism (the counterpart of philosophical transcendentalism). Classical and quantum information, particularly by their units, bit and qubit, correspond and unify the finite and infinite. As classical information is relevant to finite series and sets, as quantum information, to infinite ones. A fundamental joint relativity of the finite and infinite, of the external and internal is to be investigated. (...) The corresponding invariance is able to define physical action and its quantity only on the basis of information and especially: on the relativity of classical and quantum information. The concept of transcendental time, an epoché in relation to the direction of time arrow can be defined. Its correlate is that information invariant to the finite and infinite, therefore unifying both classical and quantum information. (shrink)

The present paper is a continuation of a previous one by the same title, the content of which faced the issue concerning the relations of coreference and qualification in compliance with the Navya-Nyāya theoretical framework, although prompted by the Advaita-Vedānta enquiry regarding non-difference. In a complementary manner, by means of a formal analysis of equivalence, equality, and identity, this section closes the loop by assessing the extent to which non-difference, the main issue here, cannot be reduced to any of the (...) former. The following sections of this study will focus on the assessment of the eventual possibility of causation and transformation in non-difference. (shrink)

This paper examines the role of reason in Shepherd's account of acquiring knowledge of the external world via first principles. Reason is important, but does not have a foundational role. Certain principles enable us to draw the required inferences for acquiring knowledge of the external world. These principles are basic, foundational and, more importantly, self‐evident and thus justified in other ways than by demonstration. Justificatory demonstrations of these principles are neither required, nor possible. By drawing on textual and contextual evidence, (...) I will show that Shepherd should have said that we know the first principles of any science, in general, and that “everything which begins to exist must have a cause”, in particular, via intuition, not via reason. Reasoning about such principles can help their self‐evidence shine through in certain cases; their justification, and our being justified in believing them, does not come from this reasoning, however. (shrink)

The paper introduces and utilizes a few new concepts: “nonstandard Peano arithmetic”, “complementary Peano arithmetic”, “Hilbert arithmetic”. They identify the foundations of both mathematics and physics demonstrating the equivalence of the newly introduced Hilbert arithmetic and the separable complex Hilbert space of quantum mechanics in turn underlying physics and all the world. That new both mathematical and physical ground can be recognized as information complemented and generalized by quantum information. A few fundamental mathematical problems of the present such as Fermat’s (...) last theorem, four-color theorem as well as its new-formulated generalization as “four-letter theorem”, Poincaré’s conjecture, “P vs NP” are considered over again, from and within the new-founding conceptual reference frame of information, as illustrations. Simple or crucially simplifying solutions and proofs are demonstrated. The link between the consistent completeness of the system mathematics-physics on the ground of information and all the great mathematical problems of the present (rather than the enumerated ones) is suggested. (shrink)

Georg Cantor's absolute infinity, the paradoxical Burali-Forti class Ω of all ordinals, is a monstrous non-entity for which being called a "class" is an undeserved dignity. This must be the ultimate vexation for mathematical philosophers who hold on to some residual sense of realism in set theory. By careful use of Ω, we can rescue Georg Cantor's 1899 "proof" sketch of the Well-Ordering Theorem––being generous, considering his declining health. We take the contrapositive of Cantor's suggestion and add Zermelo's choice function. (...) This results in a concise and uncomplicated proof of the Well-Ordering Theorem. (shrink)

This monograph proposes a new way of implementing interaction in logic. It also provides an elementary introduction to Constructive Type Theory. The authors equally emphasize basic ideas and finer technical details. In addition, many worked out exercises and examples will help readers to better understand the concepts under discussion. One of the chief ideas animating this study is that the dialogical understanding of definitional equality and its execution provide both a simple and a direct way of implementing the CTT approach (...) within a game-theoretical conception of meaning. In addition, the importance of the play level over the strategy level is stressed, binding together the matter of execution with that of equality and the finitary perspective on games constituting meaning. According to this perspective the emergence of concepts are not only games of giving and asking for reasons, they are also games that include moves establishing how it is that the reasons brought forward accomplish their explicative task. Thus, immanent reasoning games are dialogical games of Why and How. (shrink)

Prolegomena It is fitting to begin this book on intuitionistic type theory by putting the subject matter into perspective. The purpose of this chapter is to ...

This paper presents a systematic study of the prehistory of the traditional subsystems of second-order arithmetic that feature prominently in the reverse mathematics program of Friedman and Simpson. We look in particular at: (i) the long arc from Poincar\'e to Feferman as concerns arithmetic definability and provability, (ii) the interplay between finitism and the formalization of analysis in the lecture notes and publications of Hilbert and Bernays, (iii) the uncertainty as to the constructive status of principles equivalent to Weak K\"onig's (...) Lemma, and (iv) the large-scale intellectual backdrop to arithmetical transfinite recursion in descriptive set theory and its effectivization by Borel, Lusin, Addison, and others. (shrink)

The volume includes twenty-five research papers presented as gifts to John L. Bell to celebrate his 60th birthday by colleagues, former students, friends and admirers. Like Bell’s own work, the contributions cross boundaries into several inter-related fields. The contributions are new work by highly respected figures, several of whom are among the key figures in their fields. Some examples: in foundations of maths and logic ; analytical philosophy, philosophy of science, philosophy of mathematics and decision theory and foundations of economics. (...) Most articles are contributions to current philosophical debates, but contributions also include some new mathematical results, important historical surveys, and a translation by Wilfrid Hodges of a key work of arabic logic. (shrink)

In the present paper we confront Martin- Löf’s analysis of the axiom of choice with J. Hintikka’s standing on this axiom. Hintikka claims that his game theoretical semantics for Independence Friendly Logic justifies Zermelo’s axiom of choice in a first-order way perfectly acceptable for the constructivists. In fact, Martin- Löf’s results lead to the following considerations:Hintikka preferred version of the axiom of choice is indeed acceptable for the constructivists and its meaning does not involve higher order logic.However, the version acceptable (...) for constructivists is based on an intensional take on functions. Extensionality is the heart of the classical understanding of Zermelo’s axiom and this is the real reason behind the constructivist rejection of it.More generally, dependence and independence features that motivate IF-Logic, can be formulated within the frame of constructive type theory without paying the price of a system that is neither axiomatizable nor has an underlying theory of inference – logic is about inference after all.We conclude pointing out that recent developments in dialogical logic show that the CTT approach to meaning in general and to the axiom of choice in particular is very natural to game theoretical approaches where metalogical features are explicitly displayed at the object language-level. Thus, in some way, this vindicates, albeit in quite of a different manner, Hintikka’s plea for the fruitfulness of game-theoretical semantics in the context of the foundations of mathematics. (shrink)

Scientific research in the formal sciences comes in multiple degrees of formality: fully formal work; rigorous proofs that practitioners know to be formalizable in principle; and informal work like rough proof sketches and considerations about the advantages and disadvantages of various formal systems. This informal work includes informal and semi-formal debates between formal scientists, e.g. about the acceptability of foundational principles and proposed axiomatizations. In this paper, we propose to use the methodology of structured argumentation theory to produce a formal (...) model of such informal and semi-formal debates in the formal sciences. For this purpose, we propose ASPIC-END, an adaptation of the structured argumentation framework ASPIC+ which can incorporate natural deduction style arguments and explanations. We illustrate the applicability of the framework to debates in the formal sciences by presenting a simple model of some arguments about proposed solutions to the Liar paradox, and by discussing a more extensive—but still preliminary—model of parts of the debate that mathematicians had about the Axiom of Choice in the early twentieth century. (shrink)

This essay consists of two parts. In the first part, I focus my attention on the remarks that Frege makes on consistency when he sets about criticizing the method of creating new numbers through definition or abstraction. This gives me the opportunity to comment also a little on H. Hankel, J. Thomae—Frege’s main targets when he comes to criticize “formal theories of arithmetic” in Die Grundlagen der Arithmetik (1884) and the second volume of Grundgesetze der Arithmetik (1903)—G. Cantor, L. E. (...) J. Brouwer and D. Hilbert (1899). Part 2 is mainly devoted to Hilbert’s proof theory of the 1920s (1922–1931). I begin with an account of his early attempt to prove directly, and thus not by reduction or by constructing a model, the consistency of (a fragment of) arithmetic. In subsequent sections, I give a kind of overview of Hilbert’s metamathematics of the 1920s and try to shed light on a number of difficulties to which it gives rise. One serious difficulty that I discuss is the fact, widely ignored in the pertinent literature on Hilbert’s programme, that his language of finitist metamathematics fails to supply the conceptual resources for formulating a consistency statement qua unbounded quantification. Along the way, I shall comment on W. W. Tait’s objection to an interpretation of Hilbert’s finitism by Niebergall and Schirn, on G. Gentzen’s allegedly finitist consistency proof for Peano Arithmetic as well as his ideas on the provability and unprovability of initial cases of transfinite induction in pure number theory. Another topic I deal with is what has come to be known as partial realizations of Hilbert’s programme, chiefly advocated by S. G. Simpson. Towards the end of this essay, I take a critical look at Wittgenstein’s views about (in)consistency and consistency proofs in the period 1929–1933. I argue that both his insouciant attitude towards the emergence of a contradiction in a calculus and his outright repudiation of metamathematical consistency proofs are unwarranted. In particular, I argue that Wittgenstein falls short of making a convincing case against Hilbert’s programme. I conclude with some philosophical remarks on consistency proofs and soundness and raise a question concerning the consistency of analysis. (shrink)

From 1908 to 1916, articles supporting the axiom of choice were scant. The situation changed in 1916, when Wacław Sierpiński published a series of articles reviving the debate. The posterity of the axiom of choice as we know it would be unimaginable without Sierpiński’s efforts.

An idea attributable to Russell serves to extend Zermelo’s theory of systems of infinitely long propositions to infinitary relations. Specifically, relations over a given domain \ of individuals will now be identified with propositions over an auxiliary domain \ subsuming \. Three applications of the resulting theory of infinitary relations are presented. First, it is used to reconstruct Zermelo’s original theory of urelements and sets in a manner that achieves most, if not all, of his early aims. Second, the new (...) account of infinitary relations makes possible a concise characterization of parametric definability with respect to a purely relational structure. Finally, based on his foundational philosophy of the primacy of the infinite, Zermelo rejected Gödel’s First Incompleteness Theorem; it is shown that the new theory of infinitary relations can be brought to bear, positively, in that connection as well. (shrink)

Post-war argumentation theorists have tended to regard argumentation as one thing and mathematical proof as another. Perelman (1958, 1969), for example, defined the word ‘argumentation’ stipulatively as a contrast term to ‘demonstration’: whereas mathematical reasoning as theorized by modern formal logic, he writes, is a matter of deducing theorems from axioms in accordance with stipulated rules of transformation, argumentation aims at gaining the adherence of minds (Perelman 1969, pp. 1–2). Toulmin (1958) contrasted his “jurisprudential model” of argument, according to which (...) the validity of an argument is a matter of its following proper procedure, with a “geometrical model” according to which validity is a matter of its having a proper shape comparable to the shape of a triangle (Toulmin 1958, p. 95). Johnson (2000, pp. 231–232) argues explicitly that a mathematical proof is not an argument.In the collection under review, Andrew Aberdein and Ian Dove have assembled a number of recent. (shrink)

In this paper I discuss Ernst Zermelo’s ideas concerning the possibility of developing a system of infinitary logic that, in his opinion, should be suitable for mathematical inferences. The presentation of Zermelo’s ideas is accompanied with some remarks concerning the development of infinitary logic. I also stress the fact that the second axiomatization of set theory provided by Zermelo in 1930 involved the use of extremal axioms of a very specific sort.1.

We analyze the representation of binary relations in general, and in particular of functions and of total antisymmetric relations, in monadic third order logic, that is, the simple typed theory of sets with three types. We show that there is no general representation of functions or of total antisymmetric relations in this theory. We present partial representations of functions and of total antisymmetric relations which work for large classes of these relations, and show that there is an adequate representation of (...) cardinality in this theory. The relation of our work to similar work by Henrard and Allen Hazen is discussed. This work can be understood as part of a program of assessing the capabilities of weak logical frameworks: our results are applicable for example, to the framework in David Lewis’s Parts of Classes. (shrink)

Inferential communities are communities using specific substantial argumentative schemes. The religious or scientific communities are examples. I discuss the status of the mathematical community as it appears through the position held by the French mathematician Henri Poincaré during his famous ar-guments with Russell, Hilbert, Peano and Cantor. The paper focuses on the status of complete induction and how logic and psychology shape the community of mathematicians and the teaching of mathematics.