Falsity and refutations: Understanding the negative side of logic
Theoretical Computer Science
Final Report Abstract
In modern logic, the notions of falsity, refutation and denial have been mostly treated as subordinate ones, to be reduced to their “positive counterparts”, truth, proof and assertion. The goal of the project was that of challenging this view and disclosing the potential of the negative side of logic. The project started by closely scrutinizing traditional and contemporary alternatives to the dominant conception, producing an overview of the development of the relationship between positive and negative notions, and of negation, conceived as hinge between them. Among such alternatives, the project focused on the line of research stemming from the idea of introducing a constructive notion of refutation alongside the intuitionistic notion of proof, and substantial results advanced the state of the art in significant respects. A first breakthrough of a general nature was that of highlighting the importance of identity criteria for proofs and refutations. Only in presence of non-trivial criteria of identity is the constructivist analysis of the meaning of a proposition using proof- and refutation-conditions more fine-grained than the realist one based on truth- and falsity conditions. The focus on identity criteria has been taken as the starting point for the development of a novel conception of proof-theoretic semantics, dubbed “intensional” a general sketch of which has been delivered in the applicant’s Habilitation thesis, and that will be further developed in future work. This novel phiosophical stance has been backed by formal results concerning various notions of identity of proofs in joint work with Paolo Pistone. The second part of the project developed an account of the notion of refutation dualizing the computational interpretation of intuitionistic logic known as the Curry-Howard correspondence. Following Curry-Howard, a formal derivation in the system for intuitionistic logic is interpreted as a program that transforms proofs of the assumptions into a proof of the conclusion. In the proposed dual picture, an intuitionistic derivation is interpreted as a “dual program” that transforms a refutation of the conclusion into a collective refutation of the assumptions. In the case of intuitonistic logic, the Curry-Howard correspondence and its proposed dualization are “alternative” ways of interpreting the derivations of the formal system, and the same is true in the case of dual-intuitionistic logic (with proofs and refutations exchanging their role). In the case of bi-intuitionistic logic, which combines intuitionistic logic and its dual, however, the interaction of proofs and refutations is more delicate, and a clarification of the picture is being pursued in current work by the applicant. In the third part of the project explored the significance of the negative notions of falsity, refutation and denial in other areas of non-classical logic, and beyond the realm of pure logic. In joint work with Pablo Coberos and Elio La Rosa the applicant investigated various notions of duality arising in contect of consequence relations defined on the basis of the Strong-Kleene truth-tables, and used them to clarify the relationship of these consequence relations an that of classical logic. In joint work with Paolo Maffezioli, the rules governing apartness (a notion introduced in the field of constructive analysis as the “positive counterpart” of negated equality) has been reinterpreted as expressing refutation-condition, rather than proof-conditions, thereby showing the precise sense in which apartness and equality are dual of each other. In spite of the disruption caused by the COVID-19 pandemic to national and international travel, the applicant could develop strong collaborations with various collegues across Europe and present the results of the project at large number of events (some of which tool place either in hybryd or on-line form). A workshop organized by the applicant planned to take place in Tübingen in March 2020 was cancelled on a short notice, but a series of online events (the first of which was attended by more than 40 participants) has been organized as a replacement.
Publications
- „(I can’t get no) Antisatisfaction“. Synthese 198:8251–8265, 2021
Luca Tranchini, Pablo Cobreros und Elio La Rosa
(See online at https://doi.org/10.1007/s11229-020-02570-x) - „Equality and apartness in bi-intuitionistic logic“. Logical Investigations, 27(1): 82–106, 2021 [Sonderheft „Negation“– Herausgeber: Grigory Olkhovikov, Hitoshi Omori und Heinrich Wansing]
Luca Tranchini, Paolo Maffezioli
(See online at https://doi.org/10.21146/2074-1472-2021-27-1-82-106) - „Higher-level inferences in the Strong-Kleene setting: A proof-theoretic approach“. Journal of Philosophical Logic, 2021 [Sonderheft „Substructural Logics and Metainferences“– Herausgeber: Eduardo Barrio und Paul Egré]
Luca Tranchini, Pablo Cobreros und Elio La Rosa
(See online at https://doi.org/10.1007/s10992-021-09639-z) - „Negation“ In Francesca Poggiolesi und Pierre Wagner (Hrsg.), Précis de philosophie de la logique (S. 253–301), Éditions de la Sorbonne, Paris, 2021
Luca Tranchini
- „The naturality of natural deduction (II): On atomic polymorphism and generalized propositional connectives“. Studia Logica, 110:545–592, 2022
Luca Tranchini, Paolo Pistone und Mattia Petrolo
(See online at https://doi.org/10.1007/s11225-021-09964-z)
