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

In derivations of a sequent system, $\mathcal{L}\mathcal{J}$, and a natural deduction system, $\mathcal{N}\mathcal{J}$, the trails of formulae and the subformula property based on these trails will be defined. The derivations of $\mathcal{N}\mathcal{J}$ and $\mathcal{L}\mathcal{J}$ will be connected by the map $g$, and it will be proved the following: an $\mathcal{N}\mathcal{J}$-derivation is normal $\Longleftrightarrow $ it has the subformula property based on trails $\Longleftrightarrow $ its $g$-image in $\mathcal{L}\mathcal{J}$ is without maximum cuts $\Longrightarrow $ that $g$-image has the subformula property based (...) on trails. In $\mathcal{L}\mathcal{J}$-derivations, another type of cuts, sub-cuts, will be introduced, and it will be proved the following: all cuts of an $\mathcal{L}\mathcal{J}$-derivation are sub-cuts $\Longleftrightarrow $ it has the subformula property based on trails. (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 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)

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)

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)

The connection between the rules and derivations of Gentzen’s calculiNJandLJwill be explained by several steps (i.e., systems), and an analysis of the well-known problems of the connection between reduction steps of normalization and cut elimination, from Zucker (1974) and Urban (2014), will be given.