•  1
    Intensional Harmony as Isomorphism
    with Paolo Pistone
    In Thomas Piecha & Kai F. Wehmeier (eds.), Peter Schroeder-Heister on Proof-Theoretic Semantics, Springer. pp. 315-337. 2024.
    In the present paper we discuss a recent suggestion of Schroeder-Heister concerning the possibility of defining an intensional notion of harmony using isomorphism in second-order propositional logic. The latter is not an absolute notion, but its definition is relative to the choice of criteria for identity of proofs. In the paper, it is argued that in order to attain a satisfactory account of harmony, one has to consider a notion of identity stronger than the usual one (based on β- and η-convers…Read more
  •  105
    Supervaluationism: Truth, Value and Degree Functionality
    Thought: A Journal of Philosophy 3 (2): 136-144. 2014.
    This article deals with supervaluationism and the failure of truth-functionality. It draws some distinctions that may contribute to a better understanding of this semantic framework
  •  361
    (I can’t get no) antisatisfaction
    Synthese 198 (9): 8251-8265. 2020.
    Substructural approaches to paradoxes have attracted much attention from the philosophical community in the last decade. In this paper we focus on two substructural logics, named ST and TS, along with two structural cousins, LP and K3. It is well known that LP and K3 are duals in the sense that an inference is valid in one logic just in case the contrapositive is valid in the other logic. As a consequence of this duality, theories based on either logic are tightly connected since many of the arg…Read more
  •  40
    The Naturality of Natural Deduction
    with Paolo Pistone and Mattia Petrolo
    Studia Logica 107 (1): 195-231. 2019.
    Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic NI\. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equati…Read more
  •  34
    Higher-level Inferences in the Strong-Kleene Setting: A Proof-theoretic Approach
    Journal of Philosophical Logic 51 (6): 1417-1452. 2021.
    Building on early work by Girard ( 1987 ) and using closely related techniques from the proof theory of many-valued logics, we propose a sequent calculus capturing a hierarchy of notions of satisfaction based on the Strong Kleene matrices introduced by Barrio et al. (Journal of Philosophical Logic 49:93–120, 2020 ) and others. The calculus allows one to establish and generalize in a very natural manner several recent results, such as the coincidence of some of these notions with their classical …Read more
  •  17
    In a previous paper we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models of polymorphic type theory. A different approach to extract proof-theoretic properties of natural deduction derivations was proposed in a recent series of papers on the basis of an embedd…Read more
  •  72
    Supervaluationism, Subvaluationism and the Sorites Paradox
    with Pablo Cobreros
    In Sergi Oms & Elia Zardini (eds.), The Sorites Paradox, Cambridge University Press. pp. 38-62. 2019.
    One way in which we might approach the challenge posed by the Sorites Paradox is considering that Sorites-susceptible predicates have several candidate extensions, or several ways in which these expressions can be made precise. For example, a candidate extension for the predicate ‘is a baby’ is the set of humans of less than two years, but also the set of those less than two years and one second, and of those less than two years and two seconds. In this chapter we present and discuss two theorie…Read more
  •  20
    How to Ekman a Crabbé-Tennant
    with Peter Schroeder-Heister
    Synthese 199 (Suppl 3): 617-639. 2018.
    Developing early results of Prawitz, Tennant proposed a criterion for an expression to count as a paradox in the framework of Gentzen’s natural deduction: paradoxical expressions give rise to non-normalizing derivations. Two distinct kinds of cases, going back to Crabbé and Tennant, show that the criterion overgenerates, that is, there are derivations which are intuitively non-paradoxical but which fail to normalize. Tennant’s proposed solution consists in reformulating natural deduction elimina…Read more
  •  36
    Proof, Meaning and Paradox: Some Remarks
    Topoi 38 (3): 591-603. 2019.
    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 ad…Read more
  •  29
    Stabilizing Quantum Disjunction
    Journal of Philosophical Logic 47 (6): 1029-1047. 2018.
    Since the appearance of Prior’s tonk, inferentialists tried to formulate conditions that a collection of inference rules for a logical constant has to satisfy in order to succeed in conferring an acceptable meaning to it. Dummett proposed a pair of conditions, dubbed ‘harmony’ and ‘stability’ that have been cashed out in terms of the existence of certain transformations on natural deduction derivations called reductions and expansions. A long standing open problem for this proposal is posed by q…Read more
  •  30
    Ekman’s Paradox
    with Peter Schroeder-Heister
    Notre Dame Journal of Formal Logic 58 (4): 567-581. 2017.
    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 p…Read more
  •  48
    Natural deduction for bi-intuitionistic logic
    Journal of Applied Logic 25. 2017.
    We present a multiple-assumption multiple-conclusion system for bi-intuitionistic logic. Derivations in the systems are graphs whose edges are labelled by formulas and whose nodes are labelled by rules. We show how to embed both the standard intuitionistic and dual-intuitionistic natural deduction systems into the proposed system. Soundness and completeness are established using translations with more traditional sequent calculi for bi-intuitionistic logic.
  •  23
    In the first chapter, we discuss Dummett’s idea that the notion of truth arises from the one of the correctness of an assertion. We argue that, in a first-order language, the need of defining truth in terms of the notion of satisfaction, which is yielded by the presence of quantifiers, is structurally analogous to the need of a notion of truth as distinct from the one of correctness of an assertion. In the light of the analogy between predicates in Frege and open formulas in Tarksi, we concentra…Read more
  •  70
    Truth from a Proof-Theoretic Perspective
    Topoi 31 (1): 47-57. 2012.
    Validity, the central concept of the so-called ‘proof-theoretic semantics’ is described as correctly applying to the arguments that denote proofs. In terms of validity, I propose an anti-realist characterization of the notions of truth and correct assertion, at the core of which is the idea that valid arguments may fail to be recognized as such. The proposed account is compared with Dummett’s and Prawitz’s views on the matter
  •  44
    Anti-realistic Notions of Truth
    Topoi 31 (1): 5-8. 2012.
    Validity, the central concept of the so-called ‘proof-theoretic semantics’ is described as correctly applying to the arguments that denote proofs. In terms of validity, I propose an anti-realist characterization of the notions of truth and correct assertion, at the core of which is the idea that valid arguments may fail to be recognized as such. The proposed account is compared with Dummett’s and Prawitz’s views on the matter.
  •  45
    Proof-theoretic harmony: towards an intensional account
    Synthese 198 (Suppl 5): 1145-1176. 2016.
    In this paper we argue that an account of proof-theoretic harmony based on reductions and expansions delivers an inferentialist picture of meaning which should be regarded as intensional, as opposed to other approaches to harmony that will be dubbed extensional. We show how the intensional account applies to any connective whose rules obey the inversion principle first proposed by Prawitz and Schroeder-Heister. In particular, by improving previous formulations of expansions, we solve a problem w…Read more
  •  17
    Harmonising harmony
    Review of Symbolic Logic 8 (3): 411-423. 2015.
  •  54
    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 distin…Read more
  •  77
    Natural Deduction for Dual-intuitionistic Logic
    Studia Logica 100 (3): 631-648. 2012.
    We present a natural deduction system for dual-intuitionistic logic. Its distinctive feature is that it is a single-premise multiple-conclusions system. Its relationships with the natural deduction systems for intuitionistic and classical logic are discussed.