In this paper it is shown that addition of certain reductions to the standard cut removing reductions of deductions in prepositional logic makes prepositional logic non-normalizable. From this follows that some provable propositions in prepositional logic has no direct proof.

The interpretation of implications as rules motivates a different left-introduction schema for implication in the sequent calculus, which is conceptually more basic than the implication-left schema proposed by Gentzen. Corresponding to results obtained for systems with higher-level rules, it enjoys the subformula property and cut elimination in a weak form.

This paper presents and motivates a new philosophical and logical approach to truth and semantic paradox. It begins from an inferentialist, and particularly bilateralist, theory of meaning---one which takes meaning to be constituted by assertibility and deniability conditions---and shows how the usual multiple-conclusion sequent calculus for classical logic can be given an inferentialist motivation, leaving classical model theory as of only derivative importance. The paper then uses this theory of meaning to present and motivate a logical system---ST---that conservatively extends classical (...) logic with a fully transparent truth predicate. This system is shown to allow for classical reasoning over the full (truth-involving) vocabulary, but to be non-transitive. Some special cases where transitivity does hold are outlined. ST is also shown to give rise to a familiar sort of model for non-classical logics: Kripke fixed points on the Strong Kleene valuation scheme. Finally, to give a theory of paradoxical sentences, a distinction is drawn between two varieties of assertion and two varieties of denial. On one variety, paradoxical sentences cannot be either asserted or denied; on the other, they must be both asserted and denied. The target theory is compared favourably to more familiar related systems, and some objections are considered. (shrink)

This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

In this paper we show how Dummett-Prawitz-style proof-theoretic semantics has to be modified in order to cope with paradoxical phenomena. It will turn out that one of its basic tenets has to be given up, namely the definition of the correctness of an inference as validity preservation. As a result, the notions of an argument being valid and of an argument being constituted by correct inference rules will no more coincide. The gap between the two notions is accounted for by (...) introducing the distinction between sense and denotation in the proof-theoretic-semantic setting. (shrink)

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As argued in previous (...) work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

Recently Ekman gave a derivation in natural deduction such that it either contains a substantial redundant part or else is not normal. It is shown that this problem is caused by a non-normality inherent in the usual modus ponens rule.

This is a reply to the considerations advanced by Schroeder-Heister and Tranchini as prima facie problematic for the proof-theoretic criterion of paradoxicality, as originally presented in Tennant and subsequently amended in Tennant. Countering these considerations lends new importance to the parallelized forms of elimination rules in natural deduction.

From the point of view of proof-theoretic semantics, it is argued that the sequent calculus with introduction rules on the assertion and on the assumption side represents deductive reasoning more appropriately than natural deduction. In taking consequence to be conceptually prior to truth, it can cope with non-well-founded phenomena such as contradictory reasoning. The fact that, in its typed variant, the sequent calculus has an explicit and separable substitution schema in form of the cut rule, is seen as a crucial (...) advantage over natural deduction, where substitution is built into the general framework. (shrink)

The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening (...) or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only. (shrink)

Curry's paradox, sometimes described as a general version of the better known Russell's paradox, has intrigued logicians for some time. This paper examines the paradox in a natural deduction setting and critically examines some proposed restrictions to the logic by Fitch and Prawitz. We then offer a tentative counterexample to a conjecture by Tennant proposing a criterion for what is to count as a genuine paradox.

Prawitz observed that Russell’s paradox in naive set theory yields a derivation of absurdity whose reduction sequence loops. Building on this observation, and based on numerous examples, Tennant claimed that this looping feature, or more generally, the fact that derivations of absurdity do not normalize, is characteristic of the paradoxes. Striking results by Ekman show that looping reduction sequences are already obtained in minimal propositional logic, when certain reduction steps, which are prima facie plausible, are considered in addition to the (...) standard ones. This shows that the notion of reduction is in need of clarification. Referring to the notion of identity of proofs in general proof theory, we argue that reduction steps should not merely remove redundancies, but must respect the identity of proofs. Consequentially, we propose to modify Tennant’s paradoxicality test by basing it on this refined notion of reduction. (shrink)

The system of natural deduction that originated with Gentzen , and for which Prawitz proved a normalization theorem, is re-cast so that all elimination rules are in parallel form. This enables one to prove a very exigent normalization theorem. The normal forms that it provides have all disjunction-eliminations as low as possible, and have no major premisses for eliminations standing as conclusions of any rules. Normal natural deductions are isomorphic to cut-free, weakening-free sequent proofs. This form of normalization theorem renders (...) unnecessary Gentzen's resort to sequent calculi in order to establish the desired metalogical properties of his logical system.Ultimate normal forms are well-adapted to the needs of the computational logician, affording valuable constraints on proof-search. They also provide an analysis of deductive relevance. There is a deep isomorphism between natural deductions and sequent proofs in the relevantized system. (shrink)