We give a simple and direct proof that super-consistency implies the cut-elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut-elimination theorems in higher-order logic that involve V-complexes.

The present note was prompted by Weber’s approach to proving Cantor’s theorem, i.e., the claim that the cardinality of the power set of a set is always greater than that of the set itself. While I do not contest that his proof succeeds, my point is that he neglects the possibility that by similar methods it can be shown also that no non-empty set satisfies Cantor’s theorem. In this paper unrestricted abstraction based on a cut free Gentzen type sequential calculus (...) will be employed to prove both results. In view of the connection between Priest’s three-valued logic of paradox and cut free Gentzen calculi this, a fortiori, has an impact on any paraconsistent set theory built on Priest’s logic of paradox. (shrink)

The recent development and exploration of mixed metainferential logics is a breakthrough in our understanding of nontransitive and nonreflexive logics. Moreover, this exploration poses a new challenge to theorists like me, who have appealed to similarities to classical logic in defending the logic ST, since some mixed metainferential logics seem to bear even more similarities to classical logic than ST does. There is a whole ST-based hierarchy, of which ST itself is only the first step, that seems to become more (...) and more classical at each level. I think this seeming is misleading: for certain purposes, anyhow, metainferential hierarchies give us no reason to move on from ST. ST is indeed only the first step on a grand metainferential adventure; but one step is enough. This paper aims to explain and defend that claim. Along the way, I take the opportunity also to develop some formal tools and results for thinking about metainferential logics more generally. (shrink)

In this study, we prove the completeness and cut-elimination theorems for a first-order extension F4CC of Arieli, Avron, and Zamansky’s ideal paraconsistent four-valued logic known as 4CC. These theorems are proved using Schütte’s method, which can simultaneously prove completeness and cut-elimination.

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)

I investigate substitutional interpretations of quantifiers that count existential sentences true just in case they have true instances in a parametric extension of the language. I devise a semantics meeting four criteria: (1) it accounts adequately for natural language quantification; (2) it provides an account of justification in abstract sciences; (3) it constitutes a continuous semantics for natural and formal languages; and (4) it is purely substitutional, containing no appeal to referential interpretations. The prospects for a purely substitutional theory of (...) quantification are thus no worse than for a referential account. (shrink)

The recent development and exploration of mixed metainferential logics is a breakthrough in our understanding of nontransitive and nonreflexive logics. Moreover, this exploration poses a new challenge to theorists like me, who have appealed to similarities to classical logic in defending the logic ST, since some mixed metainferential logics seem to bear even more similarities to classical logic than ST does. There is a whole ST-based hierarchy, of which ST itself is only the first step, that seems to become more (...) and more classical at each level. I think this seeming is misleading: for certain purposes, anyhow, metainferential hierarchies give us no reason to move on from ST. ST is indeed only the first step on a grand metainferential adventure; but one step is enough. This paper aims to explain and defend that claim. Along the way, I take the opportunity also to develop some formal tools and results for thinking about metainferential logics more generally. (shrink)

Atserias, Galesi, and Pudlák have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK . We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut-formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.

A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion.

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)

We develop a Gentzen-style proof theory for super-Belnap logics, expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics which relax the structural rules of classical logic but keep its logical rules as well as the rules of Identity and Cut, super-Belnap logics may be seen as logics which relax Identity and Cut but keep the logical rules as well as the structural rules of classical logic. A generalization of the (...) cut elimination theorem for classical propositional logic is then proved and used to establish interpolation for various super-Belnap logics. In particular, we obtain an alternative syntactic proof of a refinement of the Craig interpolation theorem for classical propositional logic discovered recently by Milne. (shrink)