_'Nagel and Newman accomplish the wondrous task of clarifying the argumentative outline of Kurt Godel's celebrated logic bomb.'_ _– The Guardian_ In 1931 the mathematical logician Kurt Godel published a revolutionary paper that challenged certain basic assumptions underpinning mathematics and logic. A colleague of physicist Albert Einstein, his theorem proved that mathematics was partly based on propositions not provable within the mathematical system. The importance of Godel's Proof rests upon its radical implications and has echoed throughout many fields, from (...) maths to science to philosophy, computer design, artificial intelligence, even religion and psychology. While others such as Douglas Hofstadter and Roger Penrose have published bestsellers based on Godel’s theorem, this is the first book to present a readable explanation to both scholars and non-specialists alike. A gripping combination of science and accessibility, _Godel’s Proof_ by Nagel and Newman is for both mathematicians and the idly curious, offering those with a taste for logic and philosophy the chance to satisfy their intellectual curiosity. _Kurt Godel_ Born in Brunn, he was a colleague of physicist Albert Einstein and professor at the Institute for Advanced Study in Princeton, N.J. (shrink)

When ordinary people - mathematicians among them - take something to follow from something else, they are exposing the backbone of our self-ascribed ability to reason. Jody Azzouni investigates the connection between that ordinary notion of consequence and the formal analogues invented by logicians. One claim of the book is that, despite our apparent intuitive grasp of consequence, we do not introspect rules by which we reason, nor do we grasp the scope and range of the domain, as it were, (...) of our reasoning. This point is illustrated with a close analysis of a paradigmatic case of ordinary reasoning: mathematical proof. (shrink)

Much recent work on mathematical explanation has presupposed that the phenomenon involves explanatory proofs in an essential way. I argue that this view, ‘proof chauvinism’, is false. I then look in some detail at the explanation of the solvability of polynomial equations provided by Galois theory, which has often been thought to revolve around an explanatory proof. The article concludes with some general worries about the effects of chauvinism on the theory of mathematical explanation. 1Introduction 2Why I Am (...) Not a Proof Chauvinist 2.1Proof chauvinism and mathematical practice 2.2Proof chauvinism and philosophy 3An Example: Galois Theory and Explanatory Proof 4Conclusion. (shrink)

The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the epsilon-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic interpretations. (...) The problems facing the development of proof-theoretically well-behaved systems are outlined. (shrink)

Linear logic is a new logic which was recently developed by Girard in order to provide a logical basis for the study of parallelism. It is described and investigated in Gi]. Girard's presentation of his logic is not so standard. In this paper we shall provide more standard proof systems and semantics. We shall also extend part of Girard's results by investigating the consequence relations associated with Linear Logic and by proving corresponding str ong completeness theorems. Finally, we shall (...) investigate the relation between Linear Logic and previously known systems, especially Relevance logics. (shrink)

The current paper studies the formal properties of the Global Reflection Principle, to wit the assertion “All theorems of$\mathrm {Th}$are true,” where$\mathrm {Th}$is a theory in the language of arithmetic and the truth predicate satisfies the usual Tarskian inductive conditions for formulae in the language of arithmetic. We fix the gap in Kotlarski’s proof from [15], showing that the Global Reflection Principle for Peano Arithmetic is provable in the theory of compositional truth with bounded induction only ($\mathrm {CT}_0$). Furthermore, (...) we extend the above result showing that$\Sigma _1$-uniform reflection over a theory of uniform Tarski biconditionals ($\mathrm {UTB}^-$) is provable in$\mathrm {CT}_0$, thus answering the question of Beklemishev and Pakhomov [2]. Finally, we introduce the notion of a prolongable satisfaction class and use it to study the structure of models of$\mathrm {CT}_0$. In particular, we provide a new model-theoretical characterization of theories of finite iterations of uniform reflection and present a new proof characterizing the arithmetical consequences of$\mathrm {CT}_0$. (shrink)

This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that the two introductory (...) articles come first; these are then followed by articles from core classical areas of proof theory; the handbook concludes with articles that deal with topics closely related to computer science. (shrink)

On a traditional view, the primary role of a mathematical proof is to warrant the truth of the resulting theorem. This view fails to explain why it is very often the case that a new proof of a theorem is deemed important. Three case studies from elementary arithmetic show, informally, that there are many criteria by which ordinary proofs are valued. I argue that at least some of these criteria depend on the methods of inference the proofs employ, (...) and that standard models of formal deduction are not well-equipped to support such evaluations. I discuss a model of proof that is used in the automated deduction community, and show that this model does better in that respect. (shrink)

In this paper, we discuss the prevailing view amongst philosophers and many mathematicians concerning mathematical proof. Following Cellucci, we call the prevailing view the “axiomatic conception” of proof. The conception includes the ideas that: a proof is finite, it proceeds from axioms and it is the final word on the matter of the conclusion. This received view can be traced back to Frege, Hilbert and Gentzen, amongst others, and is prevalent in both mathematical text books and logic (...) text books. (shrink)

According to what has become a standard history of quantum mechanics, von Neumann in 1932 succeeded in convincing the physics community that he had proved that hidden variables were impossible as a matter of principle. Subsequently, leading proponents of the Copenhagen interpretation emphatically confirmed that von Neumann's proof showed the completeness of quantum mechanics. Then, the story continues, Bell in 1966 finally exposed the proof as seriously and obviously wrong; this rehabilitated hidden variables and made serious foundational research (...) possible. It is often added in recent accounts that von Neumann's error had been spotted almost immediately by Grete Hermann, but that her discovery was of no effect due to the dominant Copenhagen Zeitgeist. We shall attempt to tell a more balanced story. Most importantly, von Neumann did not claim to have shown the impossibility of hidden variables tout court, but argued that hidden-variable theories must possess a structure that deviates fundamentally from that of quantum mechanics. Both Hermann and Bell appear to have missed this point; moreover, both raised unjustified technical objections to the proof. Von Neumann's conclusion was basically that hidden-variables schemes must violate the "quantum principle" that all physical quantities are to be represented by operators in a Hilbert space. According to this conclusion, hidden-variables schemes are possible in principle but necessarily exhibit a certain kind of contextuality. As we shall illustrate, early reactions to Bohm's theory are in agreement with this account. Leading physicists pointed out that Bohm's theory has the strange feature that particle properties do not generally reveal themselves in measurements, in accordance with von Neumann's result. They did not conclude that the "impossible was done" and that von Neumann had been shown wrong. (shrink)

Theism and its cousins, atheism and agnosticism, are seldom taken to task for logical-epistemological incoherence. This paper provides a condensed proof that not only theism, but atheism and agnosticism as well, are all of them conceptually self-undermining, and for the same reason: All attempt to make use of the concept of “transcendent reality,” which here is shown not only to lack meaning, but to preclude the very possibility of meaning. In doing this, the incoherence of theism, atheism, and agnosticism (...) is secondary to the more general incoherence of any attempts to refer to so-called “transcendent realities.” A recognition of the conceptually fundamental incoherence of theism, atheism, and agnosticism compels our rational assent to a position the author names “paratheism.”. (shrink)

The role of audiences in mathematical proof has largely been neglected, in part due to misconceptions like those in Perelman and Olbrechts-Tyteca which bar mathematical proofs from bearing reflections of audience consideration. In this paper, I argue that mathematical proof is typically argumentation and that a mathematician develops a proof with his universal audience in mind. In so doing, he creates a proof which reflects the standards of reasonableness embodied in his universal audience. Given this framework, (...) we can better understand the introduction of proof methods based on the mathematician’s likely universal audience. I examine a case study from Alexander and Briggs’s work on knot invariants to show that we can fruitfully reconstruct mathematical methods in terms of audiences. (shrink)

Crispin Wright; IV*—On Putnam's Proof that We are not Brains-in-a-Vat1, Proceedings of the Aristotelian Society, Volume 92, Issue 1, 1 June 1992, Pages 67–94, h.

Open texture is a kind of semantic indeterminacy first systematically studied by Waismann. In this paper, extant definitions of open texture will be compared and contrasted, with a view towards the consequences of open-textured concepts in mathematics. It has been suggested that these would threaten the traditional virtues of proof, primarily the certainty bestowed by proof-possession, and this suggestion will be critically investigated using recent work on informal proof. It will be argued that informal proofs have virtues (...) that mitigate the danger posed by open texture. Moreover, it will be argued that while rigor in the guise of formalisation and axiomatisation might banish open texture from mathematical theories through implicit definition, it can do so only at the cost of restricting the tamed concepts in certain ways. (shrink)

Truth-maker analyses construe truth as existence of proof, a well-known example being that offered by Wittgenstein in theTractatus. The paper subsumes the intuitionistic view of truth as existence of proof under the general truth-maker scheme. Two generic constraints on truth-maker analysis are noted and positioned with respect to the writings of Michael Dummett and theTractatus. Examination of the writings of Brouwer, Heyting and Weyl indicates the specific notions of truth-maker and existence that are at issue in the intuitionistic (...) truth-maker analysis, namely that of proof in the sense of proof-object (Brouwer, Heyting) and existence in the nonpropositional sense of a judgement abstract (Weyl). Furthermore, possible anticipations in the writings of Schlick and Pfänder are noted. (shrink)

Public and professional debates have come to rely heavily on a special type of reasoning: the argument-from-ignorance, in which conclusions depend on the _lack_ of compelling information. "I win my argument," says the skillful advocate, "unless you can prove that I am wrong." This extraordinary gambit has been largely ignored in modern rhetorical and philosophical studies. Yet its broad force can be demonstrated by analogy with the modern legal system, where courts have long manipulated burdens of proof with skill (...) and subtlety. This legal, philosophical, and rhetorical study by Richard H. Gaskins provides the first systematic treatment of arguments-from-ignorance across a wide range of modern discourse—from constitutional law, scientific inquiry, and moral philosophy to organizational behavior, computer operation, and personal interaction. Gaskins reviews the historic shifts in constitutional proof burdens that have shaped public debate on fundamental rights and, by analogy, on the fundamental status of intellectual and cultural authority. He shows how similar shifts have dominated polemical battles between scientific and ethical modes of authority, affecting both academic and popular discussion. Finally, he discovers the philosophical roots of default reasoning strategies in the arguments of Kant and nineteenth-century Kantian schools. Concluding that shifting proof burdens are inescapable in a world of scientific and moral uncertainty, Gaskins emphasizes the common strategic ground shared by dogmatic and skeptical reasoning. Using Hegelian strategies, he describes a more pluralistic temper that can move critical thinking beyond polemics and strengthen our capacities for common discourse. (shrink)

We investigated whether mathematicians typically agree about the qualities of mathematical proofs. Between-mathematician consensus in proof appraisals is an implicit assumption of many arguments made by philosophers of mathematics, but to our knowledge the issue has not previously been empirically investigated. We asked a group of mathematicians to assess a specific proof on four dimensions, using the framework identified by Inglis and Aberdein (2015). We found widespread disagreement between our participants about the aesthetics, intricacy, precision and utility of (...) the proof, suggesting that a priori assumptions about the consistency of mathematical proof appraisals are unreasonable. (shrink)

The notion of “the burden of proof” plays an important role in real-world argumentation contexts, in particular in law. It has also been given a central role in normative accounts of argumentation, and has been used to explain a range of classic argumentation fallacies. We argue that in law the goal is to make practical decisions whereas in critical discussion the goal is frequently simply to increase or decrease degree of belief in a proposition. In the latter case, it (...) is not necessarily important whether that degree of belief exceeds a particular threshold (e.g., ‘reasonable doubt’). We explore the consequences of this distinction for the role that the “burden of proof” has played in argumentation and in theories of fallacy. (shrink)

This paper uses some modest claims about knowledge to identify a significant problem for contemporary American trial procedure. First, suppose that legal proof requires knowledge. In particular, suppose that the defendant in a jury trial is proven guilty only if the jury knows that the defendant is guilty. Second, suppose that knowledge is subject to pragmatic encroachment. In particular, whether the jury knows the defendant is guilty depends on what’s at stake in their decision to convict, including the consequences (...) that the defendant may face if convicted. Then in order to know whether a defendant has been proven guilty, jurors may need to know something about the potential consequences of conviction. But in nearly every American criminal trial, this information is withheld from jurors. -/- In §1, I lay out the philosophical premises of my argument. In §2, I say more about why these premises present a problem for American trial procedure, and I identify social and political structures that exacerbate the problem. I describe the reasoning that has led courts to withhold sentencing information from jurors, and I diagnose the flaw in this reasoning. In §3, I expand my initial argument, strengthening its conclusions and offering alternative sets of premises that still entail them. I argue that the legal ramifications of pragmatic encroachment depend on highly controversial questions in epistemology, questions about the precise nature of practical stakes. In §4, I propose strategies for legal reform. (shrink)

On some views, we can be sure that parties to a dispute over the logic of ‘exists’ are not talking past each other if they can characterise ‘exists’ as the only monadic predicate up to logical equivalence obeying a certain set of rules of inference. Otherwise, we ought to be suspicious about the reality of their disagreement. This is what we call a proof- theoretic argument. Pace some critics, who have tried to use proof-theoretic arguments to cast doubts (...) about the reality of disagreements about the logic of ‘exists’, we argue that proof-theoretic arguments can be deployed to establish the reality of several such disagreements. Along the way, we will also utilise this technique to establish similar results about some disagreements over the logic of identity. (shrink)

Truth Through Proof defends an anti-platonist philosophy of mathematics derived from game formalism. Alan Weir aims to develop a more satisfactory successor to game formalism utilising a widely accepted, broadly neo-Fregean framework, in which the proposition expressed by an utterance is a function of both sense and background circumstance.

This is the first book-length treatment of hybrid logic and its proof-theory. Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a model. This is useful for many applications, for example when reasoning about time one often wants to formulate a series of statements about what happens at specific times. There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships (...) between proof systems for different modal logics are often unclear. In the present book we demonstrate that hybrid-logical proof-theory remedies these deficiencies by giving a spectrum of well-behaved proof systems for a spectrum of different hybrid logics. (shrink)

Various real and imagined criminal law cases rest on “naked statistical evidence”. That is, they rest more or less entirely on a probability for guilt/liability derived from a single statistical model. The intuition is that there is something missing in these cases, high as the probability for guilt/liability may be, such that the relevant standard for legal proof is not met. Here we contribute to the considerable debate about how this intuition is best explained and what it teaches us (...) about evidential reasoning in the legal setting. We part ways with the recent scholarship, however. Unlike most others, our diagnosis is not that there is an important qualitative property that some evidence or bodies of evidence have, and that naked statistical evidence, most strikingly, lacks. Rather, we see cases resting on naked statistical evidence as lying at the extreme of a continuum of cases that are vulnerable to challenge due to “meta-uncertainty” about the underlying model. (shrink)

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus $\mathtt{SC2Int}$ for the bi-intuitionistic logic $\mathtt{2Int}$. A distinctive feature of $\mathtt{SC2Int}$ is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of $\mathtt{SC2Int}$, in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, mediated (...) through two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of $\mathtt{2Int}$. By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in $\mathtt{SC2Int}$ is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously. (shrink)

I have argued that without an adequate solution to the knower paradox Fitch's Proof is- or at least ought to be-ineffective against verificationism. Of course, in order to follow my suggestion verificationists must maintain that there is currently no adequate solution to the knower paradox, and that the paradox continues to provide prima facie evidence of inconsistent knowledge. By my lights, any glimpse at the literature on paradoxes offers strong support for the first thesis, and any honest, non-dogmatic reflection (...) on the knower paradox provides strong support for the second. Whether verificationists want to go the route I've suggested is not for me todecide. As in the previous section my aim has been that of defending the mere viability of verificationism in the face of what many, many philosophers have taken to be its death-knell, namely Fitch's Proof. But, as the final objection makes clear, showing that verificationism can live in the face of Fitch's Proof is one thing; showing that it should live is another project. If nothing else, I hope that this papershows that verificationists still have a project to pursue; Fitch's Proof, contrary to popular opinion, need not bury verificationism.13. (shrink)

This open access book is a superb collection of some fifteen chapters inspired by Schroeder-Heister's groundbreaking work, written by leading experts in the field, plus an extensive autobiography and comments on the various contributions by Schroeder-Heister himself. For several decades, Peter Schroeder-Heister has been a central figure in proof-theoretic semantics, a field of study situated at the interface of logic, theoretical computer science, natural-language semantics, and the philosophy of language. -/- The chapters of which this book is composed discuss (...) the subject from a rich variety of angles, including the history of logic, the proper interpretation of logical validity, natural deduction rules, the notions of harmony and of synonymy, the structure of proofs, the logical status of equality, intentional phenomena, and the proof theory of second-order arithmetic. All chapters relate directly to questions that have driven Schroeder-Heister's own research agenda and to which he has made seminal contributions. The extensive autobiographical chapter not only provides a fascinating overview of Schroeder-Heister's career and the evolution of his academic interests but also constitutes a contribution to the recent history of logic in its own right, painting an intriguing picture of the philosophical, logical, and mathematical institutional landscape in Germany and elsewhere since the early 1970s. The papers collected in this book are illuminatingly put into a unified perspective by Schroeder-Heister's comments at the end of the book. Both graduate students and established researchers in the field will find this book an excellent resource for future work in proof-theoretic semantics and related areas. (shrink)

In his Remarks on the Foundations of Mathematics, Wittgenstein claims, puzzlingly, that ‘the proof creates a new concept’ (RFM III-41). This paper aims to contribute to clarifying this idea, and to showing how it marks a major break with the traditional conception of proof. Moreover, since the most natural way to understand his claim is open to criticism, a secondary goal of what follows is to offer an interpretation of it that neutralizes the objection. The discussion proceeds by (...) analysing a well-known geometrical proof. (shrink)

I present an account of truth values for classical logic, intuitionistic logic, and the modal logic S5, in which truth values are not a fundamental category from which the logic is defined, but rather, an idealisation of more fundamental logical features in the proof theory for each system. The result is not a new set of semantic structures, but a new understanding of how the existing semantic structures may be understood in terms of a more fundamental notion of logical (...) consequence. (shrink)

According to Jim Pryor’s dogmatism, if you have an experience as if P, you acquire immediate prima facie justification for believing P. Pryor contends that dogmatism validates Moore’s infamous proof of a material world. Against Pryor, I argue that if dogmatism is true, Moore’s proof turns out to be non-transmissive of justification according to one of the senses of non-transmissivity defined by Crispin Wright. This type of non-transmissivity doesn’t deprive dogmatism of its apparent antisceptical bite.

We give a simple proof-theoretic argument showing that Glivenko’s theorem for propositional logic and its version for predicate logic follow as an easy consequence of the deduction theorem, which also proves some Glivenko type theorems relating intermediate predicate logics between intuitionistic and classical logic. We consider two schemata, the double negation shift (DNS) and the one consisting of instances of the principle of excluded middle for sentences (REM). We prove that both schemata combined derive classical logic, while each one (...) of them provides a strictly weaker intermediate logic, and neither of them is derivable from the other. We show that over every intermediate logic there exists a maximal intermediate logic for which Glivenko’s theorem holds. We deduce as well a characterization of DNS, as the weakest (with respect to derivability) scheme that added to REM derives classical logic. (shrink)

Gentzen’s sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut elimination and consistency for classical and intuitionistic logics. Among the undesirable features of those sequent calculi is that their inferences rules are low-level and frequently permute over each other. As a result, large-scale structures within sequent calculus proofs are hard to identify. In this (...) paper, we present a different approach to designing a sequent calculus for classical logic. Starting with Gentzen’s LK proof system, we examine the proof search meaning of his inference rules and classify those rules as involving either don’t care nondeterminism or don’t know nondeterminism. Based on that classification, we design the focused proof system LKF in which inference rules belong to one of two phases of proof construction depending on which flavor of nondeterminism they involve. We then prove that the cut rule and the general form of the initial rule are admissible in LKF. Finally, by showing that the inference rules for LK are all admissible in LKF, we can give a relative completeness proof for LKF provability with respect to LK provability. We shall also apply these properties of the LKF proof system to establish other meta-theoretic properties of classical logic, including Herbrand’s theorem. (shrink)

This book represents a new departure in science studies: an analysis of a scientific style of writing, situating it within the context of the contemporary style of literature. Its philosophical significance is that it provides a novel way of making sense of the notion of a scientific style. For the first time, the Hellenistic mathematical corpus - one of the most substantial extant for the period - is placed centre-stage in the discussion of Hellenistic culture as a whole. Professor Netz (...) argues that Hellenistic mathematical writings adopt a narrative strategy based on surprise, a compositional form based on a mosaic of apparently unrelated elements, and a carnivalesque profusion of detail. He further investigates how such stylistic preferences derive from, and throw light on, the style of Hellenistic poetry. This important book will be welcomed by all scholars of Hellenistic civilization as well as historians of ancient science and Western mathematics. (shrink)