We will study several weak axiom systems that use the Subtraction and Division primitives (rather than Addition and Multiplication) to formally encode the theorems of Arithmetic. Provided such axiom systems do not recognize Multiplication as a total function, we will show that it is feasible for them to verify their Semantic Tableaux, Herbrand, and Cut-Free consistencies. If our axiom systems additionally do not recognize Addition as a total function, they will be capable of recognizing the consistency of their Hilbert-style deductive (...) proofs. Our axiom systems will not be strong enough to recognize their Canonical Reflection principle, but they will be capable of recognizing an approximation of it, called the "Tangibility Reflection Principle". We will also prove some new versions of the Second Incompleteness Theorem stating essentially that it is not possible to extend our exceptions to the Incompleteness Theorem much further. (shrink)

A. Tarski [22] proposed the study of infinitary consequence operations as the central topic of mathematical logic. He considered monotonicity to be a property of all such operations. In this paper, we weaken the monotonicity requirement and consider more general operations, inference operations. These operations describe the nonmonotonic logics both humans and machines seem to be using when infering defeasible information from incomplete knowledge. We single out a number of interesting families of inference operations. This study of infinitary inference operations (...) is inspired by the results of [12] on nonmonotonic inference relations, and relies on some of the definitions found there. (shrink)

In this study, an extended paradefinite logic with classical negation (EPLC), which has the connectives of conflation, paraconsistent negation, classical negation, and classical implication, is introduced as a Gentzen-type sequent calculus. The logic EPLC is regarded as a modification of Arieli, Avron, and Zamansky’s ideal four-valued paradefinite logic (4CC) and as an extension of De and Omori’s extended Belnap–Dunn logic with classical negation (BD+) and Avron’s self-extensional four-valued paradefinite logic (SE4). The completeness, cut-elimination, and decidability theorems for EPLC are proved (...) and EPLC is shown to be embeddable into classical logic. The strong equivalence substitution property and the admissibilities of the rules of negative symmetry, contraposition, and involution are shown for EPLC. Some alternative simple Gentzen-type sequent calculi, which are theorem-equivalent to EPLC, are obtained via these characteristic properties. (shrink)

Proof theory and category theory were first drawn together by Lambek some 30 years ago but, until now, the most fundamental notions of category theory have not been explained systematically in terms of proof theory. Here it is shown that these notions, in particular the notion of adjunction, can be formulated in such as way as to be characterised by composition elimination. Among the benefits of these composition-free formulations are syntactical and simple model-theoretical, geometrical decision procedures for the commuting of (...) diagrams of arrows. Composition elimination, in the form of Gentzen's cut elimination, takes in categories, and techniques inspired by Gentzen are shown to work even better in a purely categorical context than in logic. An acquaintance with the basic ideas of general proof theory is relied on only for the sake of motivation, however, and the treatment of matters related to categories is also in general self contained. Besides familiar topics, presented in a novel, simple way, the monograph also contains new results. It can be used as an introductory text in categorical proof theory. (shrink)

The standard inferentialist approaches to modal logic tend to suffer from not being able to uniquely characterize the modal operators, require that introduction and elimination rules be interdefined, or rely on the introduction of possible-world like indexes into the object language itself. In this paper I introduce a hypersequent calculus that is flexible enough to capture many of the standard modal logics and does not suffer from the above problems. It is therefore an ideal candidate to underwrite an inferentialist theory (...) of meaning for modal operators. Here I treat specifically the modal logics K, D, T, S4, B, and S5. I show that the calculi are adequate for each set of models, and show that they meet a large set of criteria that are generally thought necessary for a calculus to underwrite a theory of meaning. (shrink)

Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...) sequent calculi are more amenable to extensive investigation using the tools of proof theory, such as cut-elimination and rule invertibility, hence allowing a full analysis of the notion of Ecumenical entailment. We then present some extensions of the Ecumenical sequent system and show that interesting systems arise when restricting such calculi to specific fragments. This approach of a unified system enabling both classical and intuitionistic features sheds some light not only on the logics themselves, but also on their semantical interpretations as well as on the proof theoretical properties that can arise from combining logical systems. (shrink)

. This paper examines the underpinnings of the preservationist approach to characterizing inference relations. Starting with a critique of the ‘truth-preservation’ semantic paradigm, we discuss the merits of characterizing an inference relation in terms of preserving consistency. Finally we turn our attention to the generalization of consistency introduced in the early work of Jennings and Schotch, namely the concept of level.

Michael Dummett and Dag Prawitz have argued that a constructivist theory of meaning depends on explicating the meaning of logical constants in terms of the theory of valid inference, imposing a constraint of harmony on acceptable connectives. They argue further that classical logic, in particular, classical negation, breaks these constraints, so that classical negation, if a cogent notion at all, has a meaning going beyond what can be exhibited in its inferential use. I argue that Dummett gives a mistaken elaboration (...) of the notion of harmony, an idea stemming from a remark of Gerhard Gentzen's. The introduction-rules are autonomous if they are taken fully to specify the meaning of the logical constants, and the rules are harmonious if the elimination-rule draws its conclusion from just the grounds stated in the introduction-rule. The key to harmony in classical logic then lies in strengthening the theory of the conditional so that the positive logic contains the full classical theory of the conditional. This is achieved by allowing parametric formulae in the natural deduction proofs, a form of multiple-conclusion logic. (shrink)

First-order intuitionistic and classical Nelson–Wansing and Arieli–Avron–Zamansky logics, which are regarded as paradefinite and connexive logics, are investigated based on Gentzen-style sequent calculi. The cut-elimination and completeness theorems for these logics are proved uniformly via theorems for embedding these logics into first-order intuitionistic and classical logics. The modified Craig interpolation theorems for these logics are also proved via the same embedding theorems. Furthermore, a theorem for embedding first-order classical Arieli–Avron–Zamansky logic into first-order intuitionistic Arieli–Avron–Zamansky logic is proved using a modified (...) Gödel–Gentzen negative translation. The failure of a theorem for embedding first-order classical Nelson–Wansing logic into first-order intuitionistic Nelson–Wansing logic is also shown. (shrink)

In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding (...) BD+ into BDi and the McKinsey–Tarski theorem for embedding BDi into BDm. (shrink)

This is a companion to a paper by the authors entitled “Gödel on deduction”, which examined the links between some philosophical views ascribed to Gödel and general proof theory. When writing that other paper, the authors were not acquainted with a system of natural deduction that Gödel presented with the help of Gentzen’s sequents, which amounts to Jaśkowski’s natural deduction system of 1934, and which may be found in Gödel’s unpublished notes for the elementary logic course he gave in 1939 (...) at the University of Notre Dame. Here one finds a presentation of this system of Gödel accompanied by a brief reexamination in the light of the notes of some points concerning his interest in sequents made in the preceding paper. This is preceded by a brief summary of Gödel’s Notre Dame course, and is followed by comments concerning Gödel’s natural deduction system. (shrink)

The hallmark of the deductive systems known as ‘conceptivist’ or ‘containment’ logics is that for all theorems of the form , all atomic formulae appearing in also appear in . Significantly, as a consequence, the principle of Addition fails. While often billed as a formalisation of Kantian analytic judgements, once semantics were discovered for these systems, the approach was largely discounted as merely the imposition of a syntactic filter on unrelated systems. In this paper, we examine a number of prima (...) facie unrelated deductive contexts in which Addition fails and attempt to harmonise them by developing a computational interpretation of conceptivist logics. (shrink)

Gödel’s first incompleteness result from 1931 states that there are true assertions about the natural numbers which do not follow from the Peano axioms. Since 1931 many researchers have been looking for natural examples of such assertions and breakthroughs were obtained in the seventies by Jeff Paris [Some independence results for Peano arithmetic. J. Symbolic Logic 43 725–731] , Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977] and Laurie Kirby [L. Kirby, Jeff Paris, Accessible independence results for Peano Arithmetic, Bull. of (...) the LMS 14 285–293]) and Harvey Friedman [S.G. Simpson, Non-provability of certain combinatorial properties of finite trees, in: Harvey Friedman’s Research on the Foundations of Mathematics, North-Holland, Amsterdam, 1985, pp. 87–117; R. Smith, The consistency strength of some finite forms of the Higman and Kruskal theorems, in: Harvey Friedman’s Research on the Foundations of Mathematics, North-Holland, Amsterdam, 1985, pp. 119–136] who produced the first mathematically interesting independence results in Ramsey theory and well-order and well-quasi-order theory .In this article we investigate Friedman-style principles of combinatorial well-foundedness for the ordinals below ε0. These principles state that there is a uniform bound on the length of decreasing sequences of ordinals which satisfy an elementary recursive growth rate condition with respect to their Gödel numbers.For these independence principles we classify their phase transitions, i.e. we classify exactly the bounding conditions which lead from provability to unprovability in the induced combinatorial well-foundedness principles.As Gödel numbering for ordinals we choose the one which is induced naturally from Gödel’s coding of finite sequences from his classical 1931 paper on his incompleteness results.This choice makes the investigation highly non-trivial but rewarding and we succeed in our objectives by using an intricate and surprising interplay between analytic combinatorics and the theory of descent recursive functions. For obtaining the required bounds on count functions for ordinals we use a classical 1961 Tauberian theorem of Parameswaran which apparently is far remote from Gödel’s theorem. (shrink)

We refute the conjecture that all negative translations are intuitionistically equivalent by giving two counterexamples. Then we characterise the negative translations intuitionistically equivalent to the usual ones.

The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi.

Though it''s difficult to agree on the exact date of their union, logic and artificial intelligence (AI) were married by the late 1950s, and, at least during their honeymoon, were happily united. What connubial permutation do logic and AI find themselves in now? Are they still (happily) married? Are they divorced? Or are they only separated, both still keeping alive the promise of a future in which the old magic is rekindled? This paper is an attempt to answer these questions (...) via a review of six books. Encapsulated, our answer is that (i) logic and AI, despite tabloidish reports to the contrary, still enjoy matrimonial bliss, and (ii) only their future robotic offspring (as opposed to the children of connectionist AI) will mark real progress in the attempt to understand cognition. (shrink)

Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems for (...) N4C and N4C+ are proved. (shrink)

Russell’s paradox is purely logical in the following sense: a contradiction can be formally deduced from the proposition that there is a set of all non-self-membered sets, in pure first-order logic—the first-order logical form of this proposition is inconsistent. This explains why Russell’s paradox is portable—why versions of the paradox arise in contexts unrelated to set theory, from propositions with the same logical form as the claim that there is a set of all non-self-membered sets. Burali-Forti’s paradox, like Russell’s paradox, (...) is portable. I offer the following explanation for this fact: Burali-Forti’s paradox, like Russell’s, is purely logical. Concretely, I show that if we enrich the language \ of first-order logic with a well-foundedness quantifier W and adopt certain minimal inference rules for this quantifier, then a contradiction can be formally deduced from the proposition that there is a greatest ordinal. Moreover, a proposition with the same logical form as the claim that there is a greatest ordinal can be found at the heart of several other paradoxes that resemble Burali-Forti’s. The reductio of Burali-Forti can be repeated verbatim to establish the inconsistency of these other propositions. Hence, the portability of the Burali-Forti’s paradox is explained in the same way as the portability of Russell’s: both paradoxes involve an inconsistent logical form—Russell’s involves an inconsistent form expressible in \ and Burali-Forti’s involves an inconsistent form expressible in \. (shrink)

This is an examination, a commentary, of links between some philosophical views ascribed to Gödel and general proof theory. In these views deduction is of central concern not only in predicate logic, but in set theory too, understood from an infinitistic ideal perspective. It is inquired whether this centrality of deduction could also be kept in the intensional logic of concepts whose building Gödel seems to have taken as the main task of logic for the future.

Inferentialism claims that expressions are meaningful by virtue of rules governing their use. In particular, logical expressions are autonomous if given meaning by their introduction-rules, rules specifying the grounds for assertion of propositions containing them. If the elimination-rules do no more, and no less, than is justified by the introduction-rules, the rules satisfy what Prawitz, following Lorenzen, called an inversion principle. This connection between rules leads to a general form of elimination-rule, and when the rules have this form, they may (...) be said to exhibit “general-elimination” harmony. Ge-harmony ensures that the meaning of a logical expression is clearly visible in its I-rule, and that the I- and E-rules are coherent, in encapsulating the same meaning. However, it does not ensure that the resulting logical system is normalizable, nor that it satisfies the conservative extension property, nor that it is consistent. Thus harmony should not be identified with any of these notions. (shrink)

The Web may critically transform the way we understand the activity of proving. The Web as a collaborative medium allows the active participation of people with different backgrounds, interests, viewpoints, and styles. Mathematical formal proofs are inadequate for capturing Web-based proofs. This article claims that Web provings can be studied as a particular type of Goguen's proof-events. Web-based proof-events have a social component, communication medium, prover-interpreter interaction, interpretation process, understanding and validation, historical component, and styles. To demonstrate its claim, the (...) article discusses the Kumo and Polymath projects, both of which employ Web-based communication as part of proving. Web proving is a novel type of proving activity that may have a serious impact on the change in mathematical practices, despite the fact that it is not currently a universally acceptable methodology. (shrink)

In 'General Propositions and Causality' Ramsey rejects his earlier view that universal generalizations are infinite conjunctions, arguing that they are not genuine propositions at all. We argue that his new position is unstable. The issues about infinity that lead Ramsey to the new view are essentially those underlying Wittgenstein's rule-following considerations. If they show that generalizations are not genuine propositions, they show that there are no genuine propositions. The connection raises interesting historical questions about the direction of influence between Ramsey (...) and Wittgenstein, the origin of the rule-following argument, and the influence of writers such as Brouwer. (shrink)

WeingartnerPaul and LeebHans-Peter, eds, Kreisel’s Interests: On the Foundations of Logic and Mathematics. Tributes; 41. London: College Publications, 2020. Pp. viii + 171. ISBN: 978-1-84890-330-2.

SummaryI defend a conventionalist view of logical and mathematical truths against the criticisms of Quine and Stroud. Conventionalism is best formulated by appealing to sense‐conferring rules governing important logical and mathematical expressions. Conventional necessity can be understood as arising from these rules in a way that is immune to Quine's and Stroud's criticisms of the earlier formulation of conventionalism, in which stress was incorrectly laid on axiomatic systems of logic.RésuméJe soutiens, en dépit des critiques de Quine et de Stroud, une (...) conception conventionnaliste des vérités logiques et de vérités mathématiques. La meilleure façon de formuler le conventionnalisme est de faire appel à des règies conférant un sens à?on;importantes expressions logiques et mathématiques. La nécessité conventionnelle peut être comprise comme provenant de ces règies par des voies qui ne donnent pas prise aux critiques de Quine et de Stroud ag ľégard de ľancienne formulation du conventionnalisme, dans laquelle ľaccent était mis, a tort, sur les systèmes axiomatiques de la logique.ZusammenfassungGegen Quines und Strouds Kritiken verteidige ich eine konventionalistische Auffassung der logischen und mathematischer Wahrheiten. Der Konventionalismus wird am besten durch Berufung auf bedeutungsstiftende Regeln, die den Gebrauch wichtiger logischer und mathematischer Ausdrücke bestimmen, formuliert. Konventionelle Notwendigkeit kann als von diesen Regeln hervorgebracht verstanden werden – und das zwar auf eine Art, die sie vor Quines und Strouds Anfechtungen schützen. In der von diesen kritisierten, früheren Fassung wurde zu unrecht das Gewicht auf axiomatische Systeme der Logik gelegt. (shrink)

We study logic translations from an abstract perspective, without any commitment to the structure of sentences and the nature of logical entailment, which also means that we cover both proof- theoretic and model-theoretic entailment. We show how logic translations induce notions of logical expressiveness, consistency strength and sublogic, leading to an explanation of paradoxes that have been described in the literature. Connectives and quantifiers, although not present in the definition of logic and logic translation, can be recovered by their abstract (...) properties and are preserved and reflected by translations under suitable conditions. (shrink)

This is a survey of Gödel's perennial preoccupations with the limits of finitism, its relations to constructivity, and the significance of his incompleteness theorems for Hilbert's program, using his published and unpublished articles and lectures as well as the correspondence between Bernays and Gödel on these matters. There is also an important subtext, namely the shadow of Hilbert that loomed over Gödel from the beginning to the end.

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.

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)

summary of work in relevant in the Anderson– tradition.]; Mares Troestra, Anne, 1992, Lectures on , CSLI Publications [A quick, easy-to.

Gentzens natural deduction. Thereby the appearance of the cuts in translation is explained.

Structural reasoning is simply reasoning that is governed exclusively by structural rules. In this context a proof system can be said to be structural if all of its inference rules are structural. A logic is considered to be structuralizable if it can be equipped with a sound and complete structural proof system. This paper provides a general formulation of the problem of structuralizability of a given logic, giving specific consideration to a family of logics that are based on the Dunn–Belnap (...) four-valued semantics. It is shown how sound and complete structural proof systems can be constructed for a spectrum of logics within different logical frameworks. (shrink)

The essential structure of proofs is proposed as the basis for a measure of complexity of formulas in FOL. The motivating idea was the recognition that distinct theorems can have the same derivation modulo some non essential details. Hence the difficulty in proving them is identical and so their complexity should be the same. We propose a notion of complexity of formulas capturing this property. With this purpose, we introduce the notions of schema calculus, schema derivation and description complexity of (...) a schema formula. Based on these concepts we prove general robustness results that relate the complexity of introducing a logical constructor with the complexity of the component schema formulas as well as the complexity of a schema formula across different schema calculi. (shrink)

✤ It is the characterization of those forms of reasoning that lead invariably from true sentences to true sentences, independently of the subject matter.

Substructural logics are logics obtained from a sequent formulation of intuitionistic or classical logic by rejecting some structural rules. The substructural logics considered here are linear logic, relevant logic and BCK logic. It is proved that first-order variants of these logics with an intuitionistic negation can be embedded by modal translations into S4-type extensions of these logics with a classical, involutive, negation. Related embeddings via translations like the double-negation translation are also considered. Embeddings into analogues of S4 are obtained with (...) the help of cut elimination for sequent formulations of our substructural logics and their modal extensions. These results are proved for systems with equality too. (shrink)

We present a syntactic proof of cut-elimination for weak Grzegorczyk logic Go. The logic has a syntactically similar axiomatisation to Gödel–Löb logic GL (provability logic) and Grzegorczyk’s logic Grz. Semantically, GL can be viewed as the irreflexive counterpart of Go, and Grz can be viewed as the reflexive counterpart of Go. Although proofs of syntactic cut-elimination for GL and Grz have appeared in the literature, this is the first proof of syntactic cut-elimination for Go. The proof is technically interesting, requiring (...) a deeper analysis of the derivation structures than the proofs for GL and Grz. New transformations generalising the transformations for GL and Grz are developed here. (shrink)

The motivation for Core Logic is explained. Its system of proof is set out. It is then shown that, although the system has no Cut rule, its relation of deducibility obeys Cut with epistemic gain.