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 wellknown program specification language with desirable properties like decidability of satisfiability and model checking, axiomatisability etc. Its expressive power is limited by Monadic SecondOrder 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 HigherOrder 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 nonregular properties and then survey results on it with a focus on open questions in this area.

Ian PrattHartmann 
Transitivity and Equivalence in Decidable Fragments of FirstOrder Logic: a Survey 
In this talk, I survey recent work on extensions of various wellknown decidable fragments of firstorder 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 stateoftheart.

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 socalled 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 setup 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 higherorder forcings), and I will show how they are used in the abovementioned 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 variablefree propositional bimodal 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 multiagent 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 nonlingual 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 nonperceived facts from perceived facts.

Yoshiki Nakamura 
The Undecidability of FO3 and the Calculus of Relations with Just One Binary Relation 
The validity problem for firstorder logic is a wellknown 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 firstorder 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 sublogic of intuitionistic propositional logic 
In this paper, we present an axiomatization for a sublogic 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 multitype calculi for rough algebras to a 'nondistributive' (i.e. general latticebased) setting

Clément Lion 
Portrait of the Intuitionist as an Opponent in Dialogues. Embedding a Brouwerian counterexample 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 counterexamples 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 gametheory 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 fixpoint 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 fixpoint 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 fixpoint 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 fixpoint of a composite transfer function defined over an appropriate product lattice of the above concrete lattice. We then reformulate the traditional meet over all paths definition in our lattice theoretic framework and prove that the maximum fixpoint (MFP) and the meetoverallpaths (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 antihole) 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 'mindpredicates' in Bangla 
This paper deals with the connection between factivity and nominalization focusing on certain attitude predicates in Bangla (aka Bengali) termed as 'mindpredicates'. These are complex predicates in nature. This work formalizes the clause selectional properties of these mindpredicates 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 vennII 
In this paper we expand the language of diagram system which is a development upon the VennPeirce 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 Σ_{2}^{0} 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.
