Contributed Talks 19
Chair: Sebastian Enqvist
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
14:00 
Simon Vonlanthen, Modal extensions of the quantified argument calculus 
The quantified argument calculus (Quarc) is a novel logic which departs from mainstream firstorder logic by having quantifiers bind unary predicates instead of variables. Moreover, it also contains devices for modelling anaphoras, activepassivevoice distinctions and sentence versus predicatenegation. 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. Quarcanalogues 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, Gentzenstyle 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 twovalued, the proof systems can also be proven to be strongly sound and complete with respect to strongKleene threevalued semantics, assuming STvalidity (cf. [3]). I argue that such semantics are crucial for capturing presuppositionfailure with respect to quantification, and finish my talk with an outlook on these threevalued semantics. Bibliography


14:25 
Raúl Ruiz Mora, Team semantics for modal mucalculus 
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 mucalculus, 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 fixedpoints [4]. Bibliography


14:50 
Davide Manca, Δ⁰_2better quasi orders in reverse mathematics 
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. 

15:15 
Giacomo Barlucchi, The limit of recursion in statebased systems. 
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 alternationfree fragment. The approach presented here develops a theory of ordinal annotations based on the notion of wellannotations previously introduced by Kozen [2]. By imposing minimality on the annotating ordinals we relate wellannotations to the existence of closure ordinals. The central argument involves a pumping lemma for wellannotations. 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 wellannotation corresponding in size to an arbitrary countable ordinal, thereby refuting the existence of closure ordinals equal or greater than \(\omega^2\). Bibliography


15:40 
Borja Sierra Miranda, Coalgebra for nonwellfounded proof theory 
Authors: Borja Sierra Miranda, Thomas Studer and Lukas Zenger Nonwellfounded 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 wellfounded frame conditions like \(\textsf{GL}\) (GödelLö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 cutelimination for nonwellfounded 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
