Past talks

Propositional modal logics can be extended by propositional quantifiers, i.e., quantifiers binding proposition letters understood as variables. This paper investigates whether such an extension is always conservative. It is shown that the answer depends on the way in which propositional quantifiers are added. On a minimal approach, according to which propositional quantifiers only have to satisfy the classical principles of quantification, every classical modal logic has a conservative extension by propositional quantifiers. However, in the context of normal modal logics it is natural to require propositionally quantified extensions also to be closed under the rule of necessitation. It is shown that in this setting, there are normal modal logics whose propositionally quantified extensions are nonconservative. Nonconservativity is shown to be a special case of a number of model-theoretic notions of incompleteness. More tentatively, it is suggested that nonconservativity indicates incompleteness in a more substantial sense, concerning the intended target of capturing the logics of modalities. (Forthcoming in the Journal of Logic and Computation, online version available at https://doi.org/10.1093/logcom/exae043.)

Although its axiomatization may appear daunting, the Grzegorczyk logic has attracted significant attention from philosophers, mathematicians, and computer scientists alike. I shall present a new, simplified account of the Grzegorczyk logic and demonstrate its remarkable significance in modal model theory.

In this talk, I present a new class of Modal logics structurally analogous to Hilbert’s Epsilon Calculus, and based on new ‘epsilon modalities’. These are connectives indexed by formulas selecting a world-witness satisfying their index (if any) through an arbitrary choice function. The obtained ‘Epsilon Modal logics’ are conservative over a language with standard modalities, and generalise many properties of Epsilon Calculus at the propositional level. Remarkably, the two systems are proven mutually embeddable. This correspondence carries over to applications. Epsilon terms have been interpreted as indefinite descriptions in linguistics,  ‘ideal objects’ of mathematical properties in Hilbert’s Program, and used to define ‘theoretical terms’ of scientific theories explicitly over their own laws by Carnap. On intensional grounds, epsilon modalities can be read as indefinite description of states, ‘ideal worlds’ abstracting over mathematical structures, and used to explicitly define ‘theoretical contexts’ of scientific theories respectively.

In this proposal, I plan to address whether the modal logic of forcing (as first developed by Hamkins and Löwe (2008)) satisfies the Free Choice Principle (Zimmermann (2000)). The Free Choice Principle (FCP) states that if a disjunction is possible, then each of the disjuncts is also possible: ♢(φ ∨ ψ) → ♢φ ∧ ♢ψ. Such a principle is usually not included as an axiom in any modal logic (Von Wright (1968)), since it would allow one to derive ♢ψ from the single assumption ♢φ. The modal logic of forcing interprets □ and ♢ in terms of set-theoretic forcing: □φ is true in M iff φ is true in all forcing extensions of M, while ♢φ is true in M iff there exists at least one extension of M in which φ is true. In this set-theoretic context, the FCP means: if there is a forcing extension of M in which φ ∨ ψ is true, then there is a forcing extensions of M in which φ is true and another one in which ψ instead is true. A natural question is to ask whether the modal logic of forcing validates the FCP. In this proposal, I argue that, in the modal logic of forcing, the FCP actually holds, but only iff φ and ψ are independent switches, i.e. iff they are always possible in any set-theoretic model M. By contrast, the FCP doesn’t hold for buttons, i.e. statements that can be forced true one time but then remain true in all further extensions. The philosophical upshot of this discussion is that it is possible to connect set-theoretic potentialism (i.e. the view that one can expand the set-theoretic universe by adding new sets) with the validity of the FCP. In particular, if the FCP holds, then the potentialist framework will be linear (i.e. new extensions includes all the previous ones), otherwise it will be branching (there are extensions with no relation to each other).

Predicate modal logic has been controversial at least since the criticisms of Quine. While predicate modal logic is now accepted, questions remain about its formulation, which has been hampered by several myths. Among these are:

1. In the context of a modal operator, substitution of equals for equals fails.

2. In the context of a modal operator, ordinary quantifier rules such as existential generalization fail.

3. De re is the result of a modal operator occurring inside the scope of a quantifier or lambda.

Applying lessons from modal type theory (Bierman and de Paiva 2000, Pfenning and Davies 2001, etc.), I argue for a countervailing principle:

A. In the context of a modal operator, all free variables will receive de re interpretation, and should be marked as such.

Where this is implemented (e.g. Zwanziger 2017), the rules for equality and quantifiers finally become unproblematic (as demanded by Quine), and de re is more evidently decoupled from scope-taking operators. Further refinements are needed, but should avoid Myths 1-3 by adhering to Principle A, roughly speaking. 

This is an introductory-level talk on completeness proofs with respect to Kripke semantics in first-order modal logic.  We will discuss the canonical model construction suitable for first-order modal logics and explain why the concept of canonicity that has proven very useful in propositional modal logic is much less so in first-order modal logic. We will also discuss the notion of quasi-canonicity, a recent attempt, by Valentin Shehtman, to devise a tool more versatile than canocity for establishing completeness of first-order modal logics with respect to Kripke semantics.

When the number of players in a game is large, dynamics typically depend on how many players make a choice. Thus payoffs are determined by choice distributions rather than strategy profiles. If the choice of a,b,c is respectively by 1/2, 1/4. 1/4 of the player population, the payoff is (say) r,s,t with r for those who chose a, s for those who chose b, etc. The players are "anonymous" and the study of improvement dynamics does not refer to specific players. Introducing variables and quantification to reason about it is natural, but leads to undecidable logics. We consider a variable free modal fragment with implicit quantification to reason about large games. Usually logics on games are parameterised by the number of players, and the syntax refers to player identities. In large games, every model comes with its own set of players, offering challenges for decision procedures and axiomatisation. 

This work is joint with Ramit Das (Intel Bangalore, India) and Anantha Padmanabha (IIT Dharwad, India). The talk is based on our paper that appeared in Synthese 201 (163), 2023. 

In classical logic the addition of quantifiers to propositional logic is essentially unique, with some minor variations of course. In modal logic things are not so monolithic. One can quantify over things or over intensions; domains can be the same from possible world to possible world, or shrink, or grow, or follow no pattern, as one moves from a possible world to an accessible one. In 1963 Kripke showed that shrinking or growing domains related to validity of the Barcan and the converse Barcan formulas, but this is a semantic result. Proof theory is trickier. Nested sequents are well behaved, but axiom systems can be unruly. A direct combination of propositional modal axioms and rules with standard quantificational axioms and rules simply proves the converse Barcan formula. It’s not easy to get rid of it. Kripke showed how one could do so, but he needed to use a less common axiomatization of the quantifiers. It works, but one has the impression of having a formal proof system with road blocks placed carefully to prevent proofs from veering into the ditch. 

Some 40 or more years later, justification logic was created by Artemov, and now there are justification systems that correspond to infinitely many different modal logics. The first justification logic was called LP, for logic of proofs. It is related to propositional S4. LP was extended to a quantified version by Artemov and Yavorskaya, with a possible world semantics supplied by Fitting. Subsequently Artemov and Yavorskaya transferred their ideas, concerning what they called binding modalities, back from quantified LP to quantified S4 itself. In the present work we carry their ideas on further to the basic normal modal logic, K, which is not as well-behaved as S4 on these matters. It turns out that this provides a natural intuition for Kripke’s non-standard axiomatization from those many years ago. It also relates quite plausibly to the distinction between de re and de dicto. But now the main work is done through a generalization of the modal operator, instead of through a restriction on allowed quantifier axiomatizations.