Nordic Online Logic Seminar

We formulate and discuss a general axiomatic theory of arbitrary objects. This theory is expressed in a simple first-order language without modal operators, and it is governed by classical logic. The theory AOT intends to be a fundamental and a fully general (and somewhat flexible) theory of arbitrary objects. Ideally, it intends to be a suitable formal framework for all legitimate applications of arbitrary object theory. According to the proposed theory, arbitrary objects are organised in correlated systems, where each such system of arbitrary objects is abstracted from a system of particular objects.

First-order modal logic (FOML) provides a natural logical language for reasoning about modal attitudes, while retaining the richness of quantification for referring to predicates over domains. However, FOML is notoriously bad computationally, as most of the useful fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic fragment) have been shown to be decidable under heavy restrictions on the syntax. In this talk, I survey our recent work on the newly discovered bundled fragments based on constructions bundling quantifiers and modalities together. The idea came from our earlier work on epistemic logics of know-how/why/what, and it led us to many expressive and decidable fragments of FOML without restricting the number of variables or the arity of the predicates. I will give an almost complete picture of the (un)decidability of all the basic bundled fragments of FOML over increasing and constant domain models. I conclude with some future directions.

The field of Belief Change studies how an agent updates its beliefs in the presence of new information. In this work, we consider the case where beliefs are represented as description logic concepts and the new information is in the format of pointed interpretations. We call this setting model change, and distinguish three main kinds of changes: eviction, which consists of only removing models; reception, which incorporates models; and revision, which combines removal with incorporation of models in a single operation. We introduce a formal notion of revision and argue that it does not reduce to a simple combination of eviction and reception, contrary to intuition. We provide positive and negative results on the compatibility of eviction and reception for EL and ALC description logic concepts and on the compatibility of revision for ALC concepts.

The claim is that intensions (or meanings) can be modeled usefully by algorithms which compute truth values, proofs (in various systems), denotations and implementations of programs (in various programming languages), etc.. I will discuss the nature of these ‘algorithms’ and present some unpublished results by me and others on this topic. Most of what I will say is in the book [1] which contains many unpublished results by Lou van den Dries, Vaughn Pratt, Anush Tserunyan and others.

1. Yiannis Moschovakis. Abstract recursion and intrinsic complexity, Cambridge University Press, Volume 48 in the Lecture Notes in Logic, Association for Symbolic Logic, 2019. (See YM’s homepage).

Team semantics is a semantic framework originally introduced by Hodges (1997) for the study of dependence and independence concepts, and later systematically developed by Väänänen (2007). It is also independently adopted in inquisitive logic by Ciardelli and Roelofsen (2011). In team semantics, formulas are evaluated with respect to sets of evaluation points, called teams, rather than single evaluation points as in standard semantics.

Logics based on team semantics are typically extensions of classical logic and thus inherit classical implication over classical formulas. However, the earliest versions of team-based logic, such as independence-friendly logic and dependence logic, do not include a conditional connective for arbitrary formulas. An adequate conditional, known as intuitionistic implication, was proposed for dependence logic by Abramsky and Väänänen (2009). This connective is also part of the syntax of inquisitive logic. Intuitionistic implication behaves well in these downward closed logics, in the sene that it preserves downward closure and satisfies both Modus Ponens and the Deduction Theorem.

In recent years, many variants of dependence logic with different closure properties have been introduced, including union closed and convex logics. In these settings, the intuitionistic implication no longer behaves well, as it either fails to preserve the relevant closure property or fails to satisfy the Deduction Theorem. In this talk, we show that this failure is unavoidable: these logics cannot be enriched with any conditional connective that simultaneously preserves the closure property and satisfies both Modus Ponens and the Deduction Theorem.

This is joint work with Fausto Barbero.