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)

We investigate the development of terms during cut-elimination in first-order logic and Peano arithmetic for proofs of existential formulas. The form of witness terms in cut-free proofs is characterized in terms of structured combinations of basic substitutions. Based on this result, a regular tree grammar computing witness terms is given and a class of proofs is shown to have only elementary cut-elimination.

A new set of conversions for derivations in the system of sequents for intuitionistic predicate logic will be defined. These conversions will be some modifications of Zucker's conversions from the system of sequents from [11], which will have the following characteristics: (1) these conversions will be sufficient for transforming a derivation into a cut-free one, and (2) in the natural deduction the image of each of these conversions will be either in the set of conversions for normalization procedure, or an (...) identity of derivations. This will be used to give a new proof of the normalization theorem for natural deduction, as a consequence of the cut-elimination theorem for the system of sequents. (shrink)

We describe a natural deduction system NDIL for the second order intuitionistic linear logic which admits normalization and has a subformula property. NDIL is an extension of the system for !-free multiplicative linear logic constructed by the author and elaborated by A. Babaev. Main new feature here is the treatment of the modality !. It uses a device inspired by D. Prawitz' treatment of S4 combined with a construction $<\Gamma>$ introduced by the author to avoid cut-like constructions used in $\otimes$ (...) -elimination and global restrictions employed by Prawitz. Normal form for natural deduction is obtained by Prawitz translation of cut-free sequent derivations. (shrink)

Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed as special (...) cases of the cut-elimination theorems for intuitionistic logic. (shrink)

Eight distinct rules for implication in the antecedent for the sequent calculus, one of which being Gentzen’s standard rule, can be derived by successively applying a number of cuts to the logical ground sequent A → B, A ⇒ B. A naive translation into natural deduction collapses four of those rules onto the standard implication elimination rule, and the remaining four rules onto the general elimination rule. This collapse is due to the fact that the difference between a formula occurring (...) in the succedent of a premise of a sequent calculus rule and that formula instead occurring in the antecedent of the conclusion cannot be adequately expressed in the framework of natural deduction. In contrast to this, the difference between a formula occurring in the succedent of the conclusion of a sequent calculus rule and that formula instead occurring in the antecedent of a premise corresponds exactly to the distinction between the standard implication elimination rule and its general counterpart. This incongruity can be remedied by introducing a notational facility that requires of the particular premise of a rule to which it is attached to be an assumption, i.e., to prevent it from being the conclusion of another rule application. Applying this facility to implication elimination results in eight distinct rules that correspond exactly to the eight sequent calculus rules. These eight rules are presented and discussed in detail. It turns out that a natural deduction calculus (for positive implication logic) that employs the rule corresponding to the standard left implication rule of the sequent calculus as well as a rule for explicit substitution can be seen as a natural deduction style sequent calculus. (shrink)

The origins of proof-theoretic semantics lie in the question of what constitutes the meaning of the logical connectives and its response: the rules of inference that govern the use of the connective. However, what if we go a step further and ask about the meaning of a proof as a whole? In this paper we address this question and lay out a framework to distinguish sense and denotation of proofs. Two questions are central here. First of all, if we have (...) two different derivations, does this always lead to a difference, firstly, in sense, and secondly, in denotation? The other question is about the relation between different kinds of proof systems with respect to this distinction. Do the different forms of representing a proof necessarily correspond to a difference in how the inferential steps are given? In our framework it will be possible to identify denotation as well as sense of proofs not only within one proof system but also between different kinds of proof systems. Thus, we give an account to distinguish a mere syntactic divergence from a divergence in meaning and a divergence in meaning from a divergence of proof objects analogous to Frege’s distinction for singular terms and sentences. (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)

In this paper we give a brief treatment of a theory of proofs for a system of Full Intuitionistic Linear Logic. This system is distinct from Classical Linear Logic, but unlike the standard Intuitionistic Linear Logic of Girard and Lafont includes the multiplicative disjunction par. This connective does have an entirely natural interpretation in a variety of categorical models of Intuitionistic Linear Logic. The main proof-theoretic problem arises from the observation of Schellinx that cut elimination fails outright for an intuitive (...) formulation of Full Intuitionistic Linear Logic; the nub of the problem is the interaction between par and linear implication. We present here a term assignment system which gives an interpretation of proofs as some kind of non-deterministic function. In this way we find a system which does enjoy cut elimination. The system is a direct result of an analysis of the categorical semantics, though we make an effort to present the system as if it were purely a proof-theoretic construction. (shrink)

There are still on-going debates on what exactly is wrong with Prior’s pathological “tonk.” In this article I argue, on the basis of categorical inferentialism, that two notions of inconsistency ought to be distinguished in an appropriate account of tonk; logic with tonk is inconsistent as the theory of propositions, and it is due to the fallacy of equivocation; in contrast to this diagnosis of the Prior’s tonk problem, nothing is actually wrong with tonk if logic is viewed as the (...) theory of proofs rather than propositions, and tonk perfectly makes sense in terms of the identity of proofs. Indeed, there is fully complete semantics of proofs for tonk, which allows us to link the Prior’s old philosophical idea with contemporary issues at the interface of categorical logic, computer science, and quantum physics, and thereby to expose commonalities between the laws of Reason and the laws of Nature, which are what logic and physics are respectively about. I conclude the article by articulating the ideas of categorical logical positivism and pluralistic unified science as its goal, including the unification of realist and antirealist conceptions of meaning by virtue of the categorical logical basis of metaphysics. (shrink)

The lambdaPi-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the lambdaPi-calculus and prove the cut-elimination theorem. The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting considered (...) here elegantly illustrates the distinction between the processes of normalization in a natural deduction system and cut-elimination in a Gentzen-style sequent calculus. (shrink)

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 collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

After an introduction to set the stage, we consider some variations on the reasoning behind Curry's Paradox arising against the background of classical propositional logic and of BCI logic and one of its extensions, in the latter case treating the "paradoxicality" as a matter of nonconservative extension rather than outright inconsistency. A question about the relation of this extension and a differently described (though possibly identical) logic intermediate between BCI and BCK is raised in a final section, which closes with (...) a handful of questions left unanswered by our discussion. (shrink)

In order to explicate Gentzen’s famous remark that the introduction-rules for logical constants give their meaning, the elimination-rules being simply consequences of the meaning so given, we develop natural deduction rules for Sheffer’s stroke, alternative denial. The first system turns out to lack Double Negation. Strengthening the introduction-rules by allowing the introduction of Sheffer’s stroke into a disjunctive context produces a complete system of classical logic, one which preserves the harmony between the rules which Gentzen wanted: all indirect proof reduces (...) to direct proof. (shrink)

The well-known picture that sequent derivations without cuts and normal derivations “are the same” will be changed. Sequent derivations without maximum cuts (i.e. special cuts which correspond to maximum segments from natural deduction) will be considered. It will be shown that the natural deduction image of a sequent derivation without maximum cuts is a normal derivation, and the sequent image of a normal derivation is a derivation without maximum cuts. The main consequence of that property will be that sequent derivations (...) without maximum cuts and normal derivations “are the same”. (shrink)

In this paper we give a new proof of cut elimination in Gentzen's sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.