The quantified argument calculus (Quarc) is a novel logic which departs from mainstream first-order logic by having quantifiers bind unary predicates instead of variables. Moreover, it also contains devices for modelling anaphoras, active-passive-voice distinctions and sentence- versus predicate-negation. First presented in [1], it has since been the subject of multiple further research directions. In [2], a first foray into modal extensions of Quarc was presented. Quarc-analogues of the Barcan formulas were shown to be invalid and existence to be contingent across the board.

\indent However, while a proof system was sketched, its completeness was not demonstrated. My talk presents the first strongly sound and complete proof systems for modal extensions of Quarc, based on work done in [4]. A family of unlabelled, Gentzen-style natural deduction systems are presented, each being an analogue of the usual modal logics K, D, T, S4 and S5. Moreover, identity is incorporated and shown to be contingent by default. Lastly, while the base semantics are two-valued, the proof systems can also be proven to be strongly sound and complete with respect to strong-Kleene three-valued semantics, assuming ST-validity (cf. [3]). I argue that such semantics are crucial for capturing presupposition-failure with respect to quantification, and finish my talk with an outlook on these three-valued semantics.

Bibliography

1. Hanoch Ben-Yami,The Quantified Argument Calculus,The Review of Symbolic Logic,vol. 7 (2014), no. 1, pp. 120–146.
2. Hanoch Ben-Yami,The Barcan Formulas and NecessaryExistence: The View from Quarc,Synthese,vol. 198 (2021), pp. 11029–11064.
3. Pablo Cobreros, Paul Egré, David Ripley, Robert van Rooij,Tolerant, classical, strict,Journal of Philosophical Logic,vol. 41 (2012), no. 2, pp. 347–385.
4. Hongkai Yin and Hanoch Ben-Yami,The Quantified ArgumentCalculus with Two- and Three-valued Truth-valuationalSemantics,Studia Logica,vol. 111 (2023), pp. 281–320.

Authors: Bahareh Afshari and Raúl Ruiz Mora

Team semantics can be seen as a generalisation of Tarskian model theoretic semantics originally developed by Hodges in [1]. In recent work, see e.g. [3], team semantics have been developed for LTL, CTL and CTL*. Also, team semantics have been defined and studied for modal logic [2] and first order logic giving rise to dependence logic, independence logic and inclusion logic [5].

We define a team semantics for modal mu-calculus, show it enjoys the flatness property and aligns well with existing team temporal logics. The approach taken utilises team semantics for modal logic and involves an algebraic study of powerset structures in order to assign a reasonable team semantics to fixed-points [4].

Bibliography

1. Hodges, W., Compositional semantics for a language of imperfect information. Logic Journal of the IGPL, 5(4) (1997) pp. 539–563.
2. Kontinen, J., Müller, J. S., Schnoor, H., & Vollmer, H., A van Benthem theorem for modal team semantics. Leibniz International Proceedings in Informatics (LIPIcs), 2014.
3. Krebs, A., Meier, A., & Virtema, J., A team based variant of CTL. 22nd International Symposium on Temporal Representation and Reasoning (TIME) (2015) pp. 140–149. IEEE.
4. Ruiz, R., Team semantics for modal mu-calculus. Master’s thesis, University of Amsterdam, 2023.
5. Väänänen, J, Dependence logic: a new approach to independence friendly logic. London Mathematical Society student texts, 70, Cambridge university Press (2007).

A quasi order \(Q\) is called a \(\Delta^0_2\)-better quasi order if every \(\Delta^0_2\) array into \(Q\) is good. This notion plays an important role in Montalb'an’s proof of Fra"iss'e’s conjecture, originally proved by Laver, in the system \(\Pi^1_1\)-CA\(_0\). We show that the property of being \(\Delta^0_2\)-better quasi order can be characterized in terms of an appropriate class of ill founded labelled trees, and discuss that result in the context of reverse mathematics.

Authors: Giacomo Barlucchi, Bahareh Afshari and Graham Leigh

In this talk we present a study about closure ordinals of the modal \(\mu\)-calculus, i.e., modal logic extended with least and greatest fixed point operators.

We show that \(\omega^2\) is a strict upper bound on the closure ordinals of the \(\Sigma\)-fragment of the modal \(\mu\)-calculus, i.e., formulas generated from closed \(\mu\)-calculus formulas and variables through the logical and modal operators, and the \(\mu\) operator. This reproves and extends the claims in [1] concerning closure ordinals of the alternation-free fragment. The approach presented here develops a theory of ordinal annotations based on the notion of well-annotations previously introduced by Kozen [2]. By imposing minimality on the annotating ordinals we relate well-annotations to the existence of closure ordinals. The central argument involves a pumping lemma for well-annotations. Assuming the existence of a sufficiently ‘large’ frame, repetition of annotated sets enables a transfinite series of substitutions, showing it possible to obtain a minimal well-annotation corresponding in size to an arbitrary countable ordinal, thereby refuting the existence of closure ordinals equal or greater than \(\omega^2\).

Bibliography

1. Bahareh Afshari and Graham E. Leigh,On closure ordinals for the modal mu-calculus,Computer Science Logic 2013 {(CSL} 2013)(Torino, Italy),(Simona Ronchi Della Rocca, editor),vol. 23,Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik, 2013,pp. 30–44.
2. Dexter Kozen,A Finite Model Theorem for the Propositional mu-Calculus,Studia Logica: An International Journal for Symbolic Logic,vol. 47 (1988), no. 3, pp. 233–241.

Authors: Borja Sierra Miranda, Thomas Studer and Lukas Zenger

Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like \(\textsf{GL}\) (Gödel-Löb logic also known as provability logic) or \(\textsf{Grz}\) (Grzegorczyk logic).

We provide a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instances of our method, we establish cut-elimination for non-wellfounded systems of the logics \(\textsf{Grz}\) and \(\textsf{wGrz}\) (weak Grzegorczyk logic). Our proof relies only on the categorical definition of corecursion via coalgebras, while an earlier proof by Savateev and Shamkanov uses ultrametric spaces and a corresponding fixed point theorem.

Bibliography

1. Yury Savateev and Daniyar Shamkanov,Non-Well-Founded Proofs Proofs for the Grzegorczyk Modal Logic,The Review of Symbolic Logic,vol. 14 (2018), pp. 22–50.
2. \bysame,Cut Elimination for the Weak Modal Grzegorczyk Logic via Non-well-Founded Proofs,Logic, Language, Information, and Computation. WoLLIC 2019. Lecture Notes in Computer Science(Rosalie Iemhoff, Michael Moortgat and Ruy de Queiroz, editors),vol. 11541,Springer, Berlin, Heidelberg,2019,pp. 569–-583.
3. Borja Sierra Miranda,Cyclic Proofs for iGL via Corecursion,to appear in Electronic Proceedings in Theoretical Computer Science, Workshop on Fixed Points in Computer Science Open Publishing Association,2024.
4. Borja Sierra Miranda, Thomas Studer and Lukas Zenger,_Coalgebraic transformations of non-wellfounded proofs_to appear in arXiv.