X Workshop on Philosophical Logic:
Week II: Meta-inferences and Proof theory
August 12, 13 2021
Online Conference via ZOOM Meetings
Thomas Ferguson (Universiteit van Amsterdam)
Andreas Fjellstad (University of Bergen)
Rea Golan (Freie Universität Berlin)
Elio La Rosa (MCMP, LMU Munich)
Isabella McAllister (University of Auckland)
Federico Pailos (University of Buenos Aires)
Mariela Rubin (University of Buenos Aires)
“Reconciling Veridical and Content-Theoretic Anomalies in Bounds Consequence”
The intuitions motivating the bounds consequence interpretation of ST—whether at the inferential or metainferential level—are compatible with multiple triggers by which a position may be out of bounds. The cases primarily cited as justification for ST like the Liar sentence are veridically anomalous, in which case bounds are transgressed upon veridical defects. But there are also positions that are content-theoretically anomalous in that the position is out-of-bounds for defects in subject-matter. Such considerations yield a system of weak ST that differs metainferentially from stock ST. In general, our positions can transgress bounds for both veridical and content-theoretic anomalies, however; so a natural question is how to characterize bounds consequence in which both types of defects coexist. In this talk, I will consider several ways to provide such accounts and discuss several interesting consequences for the notion of metainferences that follow from these considerations.
“A proof-theoretic analysis of the metainferential solution to the semantic paradoxes”
Substructural solutions to the semantic paradoxes have been broadly discussed in recent years. In particular, according to the non-transitive solution, we have to give up the metarule of Cut, whose role is to guarantee that the consequence relation is transitive. This concession—giving up a metarule—allows us to maintain the entire consequence relation of classical logic. The non-transitive solution has been generalized in recent works into a hierarchy of logics where classicality is maintained at more and more metainferential levels. All the logics in this hierarchy can accommodate a truth predicate, including the logic at the top of the hierarchy—known as CMω—which presumably maintains classicality at all levels. CMω has been accounted for mostly in model-theoretic terms. Therefore, there remains an open question: how do we account for this logic in proof-theoretic terms? Can there be found a proof system that admits each and every classical principle—at all inferential levels—but nevertheless blocks the derivation of the liar? In this talk, I present a solution to this problem, by providing such a proof system. Yet, I also argue that the outcome is philosophically unsatisfactory. In fact, I’m afraid that in light of my proof system, the metainferential solution to the paradoxes can hardly be called a “solution,” let alone a good one.
“Metainferences in Modal Logics”
Recently, it has been shown that there exists a hierarchy of logics, where each logic in the hierarchy matches the validities of classical logic up to some metainferential level, but differs at levels beyond that. I show that this phenomenon generalizes to logics characterizable by Kripke semantics, including modal and superintuitionistic logics. In particular, given any logic L characterizable by some class of frames F, we can use F to generate a hierarchy of new logics, each of which have exactly the validities of L up to some metainferential level, but differ above that level. For example, we can construct a logic IT that has exactly the theorems of intuitionistic logic, but different inferences, a logic IST that has exactly the theorems and inferences, but different metainferences, etc. The existence of these hierarchies show that the same characterizability concerns for classical logic also arise for modal and superintuitionistic logics—each logic cannot be uniquely characterized by only taking into account metainferences up to some level.
Elio La Rosa:
in the Strong-Kleene setting: A proof-theoretic approach”
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. (2019) 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 counterparts, and the possibility of expressing some notions of satisfaction for higher-level inferences using notions of satisfaction for inferences of lower level. We also show that at each level all notions of satisfaction considered are pairwise distinct and we address some remarks on the possible significance of this (huge) number of notions of consequence.
Federico Pailos and Mariela Rubin:
A metainference is usually understood as a pair consisting of a set of inferences, called premises, and a single inference, called conclusion. In the last few years, much attention has been paid to the study of metainferences —in particular, to the question of what are the valid metainferences in a given logic. So far, however, this study has been done in a quite poor language. Our usual formal apparatus have no way to represent, e.g. negated inferences, a disjunction in the premises of a metainference or a conjunction in the conclusion. In this paper we tackle these expressive issues. We define an inferential language—a language whose atomic formulas are inferences. We provide a semantic characterisation of validity for this language. We argue that our inferential language is interesting for its expressiveness. In particular, it enables forms of metainferences not yet analysed in the literature, and it allows for a better understanding of the sense in which many known non-classical logics have a classical metatheory. Barrio et al. 2016 proved that the valid metainferences of logic ST correspond to the valid inferences of logic LP. We show that this result remains true in our inferential language. Also, we prove that an analogous result holds for logics TS and K3. We provide sound complete proof systems for logics CL, LP, K3, ST and TS in our inferential language. Finally, we extend this framework to every higher (finite) metainferential level. This is a joint work with Camillo Fiore.
“Proof theory for infinitary metainferences”
The literature on metainferential logics has so far only discussed finitary propositional logics. The aim of this talk is to have a look at infinitary metainferences and how a proof theory representing such metainferences can be developed. To keep things simple, the talk will focus on the metainferences validated by the shared context ω-rule for the universal quantifier.
Federico Pailos (UBA/IIF-SADAF-CONICET)
We are thankful for the support provided by CONICET and MINCYT