Invited Talks
Mike Prest
Model Theory for Sheaves of Modules

We describe how the model theory of modules is adapted to deal with sheaves of modules.

Martin Lange
Specifying Program Properties Using Modal Fixpoint Logics: A Survey of Results

The modal μ-calculus is a well-known program specification language with desirable properties like decidability of satisfiability and model checking, axiomatisability etc. Its expressive power is limited by Monadic Second-Order Logic or parity tree automata. Hence, it can only express regular properties.

In this talk I will argue in favour of specification languages whose expressiveness reaches beyond regularity. I will present Viswanathan and Viswanathan's Higher-Order Fixpoint Logic as a natural extension of the modal μ-calculus with highly increased expressive power. We will see how this logic can be used to specify some interesting non-regular properties and then survey results on it with a focus on open questions in this area.

Ian Pratt-Hartmann
Transitivity and Equivalence in Decidable Fragments of First-Order Logic: a Survey

In this talk, I survey recent work on extensions of various well-known decidable fragments of first-order logic, in which certain distinguished predicates are required to denote transitive relations or equivalence relations. I explain the origins of this work in modal logic, and outline the current state-of-the-art.

Carolin Antos
Multiverse conceptions reconsidered

Since the introduction of the forcing technique in the 1960's, set theory has changed profoundly in its methodology as well as in its defining results. In the philosophy of set theory this change has led to the introduction of so-called multiverse conceptions, as in programs like the "Hyperuniverse program" by S. Friedman or the "Multiverse program" by J. Hamkins. Although these programs are all based on the idea of an underlying multiverse approach they differ in their technical set-up as well as their philosophical research agenda.

In the present talk I want to argue that the latter difference is heavily influenced by the former. I will reconsider the two programs mentioned above and show that already by choosing one's technical background approach one influences the philosophical outcome of one's position. By considering different forcing approaches (like the countable transitive model approach or the Boolean valued model approach) and forcing types (like higher-order forcings), and I will show how they are used in the above-mentioned programs and what role they play in bringing about the philosophical conclusions of these programs. In the end I will argue that forcing is a multifaceted technique and because choosing one's technical foundation is a philosophical, not just a mathematical step in one's philosophical argument, this choice cannot be left to considerations of mathematical expedience only. Rather, it has to become part of the philosophical discussion itself.

Contributed Talks
Anantha Padmanabha and R. Ramanujam
Propositional modal logic with implicit modal quantification

Propositional term modal logic is interpreted over Kripke structures with unboundedly many accessibility relations and hence the syntax admits variables indexing modalities and quantification over them. This logic is undecidable, and we consider a variable-free propositional bi-modal logic with implicit quantification. Thus [∀]α asserts necessity over all accessibility relations and [∃]α is classical necessity over some accessibility relation. The logic is associated with a natural bisimulation relation over models and we show that the logic is exactly the bisimulation invariant fragment of a two sorted first order logic. The logic is easily seen to be decidable and admits a complete axiomatization of valid formulas. Moreover the decision procedure extends naturally to the 'bundled fragment' of full term modal logic.

Rafal Urbaniak and Michal Tomasz Godziszewski
Modal Quantifiers, Potential Infinity, and Yablo sequences

When properly arithmetized, Yablo's paradox results in a set of formulas which (with local disquotation in the background) turns out consistent, but ω-inconsistent. Adding either uniform disquotation or the ω-rule results in inconsistency. Since the paradox involves an infinite sequence of sentences, one might think that it doesn't arise in finitary contexts. We study whether it does. It turns out that the issue turns on how the finitistic approach is formalized. On one of them, proposed by M. Mostowski, all paradoxical sentences simply fail to hold. This happens at a price: the underlying finitistic arithmetic itself is ω-inconsistent. Finally, when studied in the context of a finitistic approach which preserves the truth of standard arithmetic (developed by AUTHOR), the paradox strikes back - it does so with double force, for now inconsistency can be obtained without the use of uniform disquotation or the ω-rule.

Zhe Lin and Mihir Chakraborty
Finite embeddability property of tqBa5

In this paper we study the basic algebraic structure of Rough algebras tqBa5. We consider a important property for a class of algebras in universal algebra called the finite embeddability property (FEP). And we prove that the class of tqBa5 has FEP

Tim French, Andrew Gozzard and Mark Reynolds
A modal aleatoric calculus for probabilistic reasoning

We consider multi-agent systems where agents actions and beliefs are determined aleatorically, or "by the throw of dice". This system consists of possible worlds that assign distributions to independent random variables, and agents who assign probabilities to these possible worlds. We present a novel syntax and semantics for such system, and show that they generalise Modal Logic. We also give a sound and complete calculus for reasoning in the base semantics, and a sound calculus for the full modal semantics, that we conjecture to be complete. Finally we discuss some application to reasoning about game playing agents.

Nenad Savic and Thomas Studer
Public Announcements for Epistemic Models and Hypertheories

Artemov has recently proposed a modernization of the semantics and proof theory of epistemic logic. We take up his approach and extend his framework with public announcements and the corresponding belief change operation. We establish a soundness and completeness result and show that our model update operation satisfies the AGM postulate of minimal change. Further, we also show that the standard approach cannot be directly employed to capture knowledge change by truthful announcements.

Rohit Parikh
Logic without Language

Does a dog think? Does a prelingual child think? Creatures without language seem to be making some logical inferences which allow them to make decisions. We offer a utility and perception based account which allows us to deal with this phenomenon formally. We offer the suggestion that non-lingual creatures have a certain perception of the world and that they make the best decisions relative to that perception. Logic may be "used" to infer non-perceived facts from perceived facts.

Yoshiki Nakamura
The Undecidability of FO3 and the Calculus of Relations with Just One Binary Relation

The validity problem for first-order logic is a well-known undecidable problem. The undecidability also holds even for FO3 and (equational formulas of) the calculus of relations. In this paper we tighten these undecidability results to the following: (1) FO3 with just one binary relation is undecidable even without equality; and (2) the calculus of relations with just one character and with only composition, union, and complement is undecidable. Additionally we prove that the finite validity problem is also undecidable for the above two classes.

Cezary Cieśliński
Satisfaction classes via cut elimination

The goal of this paper is to present a fully classical construction of a satisfaction class for the language of first-order arithmetic. The initial introductory remarks describe the motivation for this endeavor.

Katsuhiko Sano and Minghui Ma
Sequent Calculi for Normal Update Logics

Normal update logic is the temporalization of normal conditional logic. Sequent calculi for the least normal update logic UCK by Andreas Herzig (1998) and some of its extensions are developed. The subformula property of these sequent calculi is shown by Takano's semantic method. Consequently we prove the finite model property and decidability of these sequent calculi.

Sankha S. Basu
A paraconsistent sub-logic of intuitionistic propositional logic

In this paper, we present an axiomatization for a sub-logic of intuitionistic propositional logic. The resulting logic is paraconsistent. We also present an algebraic semantics for this logic and prove the soundness and completeness of the logic with respect to this algebraic semantics.

Giuseppe Greco, Peter Jipsen, Apostolos Tzimoulis, Alessandra Palmigiano and Krishna Manoorkar
Logics for Rough Concept Analysis

Taking an algebraic perspective on the basic structures of Rough Concept Analysis as the starting point, in this paper we introduce some varieties of lattices expanded with normal modal operators which can be regarded as the natural rough algebra counterparts of certain subclasses of rough formal contexts, and introduce proper display calculi for the logics associated with these varieties which are sound, complete, conservative and with uniform cut elimination and subformula property. These calculi modularly extend the multi-type calculi for rough algebras to a 'nondistributive' (i.e. general lattice-based) setting

Clément Lion
Portrait of the Intuitionist as an Opponent in Dialogues. Embedding a Brouwerian counter-example within a classical play

L.E.J. Brouwer has never been a logician, but certainly a mathematician in dialogue with logic. In the present paper, we refer to the dialogical framework, in order to give a sense to Brouwer's position in regard to logic. As dialogical logic is not only dealing with valid inference, which is reserved to the strategic level, but also provides the tools to go beyond it, by exploring all the possibilities of argumentative plays, we try to locate the kind of play corresponding to Brouwer's counter-examples to classical logic. By figuring Brouwer as an Opponent in Dialogues, we do not neglect however his advocacy of introspection, but we try to render it, within a game-theory semantics, as a particular position in dialogue, and even as immanent to dialogues. At the end of the paper, we draw a sketch of what could be a formal rendering of an immanent and however introspective argument in the technical device furnished by recent developments of dialogical logic. Our proposal is to conceive Brouwer's line of argumentation as based on a quartering between two repetion ranks, a formal one and a material one.

Maya Saran
Gδ sets in σ-ideals generated by compact sets

Given a compact Polish space and the hyperspace of its compact subsets K(E), we consider Gδ σ-ideals of compact subsets of E. Solecki has shown that any σ-ideal in a broad natural class of Gδ ideals can be represented via a compact subset of K(E); in this article we examine the behaviour of Gδ subsets of E with respect to the representing set. Given an ideal I in this class, we construct a representing set that recognises a compact subset of E as being "small" precisely when it is in I, and recognises a Gδ subset of E as being "small" precisely when it is covered by countably many compact sets from I.

Jasine Babu, Karunakaran Murali Krishnan and Vineeth Paleri
A fix-point characterization of Herbrand equivalence of expressions in data flow frameworks

Computing Herbrand equivalences of terms in data flow frameworks is well studied in program analysis. While algorithms use iterative fix-point computation on some abstract lattice of expressions relevant to the flow graph, the definition of Herbrand equivalences is based on an equivalence over all program paths formulation, on the (infinite) set of all expressions. The aim of this paper is to develop a lattice theoretic fix-point formulation of Herbrand equivalence on a concrete lattice defined over the set of all terms constructible from variables, constants and operators of a program. This new formulation makes explicit the underlying lattice framework as well as the monotone function involved in computing Herbrand equivalences. We introduce the notion of Herbrand congruence and define an (infinite) concrete lattice of Herbrand congruences. Herbrand equivalence is defined as the maximum fix-point of a composite transfer function defined over an appropriate product lattice of the above concrete lattice. We then re-formulate the traditional meet over all paths definition in our lattice theoretic framework and prove that the maximum fix-point (MFP) and the meet-over-all-paths (MOP) formulations coincide as expected.

Abhishek Kr Singh and Raja Natarajan
Towards a constructive formalization of Perfect Graph Theorems

Interaction between clique num ω(G) and chromatic number χ(G) of a graph is a well studied topic in graph theory. Perfect Graph Theorems are probably the most important results in this direction. Graph G is called perfect if χ(H) = ω(H) for every induced subgraph H of G. The Strong Perfect Graph Theorem (SPGT) states that a graph is perfect if and only if it does not contain an odd hole (or an odd anti-hole) as its induced subgraph. The Weak Perfect Graph Theorem (WPGT) states that a graph is perfect if and only if its complement is perfect. In this paper, we present a formal framework for verifying these results. We model finite simple graphs in the constructive type theory of Coq Proof Assistant without adding any axiom to it. Finally, we use this framework to present a constructive proof of the Lovász Replication Lemma, which is the central idea in the proof of Weak Perfect Graph Theorem.

Arka Banerjee, Samir Karmakar and Sujata Ghosh
Factivity and nominalization: A study on 'mind-predicates' in Bangla

This paper deals with the connection between factivity and nominalization focusing on certain attitude predicates in Bangla (aka Bengali) termed as 'mind-predicates'. These are complex predicates in nature. This work formalizes the clause selectional properties of these mind-predicates in terms of factivity and eventually studies their compatibility with the complement clauses once they are nominalized. Further, it explores the semantic contribution of the light verbs, if any, in construing their meanings as whole functional units.

Reetu Bhattacharjee, Mihir Kr. Chakraborty, and Lopamudra Choudhury
A diagram system extending the system venn-II

In this paper we expand the language of diagram system which is a development upon the Venn-Peirce system by Shin. Inclusion of 'absence of individuals' in the language changes the syntax as well as semantics of the system. We state the rules of inference with illustrations and establish the completeness theorem.

Abhisekh Sankaran
Revisiting the generalized Łoś-Tarski theorem

We present a new proof of the generalized Łoś-Tarski theorem (GLT(k)), over arbitrary structures. Instead of using λ-saturation, we construct just the "required saturation" directly using ascending chains of structures. We also strengthen the failure of GLT(k) in the finite, by strengthening the failure of the Łoś-Tarski theorem in this context. In particular, we prove that not just universal sentences, but for each fixed k, even Σ20 sentences containing k existential quantifiers fail to capture hereditariness in the finite. We conclude with two problems as future directions, concerning the Łoś-Tarski theorem and GLT(k), both in the context of all finite structures.