APPLIED LOGIC SEMINAR

Cut elimination is a powerful tool of proof-theory, but sometimes we are faced with difficulties of finding a natural cut-free sequent systems even for standard logics, e.g. modal logic S5 and bi-intuitionistic logic. On the other hand, we can still find sequent systems for them with analytic cut property i.e., every sequent provable in the system has a proof in which every cut formula is a subformula of the lower sequent of cut rule. In such a case, the subformula property holds in them, and hence many useful logical property like Craig’s interpolation property can be derived.

In my talk, first we introduce a (frame) semantical framework for showing cut elimination and analytic cut property, following the idea by M. Takano. The method can be applied also for proving cut elimination of sequent systems for intuitionistic and modal predicate logics. Next, we try to establish a link of this semantical approach with existing algebraic approach to cut elimination, using quasi-embeddings of Gentzen structures into quasi-completions (by F. Belardinelli, P. Jipsen and HO, and also A. Ciabattoni, N. Galatos and K. Terui). This can be done by introducing the notion of semi-completeness of sequent systems, which came out of S. Maehara's paper of 1991. Thus, we can have a unified understanding of these two semantical approaches.

A logical approach to Bell's Inequalities of quantum mechanics has been introduced by Abramsky and Hardy. We point out that the logical Bell's Inequalities are provable in the probability logic of Fagin, Halpern and Megiddo. Since it is now considered empirically established, most notably quite recently in Delft, that quantum mechanics violates Bell's Inequalities, we introduce a modified probability logic, that we call quantum team logic, in which Bell's Inequalities are not provable, and prove a Completeness Theorem for this logic. For this end we generalise the team semantics of dependence logic first to probabilistic team semantics, and then to what we call quantum team semantics.

Markov Decision Processes (MDPs) provide a formal framework for modeling sequential decision making when outcomes are unsure. MDPs have been applied in various areas, including robotics, agriculture, and power system economics, as well as finance and investment theory. An MDP is a state-based system where, in every state, an agent makes a choice of action that results in a reward and a probabilistic transition to a next state. The special instance in which
there are no rewards and the agent has only one choice in each state is the well- known Markov chain. In an MDP, the objective of the agent is to make choices such that the expected total rewards, the long-term values, are maximized. We call a rule that in each state dictates the agent which choice to make in order to achieve such an “optimal outcome” an optimal policy. A remarkable result of the theory of Markov Decision Processes is that an optimal policy always exists. In this talk, we review the classical theory of MDPs including two algorithms to find optimal policies: Policy Iteration and Value Iteration. Finally, we also discuss how Markov Decision Processes could be aptly analyzed using coalgebraic methods.

Bisimulation relations are a well known semantic tool for investigating the expressiveness and other properties of modal languages. When a class of T-coalgebras serve as the semantics of a modal language, the coalgebraic theory provides us with generic semantic equivalence notions, namely coalgebraic bisimilarity and behavioural equivalence (both parametric in T), and the perspective is usually that of finding a modal language which is able to distinguish semantically inequivalent states. For certain applications, modal languages which are less expressive may nonetheless be of interest. Contingency logic (see e.g. Fan, Wang & Van Ditmarsch) is an example of such a weakly expressive language. The question is, what is a suitable notion of bisimilarity for such languages?

In this informal talk, I will give a general coalgebraic proposal to answer this question by introducing a notion called lambda-bisimulation which is tailored to fit the level of expressiveness of a modal language. This notion is parametric in the coalgebraic semantics (and thus implicitly also in the functor T). I will show some basic results and discuss its instantiation to contingency logic over Kripke models and neighbourhood models.

This is work in progress, joint with Zeinab Bakhtiari.

Semi-De Morgan algebras were introduced by H.P. Sankappanavar as a generalization of De Morgan algebras and distributive pseudo-complemented lattices. There are some literatures on properties of semi-De Morgan algebras from algebraic perspective. However, the proof-theoretic aspects of semi-De Morgan has not been well developed. In this talk, the display calculus for semi-De Morgan are established, which enjoy completeness, cut elimination, subformula property .The Glivenko theorem holds between De Morgan logic and semi-De Morgan logic. Compared with other different kinds of non-classical negations, we can see the position of semi-De Morgan logic in non-classical logic context clearly.
This is work in progress, joint with Giuseppe Greco and Alessandra Palmigiano

We develop algebraic semantics of refinement modal logic using duality theory. Refinement modal logic has been introduced by Bozzelli et al. A Refinement is like a bisimulation, except that from the three relational requirements only `atoms' and `back' have to be satisfied. We study the dual notion of refinement on algebras and present algebraic semantics of refinement modal logic. For this end, we have two main approaches: (1) we provide an algebraic semantics based on the semantics of arbitrary action model logic quantifier, (2) we introduce an algebraic model based on semantics of refinement quantifier in terms of refinement relation. Then we show our logic is sound and complete with respect to algebraic semantics.

A definition formulated correctly using necessary and sufficient conditions introduces new vocabulary via an interpretation in a familiar language. A recursive definition introduces the application of vocabulary to new objects in terms of previously understood applications to other, typically less complex, objects. A circular definition, such as the definition of truth that plagues our attempts to understand self-referential truth claims, may change the predicate that it defines. In this talk, I will reflect on a conception of definitions as dynamic operators. This includes the approach to relation-change dynamics introduced in [1] and studied algebraically in [2].

[1] P. Girard, J. Seligman and F. Liu. General dynamic dynamic logic. In S. Ghilardi T. Bolander and L. Moss, editors, Advances in Modal Logic, volume 9, pages 239–260. College Publications, 2012.
[2] M. Ma and J. Seligman. Algebraic semantics for dynamic dynamic logic. In W. van der Hoek, W. Holliday and W. Wang, editors, Logic and Rational Interaction (LORI 5), pages 255-267. Springer, 2015.

We present an epistemic logic for a notion of knowledge confirmed by a reliable source of information. Such notion of knowledge can be modelled as a diamond modality over a substructural logic. As the weakest propositional background logic we choose distributive non-associative full Lambek calculus with a negation and work with its relational semantics, interpreting the elements of a relational frame as information states consisting of collections of data which may be incomplete or even inconsistent. The principal epistemic relation between the states is the one of being a reliable source of information. From this point of view it is natural to define the epistemic operator existentially as a (backward-looking) diamond modality. The resulting knowledge modality satisfies axioms of factivity and consistency, admits a weak form of logical omniscience (the monotonicity rule for the modality), but avoids stronger ones (an analogue of necessitation rule and the K-axiom) as well as some closure properties discussed in normal epistemic logics (like the positive and negative introspection). For these properties we can provided characteristic frame conditions, so that they can be present in the system if they are considered to be appropriate for some specific epistemic context. The system is modular in the sense that the axiomatization sound and complete with respect to a wide class of background propositional logics, for the weakest system we can also prove decidability using a filtration method. The system can be extended with a reasonable belief modality in a similar manner, and we can provide a display style proof theory for the resulting logic.

The talk is based on a joint work with Ondrej Majer and on the previous paper:

M. Bilkova, O. Majer, M. Pelis, Epistemic logics for sceptical agents, JLC, online first March 2015.
http://logcom.oxfordjournals.org/content/early/2015/03/18/logcom.exv009.abstract
(preprint version available at: http://web.ff.cuni.cz/~bilkmaff/soubory/JA1_JLC2014.pdf )

There are two standard model-theoretic methods for proving the finite model property for modal and intermediate logics, the standard filtration and selective filtration. The standard filtration for modal and intuitionistic logics was first defined algebraically by McKinsey and Tarski in the 1940’s. In the 1960’s Lemon and Segerberg defined filtrations model theoretically. Selective filtrations were introduced by Gabbay and further developed by Fine and Zakharyaschev (1970’s and 1980’s).

In this talk I will give an algebraic description of filtrations in intuitionistic logic via locally finite reducts of Heyting algebras. In particular, I will show that the algebraic description of the standard filtration is based on the implication-free reduct of Heyting algebras, while that of selective filtration on the disjunction-free reduct. In order to define standard filtrations algebraically we will need to work with free Boolean extensions of distributive lattices. This will enable us to define the least and greatest filtrations algebraically. I will conclude by mentioning several consequences of this approach for intermediate and modal logics.

(Joint work with Vassili Vergopoulos of the Paris School of Economics)
Individuals and societies must often make difficult decisions, which are fraught with uncertainty. How should an agent decide when faced with such uncertainty? This is the subject of a branch of theoretical economics called Decision Theory.
Bernoulli (1738) claimed that we should choose the alternative which yields the highest expected utility. But what justifies this methodology? Savage (1954) showed that, if our decision-making process satisfies certain axioms (encoding basic properties of "consistency" and "rationality"), then it must maximize expected utility. Savage's Theorem is considered the foundational result of modern Decision Theory.
Savage posited a set S of possible "states of nature" and a set X of possible "outcomes". He supposed that each alternative defined a function (an "act") mapping states to outcomes. His theorem constructs a probability measure on S and a utility function on X. However, this approach raises at least three issues.
1. Savage assumed that S and X were arbitrary sets, and acts were arbitrary functions. But what if S and X are topological spaces, and acts must be continuous? What if S and X are differentiable manifolds, and acts must be differentiable? We would like a single theory which works in all of these environments (and others).
2. In many applications, it is unrealistic to suppose that we can enumerate all possible states of nature or all possible outcomes "in advance". Thus, there is growing interest in developing decision theory without an explicit specification of S or X.
3. At different times, the same agent might be faced with many different sources of uncertainty (i.e. different instances of S) and many different menus of outcomes (different instances of X), in different combinations. We would like a single holistic description of the agent's decisions over all of these possible decision problems.
In this talk, we will reformulate decision theory using the tools of category theory, and derive a version of Savage's theorem which addresses all three of these issues.

This talk proposes a new topic in substructural logic joining the fields of relevance and fuzzy logics. We first introduce fuzzy systems satisfying an old relevance principle, i.e., Dunn’s weak relevance principle. We present ways to obtain relevant companions of the weakening-free uninorm (based) systems introduced by Metcalfe and Montagna and fuzzy companions of the system R of relevant implication (without distributivity) and its neighbors. The algebraic structures corresponding to the systems are then defined, and completeness results are provided. We next consider fuzzy systems satisfying new relevance principles introduced by Yang. We show that the weakening-free uninorm (based) systems and some extensions and neighbors of R satisfy the new relevance principles.

Social choice theory studies mathematically the processes involved when groups of people make choices. There are a number of beautiful and astonishing qualitative results in this area, for example Arrow’s Theorem about the non-existence of ideal voting schemes, and the Gibbard-Satterthwaite Theorem about the manipulation of elections. These classical theorems have had tremendous impact on the field of social choice. More recently, a sequence of stronger, quantitative versions of such theorems, by Gil Kalai, Ehud Friedgut, Elchanan Mossel et al., has entered into the picture. These results depend on the theory of Fourier analysis on the Boolean cube. In this talk, we will review some of these results and techniques, and put them in a broader context. Some questions we will address include: What are the implications of the aforementioned results for real-life applications? How grievous is Arrow’s Theorem really, and how should we cope with it? Finally, we will look at possible future research. Inspired by Daniel Kahneman’s work on cognitive biases, we introduce a new and simple model to simulate the various biases that manifest themselves in small meetings involving sequential voting.

The Logic of Epistemic Actions and Knowledge is an expansion of classical modal logic introduced by A. Baltag, L. S. Moss and S. Solecki as a framework for reasoning about knowledge in a dynamic logic setting. A. Kurz and A. Palmigiano recently showed that duality theory provides a flexible framework for modelling epistemic changes, which allows one to develop dynamic epistemic logics on a propositional basis that is weaker than classical logic (e.g. an intuitionistic basis).
In this talk we explain how the techniques of Kurz and Palmigiano can be further extended to define and axiomatize a bilattice-based Logic of Epistemic Actions and Knowledge. Our propositional basis is a modal expansion of the well-known four-valued logic of Belnap and Dunn, which is a system designed for handling inconsistent as well as potentially conflicting information. These features, we believe, make our framework particularly promising from a computer science perspective.

In the literature, different axiomatizations of Public Announcement Logic (PAL) have been proposed. Most of these axiomatizations share a "core set" of the so-called "reduction axioms". In this paper, by designing non-standard Kripke semantics for the language of PAL, we show that the proof system based on this core set of axioms does not completely axiomatize PAL without additional axioms and rules. In fact, many of the intuitive axioms and rules we took for granted could not be derived from the core set. Moreover, we also propose and advocate an alternative yet meaningful axiomatization of PAL without the reduction axioms. The completeness is proved directly by a detour method using the canonical model where announcements are treated as merely labels for modalities as in normal modal logics. This new axiomatization and its completeness proof may sharpen our understanding of PAL and can be adapted to other dynamic epistemic logics.

Realizability is about interpreting logical statements with programs. A statement is realizable if we can argue for it following some programs. In this talk, we discuss a variant of realizability on typed arithmetic: it has extensional equality, and to interprete an implication, a realizing program need to be total with respect to the antecedent's type. As a formal theory, much of this realizability is known using proof-theoretic methods, and the canonical model for it is well-known. However, it is still not clear what kind of category should this logic correspond to. Towards the problem, we propose a categorical construction with good properties. It is hoped that the categories obtained by the construction could serve as concrete solutions to the problem.

The modern era in social choice theory started with Ken Arrow's ground-breaking impossibility theorem. Arrow showed that there is no preference aggregation method satisfying a minimal set of desirable properties. Social choice theory has since grown into a large and multi-faceted research area. In this talk, I focus on one type of theorem studied by social choice theorists: axiomatic characterizations of preference aggregation methods. The principles studied by social choice theorists are intended to identify procedures that ensure that every group decision depends *in the right way* on the voters' inputs. I will show how to formalize these theorems using Jouko Vaananen's dependence and independence logic. This is not merely an exercise in applying a logical framework to a new area. I will argue that dependence and independence logic offers an interesting new perspective on axiomatic characterizations of group decision methods.

Dependence logic is a new logical formalism that characterizes the notion of "dependence" and "independence" in social and natural sciences. First-order dependence logic was introduced by Väänänen (2007) as a development of Henkin quantifier (Henkin, 1961) and independence-friendly logic (Hintikka and Sandu, 1989). Recently, propositional dependence logic was studied and axiomatized in (Yang and Väänänen, 2015). It turned out that a natural variant of propositional dependence logic, called propositional intuitionistic dependence logic, is essentially equivalent to inquisitive logic, introduced by Ciardelli and Roelofsen (2011) with a different motivation.
In the first part of the talk, we will give a brief introduction to this multidisciplinary new field. Then, we will prove that propositional dependence logic and some of its variants (including inquisitive logic) are structurally complete with respect to a class of substitutions under which the logics are closed, that is, all admissible rules of these logics are derivable in their deductive systems. (This part of the talk is based on a joint work with Rosalie Iemhoff.) Finally, we will point out some interesting directions for future research.

References:
[Ciardelli and Roelofsen, 2011] I. Ciardelli and F. Roelofsen, Inquisitive Logic, Journal of Philosophical Logic, vol. 40, no. 1, pp. 55-94, 2011.
[Henkin, 1961] L. Henkin, Some remarks on infinitely long formulas, Infinitistic Methods, Proceedings Symposium Foundations of Mathematics, pp 167-183, 1961
[Hintikka and Sandu 1989] J. Hintikka and G. Sandu, Informational Independence as a Semantical Phenomenon, Logic, Methodology and Philosophy of Science, Amsterdam: Elsevier, pp. 571-589, 1989
[Väänänen 2007] J. Väänänen, Dependence Logic: A New Approach to Independence Friendly Logic, Cambridge: Cambridge University Press, 2007
[Yang and Väänänen, 2015] F. Yang and J. Väänänen, Propositional Logics of Dependence and Independence, Part I, submitted, preprint available at: http://arxiv.org/abs/1412.7998.

In this talk I will give an outline of the decision making process regarding the rebuilding of Utrecht Central Station and introduce the role logic could play in this process. ProRail, the Dutch railway infrastructure manager, has set a goal to increase the capacity of the infrastructure with 50% by 2020 as a challenge. To achieve this goal the flow-through station Utrecht has to be optimized. Therefore, the project DSSU (DoorStroomStation Utrecht; flow-through station Utrecht) was launched. I will discuss crucial points in the DSSU decision making process, such as the change of vision on railways, decreasing flexibility and safety issues. The aim of this talk, after explaining the real-world case, is to discuss together with the audience about how, which and where logic can contribute to this decision making process.

(Joint work with Guram Bezhanishvili, Nick Bezhanishvili, and Yde Venema)
We introduce the concept of a subordination, which is dual to the well-known concept of a precontact on a Boolean algebra. We develop a full categorical duality between Boolean algebras with a subordination and Stone spaces with a closed relation.
We introduce the concept of an irreducible equivalence relation, and that of a Gleason space, which is a pair (X, R), where X is an extremely disconnected compact Hausdorff space and R is an irreducible equivalence relation on X. We prove that the category of Gleason spaces is equivalent to the category of compact Hausdorff spaces, and is dually equivalent to the category of de Vries algebras, thus providing a “modal-like” alternative to de Vries duality.

Technology for supporting people in their daily lives such as personal assistant agents and smart homes carry great potential for making our lives more connected, healthy, efficient and safe by executing tasks on our behalf and guiding our actions. I make two key observations: 1) supportive technology is inherently social in the sense that its support to a user is subject to norms from people in the user's social context (e.g., family members and caregivers), and 2) existing supportive technology is rigid in its realization of this social nature by hardwiring norms into the technology. This rigidity leads to violation of unsupported norms and inflexibility in dealing with violation of supported norms.
I argue that supportive technology should be able to adapt to diverse and evolving norms of people in unforeseen circumstances, in order to better support people in their daily lives. I conceptualize this vision by proposing the novel concept of a Socially Adaptive Electronic Partner (SAEP), and outline computational reasoning, interaction, and ethical challenges that need to be addressed to realize the creation of SAEPs.

Analysis of theoretical accounts of privacy suggests that 'privacy' should be treated as a degree concept rather than as a crisp one. Proposed conceptualisation of privacy in epistemic terms allows for identification of several dimensions of gradability and vagueness. Potential drawback of such approach is a certain apprehension that vagueness can be harmful for the explanatory value of the concept. I will argue that it is not an insurmountable issue.

In this survey we present various recent work proposing adjustments to the standard notion of bisimulation in order to have proper structural correspondents with epistemic, or epistemically motivated, modalities: contingency bisimulation, awareness bisimulation, plausibility bisimulation, refinement, and bisimulation for sabotage.

(Joint work with Yde Venema)
Many people believe it to be an open question whether Propositional Dynamic Logic has Craig Interpolation. At least three proofs have been attempted and two of them published but all of them have also been claimed to be wrong, both more or less publicly. This talk will first make the question precise and then shortly discuss its strange and unfortunate history. We will then recover a proof originally presented in a conference paper by Daniel Leivant (1981). The main idea and method here is still the same: Using the small model property we obtain a finitely sequent calculus for PDL. Furthermore, in proofs of star-formulas we find a repetitive pattern that allows us to construct interpolants. Our new presentation fixes many details and uses new results to simplify and clarify the proof. In particular we defend the argument against a criticism expressed by Marcus Kracht (1999), to show that the method indeed does not only apply to finitary variants of PDL but covers the whole logic.

(joint work undergoing with the Applied Logic group at TU Delft)
A logic L has the disjunction property (DP), if for every formula A OR B, if A OR B is provable in L, then A is provable in L, or B is provable in L.
The disjunction property for intermediate logics has been well studied in the literature. In this talk, firstly, I will introduce a class of propositional logics that are defined via Kripke semantics. I call them "normal propositional logics".
The minimal normal propositional logic F, the Hilbert system of which is sound and complete w.r.t the class of all frames, was first presented in [Corsi 1987], and later studied in [Dosen 1993]. It is embedded into the minimal normal modal logic K. The algebras for F, namely, weakly Heyting algebras, was studied in [Celani & Jansana 2001]. A normal propositional logic is a set of formulas that contains F and is closed under rules of MP, AF, AD and US.

For normal propositional logics, we present a purely syntactical characterization of the disjunction property via Kleene slash, which is a notion defined inductively on formulas. Actually, both a semantic characterization of DP, and an algebraic characterization of DP can be given for normal propositional logic.
The Kleene slash can also be used to give a syntactical characterization of DP in substructural logics. [Horcik & Teuri 2011] provided a syntax that can be used to generate substructural logics based on FL which have the DP. Our
Kleene slash can be used to prove it. We extend that syntax to normal propositional logics and prove the DP via the Kleene slash.

Alan Ross Anderson was interested in eubouliatic logic, the logic of prudence and related concepts, such as safety and risk. He ob- served that these concepts can be illustrated by means of a square of opposition. However, safety and risk are nowadays often seen as fuzzy concepts. We investigate which consequences this has for eubouliatic logic and for the corresponding square of opposition.

We present a new structural characterization of the expressive power of the acyclic conjunctive queries in terms of guarded simulations, and give a finite preservation theorem for the guarded simulation invariant fragment of first order logic.
We discuss the relevance of these results as a formal basis for constructing so-called guarded structural indexes. Structural indexes were first proposed in the context of semi-structured query languages and later successfully applied as an XML indexation mechanism for XPath-like queries on trees and graphs. Guarded structural indexes provide a generalization of structural indexes from graph databases to relational databases.

In this talk we present a different approach to the dual adjunction between MV-algebras and Tychonoff spaces presented by Marra and Spada, bringing their result closer to the natural duality framework. Our first observation is that the adjunction can be obtained independently of the presentation. We also present a geometric description of the duals of homomorphisms.
Using this duality we ask the questions: Can we represent modal operators on semisimple MV-algebras? Are relations the dual of modal operators?

How should we update a probability distribution when given new information? The standard answer is: "conditioning", but this is not always correct: as shown by examples such as the three prisoners problem, the Monty Hall (three cars, quizmaster) problem and the two-children puzzle, at least when applied in the common "naive" form, conditioning often gives the wrong answers. We give a detailed explanation of this phenomenon and show that a criterion known as CAR (`coarsening at random') in the statistical literature characterizes when "naive" conditioning works. We also show that in many situations, CAR essentially*cannot* hold, so that naive conditioning must give the wrong answer. We provide a radical solution: in a coherent approach to updating, updating on events taken from certain sets should simply not be allowed. We might call such sets 'unconditionable'. This is analogous to the idea of an 'unmeasurable' set, which is of course broadly accepted.

(Joint work with Hector Levesque)
Reasoning about degrees of belief in uncertain dynamical worlds is fundamental to many applications, such as robotics and planning, where actions modify state properties and sensors provide measurements, both of which are prone to noise. With the exception of limited cases such as Gaussian processes over linear phenomena, belief state evolution can be complex and hard to reason with in a general way. Be that as it may, different applications necessitate different kinds of specifications: some are instantiated in partially observable settings, some require both continuous and discrete properties, and most significantly, many involve incomplete specifications and non-trivial actions.

This talk presents our recent results to address representational and reasoning concerns on this front. On the representation side, it develops a general framework to combine logic, actions and probability. On the reasoning side, we show how goal regression can be generalized to noisy effectors and sensors over degrees of belief. More recently, we have also shown how progression can be generalized along the same lines, thereby relating database progression (as in Lin and Reiter) and stochastic filtering mechanisms, such as Kalman filtering. We also discuss how this led to the development of a new planning/representation language and system called PREGO.

(joint work with Alexandru Baltag and Sonia Smets)
In this talk, I will introduce a framework to model belief revision in social networks. Agent’s own judgment towards evidence for her beliefs, as well as how much trust she has towards other agents will be taken into account.

(joint work with Szabolcs Mikulas (University of London) and Jan Hidders (TU Delft))
We study an interpretation of lattice connectives as natural join and inner union between database relations with non-uniform headers. We show that this interpretation proposed by database experts (Vadim Tropashko from Oracle) yields a class of lattices which has not been considered in the existing lattice-theoretical literature. We discuss axiomatizability and decidability of their (quasi-)equational theory and propose an equational axiomatization for a corresponding abstract algebraic class. It turns out that addition of just the “header constant” to the lattice signature already allows mimicking the Maddux technique for cylindric algebras and encode the word problem for semigroups in the quasiequational theory. Relational lattices, however, are not as intangible as one may fear: for example, they do form a pseudoelementary class. We also apply the tools of Formal Concept Analysis and investigate standard contexts of relational lattices, obtaining, e.g., results on their subdirect irreducibility.

In his discussion of the deontic fragments of certain alethic modal systems, Lennart Aqvist wrote that "proof-theoretical methods seem to be less natural here". I disagree. I show that some results in this area can easily be obtained by proof-theoretical methods. The proofs are at least as "natural" as Aqvist's proofs.

Real Option Analysis (ROA) is a methodology for decision-making under uncertainty, successfully applied by private firms and public authorities in natural resource exploration, market entry, development of new technologies, infrastructure-planning. In this seminar we will present a logical approach to ROA framed into the formal setting of Lukasiewicz logic.

The Bayesian decision theory is very simple in structure. Its algorithmic steps are the following:
(1) Use the product and sum rules of Bayesian probability theory to construct outcome probability distributions.
(2) If our outcomes are monetary in nature, then by way of the Bernoulli law we may map utilities to the monetary outcomes of our outcome probability distributions.
(3) Maximize either the lower or upper bounds, depending on the specific context of the problem of choice we are studying, of the resulting utility probability distributions.

In this talk we continue the work by List, Herzberg and others on propositional-attitude aggregation theory, a generalized unification of the judgement aggregation and probabilistic opinion-pooling literatures.
We show how Abstract Algebraic Logic can contribute to broader the framework of such theory, characterizing systematic propositional-attitude aggregators as homomorphisms. We show that for any fregean logic whose algebraic counterpart is closed under direct products, any algebra in its algebraic counterpart can be taken as the set of truth values on which an aggregation problem can be formulated. By that means, aggregation of intuitionistic, fuzzy or relevance propositional attitudes could be studied as particular cases. Moreover, Arrow’s theorem for judgement aggregation as well as McConway’s characterization of linear opinion pools also follow straightforwardly from the general theory.

The main goal of the thesis is to isolate the technique of pulling back combinatorial properties (for example ultrafilters) from the models that satisfy the Axiom of Determinacy to get embedding properties (elementary embeddings) in inner models that satisfy the Axiom of Choice. This technique is not new; it is the backbone of Woodin’s theorem and has been used by other authors. However, the technique has never been presented in isolation, independent of a particular application. By focusing on large cardinal properties that are much weaker than Woodinness, we manage to present the technique in its purest form, allowing for easily accessible proofs.

We identify the universal n-model of the negation-free fragment of the intuitionistic propositional calculus IPC. We denote it by U*(n) and show that it is isomorphic to a generated submodel of the universal n-model of IPC, which is denoted by U(n). We show that this close resemblance makes U*(n) mirror many properties of U(n). Finally, using U*(n), we give an alternative proof of Jankov's Theorem that the intermediate logic KC, the logic of the weak excluded middle, is the greatest intermediate logic extending IPC that proves exactly the same negation-free formulas as IPC.

This talk aims at investigating the role played by relational structures in the study of quantum logic. It will start with some background from quantum physics. Then a brief survey will follow about the traditional lattice-theoretic approach to quantum logic started by Birkhoff and von Neumann (1936). After this, we will proceed to the perspective from relational structures on quantum logic. Various relational structures will be discussed about, including orthoframes and orthomodular frames in Goldblatt (1974), state spaces in Moore (1995) and quantum dynamic frames in Baltag and Smets (2005). Their significance will be manifested by several representation theorems for different lattices in quantum logic. Then I will introduce a kind of relational structures called quantum Kripke frames proposed by myself. I will present the definition and explain how they relate to other structures in the study of quantum logic. The talk will end with some directions for future work, including axiomatization of quantum Kripke frames and probabilistic quantum Kripke frames.
No knowledge about quantum physics and its mathematical formalism is assumed, but familiarity with some basic notions from linear algebra will be helpful.

References
• Baltag, A. and Smets, S. (2005). Complete Axiomatizations for Quantum Actions. International Journal of Theoretical Physics, 44(12):2267-2282.
• Birkhoff, G. and von Neumann, J. (1936). The Logic of Quantum Mechanics. The Annals of Mathematics, 37:823-843.
• Goldblatt, R. (1974). Semantic Analysis of Orthologic. Journal of Philosophical Logic, 3:19-35.
• Moore, D. (1995). Categories of Representations of Physical Systems. Helv Phys Acta, 68:658-678.

Conditional logic can be seen as a formal account of non-monotonic reasoning. The purpose of this talk is to give an overview of some existing proof systems and semantics for conditional logic. We focus on those parts of the theory which we deem relevant for the problem of developing a satisfactory proof theory for non-monotonic reasoning.

We begin by presenting the Hilbert calculus of conditional logic and a more natural inference system that has been proposed in the non-monotonic reasoning literature. We then introduce the two most common semantics, one based on preorders and the other on selection functions, and explain their applications. Moreover, we outline further approaches to the semantics of conditional logic which we have been working on recently. These include a topological semantics via closure operators and a game theoretic semantics. Finally we discuss the open problem of giving a proof theory for non-monotonic reasoning in which the turnstile is non-monotonic.

This talk presents a dynamic logic approach towards modelling agency, in particular the change that learning and accepting a norm trigger in agent’s actions and intentions. Current works on the logic of agency fall within two different groups: stit-frameworks which adopt a so-called “external perspective” (e.g., Belnap and Horty 1995, Horty 2001) and represent agency in terms of possible outcomes of actions, and a variety of frameworks (e.g., Veltman 2012) which instead endorse an “internal perspective” and give the priority to agent’s intentions. The latter provide a limited account of the way intentions can be realized, while the former completely ignore the role of intentions as drives for action. We argue that both perspectives need to be taken into account, especially when dealing with the constraints triggered by a norm. We provide a dynamic modal logic which represents both agent’s intentions (in terms of to-do-lists) and agent’s actions (through a tree-like temporal structure). The acceptance of a norm triggers a change in the agent’s intentions in such a way that the agent now intends to bring about what the norm prescribes. Consequently, it affects also agent’s actions by restricting the set of admissible actions to the ones which permit her to fulfill the norm.

Discrete-event simulation is used on a large scale to model complex systems, and many commercial simulation packages exist to construct discrete-event simulation models and experiment with them. Few users of these simulation packages and simulation models realize that simulation is deeply rooted in systems theory, and that a good understanding of systems theory is necessary to conduct proper discrete-event simulation studies. The talk will address the following topics: Systems Thinking and Modeling, System Conceptual Frameworks, Simulation Conceptual Framework, Discrete-event Simulation, DEVS, and will conclude with a discussion.

Dichotomous inquisitive semantics generalizes propositional logic to a richer semantic setting where standard declarative sentences and interrogative sentences may be given a uniform interpretation. In this talk, I will discuss how this framework gives rise to an interesting combined notion of logical consequence that unifies standard declarative entailment, answerhood, and interrogative dependencies. I will present a sound and complete deduction system for this logic, and I will show that proofs in this system have a specific kind of constructive content.

In classical algebraic geometry, one studies the solutions sets over an algebraically closed field K of systems of equations between polynomials in n variables with coefficients in K. In fact, there is a (contravariant) Galois connection between subsets of K^n and of the polynomial ring K[x_1,...,k_n]. The first aim of this talk is to show how the above generalises to any equationally definable class of algebras. Further, we will show that the classical Galois connection just described can always be made functorial, and thus lifted to a dual adjunction between the category of "affine sets" with their "polynomially definable" maps, and the category defined by the objects in the variety and their homomorphisms. This general adjunction, together with its induced duality between the full subcategories on the fixed objects, provides a link between Birkhoff's subdirect representation theorem, Hilbert's Nullstellensatz and topological dualities in the style of Marshall Stone for varieties of algebras. We show how several dualities of this sort, such as Stone duality for Boolean algebras, Priestley duality for distributive lattices, Gelfand duality for real C*-algebras, Pontryagin duality for locally compact abelian groups can be perfectly framed in this picture. Finally, we perform the last step in the abstraction and land in a general categorical framework which encompasses an even larger number of dualities, being able to give an account of, e.g., Galois theory of field extensions and the adjoint connection between subgroups of the fundamental group of a path-connected and semi-locally simply connected topological space and its path-connected covering spaces.

Working with intuitionistic mathematics as it is meant by Brouwer means accepting different results than one would get by looking to problems classically. We study the most crucial intuitionistic axiom: Brouwer's Principle of Continuity.
Descriptive Set Theory is the study of Borel-sets, which come with classes \Sigma^0_1, \Pi^0_1, etc. It is a field that suits for being an application of intuitionistic mathematics. We will see what could happen when intuitionists think about the classes \Sigma^0_n, \Pi^0_n.

The admissible rules of a logic are those rules under which the set of the logics’s theorems are closed. In the case of classical propositional logic all admissible rules are derivable, that is to say, they correspond to theorems of the logic. In intuitionistic logic, and in many of its extensions, the situation is far more interesting.
In this talk we present some of the machinery to describe admissible rules. We apply this to give a description of the admissible rules of the intermediate logic complete with respect to frames of height at most two, also known as BD2.

Belief revision is the transformation of the beliefs of an agent when new information comes in. The mechanism belief revision is not trivial, and there are many problems encountered. For example, the agent might have different degrees of beliefs, the new information might have different degrees of reliability, and the agent's deduction ability varies, etc. Hence, what constitutes a valid belief revision become a central question in the research of belief revision. In this talk, we briefly introduce three approaches, namely functional approach, relational approach and B-structure approach, and compare their differences.
References
• Lindsey Craig Jefta, "A Topological Framework for Modelling Belief Revision" (PhD thesis).

In this talk I will deal with the problem of identity of proofs. In the first part I will focus on natural deduction and sequent systems for intuitionistic (propositional) logic, con- sidering the well-known identity criterion of proof normalization. Naively, according to this criterion, two (natural deduction/sequent calculus) proofs should be identified if they have the same normal form. Such a criterion perfectly fits the intuitionistic setting as can be seen on the structural level of proofs as syntactic objects, as well as on the computational (via the Curry-Howard Isomorphism) and categorial (via the Lambek Isomorphism) level.
A similar criterion is not available in the setting of classical logic. Moreover, the absence of good syntactic formalisms makes the problem of identifying two proofs not trivial at all. I will give an overview on alternative calculi specifically designed for achieving better proofs’ representations in the setting of linear logic, such as proof-nets and deep inference systems.
I will conclude by presenting and discussing some recent proposals about syntactical representations of classical proofs.

(joint work with David R. Gilbert)
I will present sequent calculi for several classical modal logics. Utilizing a polymodal translation of the standard modal language, I will establish a base system for the minimal classical modal logic from which I generate extensions in a modular, and uniform, manner. I also briefly suggest potential applications to epistemic logic.

We employ algebraic semantics and topological duality to set up a Kripke semantics for a modal expansion of Arieli and Avron’s bilattice logic, itself based on Belnap’s four-valued logic. We obtain soundness and completeness of a Hilbert-style derivation system for this logic with respect to four-valued Kripke frames, the standard notion of model in this setting. Both local and global consequence on the models are covered.

Two complementary conceptualizations of uncertainty will be discussed: fuzzy and statistical uncertainty. These uncertainties can be combined into one theory on probabilistic fuzzy events. Using this theory, classical fuzzy systems can be generalized to probabilistic fuzzy systems (PFS). PFS can be induced using both expert knowledge and data enabling both interpretability and accuracy (despite the fact there remains an accuracy-interpretability dilemma we have to deal with in practice). To finalize, one or two examples of PFSs we developed will be shown.

Display calculi enjoy a modular Belnap’s cut elimination procedure that is verified by checking a minimal set of conditions. When a multi-type environment is introduced these conditions change. In the talk, the multi-type display calculus for Baltag-Moss-Solecki’s logic of epistemic actions and knowledge will be presented, with the goal of discussing the changes in the conditions that guarantee cut elimination in this new setting.

Monotone modal logic is a weaker version of normal modal logic, where modalities are monotone but do not distribute over either joins or meets.
In this talk I will explain why the proof theory for these logics is still unsatisfactory and I will argue that a display-style calculus for monotone modal logic would be adequate.
I will show that a naive design for such a calculus runs into technical difficulties.
Finally I will present a generalization of display calculi that does not automatically force modal operators to be adjoints, and I will explain why it can be considered adequate from a proof-theoretical perspective.

This talk concerns the relationship between probabilistic (Bayesian) and qualitative (AGM-based) models of belief dynamics. I address the question of how AGM belief revision operators can be related to Bayesian conditioning, in order to flesh out some (in)compatibilities between the Bayesian and AGM-based formalisms.
This is done by analysing the behaviour of acceptance rules, which map probabilistic credal states to qualitative representations of belief. Given an acceptance rule, the ideal of compatibility between Bayesian conditioning and qualitative revision is embodied by the tracking property, which imposes a commutativity requirement to ensure that conditioning and revision agree modulo the acceptance map.
I focus on an acceptance rule based on the notion of stably high probability, due to Leitgeb. As a consequence of a 'No-Go' theorem by Lin & Kelly, Leitgeb's rule does not allow AGM revision to track conditioning. Nonetheless, given this rule's inherent attractiveness as an acceptance principle and its close connection to AGM revision, I consider some ways in which one may circumvent the No-Go Theorem and use the rule so as to approximate agreement between AGM and Bayesian conditioning.
I show that one rather natural such method – threshold-raising – fails, which poses some difficulties for the 'peace project' between Bayesian and AGM-compliant operators. However, another interesting connection exists: I show that there is a sense in which AGM revision derives from (1) Leitgeb's rule, (2) Bayesian conditioning, and (3) a version of the maximum entropy principle. This suggests that one could study qualitative revision operators as special cases of Bayesian reasoning which naturally arise in situations of information loss or incomplete probabilistic information.

The theory of partial combinatory algebras can be regarded as a generalization of both recursion theory and the theory of realizability. Partial combinatory algebras give rise to structures called realizability toposes, the archetype of which is the effective topos. The combination of the geometrical nature of a topos and the computational character of a partial combinatory algebra yields an interesting theory in which a lot is still to discover. In my talk, I will treat both sides, and discuss some results of my thesis that, for example, point out the role of generalized relative recursion in this study.

A calculus of circular proofs was introduced for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called µ-bicomplete categories).
In this talk we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free µ-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.