The Equivalence Principle is an informal principle asserting that equivalent mathematical objects have the same properties. For example, group theory has been developed so that isomorphic groups have the same group-theoretic properties, and category theory has been developed so that equivalent categories have the same category-theoretic properties (though sometimes other, ‘evil’ properties are considered). Vladimir Voevodsky established Univalent Foundations as a foundation of mathematics (based on dependent type theory) in which the Equivalence Principle for types (the basic objects of type theory) is a theorem. Later, versions of the Equivalence Principle for set-based structures such as groups and categories were shown to be theorems in Univalent Foundations.

In this work, we formulate and prove versions of the Equivalence Principle (using the “Univalence Principle”) for a large class of categorical and higher categorical structures in Univalent Foundations. Our work encompasses bicategories, dagger categories, opetopic categories, and more. Many of the notions used in our work were inspired by Makkai’s First-order logic with dependent sorts.

In team semantics (introduced by Hodges (1997)), formulas are evaluated with respect to sets of evaluation points called teams, as opposed to the single evaluation points of standard Tarski-style semantics. The shift to teams allows for the perspicuous articulation of certain phenomena which are not readily expressible in the standard semantics: Väänänen’s (2007) dependence logic, for instance, introduces team-semantic atoms which denote dependence relations not expressible in first-order logic.

The most prominent team-based logics are downward closed, meaning that if a formula of one of these logics is true in a team T, it is also true in all subteams of T. Expressive completeness theorems with respect to closure properties such as downward closure play an important role in the study of propositional and modal team semantics—a common method for proving the completeness of an axiomatization, for instance, makes use of such theorems. In this talk, I examine a number of propositional and modal team-based logics which fail to be downward closed, present expressive completeness theorems for these logics, and give examples of how such theorems are utilized.

​Time: 15.30 – 17.00

Tarski’s model-theoretic definition of logical consequence relies on a division of the expressions of the language under considerations into logical and non-logical. Finding a philosophically motivated and mathematically precise criterion to delineate the logical expressions of a language constitutes the demarcation problem of the logical constants.

In this talk, we propose a novel criterion of logicality designed to address the demarcation problem. It combines insights from the model-theoretic as well as from the inferentialist approaches to meaning. According to it a notion qualifies as logical if its inferential behaviour determines a unique denotation among logically acceptable interpretations.

In this talk, we propose a novel criterion of logicality designed to address the demarcation problem. It combines insights from the model-theoretic as well as from the inferentialist approaches to meaning. According to it a notion qualifies as logical if its inferential behaviour determines a unique denotation among logically acceptable interpretations.

Time: 15.30 – 17.00

Partial Combinatory Algebras, between realizability and oracle computation​

Time: 16.00 – 17.30

Deontic games are normal form games equipped with a classification of action profiles into those that are acceptable and those that are not. These games have been used in past work to tackle various questions concerning individual and group obligation, group plans and coordination, and method- ological individualism. This paper is the first to develop a combinatorial perspective on such games. In particular, we define three ways to combine any two deontic games, resulting in a new game that represents the simulta- neous play of both original games. We then study the relation between the deontic status of group actions in the new game and the deontic status of the corresponding sub-actions in the original games, establishing a number of fundamental reduction theorems. From these, we derive several corollaries concerning the existence of acceptability voids in interaction scenarios.

​Time: 15.30 – 17.00

In a recent article, Gillian Russell (2020) claims that logic isn’t normative: according to her, the usual bridge principles are just derived from general principles for truth and falsity, such as “believe the truth” or “avoid falsity”. For example, we should believe tautologies just because we should believe the truth. Russell argues that this rejection of logical normativity can avoid the collapse objection for logical pluralism. In a different paper, Russell and Blake Turner (2021) defend a telic pluralism, where different logics may correspond to different epistemic aims, without assuming that logic is normative.

In a response to that paper, Stei (2020) claims that even if logic is normative in this weak derivative sense, the collapse objection re-emerges. His main point is that the collapse argument can still work even if the bridge principles are derivative (they just need to be true).

In this talk I will argue against Stei’s point. I will show that there is a possible strategy which maintains the derivative normativity of logic and provides a non-trivial logical pluralism. My proposal is different from the telic pluralism, for it does not depend on the epistemic aims of the agent. The key of my approach is the possibility of having different normative sources for different logics. I will argue that the distinction between classical and relevant logic can be understood in this way.

References

Blake-Turner, C. and G. Russell, “Logical pluralism without the normativity”, Synthese 198, 2021, pp. 4859-4877.

Russell, G. “Logic isn’t normative”, Inquiry 63(3-4), 2020, pp. 371-388.

Stei, E. “Non-normative logical pluralism and the revenge of the normativity objection”, Philosophical Quarterly 70 (278), 2020, pp. 162–177.

​Time: 15.30 – 17.00

Arimaa is a two-player strategy game played on an 8 x 8 board. Like chess, checkers, and Go, it is a perfect-information, deterministic, turn-based game in which there is at most one winner. Arimaa has been a focus of much attention in applied AI research, as it was originally designed purposely to be difficult for computers to play.

This talk considers the more theoretical question, “Given a position in Arimaa and specified player, does that player have a winning strategy?” As with chess and checkers, this question is trivially solvable in constant time if the game is played on a standard 8 x 8 board (albeit for an impractically large constant). Accordingly, we focus instead on the question for the generalized case of an n x n board. For the aforementioned strategy games, the corresponding question is known to be PSPACE-hard. That is, solving (n x n) chess, checkers, etc. is at least as complex as any computational task in PSPACE–the class of problems solvable by Turing machines using an amount of space (memory) that grows as a polynomial function of the input size n. We prove in this talk that the same is true for Arimaa. Thus Arimaa is about as computationally complex as these other (classic) games. We prove this result by reduction from the known PSPACE-hard problem Generalized Geography, adapting a technique of Storer’s in his 1983 paper originally showing the PSPACE-hardness of (n x n) chess.

(Joint work with A. Schipper.)

​Time: 15.30 – 17.00

According to Russell, a definite description is an expression of the form `The F’. They are incomplete symbols that mean nothing in isolation, and only in the context of complete sentences of the form `The F is G’, from which they disappear upon analysis. `The F is G’ is equivalent to `There is exactly one F and it is G’. For Russell, if there is no F, then any sentence of this form is false. Free logicians argue against Russell and that sometimes such sentences can be true. In free logic, definite descriptions are generally treated as genuine singular terms. But Russell surely had a point that we can draw distinctions of scope, for instance between `The F is not G’ and `It is not the case that the F is G’. This would require a means of introducing scope distinctions into the logic, which in free logic is generally not done. In my talk I will present a sequent calculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier I. I forms a formula from two formulas. Ix[F, G] means `The F is G’. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is proved for a system of classical positive free logic with I and it is shown to be sound and complete for the semantics. The system has a number of novel features and is briefly compared to the usual approach of formalising `the F’ by a term forming operator in free logic. It does not coincide with Hintikka’s and Lambert’s preferred theories, but the divergence is well-motivated and attractive. Viewed from the perspective of proof theoretic semantics, the systems lets us decide various questions concerning the logic of definite descriptions in a principled way.

​Time: 16.00 – 17.15

Mares and Goldblatt have introduced a general framework for providing frame-based semantics for which quantified relevant logics are complete (avoiding the incompleteness noted by Fine of these logics w.r.t. the simple `constant domain’ extensions of their usual frame-based semantics). In this talk, I’ll generalise and abstract away some of the frame-specific machinery of the Mares-Goldblatt framework in order to get a clearer idea of their algebraic structure. In so doing, I’ll consider issues relating to general completeness proofs for quantified extensions of logics complete w.r.t. certain classes of algebras (especially gaggles, following Dunn), mention some connections to related avenues of research in the model-theory of quantified non-classical logics, and suggest some potential applications of the resulting framework.

​Time: 16.00 – 17.15

Cut-elimination is a fundamental result of proof theory. It is the algorithm for eliminating cuts from a sequent calculus proof, leading to cut-free calculi and applications. Although the algorithm is remarkably robust in the sense that it applies with few amendments to many logics (irrespective of their semantics), it simply does not hold for most logics. Its importance is such that the invariable response is a move from the sequent calculus to richer proof formalisms in a bid to regain the cut-elimination. In this talk I will discuss the first steps in a radically different approach called cut-restriction: identifying how to adapt Gentzen’s age-old cut-elimination arguments to restrict the shape of the cut-formulas when elimination is not possible. I will present the “first level above cut-free”: restricting the standard sequent calculi for bi-intuitionistic logic and S5 to analytic cuts. These are two logics where (analytic) cuts are known to be essential.

This is joint work with Agata Ciabattoni (TU Wien) and Timo Lang (UCL).

​Time: 16.00 – 17.15

In Montague–Scott semantics, the modal box operator represents a property of sentential intensions, that is, propositions or sets of possible worlds. It follows that all logics modelled by this kind of semantics are intensional: if A and B necessarily express the same proposition, then so do Box A and Box B. This is obejctionable on many readings of Box, notorious examples being propositional attitudes. A more realistic formalization of such examples, it is argued, calls for hyperintensional modal logics, where Box A and Box are are not necessarily equivalent even for necessarily equivalent A and B.

Different semantic frameworks for hyperintensional modal logics have been formulated. In a recent paper (Hyperintensional logics for everyone. Synthese 198, 933-956, 2021), I have introduced a generalization of Montague–Scott semantics in which the Box operator expresses properties of “semantic contents” which in turn determine propositions in the standard sense. The nature of these contents is left undetermined, which renders the semantic framework rather general.

In the first part of the talk, I will outline the generalized Scott–Montague semantic framework and I will show that many well-known semantics for hyperintensional modalities are special cases. In the second part of the talk, I outline recent joint work with M. Pascucci in which we use the framework to give a semantics for some weak modal logics.

​Time: 16.00 – 17.15

In the 1980s, John Pollock’s work on defeasible reasons started the quest in the AI community for a formal system of defeasible argumentation. My goal in this talk is to present a logic of structured defeasible argumentation using the language of justification logic. One of the key features that is absent in standard justification logics is the possibility to weigh different epistemic reasons that might conflict with one another. To amend this, we develop a semantics for “defeaters”: conflicting reasons forming a basis to doubt the original conclusion or to believe an opposite statement. Formally, non-monotonicity of reasons is introduced through default rules with justification logic formulas.

Justification logic formulas are then interpreted as arguments and their acceptance semantics is given in analogy to Dung’s abstract argumentation framework semantics. In contrast to argumentation frameworks, determining arguments’ acceptance in default justification logic simply turns into finding (non-monotonic) logical consequences from a starting theory with justification assertions. We can show that a large subclass of Dung’s frameworks is a special case of default justification logic. By the end of the talk, I will briefly connect this logic with Pollock’s original motivation to deal with the justified-true-belief definition of knowledge.

In this TULiPS talk, I would like to provide a high-level overview of the work of my PhD under supervision of Rosalie Iemhoff and Nick Bezhanishvili. I am studying two topics in the field of proof theory: uniform interpolation and admissible rules. I apply both topics to (intuitionistic) modal logics.

The first is used to describe the form of proof systems in terms of so-called negative results: if a logic does not have uniform interpolation then it cannot have a sequent calculus with certain nice properties.  The aim of my research is to widen the scope to proof formalisms such as nested sequents. The second part is a study on the structure of logics. The admissible rules are those rules that you can add to a logic without changing its set of theorems. One of my main results is a characterization of the admissible rules of six interesting intuitionistic modal logics.

I present a “fully schematic”, proof-theoretic account of higher-order logic. The framework allows for the explicit definition of truth predicates for arbitrarily strong theories formulated in the framework. Thus, arguably, for any reasonable language, a truth predicate is explicitly definable with purely logical, proof-theoretic means. Enough “truth” should thus be available to the inferentialist to do the theoretical work that opponents claim is wanting. Furthermore, deflationists claim that the truth-predicate does not express a substantive property, but is only required to express generalizations (and such like). On the account presented here, truth-predicates are strictly purely logical, and indeed eliminable since they are logically definable. Deflationism appears to collapse into a redundancy theory of truth.

Responsibility for team plan failures and other events arising in the context of multi-agent interaction is an interesting concept to model formally. I will talk about previous joint work with Joseph Halpern and Brian Logan on modelling responsibility for failure of team plans in causal models, and an on-going work in progress on expressing the same notion in logics of strategic ability.

The framework of topic-sensitive intentional modal operators (TSIMs) described by Berto provides a general platform for representing agents’ intentional states of various kinds. For example, a TSIM can model doxastic states, capturing a notion that given the acceptance of antecedent information P, an agent will have a consequent belief Q. Notably, the truth conditions for TSIMs include a subject-matter filter so that the topic of the consequent Q must be “included” within that of the antecedent P. In practice, the types of intentional states modeled by TSIMs can be nested within one another–one can have beliefs about beliefs, one can imagine that one knows, etc. The device of the subject-matter filter, however, requires that modeling the semantics of such nested TSIMs requires an adequate account of the subject-matter of sentences in which a TSIM appears. In this talk, I will discuss extending earlier work on the subject-matter of intensional conditionals to the special case of TSIMs and argue that the account provided is adequate both formally and philosophically.

Recent works about ecumenical systems, where connectives from classical and intuitionistic logics can co-exist in peace, warmed the discussion of proof systems for combining logics, called Ecumenical systems by Prawitz and others.

In Prawitz’ system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation, and the constant for the absurd, but they would each have their own existential quantifier, disjunction, and implication, with different meanings.

We extended this discussion to alethic K-modalities: using Simpson’s meta-logical characterization, necessity is shown to be independent of the viewer, while possibility can be either intuitionistic or classical.

We furthermore proposed an internal and pure calculus for ecumenical modalities, where every basic object of the calculus can be read as a formula in the language of the ecumenical modal logic.

(joint work with Elaine Pimentel, Luiz Carlos Pereira, and Emerson Sales, partially published in the proceedings of Dali’20 and WoLLiC’21)

In this talk, we explore the universe of iterated information updates on a logical model. In particular, we show how iterated updates can be understood as a discrete time dynamic system.