This volume examines the limitations of mathematical logic and proposes a new approach to logic intended to overcome them. To this end, the book compares mathematical logic with earlier views of logic, both in the ancient and in the modern age, including those of Plato, Aristotle, Bacon, Descartes, Leibniz, and Kant. From the comparison it is apparent that a basic limitation of mathematical logic is that it narrows down the scope of logic confining it to the study of deduction, without (...) providing tools for discovering anything new. As a result, mathematical logic has had little impact on scientific practice. Therefore, this volume proposes a view of logic according to which logic is intended, first of all, to provide rules of discovery, that is, non-deductive rules for finding hypotheses to solve problems. This is essential if logic is to play any relevant role in mathematics, science and even philosophy. To comply with this view of logic, this volume formulates several rules of discovery, such as induction, analogy, generalization, specialization, metaphor, metonymy, definition, and diagrams. A logic based on such rules is basically a logic of discovery, and involves a new view of the relation of logic to evolution, language, reason, method and knowledge, particularly mathematical knowledge. It also involves a new view of the relation of philosophy to knowledge. This book puts forward such new views, trying to open again many doors that the founding fathers of mathematical logic had closed historically. (shrink)

According to a main idea of Gentzen the meanings of the logical constants are reflected by the introduction rules in his system of natural deduction. This idea is here understood as saying roughly that a closed argument ending with an introduction is valid provided that its immediate subarguments are valid and that other closed arguments are justified to the extent that they can be brought to introduction form. One main part of the paper is devoted to the exact development of (...) this notion. Another main part of the paper is concerned with a modification of this notion as it occurs in Michael Dummett’s book The Logical Basis of Metaphysics. The two notions are compared and there is a discussion of how they fare as a foundation for a theory of meaning. It is noted that Dummett’s notion has a simpler structure, but it is argued that it is less appropriate for the foundation of a theory of meaning, because the possession of a valid argument for a sentence in Dummett’s sense is not enough to be warranted to assert the sentence. (shrink)

In the proof-theoretic semantics approach to meaning, harmony , requiring a balance between introduction-rules (I-rules) and elimination rules (E-rules) within a meaning conferring natural-deduction proof-system, is a central notion. In this paper, we consider two notions of harmony that were proposed in the literature: 1. GE-harmony , requiring a certain form of the E-rules, given the form of the I-rules. 2. Local intrinsic harmony : imposes the existence of certain transformations of derivations, known as reduction and expansion . We propose (...) a construction of the E-rules (in GE-form) from given I-rules, and prove that the constructed rules satisfy also local intrinsic harmony. The construction is based on a classification of I-rules, and constitute an implementation to Gentzen’s (and Pawitz’) remark, that E-rules can be “read off” I-rules. (shrink)

The standard approach to what I call “proof-theoretic semantics”, which is mainly due to Dummett and Prawitz, attempts to give a semantics of proofs by defining what counts as a valid proof. After a discussion of the general aims of proof-theoretic semantics, this paper investigates in detail various notions of proof-theoretic validity and offers certain improvements of the definitions given by Prawitz. Particular emphasis is placed on the relationship between semantic validity concepts and validity concepts used in normalization theory. It (...) is argued that these two sorts of concepts must be kept strictly apart. (shrink)

Proof-theoretic semantics is an alternative to model-theoretic semantics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence relation (...) to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof-theoretic semantics is the one given by the sequent-to-sequent derivability relation in Gentzen systems. (shrink)

The fundamental problem of Christology is the apparent contradiction of Christ as recorded at Chalcedon. Christ is human and Christ is divine. Being divine entails being immutable. Being human entails being mutable. Were Christ two different persons there’d be no apparent contradiction. But Chalcedon rules as much out. Were Christ only partly human or only partly divine there’d be no apparent contradiction. But Chalcedon rules as much out. Were the very meaning of ‘mutable’ and/or ‘immutable’ other than what they are, (...) there’d be no apparent contradiction. But the meaning is what it is, and changing the meaning of our terms to avoid the apparent contradiction of Christ is an apparent flight from reality. What, in the end, is the explanation of the apparent contradiction of Christ? Theologians and philosophers have long advanced many consistency-seeking answers, all of which increase the metaphysical or semantical complexity of the otherwise strikingly simple but radical core of Christianity’s GodMan. In this paper, I put the simplest explanation on the theological table: namely, Christ appears to be contradictory because Christ is contradictory. This explanation may sound complicated to the many who are steeped in the mainstream account of logic according to which logic precludes the possibility of true contradictions. But the mainstream account of logic can and should be rejected. Ridding theology of the dogma of mainstream logic illuminates the simple though striking explanation of the apparent contradiction of Christ — namely, that Christ is a contradictory being. Just as the simplest explanation to the apparent roundness of the earth has earned due acceptance, so too should the simplest explanation of the apparent contradiction of Christ. (shrink)

This volume is the first ever collection devoted to the field of proof-theoretic semantics. Contributions address topics including the systematics of introduction and elimination rules and proofs of normalization, the categorial characterization of deductions, the relation between Heyting's and Gentzen's approaches to meaning, knowability paradoxes, proof-theoretic foundations of set theory, Dummett's justification of logical laws, Kreisel's theory of constructions, paradoxical reasoning, and the defence of model theory. The field of proof-theoretic semantics has existed for almost 50 years, but the term (...) itself was proposed by Schroeder-Heister in the 1980s. Proof-theoretic semantics explains the meaning of linguistic expressions in general and of logical constants in particular in terms of the notion of proof. This volume emerges from presentations at the Second International Conference on Proof-Theoretic Semantics in Tübingen in 2013, where contributing authors were asked to provide a self-contained description and analysis of a significant research question in this area. The contributions are representative of the field and should be of interest to logicians, philosophers, and mathematicians alike. (shrink)

This paper argues that logical inferentialists should reject multiple-conclusion logics. Logical inferentialism is the position that the meanings of the logical constants are determined by the rules of inference they obey. As such, logical inferentialism requires a proof-theoretic framework within which to operate. However, in order to fulfil its semantic duties, a deductive system has to be suitably connected to our inferential practices. I argue that, contrary to an established tradition, multiple-conclusion systems are ill-suited for this purpose because they fail (...) to provide a 'natural' representation of our ordinary modes of inference. Moreover, the two most plausible attempts at bringing multiple conclusions into line with our ordinary forms of reasoning, the disjunctive reading and the bilateralist denial interpretation, are unacceptable by inferentialist standards. (shrink)

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening (...) or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. (shrink)

Inference versus consequence , an invited lecture at the LOGICA 1997 conference at Castle Liblice, was part of a series of articles for which I did research during a Stockholm sabbatical in the autumn of 1995. The article seems to have been fairly effective in getting its point across and addresses a topic highly germane to the Uppsala workshop. Owing to its appearance in the LOGICA Yearbook 1997 , Filosofia Publishers, Prague, 1998, it has been rather inaccessible. Accordingly it is (...) republished here with only bibliographical changes and an afterword. (shrink)

The rather unrestrained use of second-order logic in the neo-logicist program is critically examined. It is argued in some detail that it brings with it genuine set-theoretical existence assumptions and that the mathematical power that Hume’s Principle seems to provide, in the derivation of Frege’s Theorem, comes largely from the ‘logic’ assumed rather than from Hume’s Principle. It is shown that Hume’s Principle is in reality not stronger than the very weak Robinson Arithmetic Q. Consequently, only a few rudimentary facts (...) of arithmetic are logically derivable from Hume’s Principle. And that hardly counts as a vindication of logicism. (shrink)

Proof-theoretic semantics is an alternative to model-theoretic semantics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence relation (...) to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof-theoretic semantics is the one given by the sequent-to-sequent derivability relation in Gentzen systems. (shrink)

Prawitz observed that Russell’s paradox in naive set theory yields a derivation of absurdity whose reduction sequence loops. Building on this observation, and based on numerous examples, Tennant claimed that this looping feature, or more generally, the fact that derivations of absurdity do not normalize, is characteristic of the paradoxes. Striking results by Ekman show that looping reduction sequences are already obtained in minimal propositional logic, when certain reduction steps, which are prima facie plausible, are considered in addition to the (...) standard ones. This shows that the notion of reduction is in need of clarification. Referring to the notion of identity of proofs in general proof theory, we argue that reduction steps should not merely remove redundancies, but must respect the identity of proofs. Consequentially, we propose to modify Tennant’s paradoxicality test by basing it on this refined notion of reduction. (shrink)

In bilateral systems for classical logic, assertion and denial occur as primitive signs on formulas. Such systems lend themselves to an inferentialist story about how truth-conditional content of connectives can be determined by inference rules. In particular, for classical logic there is a bilateral proof system which has a property that Carnap in 1943 called categoricity. We show that categorical systems can be given for any finite many-valued logic using $n$-sided sequent calculus. These systems are understood as a further development (...) of bilateralism—call it multilateralism. The overarching idea is that multilateral proof systems can incorporate the logic of a variety of denial speech acts. So against Frege we say that denial is not the negation of assertion and, with Mark Twain, that denial is more than a river in Egypt. (shrink)

Prawitz conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister. This article resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The paper further defines a notion of quasi-proof-theoretic validity by restricting proof-theoretic validity to allow double negation elimination (...) for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic. (shrink)

Some thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal form in natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the same generality if after generalizing maximally (...) the rules involved in them they yield the same premises and conclusions up to a renaming of variables. These two proposals proved to be extensionally equivalent only for limited fragments of logic. The normalization proposal stands behind very successful applications of the typed lambda calculus and of category theory in the proof theory of intuitionistic logic. In classical logic, however, it did not fare well. The generality proposal was rather neglected in logic, though related matters were much studied in pure category theory in connection with coherence problems, and there are also links to low-dimensional topology and linear algebra. This proposal seems more promising than the other one for the general proof theory of classical logic. (shrink)

From ancient times to the present, the discovery and presentation of new proofs of previously established theorems has been a salient feature of mathematical practice. Why? What purposes are served by such endeavors? And how do mathematicians judge whether two proofs of the same theorem are essentially different? Consideration of such questions illuminates the roles that proofs play in the validation and communication of mathematical knowledge and raises issues that have yet to be resolved by mathematical logicians. The Appendix, in (...) which several proofs of the Fundamental Theorem of Arithmetic are compared, provides a miniature case study. (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)

The idea of an ?inversion principle?, and the name itself, originated in the work of Paul Lorenzen in the 1950s, as a method to generate new admissible rules within a certain syntactic context. Some fifteen years later, the idea was taken up by Dag Prawitz to devise a strategy of normalization for natural deduction calculi (this being an analogue of Gentzen's cut-elimination theorem for sequent calculi). Later, Prawitz used the inversion principle again, attributing it with a semantic role. Still working (...) in natural deduction calculi, he formulated a general type of schematic introduction rules to be matched ? thanks to the idea supporting the inversion principle ? by a corresponding general schematic Elimination rule. This was an attempt to provide a solution to the problem suggested by the often quoted note of Gentzen. According to Gentzen ?it should be possible to display the elimination rules as unique functions of the corresponding introduction rules on the basis of certain requirements?. Many people have since worked on this topic, which can be appropriately seen as the birthplace of what are now referred to as ?general elimination rules?, recently studied thoroughly by Sara Negri and Jan von Plato. In this study, we retrace the main threads of this chapter of proof-theoretical investigation, using Lorenzen's original framework as a general guide. (shrink)

Several proof-theoretic notions of validity have been proposed in the literature, for which completeness of intuitionistic logic has been conjectured. We define validity for intuitionistic propositional logic in a way which is common to many of these notions, emphasizing that an appropriate notion of validity must be closed under substitution. In this definition we consider atomic systems whose rules are not only production rules, but may include rules that allow one to discharge assumptions. Our central result shows that Harrop’s rule (...) is valid under substitution, which refutes the completeness conjecture for intuitionistic logic. (shrink)

The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order (...) logics in a general way, and to present some of the more important results in this area. In Systems covered are the resolution calculus, sequent calculus, tableaux, and natural deduction. This report is actually a template, from which all results can be specialized to particular logics. (shrink)

In the present paper I wish to regard constructivelogic as a self-contained system for the treatment ofepistemological issues; the explanations of theconstructivist logical notions are cast in anepistemological mold already from the outset. Thediscussion offered here intends to make explicit thisimplicit epistemic character of constructivism.Particular attention will be given to the intendedinterpretation laid down by Heyting. This interpretation, especially as refined in the type-theoretical work of Per Martin-Löf, puts thesystem on par with the early efforts of Frege andWhitehead-Russell. This quite (...) recent work, however,has proved valuable not only in the philosophy andfoundations of mathematics, but has also foundpractical application in computer science, where thelanguage of constructivism serves as an implementableprogramming language, and within the philosophy oflanguage.\footnote{Nordstr\"{o}m et al. give an overview of the work in computerscience, whereas Ranta provides an impressiveconstructivist alternative to Montague Grammar usingthe richer type structure of Martin-L\"{o}f in placeof the simple classical type theory of Church.} Mypresentation will be carried out through a contrastwith standard metamathematical work.\footnote{Troelstra and van Dalen give an encyclopedictreatment of the metamathematics of constructivism.}In the course of the development I have occasion tooffer some novel considerations on thenature of proof and inference. (shrink)

This paper develops some respects in which the philosophy of mathematics can fruitfully be informed by mathematical practice, through examining Frege's Grundlagen in its historical setting. The first sections of the paper are devoted to elaborating some aspects of nineteenth century mathematics which informed Frege's early work. (These events are of considerable philosophical significance even apart from the connection with Frege.) In the middle sections, some minor themes of Grundlagen are developed: the relationship Frege envisions between arithmetic and geometry and (...) the way in which the study of reasoning is to illuminate this. In the final section, it is argued that the sorts of issues Frege attempted to address concerning the character of mathematical reasoning are still in need of a satisfying answer. (shrink)

The standard natural deduction rules for the identity predicate have seemed to some not to be harmonious. Stephen Read has suggested an alternative introduction rule that restores harmony but presupposes second-order logic. Here it will be shown that the standard rules are in fact harmonious. To this end, natural deduction will be enriched with a theory of definitional identity. This leads to a novel conception of canonical derivation, on the basis of which the identity elimination rule can be justified in (...) a proof-theoretical manner. (shrink)

Semantic justifications of the classical rules of logical inference typically make use of a notion of bivalent truth, understood as a property guaranteed to attach to a sentence or its negation regardless of the prospects for speakers to determine it as so doing. For want of a convincing alternative account of classical logic, some philosophers suspicious of such recognition-transcending bivalence have seen no choice but to declare classical deduction unwarranted and settle for a weaker system; intuitionistic logic in particular, buttressed (...) by assertion-conditional semantics, is often considered to enjoy a degree of meaning-theoretical respectability unattainable by classical logic.The decision to forgo the classical inference rules is not always made lightly. Thus, Dummett: " In the resolution of the conflict between [the view that generally accepted classical modes of inference ought to be theoretically accommodated, and the demand that any such accommodation be achieved without recourse to bivalence] lies, as I see it, one of the most fundamental and intractable problems in the theory of meaning; indeed, in all philosophy. "The present article ventures to suggest that the conflict need not be irresoluble. Helping ourselves only to such conceptual resources as are standardly invoked by proponents of intuitionistic logic, we shall formulate a rudimentary meaning theory for a selection of logical constants, define a relation of valid inferability, and prove that the latter includes all of classical first-order logic. The result is essentially that reported in Sandqvist as Theorem 2.20.2. TheoryWe will be considering a standard-syntax first-order language with ⊃, ⊥ and ∀ as its only primitive logical constants. We assume countable supplies of individual constants, individual functors , and predicates , as well as a denumerably infinite set of individual variables. By a basic 1 formula we will mean one that …[Full Text of this Article]. (shrink)

On the basis of Martin-Löf’s meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As argued in previous (...) work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

What is the proper role of logic in analytic theology? This question is thrown into sharp relief when a basic logical principle is questioned, as in Beall’s ‘Christ – A Contradiction.’ Analytic philosophers of logic have debated between exceptionalism and anti-exceptionalism, with the tide shifting towards anti-exceptionalism in recent years. By contrast, analytic theologians have largely been exceptionalists. The aim of this paper is to argue for an anti-exceptionalist view, specifically treating logic as a modelling tool. Along the way I (...) critically engage with Beall on the role of logic in theology, maintaining that theological inquiry is in some ways disanalogous with other theoretical enterprises. (shrink)

A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.

In this paper we argue that an account of proof-theoretic harmony based on reductions and expansions delivers an inferentialist picture of meaning which should be regarded as intensional, as opposed to other approaches to harmony that will be dubbed extensional. We show how the intensional account applies to any connective whose rules obey the inversion principle first proposed by Prawitz and Schroeder-Heister. In particular, by improving previous formulations of expansions, we solve a problem with quantum-disjunction first posed by Dummett. As (...) recently observed by Schroeder-Heister, however, the specification of an inversion principle cannot yield an exhaustive account of harmony. The reason is that there are more collections of elimination rules than just the one obtained by inversion which we are willing to acknowledge as being in harmony with a given collection of introduction rules. Several authors more or less implicitly suggest that what is common to all alternative harmonious collection of rules is their being interderivable with each other. On the basis of considerations about identity of proofs and formula isomorphism, we show that this is too weak a condition for a given collection of elimination rules to be in harmony with a collection of introduction rules, at least if the intensional picture of meaning we advocate is not to collapse on an extensional one. (shrink)

The topic of identity of proofs was put on the agenda of general (or structural) proof theory at an early stage. The relevant question is: When are the differences between two distinct proofs (understood as linguistic entities, proof figures) of one and the same formula so inessential that it is justified to identify the two proofs? The paper addresses another question: When are the differences between two distinct formulas so inessential that these formulas admit of identical proofs? The question appears (...) to be especially natural if the idea of working with more than one kind of derivations is taken seriously. If a distinction is drawn between proofs and disproofs (or refutations) as primitive entities, it is quite conceivable that a proof of one formula amounts to a disproof of another formula, and vice versa. A notion of inherited identity of derivations is introduced for derivations in a cut-free sequent system for Almukdad and Nelson’s constructive paraconsistent logic N4 with strong negation. The notion is obtained by identifying sequent rules the application of which has no effect on the identity of derivations. Then the notion of inherited identity is used to define a bilateralist notion of synonymy between formulas, which is a relation drawing more fine-grained distinctions between formulas than strong equivalence. (shrink)

This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions (...) in normal form have the subformula property. (shrink)

The thesis that, in a system of natural deduction, the meaning of a logical constant is given by some or all of its introduction and elimination rules has been developed recently in the work of Dummett, Prawitz, Tennant, and others, by the addition of harmony constraints. Introduction and elimination rules for a logical constant must be in harmony. By deploying harmony constraints, these authors have arrived at logics no stronger than intuitionist propositional logic. Classical logic, they maintain, cannot be justified (...) from this proof-theoretic perspective. This paper argues that, while classical logic can be formulated so as to satisfy a number of harmony constraints, the meanings of the standard logical constants cannot all be given by their introduction and/or elimination rules; negation, in particular, comes under close scrutiny. (shrink)

I see the question what it is that makes an inference valid and thereby gives a proof its epistemic power as the most fundamental problem of general proof theory. It has been surprisingly neglected in logic and philosophy of mathematics with two exceptions: Gentzen’s remarks about what justifies the rules of his system of natural deduction and proposals in the intuitionistic tradition about what a proof is. They are reviewed in the paper and I discuss to what extent they succeed (...) in answering what a proof is. Gentzen’s ideas are shown to give rise to a new notion of valid argument. At the end of the paper I summarize and briefly discuss an approach to the problem that I have proposed earlier. (shrink)

The Knowability Paradox purports to show that the controversial but not patently absurd hypothesis that all truths are knowable entails the implausible conclusion that all truths are known. The notoriety of this argument owes to the negative light it appears to cast on the view that there can be no verification-transcendent truths. We argue that it is overly simplistic to formalize the views of contemporary verificationists like Dummett, Prawitz or Martin-Löf using the sort of propositional modal operators which are employed (...) in the original derivation of the Paradox. Instead we propose that the central tenet of verificationism is most accurately formulated as follows: if φ is true, then there exists a proof of φ Building on the work of Artemov (Bull Symb Log 7(1): 1-36, 2001), a system of explicit modal logic with proof quantifiers is introduced to reason about such statements. When the original reasoning of the Paradox is developed in this setting, we reach not a contradiction, but rather the conclusion that there must exist non-constructed proofs. This outcome is evaluated relative to the controversy between Dummett and Prawitz about proof existence and bivalence. (shrink)

A proof-theoretic test for paradoxicality was famously proposed by Tennant: a paradox must yield a closed derivation of absurdity with no normal form. Drawing on the remark that all derivations of a given proposition can be transformed into derivations in normal form of a logically equivalent proposition, we investigate the possibility of paradoxes in normal form. We compare paradoxes à la Tennant and paradoxes in normal form from the viewpoint of the computational interpretation of proofs and from the viewpoint of (...) proof-theoretic semantics. (shrink)