We consider a family of logical systems for representing entailment relations of various kinds. This family has its root in the logic of first-degree entailment formulated as a binary consequence system, i.e. a proof system dealing with the expressions of the form \, where both \ and \ are single formulas. We generalize this approach by constructing consequence systems that allow manipulating with sets of formulas, either to the right or left of the turnstile. In this way, it is possible (...) to capture proof-theoretically not only the entailment relation of the standard four-valued Belnap’s logic, but also its dual version, as well as some of their interesting extensions. The proof systems we propose are, in a sense, of a hybrid Hilbert–Gentzen nature. We examine some important properties of these systems and establish their completeness with respect to the corresponding entailment relations. (shrink)

Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator εx. Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential (...) theorems obtained by this elimination procedure. (shrink)

Motivated by the problem of finding finite versions of classical incompleteness theorems, we present some conjectures that go beyond NP ≠ coNP. These conjectures formally connect computational complexity with the difficulty of proving some sentences, which means that high computational complexity of a problem associated with a sentence implies that the sentence is not provable in a weak theory, or requires a long proof. Another reason for putting forward these conjectures is that some results in proof complexity seem to be (...) special cases of such general statements and we want to formalize and fully understand these statements. Roughly speaking, we are trying to connect syntactic complexity, by which we mean the complexity of sentences and strengths of the theories in which they are provable, with the semantic concept of complexity of the computational problems represented by these sentences. -/- We have introduced the most fundamental conjectures in our earlier works. Our aim in this article is to present them in a more systematic way, along with several new conjectures, and prove new connections between them and some other statements studied before. (shrink)

Call an argument a ‘happy sorites’ if it is a sorites argument with true premises and a false conclusion. It is a striking fact that although most philosophers working on the sorites paradox find it at prima facie highly compelling that the premises of the sorites paradox are true and its conclusion false, few (if any) of the standard theories on the issue ultimately allow for happy sorites arguments. There is one philosophical view, however, that appears to allow for at (...) least some happy sorites arguments: strict finitism in the philosophy of mathematics. My aim in this paper is to explore to what extent this appearance is accurate. As we shall see, this question is far from trivial. In particular, I will discuss two arguments that threaten to show that strict finitism cannot consistently accept happy sorites arguments, but I will argue that (given reasonable assumptions on strict finitistic logic) these arguments can ultimately be avoided, and the view can indeed allow for happy sorites arguments. (shrink)

Many mathematicians and philosophers of mathematics believe some proofs contain elements extraneous to what is being proved. In this paper I discuss extraneousness generally, and then consider a specific proposal for measuring extraneousness syntactically. This specific proposal uses Gentzen's cut-elimination theorem. I argue that the proposal fails, and that we should be skeptical about the usefulness of syntactic extraneousness measures.

The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...) In sections 5 and 6 I discuss some problems arising with regard to Prawitz’s views. (shrink)

This article presents a sequent calculus for a negative free logic with identity, called N . The main theorem (in part 1) is the admissibility of the Cut-rule. The second part of this essay is devoted to proofs of soundness, compactness and completeness of N relative to a standard semantics for negative free logic.

Written by experts in the field, this volume presents a comprehensive investigation into the relationship between argumentation theory and the philosophy of mathematical practice. Argumentation theory studies reasoning and argument, and especially those aspects not addressed, or not addressed well, by formal deduction. The philosophy of mathematical practice diverges from mainstream philosophy of mathematics in the emphasis it places on what the majority of working mathematicians actually do, rather than on mathematical foundations. -/- The book begins by first challenging the (...) assumption that there is no role for informal logic in mathematics. Next, it details the usefulness of argumentation theory in the understanding of mathematical practice, offering an impressively diverse set of examples, covering the history of mathematics, mathematics education and, perhaps surprisingly, formal proof verification. From there, the book demonstrates that mathematics also offers a valuable testbed for argumentation theory. Coverage concludes by defending attention to mathematical argumentation as the basis for new perspectives on the philosophy of mathematics. ​. (shrink)

A quasi-canonical Gentzen-type system is a Gentzen-type system in which each logical rule introduces either a formula of the form , or of the form , and all the active formulas of its premises belong to the set . In this paper we investigate quasi-canonical systems in which exactly one of the two classical rules for negation is included, turning the induced logic into either a paraconsistent logic or a paracomplete logic, but not both. We provide a constructive coherence criterion (...) for such systems, and show that a quasi-canonical system of the type we investigate is coherent iff it is strongly paraconsistent or strongly paracomplete (in a sense defined in the paper), iff it has a trivalent, non-deterministic semantics of a special type (also defined in the paper) for which it is sound and complete. Finally, we determine when a system of this sort admits cut-elimination, and provide a simple procedure for transforming one which does not into one which does. (shrink)

The paper proves refined feasibility properties for the disjunction property of intuitionistic propositional logic. We prove that it is possible to eliminate all cuts from an intuitionistic proof, propositional or first-order, without increasing the Horn closure of the proof. We obtain a polynomial time, interactive, realizability algorithm for propositional intuitionistic proofs. The feasibility of the disjunction property is proved for sequents containing Harrop formulas. Under hardness assumptions for NP and for factoring, it is shown that the intuitionistic propositional calculus does (...) not always have polynomial size proofs and that the classical propositional calculus provides a superpolynomial speedup over the intuitionistic propositional calculus. The disjunction property for intuitionistic propositional logic is proved to be P-hard by a reduction to the circuit value problem. (shrink)

We develop an arithmetical theory and its variant , corresponding to “slightly nonuniform” . Our theories sit between and , and allow evaluation of log-depth bounded fan-in circuits under limited conditions. Propositional translations of -formulas provable in admit L-uniform polynomial-size Frege proofs.

Let Con↾x denote the finite consistency statement “there are no proofs of contradiction in T with ≤x symbols.” For a large class of natural theories T, Pudlák has shown that the lengths of the shortest proofs of Con↾n in the theory T itself are bounded by a polynomial in n. At the same time he conjectures that T does not have polynomial proofs of the finite consistency statements Con)↾n. In contrast, we show that Peano arithmetic has polynomial proofs of Con)↾n, (...) where Con∗ is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen, and Weiermann. We also obtain a new proof of the result that the usual consistency statement Con is equivalent to ε0 iterations of slow consistency. Our argument is proof-theoretic, whereas previous investigations of slow consistency relied on nonstandard models of arithmetic. (shrink)

We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley–Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities such as AB=I→BA=I.

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.

Bounds consequence provides an interpretation of a multiple-conclusion consequence relation in which the derivability of a sequent is understood as the claim that it is conversationally out-of-bounds to take a position in which each member of Γ is asserted while each member of Δ is denied. Two of the foremost champions of bounds consequence—Greg Restall and David Ripley—have independently indicated that the shape of the bounds in question is determined by conversational practice. In this paper, I suggest that the standard (...) treatments of bounds consequence have focused heavily on the matter of veridicality at the expense of ignoring other features by which conversational bounds are set, prime among them being the matter of content or subject-matter. Furthermore, I argue that the semantic behavior of propositions containing “monstrous” content—content whose introduction is inappropriate to a context independently of veridical considerations—leads to a weak Kleene account of bounds consequence. (shrink)

Let H be a proof system for quantified propositional calculus (QPC). We define the Σqj-witnessing problem for H to be: given a prenex Σqj-formula A, an H-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the Σq1-witnessing problems for the systems G*1and G1 are complete for polynomial time and PLS (polynomial local search), respectively. We introduce and study the systems G*0 and G0, (...) in which cuts are restricted to quantifier-free formulas, and prove that the Σqj-witnessing problem for each is complete for NC1. Our proof involves proving a polynomial time version of Gentzen’s midsequent theorem for G*0 and proving that G0-proofs are TC0-recognizable. We also introduce QPC systems for TC0 and prove witnessing theorems for them. We introduce a finitely axiomatizable second-order system VNC1 of bounded arithmetic which we prove isomorphic to Arai’s first order theory AID + Σb0-CA for uniform NC1. We describe simple translations of VNC1 proofs of all bounded theorems to polynomial size families of G*0 proofs. From this and the above theorem we get alternative proofs of the NC1 witnessing theorems for VNC1 and AID. (shrink)

To investigate the relationship between logical reasoning and majority voting, we introduce logic with groups Lg in the style of Gentzen’s sequent calculus, where every sequent is indexed by a group of individuals. We also introduce the set-theoretical semantics of Lg, where every formula is interpreted as a certain closed set of groups whose members accept that formula. We present the cut-elimination theorem, and the soundness and semantic completeness theorems of Lg. Then, introducing an inference rule representing majority voting to (...) Lg, we introduce logic with majority voting Lv. Formalizing the discursive paradox in judgment aggregation theory, we show that Lv is inconsistent. Based on the premise-based and conclusion-based approaches to avoid the paradox, we introduce logic with majority voting for axioms Lva, where majority voting is applied only to non-logical axioms as premises to construct a proof in Lg, and logic with majority voting for conclusions Lvc, where majority voting is applied only to the conclusion of a proof in Lg. We show that both Lva and Lvc are syntactically complete and consistent, and we construct collective judgments based on the provability in Lva and Lvc, respectively. Then, we discuss how these systems avoid the discursive paradox. (shrink)

There are many classical connections between the proof-theoretic strength of systems of arithmetic and the provable totality of recursive functions. In this paper we study the provability strength of the totality of recursive functions by investigating the degree structure induced by the relative provability order of recursive algorithms. We prove several results about this proof-theoretic degree structure using recursion-theoretic techniques such as diagonalization and the Recursion Theorem.

Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic modal (...) logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are such that there is an algorithm for checking if they are satisfied by a sequent calculus. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis with a PRA consistency proof, proposed in around 1995 by Patrick Suppes and Richard Sommer. It is based on an earlier system developed by Rolando Chuaqui and Patrick Suppes. Here, we discuss the inherent problems and limitations of the classical nonstandard framework and propose a much-needed refinement of ERNA, called , in the spirit of Karel Hrbacek’s stratified set theory. We study the metamathematics of and its (...) extensions. In particular, we consider several transfer principles, both classical and ‘stratified’, which turn out to be related. Finally, we show that the resulting theory allows for a truly general, elegant and elementary treatment of basic analysis. (shrink)

The Liar paradox arguably shows that a coherent and self-applicable notion of truth is governed by nonclassical logic. It then seems natural to conclude that classical logic is inadequate for defining a truth theory. In this article, we argue that this is not the case. In the spirit of Reinhardt (Math Logic Formal Syst 94:227, 1985; J Philos Logic 15:219–251, 1986), and in analogy with Hilbert’s program for the foundation of classical mathematics, we will articulate an instrumentalist justification for the (...) use classical logic: it will be argued that classical reasoning is a _useful but dispensable instrument_, which can yield philosophically adequate truth theories. (shrink)

At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in emphasis away (...) from calculation gave rise to concerns as to whether such methods were meaningful, or appropriate to mathematics. The discovery of paradoxes stemming from overly naive use of set-theoretic language and methods led to even more pressing concerns as to whether the modern methods were even consistent. This led to heated debates in the early twentieth century and what is sometimes called the “crisis of foundations.” In lectures presented in 1922, David Hilbert launched his Beweistheorie, or Proof Theory, which aimed to justify the use of modern methods and settle the problem of foundations once and for all. This, Hilbert argued, could be achieved as follows. (shrink)

Mathematicians often speak of conjectures, yet unproved, as probable or well-confirmed by evidence. The Riemann Hypothesis, for example, is widely believed to be almost certainly true. There seems no initial reason to distinguish such probability from the same notion in empirical science. Yet it is hard to see how there could be probabilistic relations between the necessary truths of pure mathematics. The existence of such logical relations, short of certainty, is defended using the theory of logical probability (or objective Bayesianism (...) or non-deductive logic), and some detailed examples of its use in mathematics surveyed. Examples of inductive reasoning in experimental mathematics are given and it is argued that the problem of induction is best appreciated in the mathematical case. (shrink)

We introduce the axiom of the existence of axioms and discuss its implications for logical systems and beyond.

Frege’s theory is inconsistent. However, the predicative version of Frege’s system is consistent. This was proved by Richard Heck in 1996 using a model-theoretic argument. In this paper, we give a finitistic proof of this consistency result. As a consequence, Heck’s predicative theory is rather weak. We also prove the finitistic consistency of the extension of Heck’s theory to $\Delta^{1}_{1}$-comprehension and of Heck’s ramified predicative second-order system.

Why is it that even strong formal theories of truth fail to prove their own consistency? Although Field has addressed this question for many theories of truth, I argue that there is an important and attractive class of theories of truth that he omitted in his analysis. Such theories cannot prove that all their axioms are true, though unlike many of the cases Field considers, they do not prove that any of their axioms are false or that any of their (...) rules of inference are not truth preserving. I argue that it is the fact that such theories are not finitely axiomatizable that stops them from proving their own consistency. (shrink)

We present sharpened lower bounds on the size of cut free proofs for first-order logic. Prior lower bounds for eliminating cuts from a proof established superexponential lower bounds as a stack of exponentials, with the height of the stack proportional to the maximum depth d of the formulas in the original proof. Our results remove the constant of proportionality, giving an exponential stack of height equal to d — 0(1). The proof method is based on more efficiently expressing the Gentzen-Solovay (...) cut formulas as low depth formulas. (shrink)

It can be argued that only the equational theories of some sub-elementary function algebras are finitistic or intuitive according to a certain interpretation of Hilbert's conception of intuition. The purpose of this paper is to investigate the relation of those restricted forms of equational reasoning to classical quantifier logic in arithmetic. The conclusion reached is that Edward Nelson's ‘predicative arithmetic’ program, which makes essential use of classical quantifier logic, cannot be justified finitistically and thus requires a different philosophical foundation, possibly (...) as a restricted form of logicism. (shrink)

In this paper, we show the equivalence between the provability of a proof system of basic hybrid logic and that of translated formulas of the classical predicate logic with equality and explicit substitution by a purely proof–theoretic method. Then we show the equivalence of two groups of proof systems of hybrid logic: the group of labelled deduction systems and the group of modal logic-based systems.

This paper explores the main philosophical approaches of David Hilbert’s theory of proof. Specifically, it is focuses on his ideas regarding logic, the concept of proof, the axiomatic, the concept of truth, metamathematics, the a priori knowledge and the general nature of scientific knowledge. The aim is to show and characterize his epistemological approach on the foundation of knowledge, where logic appears as a guarantee of that foundation. Hilbert supposes that the propositional apriorism, proposed by him to support mathematics, sustains (...) — on its turn — a general method for the treatment of the problem in other areas such as natural sciences. This method is axiomatic. Broadly speaking, we intend to recover and update the Hilbert’s philosophical thinking about the role of logic for scientific knowledge. (shrink)

An important open problem in Reverse Mathematics is the reduction of the first-order strength of the base theory from IΣ1IΣ1 to IΔ0+expIΔ0+exp. The system ERNA, a version of Nonstandard Analysis based on the system IΔ0+expIΔ0+exp, provides a partial solution to this problem. Indeed, weak Königʼs lemma and many of its equivalent formulations from Reverse Mathematics can be ‘pushed down’ into ERNA, while preserving the equivalences, but at the price of replacing equality with ‘≈’, i.e. infinitesimal proximity . The logical principle (...) corresponding to weak Königʼs lemma is the universal transfer principle from Nonstandard Analysis. Here, we consider the intermediate and mean value theorem and their uniform generalizations. We show that ERNAʼs Reverse Mathematics mirrors the situation in classical Reverse Mathematics. This further supports our claim from Sanders [19] that the Reverse Mathematics of ERNA plus universal transfer is a copy up to infinitesimals of that of WKL0. We discuss some of the philosophical implications of our results. (shrink)