Logische Folgerung und paradoxes Schließen
Mathematik
Zusammenfassung der Projektergebnisse
In proof-theoretic semantics the validity of an argument (or formal derivation) has been equated with the possibility of transforming it into another argument in “normal form” using certain operations called reduction procedures. The Prawitz-Tennant analysis of paradoxes is the thesis that, in presence of paradoxical expressions, one can establish contradictions, but the arguments establishing them are not valid, as the process of reduction to normal form gets stuck in a loop. The project closely scrutinized the tenability of the Prawitz-Tennant analysis and proposed to refine it by adopting a qualified notion of reduction procedure. The need for this refinement is that, without clear criteria for telling which reduction procedures are to qualify as acceptable, one can show that the Prawitz-Tennant criterion for paradoxicality overgenerates, that is, it attributes paradoxicality to derivations about which, intuitively, there is nothing paradoxical. The proposed criteria for acceptability of reduction procedures are based on the notion of identity of proof, developed in computational and categorial interpretation of – especially natural deduction – proof-systems. Formal derivations in such systems should be regarded as linguistic means for representing abstract entitites: proofs. Different derivations may represent the same proof and a reduction procedure is acceptable if and only if whenever it is applied to a given derivation it yields another derivation representing the same proof. In other words, the process of reduction should not modify the essence of (i.e. the proof represented by) the derivation. The conception of derivations as representing proofs has been taken as the core of a novel conception of proof-theoretic semantics, that has been dubbed “intensional”, in contrast to the more traditional “extensional” conception. From an intensional standpoint, the focus of proof-theoretic semantics should not be simply on “what” can be proved (in a given proofsystem) but on the “how”, that is on the (essentially) different ways of proving something within a given proof-system. The investigation of families of acceptable reduction procedures has been linked in the project to the study of the notion of harmony. A major outcome of the project was the development of an intensional notion of harmony, thanks to which harmonious rules are defined simultanously with acceptable reduction procedures. The intensional characterization of harmony has been shown to be superior to the extensional accounts known from the literature, in particular for being capable to resolve a long standing puzzle represented by the rules for the so-called quantum disjunction (intuitively disharmonious but passing all tests for harmony formulated so far). These groundbreaking results opened different further research directions: on the one hand, the reduction procedures underlying intensional harmony have been connected to certain features of the categorial interpretation of subsystems of quantified propositional intuitionistic logic (System F); on the other hand, the possibility of defining harmony beyond the realm of propositional connectives (that is also to quantifiers and inductively definable predicates, such as identity) is the object of ongoing work by the applicant. Finally, the project investigated the prospects of bringing together the revised Prawitz-Tennant anaylsis of paradoxes with the intensional conception of proof-theoretic semantics and registered a tension between—on the one hand—an intensional understanding of function, and—on the other hand—the adoption of normalizability as a criterion of validity. The proposed solution, consisting in restricting the application of reduction procedure to categorical arguments, opens the way towards a fine-grained analysis of reduction strategies using tools coming from the study of functional languages in theoretical computer science.
Projektbezogene Publikationen (Auswahl)
-
«Ekman’s paradox» Notre Dame Journal of Formal Logic, 58(4):567–581, 2017
Luca Tranchini, Peter Schroeder-Heister
-
«How to Ekman a Crabbé-Tennant» Synthese [Sonderheft Substructural approaches to paradoxes], 2018
Luca Tranchini, Peter Schroeder-Heister
-
«Stabilizing quantum disjunction» Journal of Philosophical Logic, 47(6):1029–1047, 2018
Luca Tranchini
-
«The naturality of natural deduction» Studia Logica [Sonderheft General Proof Theory], 107(1):195–231, 2019
Luca Tranchini, Mattia Petrolo und Paolo Pistone
