View: session overviewtalk overview
08:45  FLoC Plenary Talk: From Reachability to Temporal Specifications in Game Theory SPEAKER: Orna Kupfermann ABSTRACT. Multiagents games are extensively used for modelling settings in which different entities share resources. For example, the setting in which entities need to route messages in a network is modelled by networkformation games: the network is modelled by a graph, and each agent has to select a path satisfying his reachability objective. In practice, the objectives of the entities are often more involved than reachability. The need to specify and reason about rich specifications has been extensively studied in the context of verification and synthesis of reactive systems. The talk describes a lifting of ideas from formal methods to multiagent games. For example, in networkformation games with regular objectives, the edges of the graph are labeled by alphabet letters and the objective of each player is a regular language over the alphabet of labels. Thus, beyond reachability, a player may restrict attention to paths that satisfy certain properties, referring, for example, to the providers of the traversed edges, the actions associated with them, their quality of service, security, etc. The talk assumes no previous knowledge in game theory. We will introduce the basic concepts and problems, describe how their extension to games with more expressive specification of objectives poses new challenges, and study the resulting games. Joint work with Guy Avni and Tami Tamir. 
09:00  Ludics and interactive completeness SPEAKER: Kazushige Terui 
09:45  Forward and backward induction in dynamic games: Distilling the axiomatic differences on common ground SPEAKER: Sujata Ghosh ABSTRACT. Backward Induction (BI) is the basic solution concept for finite games with perfect information. It is the procedure to find out all the subgameperfect equilibria in such games, i.e. the Nash equilibria in which incredible threats are precluded. An alternative approach to solving games with perfect information is to employ Forward Induction (FI), with which players do assess their opponents’ future behavior on the basis of these opponents’ past moves. A prominent solution concept embodying FI is ExtensiveForm Rationalizability (EFR), in which the active player at each node reacts optimally to a best rationalization of her opponents’ past behavior. Both BI and EFR are, strictly speaking, distinct iterative heuristics of strategy sieving, whose technical definitions do not directly disclose their epistemic motivation. This calls for exposing the different axiomatic assumptions underlying the two solution concepts, in a way that will enable an explicit comparison between them. This (ongoing) work aims at setting up an appropriate epistemic logic syntax, and at formulating directly comparable axiom systems characterizing BI and EFR. 
09:15  Definability, automorphisms and enumeration degrees SPEAKER: Mariya I. Soskova ABSTRACT. The enumeration degrees are an upper semilattice with a least element and jump operation. They are based on a positive reducibility between sets of natural numbers, enumeration reducibility, introduced by Friedberg and Rogers in 1959. The Turing degrees have a natural isomorphic copy in the structure of the enumeration degrees, namely the substructure of the total enumeration degrees. A longstanding question of Rogers is whether the substructure of the total enumeration degrees has a natural first order definition. The first advancement towards an answer to this question was made by Kalimullin. He discovered the existence of a special class of pairs of enumeration degrees, Kpairs, and showed that this class has a natural first order definition. Building on this result, he proved the first order definability of the enumeration jump operator and consequently obtained a first order definition of the total enumeration degrees above 0'. Ganchev and Soskova showed that when we restrict ourselves to the local structure of the enumeration degrees bounded by 0', the class of Kpairs is still first order definable. They investigated maximal Kpairs and showed that within the local structure the total enumeration degrees are first order definable as the least upper bounds of maximal Kpairs. The question of the global definability of the total enumeration degrees is finally solved by Cai, Ganchev, Lempp, Miller and Soskova. They show that Ganchev and Soskova's local definition of total enumeration degrees is valid globally. Then using this fact, they show that the relation ``c.e. in'', restricted to total enumeration degrees is also first order definable. We will discuss these results and certain consequences, regarding the automorphism problem in both degree structures. This research was supported by a BNSF grant No. DMU 03/07/12.12.2011, by a Sofia University SF grant and by a Marie Curie international outgoing fellowship STRIDE (298471) within the 7th European Community Framework Programme. 
10:45  ZeroReachability in Probabilistic MultiCounter Automata SPEAKER: Petr Novotný ABSTRACT. We study the qualitative and quantitative zeroreachability problem in probabilistic multicounter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zeroreachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zeroreaching runs can be effectively approximated up to an arbitrarily small given error eps > 0 in time which is polynomial in log(eps), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter. Here we show that the qualitative zeroreachability is decidable and SquareRootSumhard, and the probability of all zeroreaching runs can be effectively approximated up to an arbitrarily small given error eps > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets. 
11:15  Senescent Ground Tree Rewrite Systems SPEAKER: Matthew Hague ABSTRACT. Ground Tree Rewrite Systems with State are known to have an undecidable control state reachability problem. Taking inspiration from the recent introduction of scopebounded multistack pushdown systems, we define Senescent Ground Tree Rewrite Systems. These are a restriction of ground tree rewrite systems with state such that nodes of the tree may no longer be rewritten after having witnessed an a priori fixed number of control state changes. As well as generalising scopebounded multistack pushdown systems, we show  via reductions to and from reset Petrinets  that these systems have an Ackermanncomplete control state reachability problem. However, reachability of a regular set of trees remains undecidable. 
11:45  Abstract Interpretation from Buchi Automata SPEAKER: unknown ABSTRACT. We describe the construction of an abstract lattice from a given Buchi automata. The abstract lattice is finite and has the following key properties. (i) There is a Galois connection between the (infinite) lattice of languages of finite and infinite words over a given alphabet. (ii) The abstraction is faithful with respect to acceptance by the automaton. (iii) Least fixpoints and witerations (but not in general greatest fixpoints) can be computed on the level of the abstract lattice. This allows one to develop an abstract interpretation capable of checking whether finite and infinite traces of a (recursive) program are accepted by a policy automaton. It is also possible to cast this analysis in the form of a type and effect system with the effects being elements of the abstract lattice. While the resulting decidability and complexity results are known (regular model checking for pushdown systems) the abstract lattice provides a new point of view and enables smooth integration with data types, objects, higherorder functions which are best handled with abstract interpretation or type systems. We demonstrate this by generalising our typeandeffect systems to objectoriented programs and higherorder functions. 
12:15  Separating Regular Languages with FirstOrder Logic SPEAKER: unknown ABSTRACT. Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a firstorder definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words. 
10:45  Coinduction UpTo in a Fibrational Setting SPEAKER: Daniela Petrisan ABSTRACT. Bisimulation upto enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for equivalences of different kinds of systems. Even before Milner introduced and applied such methods in his work on CCS, Hopcroft and Karp used upto techniques to check equivalence of deterministic automata. In this work, we prove the soundness of such techniques in an abstract fibrational setting building on the seminal work of Hermida and Jacobs. To do this in a modular way we generalise Pous and Sangiorgi's notion of \emph{compatibility}. This allows us to systematically prove the soundness of upto techniques, not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. By tuning the parameters of our framework, we obtain novel proof techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity. 
11:15  Deadlock and lock freedom in the linear picalculus SPEAKER: Luca Padovani ABSTRACT. We study two refinements of the linear πcalculus that ensure deadlock freedom (the absence of stable states with pending linear communications) and lock freedom (the eventual completion of pending linear communications). The main feature of both type systems is a new form of channel polymorphism that affects their accuracy in a significant way: they are the first of their kind that can deal with recursive processes communicating in cyclic network topologies. 
11:45  Secure Equilibria in Weighted Games SPEAKER: Noémie Meunier ABSTRACT. We consider twoplayer non zerosum infinite duration games played on weighted graphs. We extend the notion of secure equilibrium introduced by Chatterjee et al., from the Boolean setting to this quantitative setting. As for the Boolean setting, our notion of secure equilibrium refines the classical notion of Nash equilibrium. We prove that secure equilibria always exist in a large class of weighted games which includes common measures like sup, inf, lim sup, lim inf, meanpayoff, and discounted sum. Moreover we show that it is possible to synthesize such strategy profiles that are finitememory and use few memory. Finally, we prove that the constrained existence problem for secure equilibria is decidable for sup, inf, lim sup, lim inf and meanpayoff measures. Our solutions rely on new results for zerosum quantitative games with lexicographic objectives that are interesting on their own right. 
12:15  Infinite sequential games with realvalued payoffs SPEAKER: Stephane Le Roux ABSTRACT. We investigate the existence of certain types of equilibria (Nash, epsilonNash, subgame perfect, epsilonsubgame perfect) in infinite sequential games with realvalued payoff functions depending on the class of payoff functions (continuous, upper semicontinuous, Borel) and whether the game is zerosum. Our results hold for games with two or up to countably many players. Several of these results are corollaries of stronger results that we establish about equilibria in infinite sequential games with some weak conditions on the occurring preference relations. We also formulate an abstract equilibrium transfer result about games with compact strategy spaces and open preferences. Finally, we consider a dynamical improvement rule for infinite sequential games with continuous payoff functions. 
10:45  A Formal Library for Elliptic Curves in the Coq Proof Assistant SPEAKER: unknown ABSTRACT. A preliminary step towards the verification of elliptic curve cryptographic algorithms is the development of formal libraries with the corresponding mathematical theory. In this paper we present a formalization of elliptic curves' theory, in the SSReflect extension of the Coq proof assistant. Our central contribution is a library containing many of the objects and core properties related to elliptic curve theory. We demonstrate the applicability of our library by formally proving a nontrivial property of elliptic curves: the existence of an isomorphism between a curve and its Picard group of divisors. 
11:15  A Verified GenerateTestAggregate Coq Library for Parallel Programs Extraction SPEAKER: unknown ABSTRACT. The integration of the generateandtest paradigm and semirings for the aggregation of results provides a parallel programming framework for large scale dataintensive applications. The socalled GTA framework allows a user to define an inefficient specification of his/her problem as a composition of a generator of all the candidate solutions, a tester of valid solutions, and an aggregator to combine the solutions. Through two calculation theorems a GTA specification is transformed into a divideandconquer efficient program that can be efficiently implemented in parallel. In this paper we present a verified implementation of this framework in the Coq proof assistant: efficient bulk synchronous parallel functional programs can be extracted from naive GTA specifications. We show how to apply this framework on an example, including performance experiments on parallel machines. 
11:45  Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm SPEAKER: Peter Lammich ABSTRACT. We present an Isabelle/HOL formalization of Gabow's algorithm for finding the strongly connected components of a directed graph. Using data refinement techniques, we extract efficient code that performs comparable to a reference implementation in Java. Our style of formalization allows for reusing large parts of the proofs when defining variants of the algorithm. We demonstrate this by verifying an algorithm for the emptiness check of generalized Buchi automata, reusing most of the existing proofs. 
12:15  Cardinals in Isabelle/HOL SPEAKER: Andrei Popescu ABSTRACT. We report on a formalization of ordinals and cardinals in Isabelle/HOL. A main challenge we faced was the inability of higherorder logic to represent ordinals canonically, as transitive sets (as done in set theory). We resolved this into a “decentralized” representation identifying ordinals with wellorders, with all concepts and results proved to be invariant under order isomorphism. We also discuss several applications of this general theory in formal developments. 
12:45  HOL Constant Definitions Done Right SPEAKER: Rob Arthan ABSTRACT. This note gives a proposal for a simpler and more powerful replacement for the mechanisms currently provided in the various HOL implementation for defining new constants. 
10:45  Ramsey Theorem as an intuitionistic property of well founded relations SPEAKER: unknown ABSTRACT. Ramsey Theorem for pairs is a combinatorial result that cannot be intuitionistically proved. In this paper we present a new form of Ramsey Theorem for pairs we call Hclosure Theorem. Hclosure is a property of well founded relations, intuitionistically provable, informative, and possibly simpler to use in intuitionistic proofs. Using our intuitionistic version of Ramsey Theorem we intuitionistically prove the Termination Theorem by Poldenski and Rybalchenko. This theorem concerns an algorithm inferring termination for whileprograms, and was originally proved from the classical Ramsey Theorem, then intuitionistically, but using a intuitionistic version of Ramsey Theorem different from our one. Our longterm goal is to extract effective bounds for the whileprograms from the proof of Termination Theorem, and our new intuitionistic version of Ramsey Theorem is designed for this goal. 
11:15  Termination of Cycle Rewriting SPEAKER: unknown ABSTRACT. String rewriting can not only be applied on strings, but also on cycles and even on general graphs. In this paper we investigate ter mination of string rewriting applied on cycles, shortly denoted as cycle rewriting, which is a strictly stronger requirement than termination on strings. Most techniques for proving termination of string rewriting fail for proving termination of cycle rewriting, but match bounds, arctic ma trices and tropical matrices can be applied. Further we show how any terminating string rewriting system can be transformed to a terminating cycle rewriting system, preserving derivational complexity. 
11:45  FirstOrder Formative Rules SPEAKER: Cynthia Kop ABSTRACT. This paper discusses the method of formative rules for firstorder rewriting, which was previously defined for a class of higherorder rewriting. Dual to the wellknown notion of usable rules, this technique allows for further simplifications of the term constraints that need to be solved during a termination proof. Compared to the higherorder definition, we can obtain significant improvements in the firstorder setting, with or without types. 
12:15  Formalizing monotone algebras for certification of termination and complexity proofs SPEAKER: René Thiemann ABSTRACT. Monotone algebras are frequently utilized to generate reduction orders in automated termination and complexityproofs. To be able to certify these proofs, we formalized several kinds of interpretations in the proof assistant Isabelle/HOL. Here, we report on our integration of matrix interpretations, arctic interpretations, and nonlinear polynomial interpretations over various domains, including the reals. 
12:45  Nagoya Termination Tool (System Description) SPEAKER: Akihisa Yamada ABSTRACT. This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination analyzer for term rewrite systems. The tool is special for its power due to the implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the deep cooperation with SMT solvers. We present some new ideas that contribute to the efficiency and the power of the tool. 
10:45  Signaling in independencefriendly logic SPEAKER: Gabriel Sandu 
11:30  Game Reductions SPEAKER: Dietmar Berwanger ABSTRACT. One recurring pattern in strategic reasoning consists in constructing a strategy for one game while playing another, auxiliary game on the side. EhrenfeuchtFraisse games can be seen as an instance of this technique. Although close to the concept of reduction in computation, transferring strategies between games is typically used as a proof artifice, without explicit formalisation. In this talk, we set out with a construction that underlies recent results about infinite games with imperfect monitoring. On basis of this, we illustrate more general features of a strategy transfer mechanism and outline a formal approach via metagames.

12:00  Game Semantics from a Cognitive Modeling Standpoint SPEAKER: unknown ABSTRACT. Wittgenstein has suggested an analogy between having a proof and winning a game. Two research programs that have undertaken to make this analogy formally precise: gametheoretic semantics (GTS) and dialogical logic (DL) but have so come up only with a partial reduction of logic to language games. Specifically, they have failed to specify preferences for the players, and inference mechanisms by which dominated strategies are eliminated, and by which strategic profiles that realize proofs are selected. Instead, they introduce ad hoc restrictions on strategies by means of game rules that guarantee the games to realize modelchecking (GTS) and proofs (DL) procedures. We show how these restrictions can be derived from preference profiles of boundedrational players, and specify inference mechanisms for strategy selection, based on some assumptions that select the player types. Our model does not answer a foundational agenda but should be viewed as an exercise in cognitive modeling, which bridges the watershed between formal and cognitive semantics, and may yield some insights into how logical reasoning could have emerged from natural language argumentation. 
12:30  Emulating Diffusion and Best Response Dynamics in Social Networks using Action Models SPEAKER: Rasmus K. Rendsvig ABSTRACT. Threshold models and their dynamics may be used to model the spread of behaviors, fashions or language use in social networks. Regarding such as Kripke models, it is shown how standard update mechanisms may be emulated using action models. The suitable class of action models is specified and shown to include models charaterizing best response dynamics of both coordination and anticoordination games played on graphs. Hereby, new links between social network theory, game theory and dynamic ‘epistemic’ logic are drawn. 
10:45  Long Proofs of (Seemingly) Simple Formulas SPEAKER: Mladen Miksa ABSTRACT. In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for stateoftheart SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become very easy). Somewhat intriguingly, however, the very hardest instances in practice seem to arise from socalled fixed bandwidth matrices, which are provably easy for resolution and are also simple in practice if the solver is given a hint about the right branching order to use. This would seem to suggest that CDCL with current heuristics does not always search efficiently for short resolution proofs, despite the theoretical results of [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte, and Thurley2011]. 
11:15  Proof complexity and the LovaszKneser Theorem SPEAKER: Adrian Crăciun ABSTRACT. We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the KneserLovasz Theorem. This is a family of propositional tautologies, indexed by an nonnegative integer parameter k that generalizes the Pigeonhole Principle (PHP, obtained for k=1). We show for all fixed $k$ $2^{\Omega(n)}$ lower bounds on resolution complexity and exponential lower bounds for bounded depth Frege proofs. These results hold even for the more restricted class of formulas encoding Schrijver's strengthening of the KneserLovasz Theorem. On the other hand for the cases $k=2,3$ (for which combinatorial proofs of the KneserLovasz Theorem are known) we give polynomial size Frege (k=2), respectively extended Frege (k=3) proofs. The paper concludes with a brief discussion of the results (that will be presented in a subsequent paper) on the complexity of the general case of the KneserLovasz theorem. 
11:00  Tutorial on Stategic and Extensive Games 2 SPEAKER: Krzysztof Apt 
12:00  Logic meets number theory in ominimality SPEAKER: Matthias Aschenbrenner 
14:30  TwoWay Cost Automata and Cost Logics over Infinite Trees SPEAKER: Michael Vanden Boom ABSTRACT. Regular cost functions provide a quantitative extension of regular languages that retains most of their important properties, such as expressive power and decidability, at least over finite and infinite words and over finite trees. Much less is known over infinite trees. We consider cost functions over infinite trees defined by an extension of weak monadic secondorder logic with a new fixedpointlike operator. We show this logic to be decidable, improving previously known decidability results for cost logics over infinite trees. The proof relies on an equivalence with a form of automata with counters called quasiweak cost automata, as well as results about converting twoway alternating cost automata to oneway alternating cost automata. 
15:00  Logical Characterization of Weighted Pebble Walking Automata SPEAKER: Benjamin Monmege ABSTRACT. Weighted automata are a conservative quantitative extension of finite automata that enjoys applications, e.g., in language processing and speech recognition. Their expressive power, however, appears to be limited when they are applied to more general structures than words, such as graphs. To address this drawback, weighted automata have recently been generalized to weighted pebble walking automata, which proved useful as a tool for the specification and evaluation of quantitative properties over words and nested words. In this paper, we establish the expressive power of weighted pebble walking automata in terms of transitive closure logic, lifting a similar result by Engelfriet and Hoogeboom from the boolean case to a quantitative setting. This result applies to a general class of graphs that subsumes all the aforementioned classes. 
15:30  Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic SPEAKER: Georg Gottlob ABSTRACT. The hypergraph duality problem DUAL is defined as follows: given two simple hypergraphs G and H, decide whether H consists precisely of all minimal transversals of G (in which case we say that G is the dual of H). This problem is equivalent to decide whether two given nonredundant monotone DNFs are dual. It is known that nonDUAL, the complementary problem to DUAL, is in GC(log^{2} n,PTIME), where GC(f(n),C) denotes the complexity class of all problems that after a nondeterministic guess of O(f(n)) bits can be decided (checked) within complexity class C. It was conjectured that nonDUAL is in GC(log^{2} n,LOGSPACE). In this paper we prove this conjecture and actually place the nonDUAL problem into the complexity class GC(log^{2} n,TC^{0}) which is a subclass of GC(log^{2} n,LOGSPACE). We here refer to the logtimeuniform version of TC^{0}, which corresponds to FO(COUNT), i.e., first order logic augmented by counting quantifiers. We achieve the latter bound in two steps. First, based on existing problem decomposition methods, we develop a new nondeterministic algorithm for nonDUAL that requires to guess O(log^{2} n) bits. We then proceed by a logical analysis of this algorithm, allowing us to formulate its deterministic part in FO(COUNT). 
14:30  Decomposition Theorems and ModelChecking for the Modal mucalculus SPEAKER: Christoph Dittmann ABSTRACT. The modal $\mu$calculus, introduced by Dexter Kozen in 1981, is among the best known temporal logics studied in the theory of verification. Despite 30 years of continuous efforts, the exact complexity of its model checking problem remains elusive, and the question whether the problem can be solved in polynomial time is still unsolved. Most work in the literature uses a game or automata theoretic approach by reducing the model checking problem to the problem of solving parity games, a twoplayer game in which the formula and the transition system is combined into a single game arena. In this paper we take a different route and study the model checking problem directly, keeping the formula and the transition system separate. This allows us to develop logical tools which manipulate the formula only and thereby studying the problem within the framework of parameterized complexity. This approach has been very successful for first or monadic secondorder logic, for instance in the work on algorithmic meta theorems. As the main logical result of this paper we develop decomposition or splittertheorems for the modal $\mu$calculus in the style of FefermanVaught theorems for FO and MSO. In particular, we show that if a transition system $M$ is composed of the union of two systems $M_1 \cup M_2$, then the truth of $L_\mu$formulas at a node in $M$ essentially only depends on the truth of suitable formulas in the two systems $M_1$ and $M_2$. This result even applies to the much more general case where we allow additional edges in $M$ which start in $M_1$ and end in $M_2$. As an algorithmic consequence we get that $L_\mu$ modelchecking is fixedparameter tractable on various classes of transition systems such as transition systems of bounded directed path width and bounded Kellywidth. To the best of our knowledge, these are among the first FPTresults for $L_\mu$ that do not follow immediately from tractability of monadic secondorder logic. 
15:00  Logics with Counting and Equivalence SPEAKER: Ian PrattHartmann ABSTRACT. We consider the twovariable fragment of firstorder logic with counting quantifiers, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NExpTimecomplete. 
15:30  Local Temporal Reasoning SPEAKER: unknown ABSTRACT. We present the first method for reasoning about temporal logic properties of higherorder, infinitedata programs. By distinguishing between the finite traces and infinite traces in the specification, we obtain rules that permit us to reason about the temporal behavior of program parts via a typeandeffect system, which is then able to compose these facts together to prove the overall target property of the program. The type system alone is strong enough to derive many temporal safety properties, for example when using refinement types and temporal effects. We also show how existing techniques can be used as oracles to provide liveness information (e.g. termination) about program parts and that the typeandeffect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higherorder software, as well as modular strategies for procedural programs. 
14:30  Balancing lists: a proof pearl SPEAKER: Arnaud Spiwack ABSTRACT. Starting with an algorithm to turn lists into full trees which uses nonobvious invariants and partial functions, we progressively encode the invariants in the types of the data, removing most of the burden of a correctness proof. The invariants are encoded using nonuniform inductive types which parallel numerical representations in a style advertised by Okasaki, and a small amount of dependent types. 
15:00  Invited talk: Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK SPEAKER: unknown 
14:30  A unified approach to Univalent Foundations and Homotopical Algebra SPEAKER: Nicola Gambino ABSTRACT. Voevodsky's Univalent Foundations of Mathematics programme seeks to develop a new approach to the foundations of mathematics, based on dependent type theories extended with axioms inspired by homotopy theory. The most remarkable of these new axioms is the socalled Univalence Axiom, which allows us to treat isomorphic types as if there were equal. Quillen's homotopical algebra, instead, provides a categorytheoretic framework in which it is possible to develop an abstract version of homotopy theory, giving a homogeneous account of several situations where objects are identified up to a suitable notion of `weak equivalence'. The central notion here is that of a model category, examples of which arise naturally in several different areas of mathematics. The aim of this talk is to explain how the type theories considered in Univalent Foundations and the categorical structures considered in homotopical algebra are different but related, and to describe categorically the common core of Univalent Foundations and homotopical algebra, thus allowing a simoultaneous development of the two subjects. The axiomatisation will be based on work of several authors, including Awodey, van den Berg, Garner, Joyal, Lumsdaine, Shulman and Warren.

15:30  Amortised Resource Analysis and Typed Polynomial Interpretations SPEAKER: unknown ABSTRACT. We introduce a novel resource analysis for typed term rewrite systems based on a potentialbased type system. This type system gives rise to polynomial bounds on the runtime complexity. We relate the thus obtained amortised resource analysis to polynomial interpretations and obtain the perhaps surprising result that whenever a rewrite system R can be welltyped, then their exists a polynomial interpretation that orients R. For this we suitable adapt the standard notion of polynomial interpretations to the typed setting. 
14:30  Semantic games for Łukasiewicz logic SPEAKER: Ondrej Majer 
15:15  Game Semantics for Conditional Logic SPEAKER: Johannes Marti ABSTRACT. In this talk we introduce a game semantics for conditional logic. We 
15:45  MultiAgent Dialogical Games for Modal Logic SPEAKER: Martin Sticht ABSTRACT. Dialogical Logic as a gametheoretic approach was introduced by Lorenzen and Lorenz and can be used to check validity of formulae for different kinds of logics. The system has been extended by Rahman and Rückert to cope with modal logic. Dialogues are very flexible as one can simply exchange their underlying rules to obtain decision procedures for other kinds of logic. A problem that occurs with the dialogues is that the amount of possible moves the players can perform in the game often cause a very high branching which makes the implementation inefficient when one wants to show or refute validity of formulae. We modify the system by introducing further players who all try to show validity of a formula together. This new approach works in a more deterministic way and thereby provides a plan to parallelize the reasoning process. 
14:30  A (Biased) Proof Complexity Survey for SAT Practitioners SPEAKER: Jakob Nordström 
14:30  Elections and knowledge SPEAKER: Rohit Parikh ABSTRACT. There are (at least) two ways in which knowledge can enter into elections. 1. When a voter strategizes, i.e. votes for someone who is not her first preference then she needs to know something about how the others are voting. In the absence of knowledge, the only safe vote is an honest vote. But in the presence of knowledge, a "dishonest" vote may be better than an honest one. Also, perhaps they too want to know how she is voting. We discuss how knowledge affects strategizing and when cycles will form. 2. When a politician campaigns, he wants to influence the voters’ beliefs. What should he say in order to appeal to them in the best way? If the politician knows the preferences of various groups of voters then he will choose the right thing to say so as to make a favorable impression on most voters and antagonize the fewest voters. We also consider the temperament of the voters  voters may be pessimistic, optimistic, or use some form of expected value to evaluate the candidate and his utterances. We will make use of joint work with Samir Chopra, Walter Dean and Eric Pacuit, as well as suggest some new ideas. 
15:15  Nash equilibrium semantics for IndependenceFriendly Logic SPEAKER: Gabriel Sandu ABSTRACT. Henkin (1961) enriched firstorder logic with socalled branching or Henkin quantifiers such as $\left(\begin{array}{c} \forall x\\ \exists y \end{array}\right)$ and $\left(\begin{array}{cc} \forall x & \exists y\\ \forall z & \exists w \end{array}\right).$ The former is intended to express the fact that the existential qua ntifier $\exists y$ is independent of the universal quantifier $\forall x$. The latter is more easily introduced in terms of the idea of dependence: the existential quantifier $\exists y$ depends only on the universal quantifier $\forall x$, and the existential quantifier $\exists w$ depends only on the universal quantifier $\forall z$. The notions of independence and dependence are codified in terms of the existence of certain (Skolem) functions. It turns out that prefixing firstorder formulas with branching quantifiers results in a logic which is strictly stronger than ordinary firstorder logic. In the first part of my presentation I will quickly review various formalisms which develop Henkin's ideas. One of them is IndependenceFriendly logic introduced by Hintikka and Sandu (1989). The first branching quantifier is expressed in IF logic by $\forall x(\exists y/\left\{ x\right\} $) (``for all $x$ there is a $y$ which is independent of $x$''). Similarly, the second branching quantifier is expressed by $\forall x\exists y\forall z( \exists w/\left\{ x,y\right\} )$ (``for all $x$ there is a $y$ and for all $z$ there is a $w$ which is independent from both $x$ and $y$''). The notion of independence is spelled out in gametheoretical terms. With each IF formula $\varphi$, model $\mathbb{M}$, and partial assignment $s$ whose domain is restricted to the free variables of $\varphi$, we associate an extensive winlose game of imperfect information $G(\mathbb{M},\varphi,s)$. When $\varphi$ is the sentence $\forall x(\exists y/\left\{ x\right\} )x=y$, and $s$ is the empty assignment, in a play of the game $G(\mathbb{M},\varphi,s)$ $\forall$ chooses an individual $a\in M$ to be the value of $x$ after which $\exists$ chooses an individual $b\in M$ to be the value of $y$ without knowing the choice made earlier by $\forall$. Player $\exists$ wins the play if $a$ is the same individual as $b$. Otherwise player $\forall$ wins. We stipulate that $\varphi$ is true (false) in $\mathbb{M}$ if there is a winning strategy for player $\exists$ ($\forall$). The notion of strategy is the standard notion of choice function in classical game theory. In games of imperfect information such a function is required to be uniform. A comprehensive presentation of the modeltheoretical properties of IF logic may be found in Mann, Sandu, and Sevenster (2011). Hintikka (1996) explores the significance of IF logic for the foundations of mathematics. As expected, games of imperfect information may be indeterminate. For instance, on models with at least two elements, the IF sentence $\forall x(\exists y/\left\{ x\right\} )x=y$ is neither true nor false. Blass and Gurevich (1986) follow a suggestion by Aitaj and resolve the indeterminacy of this sentence by applying von Neumann's Minimax theorem: $\forall x(\exists y/\left\{ x\right\} )x=y$ gets the probabilistic value $\frac{1}{n}$ on any finite model with $n$ elements. This value is the expected utility returned to the existential player by any mixed strategy equilibrium in the underlying game. This idea has been explored systematically for the first time in Sevenster (2006), and then further developed in Sevenster and Sandu (2010), and in Mann, Sandu and Sevenster (2011). In the second part of my talk I will review some of the recent results on probabilistic IF logic. Finally I will address the question: What kind of probabilistic logic is probabilistic IF logic? Here I shall draw some comparisons to other probabilistic semantics (Leblanc's probabilistic semantics, Bacchus' and Halpern's probabilistic interpretations of firstorder logic.) \begin{thebibliography}{10} %% INSERT YOUR BIBLIOGRAPHIC ENTRIES HERE; %% SEE (4) BELOW FOR PROPER FORMAT. %% EACH ENTRY MUST BEGIN WITH \bibitem{citation key} %% %% IF THERE ARE NO ENTRIES %% DELETE THE LINE ABOVE (\begin{thebibliography}{20}) %% AND THE LINE BELOW (\end{thebibliography}) \bibitem{BG} {\scshape A. Blass and Y. Gurevich}, {\itshape Henkin quantifiers and complete problems}, {\bfseries\itshape Annals of pure and Applied Logic}, vol.~32 (1986), no.~1, pp.~116. \bibitem{He} {\scshape L. Henkin}, {\itshape Some remarks on infinitely long formulas}, {\bfseries\itshape Intuitionistic Methods: Proceedings of the Symposium on Foundations of Mathematics} (P. Bernays, editor), Pergamon Press, Oxford, 1959, pp.~169183. \bibitem{HS} {\scshape J. Hintikka and G. Sandu}, {\itshape Informational Independence as a Semantic Phenomenon}, {\bfseries\itshape Logic, Methodology and Philosophy of Science} (J.~E.~Fenstead et al, editors), Elsevier, Amsterdam, 1989, pp.~571589. \bibitem{MSS} {\scshape A. I. Mann, G. Sandu and M. Sevenster}, {\bfseries\itshape IndependenceFriendly Logic: A GameTheoretic Approach}, Cambridge University Press, 2011. \bibitem{S} {\scshape M. Sevenster}, {\bfseries\itshape Branches of Imperfect Information: Logic, Games, and Computation}, PhD Thesis, University of Amsterdam, 2006. \bibitem{SS} {\scshape M. Sevenster and G. Sandu}, {\itshape Equilibrium Semantics of Languages of Imperfect Information}, {\bfseries\itshape Annals of Pure and Applied Logic}, vol.~161 (2010), pp.~618631. \end{thebibliography} 
14:30  UDrandomness and the Turing degrees SPEAKER: Johanna Franklin ABSTRACT. The roots of UDrandomness are firmly analytic: Avigad defined it in 2013 using concepts from a 1916 theorem of Weyl concerning uniform distribution. Avigad showed in his original paper that UDrandomness is very weak. While every Schnorr random real is UDrandom, the class of UDrandom reals is incomparable with the class of the Kurtz random reals. In this talk, I will present some subsequent work on the Turing degrees of the UDrandom reals and the relationships between UDrandomness and other randomness notions. This work is joint with Wesley Calvert. 
15:15  On finitely presented expansions of groups and algebras SPEAKER: Bakhadyr Khoussainov 
14:30  Matrix iterations and Cichoń's diagram SPEAKER: Diego A. Mejía ABSTRACT. Using matrix iterations of ccc posets we prove the consistency, with ZFC, of some constellations of Cichoń's diagram where the cardinals on the right hand side assume three different values. We also discuss the influence of the constructed models on other classical cardinal invariants of the continuum. 
15:15  Regular crosssections of Borel flows SPEAKER: Konstantin Slutsky ABSTRACT. When working with measurable flows, it is sometimes convenient to choose a countable crosssection and to reduce a problem of interest to a similar question for the action induced by the flow on this crosssection. In some cases, one wants to impose additional restrictions on the crosssection, usually by restricting possible distances between points within each orbit. Historically, crosssections of flows were studied mainly in the context of ergodic theory. One of the most important results here is a theorem of D. Rudolph, which states that any free measure preserving flow, when restricted to an invariant subset of full measure, admits a crosssection with only two possible distances between adjacent points. Borel dynamics deals with actions of groups on standard Borel spaces, when the latter is not equipped with any measure. In this more abstract context, one needs to construct crosssections that are regular on all orbits without exceptions, and methods of ergodic theory, which tend to produce crosssections only almost everywhere, are therefore frequently insufficient. In this regard, M. G. Nadkarni posed a question whether the analog of Rudolph's Theorem holds true in the Borel setting: Does every free Borel flow admit a crosssection with only two different distances between adjacent points? The talk will provide an overview of these and other results concerning the existence of regular crosssections, and a positive answer to Nadkarni's question will be given. As an application of our methods, we give a classification of free Borel flows up to Lebesgue Orbit Equivalence, by which we understand orbit equivalence preserving Lebesgue measure on each orbit. This classification is an analog of the classification of hyperfinite equivalence relations obtained by R. Daugherty, S. Jackson, and A. S. Kechris. 
16:30  Abstract Interpretation: Past, Present and Future SPEAKER: Patrick Cousot ABSTRACT. Abstract interpretation is a theory of abstraction and constructive approximation of the mathematical structures used in the formal description of complex or infinite systems and the inference or verification of their combinatorial or undecidable properties. Developed in the late seventies, it has been since then used, implicitly or explicitly, to many aspects of computer science (such as static analysis and verification, contract inference, type inference, termination inference, modelchecking, abstraction/refinement, program transformation (including watermarking, obfuscation, etc), combination of decision procedures, security, malware detection, database queries, etc) and more recently, to system biology and SAT/SMT solvers. Productionquality verification tools based on abstract interpretation are available and used in the advanced software, hardware, transportation, communication, and medical industries. The talk will consist in an introduction to the basic notions of abstract interpretation and the induced methodology for the systematic development of sound abstract interpretationbased tools. Examples of abstractions will be provided, from semantics to typing, grammars to safety, reachability to potential/definite termination, numerical to proteinprotein abstractions, as well as applications (including those in industrial use) to software, hardware and system biology. This paper is a general discussion of abstract interpretation, with selected publications, which unfortunately are far from exhaustive both in the considered themes and the corresponding references. 
16:30  An Isabelle Proof Method Language SPEAKER: Daniel Matichuk ABSTRACT. Machinechecked proofs are becoming everlarger, presenting an increasing maintenance challenge. Isabelle’s most popular language interface, Isar, is attractive for new users, and powerful in the hands of experts, but has previously lacked a means to write automated proof procedures. This can lead to more duplication in large proofs than is acceptable. In this paper we present IsaTac, a proof method language for Isabelle, which aims to fill this gap by incorporating Isar language elements, thus making it accessible to existing users. We describe the language and the design principles on which it was developed. We evaluate its effectiveness by implementing some tactics widelyused in the seL4 verification stack, and report on its strengths and limitations. 
17:00  Asynchronous User Interaction and Tool Integration in Isabelle/PIDE SPEAKER: Makarius Wenzel ABSTRACT. Historically, the LCF tradition of interactive theorem proving was tied to the readevalprint loop, with sequential and synchronous evaluation of prover commands given on the commandline. This userinterface technology was adequate when R. Milner introduced his LCF proof assistant in the 1970ies, but it severely limits the potential of current multicore hardware and advanced IDE frontends. Isabelle/PIDE breaks this loop and retrofits the readevalprint phases into an asynchronous model of documentoriented proof processing. Instead of feeding a sequence of individual commands into the prover process, the primary interface works via edits over a family of document versions. Execution is implicit and managed by the prover on its own account in a timeless and stateless manner. Various aspects of interactive proof checking are scheduled according to requirements determined by the frontend perspective on the proof document, while making adequate use of the CPU resources on multicore hardware on the backend. Recent refinements of Isabelle/PIDE provide an explicit concept of asynchronous print functions over existing proof states. This allows to integrate longrunning or potentially nonterminating tools into the documentmodel. Applications range from traditional proof state output (which may consume substantial time in interactive development) to automated provers and disprovers that report on existing proof document content (e.g. Sledgehammer, Nitpick, Quickcheck in Isabelle/HOL). Moreover, it is possible to integrate query operations via additional GUI panels with separate input and output (e.g. for Sledgehammer or findtheorems). Thus the Prover IDE provides continuous proof processing, augmented by addon tools that help the user to continue writing proofs. 
17:30  Collaborative Interactive Theorem Proving with Clide SPEAKER: Martin Ring ABSTRACT. This paper introduces Clide, a collaborative web interface for the Isabelle theorem prover. The interface allows a documentoriented interaction with Isabelle very much like Isabelle's desktop interface. Moreover, it allows users to jointly edit Isabelle proof scripts over the web; editing operations are synchronised to all users who have opened the proof script. The paper describes motivation, user experience, implementation and system architecture of Clide. The implementation is based on the theory of operational transformations; its key concepts have been formalised in Isabelle, its correctness proven and critical parts of the implementation on the server are generated from the formalisation, thus increasing confidence in the system. 
16:30  Self Types for Dependently Typed Lambda Encodings SPEAKER: Peng Fu ABSTRACT. We revisit lambda encodings of data, proposing new solutions to several old problems, in particular dependent elimination with lambda encodings. We start with a type assignment form of the Calculus of Constructions, restricted recursive definitions and Miquel’s implicit product. We add a type construct \iota x . T, called a self type, which allows T to refer to the subject of typing. We show how the resulting System S with this novel form of dependency supports dependent elimination with lambda encodings, including induction principles. Strong normalization of S is established by defining an erasure from S to a version of Fomega with positive recursive type definitions, which we analyze. We also prove type preservation for S. 
17:00  The Structural Theory of Pure Type Systems SPEAKER: Floris van Doorn ABSTRACT. We investigate possible extensions of arbitrary given Pure Type Systems with additional sorts and rules which preserve the normalization property. In particular we identify the following interesting extensions: the disjoint union P+Q of two PTSs P and Q, the PTS ∀P.Q which intuitively captures the "Qlogic of Pterms'' and Ppoly which intuitively denotes the "predicative polymorphism" extension of P. These results suggest a new approach to the study of the metatheory of PTSs, by examination of the relationships between different calculi and "predicative extensions" which allow more expressiveness with equivalent logical strength. 
17:30  Unnesting of Copatterns SPEAKER: unknown ABSTRACT. Inductive data such as finite lists and trees can elegantly be defined by constructors which allow programmers to analyze and manipulate finite data via pattern matching. Dually, coinductive data such as streams can be defined by observations such as head and tail and programmers can synthesize infinite data via copattern matching. This leads to a symmetric language where finite and infinite data can be nested. In this paper, we compile nested pattern and copattern matching into a core language which only supports simple nonnested (co)pattern matching. This core language may serve as an intermediate language of a compiler. We show that this translation is conservative, i.e., the multistep reduction relation in both languages coincides for terms of the original language. Furthermore, we show that the translation preserves strong normalisation: a term of the original language is strongly normalising in one language if and only if it is so in the other. 
16:30  Noncharacterizability in belief revision: an application of finite model theory SPEAKER: Jon Yaggie ABSTRACT. A formal framework is given for the characterizability of a class of belief revision operators, defined using minimization over a class of partial preorders, by postulates. It is shown that for partial orders characterizability implies a definability property of the class of partial orders in monadic secondorder logic. Based on a nondefinability result for a class of partial orders, an example is given of a noncharacterizable class of revision operators. This appears to be the first noncharacterizability result in belief revision. 
17:00  Game Semantics for Some NonClassical Logics SPEAKER: Can Baskent ABSTRACT. Our main goal in this paper is to give game semantics for various nonclassical logics, and observe how nonclassical logical elements change the verification game. 
16:30  QBF Resolution Systems and their Proof Complexities SPEAKER: Valeriy Balabanov ABSTRACT. Quantified Boolean formula (QBF) evaluation has a broad range of applications in computer science and is gaining increasing attention. Recent progress has shown that for a certain family of formulas Qresolution, which forms the foundation of learning in modern searchbased QBF solvers, is exponentially inferior in proof length to its extended variants: longdistance Qresolution (LQresolution) and Qresolution with resolution over universal literals (QUresolution). The relative proof power between LQresolution and QUresolution, however, remains unknown. In this paper, we show their incomparability by exponential separations on two families of QBFs, and further proposes a combination of the two resolution methods to achieve an even more powerful proof system. These results may shed light on solver development with enhanced learning mechanisms. In addition, we show how QBF Skolem/Herbrand certificate extraction can benefit from polynomial LQresolution proofs in contrast to their exponential Qresolution counterparts. 
16:30  Modal logic of clocks: Modalizing a firstorder theory of time to get a better understanding of relativity theories SPEAKER: Attila Molnar ABSTRACT. Goldblatt proved that the modal logic S4.2 characterizes Minkowski spacetimes; the possible worlds represent events, and the intended interpretation of the modal operator is ``it is now or it will be the case in the causal future that''. Unfortunately, the expressive power of this logic is very limited; the fundamental relativistic effects such as the twin paradox, time dilatation, etc. are inexpressible. In our talk, we will modalize the firstorder theory of reals to answer this challenge. The worlds, again, will represent events, while the modal operator will represent ``It is visible that'' or ``it was the case in the lightlike separated past that''. We use only functions and relations of reals; the solely modal novelty is the presence of nonrigid designators to deal with the clocks of observers. This theory, beyond its expressive power could be a first step towards a connection of the axiomatic operational foundations of spacetime and the research inspired by Prior and Belnap such as theories of branching spacetimes. 
16:50  Towards a Conditional for The Liar and the Sorites. SPEAKER: Sergi Oms ABSTRACT. I want to present a threevalued paracomplete logic, based on the work of Hartry Field, that captures, in a reasonably intuitive way, how we reason under the phenomenon of vagueness in languages with a truth predicate. I claim that this is a first step towards a satisfactory logic for the Vagueness and Liarlike paradoxes where the naive theory of truth can be implemented; that is, where we can have the Intersubstitutivity Principle (IP): If two sentences A and B are alike except that one has a sentence C where the other has Tr^{⌈}C^{⌉}, then A = B and B = A. I will use a language L suitable to express canonical names for its own sentences and I will extend it to a new language, L^{+}, with a truth predicate, Tr. I will use models with a set W of ordered three valued points and create a process of revision for the conditional where each point is enlarged to a Kripke fixed point. 
17:10  On graph calculus approach to modalities SPEAKER: unknown ABSTRACT. We introduce a graphical approach to modalities. We employ formal systems where graphs are expressions that can be manipulated so as to mirror reasoning at the semantical level. This visual approach is exible and modular providing decision procedures for several normal logics. Promising cases are the application of this approach to PDL for structured data [1] and to memory logics [2]. [1] Veloso, P., Veloso, S. Benevides, M.: PDL for Structured Data: a GraphCalculus Approach. Journal of the IGPL, to appear (2014) [2] Areces, C., Figueira, S. Mera, S. : Completeness Results for Memory Logics. LNCS 5407, pp. 16{30, Springer (2009) 
17:30  Complexity of generalized grading with inverse relations and intersection of relations SPEAKER: Mitko Yanchev ABSTRACT. The language of Graded Modal Logic (GML, Kit Fine, 1972) is an extension of the classical propositional modal language with counting (or \emph{grading}) modal operators $\lozenge_n$, for $n\geq 0$, which have purely quantitative meaning. S. Tobies proves (Tobies, 2000) that the satisfiability problem for the graded modal language is PSPACEcomplete. The language of Majority Logic (MJL, Pacuit and Salame, 2004) augments the graded modal language with some qualitative capabilities. Two extra unary modal operators, $M$ and $W$, are added. In Kripke models $M\varphi$ says that more than half of all accessible worlds satisfy $\varphi$, what represents the simplest case of \emph{rational grading}. The language of Presburger Modal Logic (PML, Demri and Lugiez, 2006) is a manyrelational modal language with independent relations, having the socalled \emph{presburger constraints}, which can express both integer and rational grading. Demri and Lugiez show that the satisfiability for the PML language is PSPACEcomplete, what strengthens the main result of Tobies, and answers the open question about MJL. At that time a generalization of modal operators for rational grading in the spirit of the majority operators is given (Tinchev and Y., 2006), and it is used in the language of Generalized Graded Modal Logic (GGML, Tinchev and Y., 2010). New unary grading operators are considered, $M^r$ and $W^r$, where $r$ is a rational number in (0,1). These operators distinguish the part of accessible worlds having some property. The generalized rational grading operators are expressible by presburger constraints, so the PSPACE completeness of the satisfiability for the generalized graded modal language is a consequence of that for PML. On the other hand an independent proof using a specific technique for exploring the complexity of rational grading is given (Y., 2011). The presence of separate integer and rational grading operators, and the use of the technique developed for the latter allow following a common way for obtaining complexity results as in less, so in more expressive languages with rational grading. In particular, complexity resultsfrom polynomial to PSPACEfor a range of description logics, syntactic analogs of fragments of GGML, are obtained (Y., 2012, 2013). In this talk we consider manyrelational generalized graded modal language adopting \emph{inverse relations} and \emph{intersection of relations}. Rational grading operators are $\upharpoonright\!\!\sigma\!\!\upharpoonleft^r$ and $\downharpoonright\!\!\sigma\!\!\downharpoonleft^r$, where $\sigma$ is an intersection of (possibly inverse) relations. We show that the satisfiability problem for this expressive modal language with generalized grading keeps the PSPACE complexity. 
17:50  Fuzzy Bsimulation for Standard Godel Modal Logic SPEAKER: TuanFang Fan ABSTRACT. We define the notion of fuzzy bisimulation for the standard Godel modal logic and prove the corresponding HennessyMilner style theorem. 
18:10  Hybrid extensions of S4 with the finite model property SPEAKER: unknown ABSTRACT. In R.A. Bull characterized a class of axiomatic extensions of the modal logic S4 (the logic of the class of transitive and symmetric frames) with the finite model property. This result takes the form of a syntactic characterization of a class of formulas that may be added as axioms to S4, somewhat in the spirit of Sahlqvist's famous result in modal correspondence theory. Hybrid logics expand the syntax of modal logic by adding special variables, know as nominals, which are always interpreted as singletons in models and thus act as names for the states at which they hold. Additional syntactic machinery which capitalizes on the naming power of the nominals, like the satisfaction operator or the universal modality, is often added. This makes hybrid languages significantly more expressive than their modal cousins, while retaining their good computational behaviour. In this talk we show how to extend Bull's result to three hybrid languages. The proof we offer is algebraic and serves to illustrate the usefulness of the new algebraic semantics for hybrid logics recently introduced by the authors. Bull's proof makes essential use of the algebraic property of `wellconnectedness' which is equivalent, in the dual relational semantics, to the ability to take generated submodels. Since the truth of hybrid languages is not invariant under generated submodels, the generalization to hybrid logic is not straightforward. 
16:30  Almost structurally complete consequence operations extending S4.3 SPEAKER: unknown ABSTRACT. We prove that a modal consequence operation extending S4.3 is almost structurally complete (with respect to infinitary rules) if and only it is finitely approximable. We also provide an uniform basis, consisting of infinitary rules, for all admissible rules there. 
16:50  Truth theory for logic of selfreference statements as a quaternion structure SPEAKER: Vladimir Stepanov ABSTRACT. On the basis of dynamic model of selfreference statements the variant of multiplevalued logic describing external operations of such statements is considered. It is noted that for formulations and selfreference statements descriptions is enough the language with negation (~) and biconditional (<>) . The truth table for biconditional for type formulae of True, Liar, TruthTeller and (TruthTeller <> Liar), is Cayley table for the Klein fourgroup V . It suggests that the truth space for values of selfreference statements is described by quaternion algebra H. 
17:10  A RoutleyMeyer semantics for Göodel 3valued logic G3 SPEAKER: Gemma Robles ABSTRACT. G\"{o}del 3valued logic G3 is the strongest of the G\"{o}del manyvalued logics introduced in [1]. Although the RoutleyMeyer semantics (RMsemantics) was defined for interpreting relevant logics in the early seventies of the last century (cf. [4]), it was soon found out to be suitable for characterizing a wide family of logics regardless of their being relevant or not, due to its malleability. Still, a necessary condition for a logic S to be characterized by the RMsemantics is that Routley and Meyer's basic positive logic B$_{+}$ is included in S (cf. [4]). The aim of this paper is to provide an RMsemantics for G3 once this logic has been axiomatized as an extension of B$_{+}$ (cf. [2], [3]). 
17:30  Blocking the routes to triviality with depth relevance SPEAKER: José M. Méndez ABSTRACT. The depth relevance condition (drc) is a strengthening of the variablesharing property. A logic S has the drc if $A$ and $B$ share at least a propositional variable at the same depth in all theorems of the form $A\rightarrow B$ (cf. [1]). Logics with the drc have been used for defining nontrivial strong na\"{\i}ve set theories. In [3], \textquotedblleft the class of implication formulas known to trivialize NC\textquotedblright\ is recorded. (NC abbreviates \textquotedblleft na\"{\i}ve comprehension\textquotedblright ; cf. [3], p. 435.) The aim of this paper is to show how to invalidate any member in this class by using \textquotedblleft weak relevant model structures\textquotedblright\ (cf. [2]). Weak relevant model structures only verify logics with the drc. 
16:30  On the almost sure validities in the finite in some fragments of monadic secondorder logic SPEAKER: Valentin Goranko ABSTRACT. This work builds on the wellknown 01 law for the asymptotic probabilities of firstorder definable properties of finite graphs (in general, relational structures). Fagin's proof of this result is based on a transfer between almost sure properties in finite graphs and true properties of the countable random graph (aka, Rado graph). Both the transfer theorem and the 01 law hold in some nontrivial extensions of firstorder logic (e.g., with fixed point operators) but fail in others, notably in most natural fragments of monadic secondorder (MSO) and even for modal logic formulae, in terms of frame validity. The question we study here is how to characterise  axiomatically or modeltheoretically  the set of almost surely valid in the finite formulae of MSO, i.e. those with asymptotic probability 1. This question applies likewise to every logical language where truth on finite structures is welldefined. The set of almost sure validities in the finite of a given logical language is a welldefined logical theory, containing all validities of that language and closed under all sound finitary rules of inference. Beyond that, very little is known about these theories in cases where the transfer theorem fails. In this work we initiate a study of the theories of almost sure validity in modal logic and in the universal and existential fragments of MSO on binary relational structures, aiming at obtaining explicit logical characterisations of these theories. We provide such partial characterisations in terms of characteristic formulae stating almost sure existence (for the existential fragment) or nonexistence (for the universal fragment) of bounded morphisms to special target finite graphs. Identifying explicitly the set of such finite graphs that generate almost surely valid characteristic formulae seems a quite difficult problem, to which we so far only provide some partial answers and conjectures. 
16:50  Completeness of secondorder separation logic for program verification SPEAKER: Makoto Tatsuta ABSTRACT. This paper extends Reynolds' separation logical system for pointer while program verification to secondorder logic. This extension enables us, for example, to capture a set of integer values, in order to capture the set of reachable nodes in a heap predicate. This paper proves its completeness theorem that states that every true asserted program is provable in the logical system. In order to prove the completeness, this paper also shows the expressiveness theorem that states the weakest precondition of every program and every assertion can be expressed in the assertion language. 
17:10  Infinite Games Specified by 2Tape Automata SPEAKER: Olivier Finkel ABSTRACT. We prove that the determinacy of GaleStewart games whose winning sets are infinitary rational relations accepted by 2tape Büchi automata is equivalent to the determinacy of (effective) analytic GaleStewart games which is known to be a large cardinal assumption. Then we prove that winning strategies, when they exist, can be very complex, i.e. highly noneffective, in these games. We prove the same results for GaleStewart games with winning sets accepted by realtime 1counter Büchi automata, then extending previous results obtained about these games. (1) There exists a 2tape Büchi automaton (respectively, a realtime 1counter Büchi automaton) A such that: (a) there is a model of ZFC in which Player 1 has a winning strategy $\sigma$ in the game $G(L(A))$ but $\sigma$ cannot be recursive and not even in the class $(\Sigma_2^1 \cup \Pi_2^1)$; (b) there is a model of ZFC in which the game $G(L(A))$ is not determined. (2) There exists a 2tape Büchi automaton (respectively, a realtime 1counter Büchi automaton) A such that $L(A)$ is an arithmetical $\Delta_3^0$set and Player 2 has a winning strategy in the game $G(L(A))$ but has no hyperarithmetical winning strategies in this game. (3) There exists a recursive sequence of 2tape Büchi automata (respectively, of realtime 1counter Büchi automata) $A_n$, $n\geq 1$, such that all games $G(L(A_n))$ are determined, but for which it is $\Pi_2^1$complete hence highly undecidable to determine whether Player 1 has a winning strategy in the game $G(L(A_n))$. 
17:30  Circuit lower bounds in bounded arithmetics SPEAKER: Ján Pich ABSTRACT. We prove that $T_{NC^1}$, the true universal firstorder theory in the language containing names for all uniform $NC^1$ algorithms, cannot prove that for sufficiently large $n$, SAT is not computable by circuits of size $n^{2kc}$ where $k\geq 1, c\geq 4$ unless each function $f\in SIZE(n^k)$ can be approximated by formulas $\{F_n\}^{\infty}_{n=1}$ of subexponential size $2^{O(n^{2/c})}$ with subexponential advantage: $P_{x\in \{0,1\}^n}[F_n(x)=f(x)]\geq 1/2+1/2^{O(n^{2/c})}$. Unconditionally, $V^0$ cannot prove that for sufficiently large $n$, SAT does not have circuits of size $n^{\log n}$. The proof is based on an interpretation of Kraj\'{i}\v{c}ek's proof \cite{cite1} that certain NWgenerators are hard for $T_{PV}$, the true universal theory in the language containing names for all ptime algorithms. \begin{thebibliography}{10} \bibitem{cite1} {\scshape Jan Kraj\'{i}\v{c}ek}, {\itshape On the proof complexity of the NisanWigderson generator based on a hard NP$\cap$coNP function}, {\bfseries\itshape Journal of Mathematical Logic}, vol.~11 (1), 2011, pp.~1127. \end{thebibliography} 
17:50  Model theory of bounded arithmetic and complexity theory SPEAKER: Michal Garlik ABSTRACT. It is well known that some problems in complexity theory can be cast as problems of constructions of expanded extensions of models of bounded arithmetic. These models are usually required to satisfy some form of bounded induction but at the same time not introduce any new lengths of strings. We shall discuss some general facts and one specific construction of this kind. 
18:10  Weak Arithmetical Semantics for the Logic of Proofs SPEAKER: Thomas Studer ABSTRACT. Artemov established an arithmetical interpretation for the Logics of Proofs LP(CS), which yields a classical provability semantics for the modal logic S4. These Logics of Proofs are parameterized by socalled constant specifications CS that state which axioms can be used in the reasoning process, and the arithmetical interpretation relies on the constant specifications being finite. In our paper, we remove this restriction by introducing weak arithmetical interpretations that are sound and complete for a wide class of constant specifications, including infinite ones. In particular, they interpret the full Logic of Proofs LP. 
16:30  Boolean algebras and degrees of autostability relative to strong constructivizations SPEAKER: Nikolay Bazhenov ABSTRACT. Let $\mathbf{d}$ be a Turing degree. A computable structure $\mathfrak{A}$ is {\itshape $\mathbf{d}$autostable} if, for every computable structure $\mathfrak{B}$ isomorphic to $\mathfrak{A}$, there exists a $\mathbf{d}$computable isomorphism from $\mathfrak{A}$ onto $\mathfrak{B}$. A decidable structure $\mathfrak{A}$ is {\itshape $\mathbf{d}$autostable relative to strong constructivizations} if every decidable copy $\mathfrak{B}$ of $\mathfrak{A}$ is $\mathbf{d}$computably isomorphic to $\mathfrak{A}$. Let $\mathfrak{A}$ be a computable structure. A Turing degree $\mathbf{d}$ is called the {\itshape degree of autostability} of $\mathfrak{A}$ if $\mathbf{d}$ is the least degree such that $\mathfrak{A}$ is $\mathbf{d}$austostable. A degree $\mathbf{d}$ is the {\itshape degree of autostability relative to strong constructivizations} ({\itshape degree of $SC$autostability}) of a decidable structure $\mathfrak{A}$ if $\mathbf{d}$ is the least degree such that $\mathfrak{A}$ is $\mathbf{d}$autostable relative to strong constructivizations. Note that here we follow~\cite{Goncharov11} and use the term {\itshape degree of autostability} in place of {\itshape degree of categoricity}. A great number of works (see, e.g.,~\cite{FKM10,CFS13,Bazhenov13}) uses the term {\itshape degree of categoricity}. \begin{theorem} Let $\alpha$ be a computable ordinal. (1)\ $\mathbf{0}^{(\alpha)}$ is the degree of autostability of some computable Boolean algebra; (2)\ $\mathbf{0}^{(\alpha)}$ is the degree of $SC$autostability of some decidable Boolean algebra. \end{theorem} Using the results of~\cite{CFS13}, we obtain the following corollaries. \begin{corollary} There exists a decidable Boolean algebra without degree of $SC$au\to\sta\bi\li\ty. \end{corollary} \begin{corollary} The index set of decidable Boolean algebras with degrees of $SC$autostability is $\Pi^1_1$complete. \end{corollary} This work was supported by RFBR (grant 140100376), and by the Grants Council (under RF President) for State Aid of Leading Scientific Schools (grant NSh860.2014.1). \begin{thebibliography}{10} \bibitem{Goncharov11} {\scshape S. S. Goncharov}, {\itshape Degrees of Austostability Relative to Strong Constructivizations}, {\bfseries\itshape Proceedings of the Steklov Institute of Mathematics}, vol.~274 (2011), no.~1, pp.~105115. \bibitem{FKM10} {\scshape E. B. Fokina, I. Kalimullin, R. Miller}, {\itshape Degrees of Categoricity of Computable Structures}, {\bfseries\itshape Archive for Mathematical Logic}, vol.~49 (2010), no.~1, pp.~5167. \bibitem{CFS13} {\scshape B. F. Csima, J. N. Y. Franklin, R. A. Shore}, {\itshape Degrees of Categoricity and the Hyperarithmetic Hierarchy}, {\bfseries\itshape Notre Dame Journal of Formal Logic}, vol.~54 (2013), no.~2, pp.~215231. \bibitem{Bazhenov13} {\scshape N. A. Bazhenov}, {\itshape Degrees of Categoricity for Superatomic Boolean Algebras}, {\bfseries\itshape Algebra and Logic}, vol.~52 (2013), no.~3, pp.~179187. \end{thebibliography} 
16:50  The $ \Delta^{0}_{\alpha} $dimension of computable structures SPEAKER: Pavel Alaev ABSTRACT. Let $ \alpha \geqslant 1 $ be a computable ordinal and $ {\mathfrak A} $ be a computable structure. The $ \Delta^{0}_{\alpha} $dimension of $ {\mathfrak A} $ is maximal $ n \leqslant \omega $ such that there exist $ n $ computable presentations of $ {\mathfrak A} $ without any $ \Delta^{0}_{\alpha} $ isomorphism between them. $ {\mathfrak A} $ is $ \Delta^{0}_{\alpha} $categorical if this dimension is 1. In \cite {Ash87}, it was noted that if $ {\mathfrak A} $ has a $ \Sigma^{0}_{\alpha} $ Scott family then it is $ \Delta^{0}_{\alpha} $categorical. Moreover, a set of conditions $ \Phi ({\mathfrak A}) $ was found, under which this sufficient condition becomes necessary: if $ \Phi ({\mathfrak A}) $ holds then $ {\mathfrak A} $ has a $ \Sigma^{0}_{\alpha} $ Scott family iff it is $ \Delta^{0}_{\alpha} $categorical. We prove that under a similar set of conditions $ \Phi' ({\mathfrak A}) $, this equivalence also holds, and, in addition, the $ \Delta^{0}_{\alpha} $dimension of $ {\mathfrak A} $ is $ 1 $ or $ \omega $. The main part of this result is the theorem below. In addition, we fix a small error in the original formulation of $ \Phi ({\mathfrak A}) $. If $ \bar {a}, \bar {b} $ are tuples in $ {\mathfrak A} $ of the same length, then $ \bar {a} \leqslant_{\alpha} \bar {b} $ means that every infinite $ \Pi_{\alpha} $ formula true on $ \bar {a} $ is true on $ \bar {b} $. $ {\mathfrak A} $ is $ \alpha $friendly if the relations $ \leqslant_{\beta} $ are c.e.\ uniformly in $ \beta < \alpha $. Let $ \Rightarrow $ be a binary relation on finite tuples in $ {\mathfrak A} $. We define a relation $ \text {{\rm Free}}^{\Rightarrow}_{\alpha} (\bar {a}, \bar {c}) $ on tuples in $ {\mathfrak A} $ as follows: $$ \forall \beta \,{<}\, \alpha \,\, \forall \bar {a}_{1} \,\, \exists \bar {a}' \,\, \exists \bar {a}'_{1} \,\, \bigl[\: \bar {a} = \bar {a}' \text {, }\,\, \bar {c}, \bar {a}, \bar {a}_{1} \leqslant_{\beta} \bar {c}, \bar {a}', \bar {a}'_{1} \text {, } \, \text {and} \,\, \bar {c}, \bar {a} \not\Rightarrow \bar {c}, \bar {a}' \: \bigl] \text {.} $$ If $ \Rightarrow $ is $ \geqslant_{\alpha} $ then this definition coincides with the one in \cite {Ash87}. {\bf Theorem}. Let $ {\mathfrak A} $ be a computable $ \alpha $friendly structure. Suppose that $ \Rightarrow $ is a relation on finite tuples in $ {\mathfrak A} $ such that \\ {\rm a)} $ \Rightarrow $ is transitive, i.e., $ \bar {a} \Rightarrow \bar {b} $ and $ \bar {b} \Rightarrow \bar {c} $ imply $ \bar {a} \Rightarrow \bar {c} $; \\ {\rm b)} if $ g : {\mathfrak A} \to {\mathfrak A} $ is an automorphism then $ \bar {a} \Rightarrow g (\bar {a}) $ for every $ \bar {a} $ in $ {\mathfrak A} $. \\ If the relation $ \not\Rightarrow $ is c.e.\ and for every $ \bar {c} $ in $ {\mathfrak A} $, we can effectively find $ \bar {a} $ s.t.\ $ \text {{\rm Free}}^{\Rightarrow}_{\alpha} (\bar {a}, \bar {c}) $, then there exists a computable sequence $ \{ {\mathfrak B}_{i} \}_{i \in \omega} $ of computable presentations of $ {\mathfrak A} $ s.t.\ there is no $ \Delta^{0}_{\alpha} $ isomorphism between $ {\mathfrak B}_{i} $ and $ {\mathfrak B}_{j} $ for $ i \neq j $. \begin{thebibliography}{10} \bibitem {Ash87} {\scshape C.J.\ Ash}, {\itshape Categoricity in hyperarithmetical degrees}, {\bfseries\itshape Annals of Pure and Applied Logic}, vol.~34 (1987), no.~1, pp.~114. \end{thebibliography} 
17:10  On categoricity of scattered linear orders SPEAKER: unknown ABSTRACT. We consider the categoricity of countable scattered linear orders. Recall that linear order is \emph{scattered} if it has no dense suborder. A computable linear order $L$ is \emph{computably ($\Delta^0_n$, resp.) categorical} if for every computable copy $L'$ of $L$ there is a computable ($\Delta^0_n$, resp.) isomorphism between $L'$ and $L$. J.~Remmel, S. Goncharov, V. Dzgoev obtained the description of computably categorical linear orders. Namely, they proved that a computable linear order is computably categorical if and only if it contains finitely many pairs of successors. Ch. McCoy} obtained the description of $\Delta^0_2$categorical computable linear order with additional conditions. We proved that if $L$ is a computable scattered linear order such that $L$ is a finite sum of scattered orders of rank $n$ then $L$ is $\Delta^0_{2n}$categorical. 
17:30  A DNC function that computes no effectively biimmune set SPEAKER: Achilles Beros ABSTRACT. In Diagonally NonComputable Functions and BiImmunity, Carl Jockusch and Andrew LewisPye proved that every DNC function computes a biimmune set. They asked whether every DNC function computes an effectively biimmune set. Several attempts have been made to solve this problem in the last few years. We construct a DNC function that computes no effectively biimmune set, thereby answering their question in the negative. We obtain a few corollaries that illustrate how our technique can be applied more broadly. 
17:50  Integervalued randomness and degrees SPEAKER: Michael McInerney ABSTRACT. Analysing betting strategies where only integer values are allowed, perhaps for a given set F, gives an interesting variant on algorithmic randomness where category and measure intersect. We build on earlier work of Bienvenu, Stephan, and Teutsch, and study reals random in this sense, and their intricate relationship with the c.e. degrees. This is joint work with George Barmpalias and Rod Downey. 
18:10  Effective genericity and differentiable functions SPEAKER: Rutger Kuyper ABSTRACT. Recently, connections between differentiability and various notions of effective randomness have been studied. These results are typically of the form ``x in [0,1] is random if and only if every function f in C is differentiable at x,'' where C is some subclass of the computable functions; for example, Brattka, Miller and Nies gave such characterisations for computable and MartinLöf randomness. In this talk we will present a complementary result for effective genericity. More precisely, our result says that x in [0,1] is 1generic if and only if every differentiable computable function has continuous derivative at x. This result can be seen as an effectivisation of a result by Bruckner and Leonard. This talk is based on joint work with Sebastiaan Terwijn. 
16:30  On $\Sigma^0_2$initial segments of computable linear orders SPEAKER: Ravil Bikmukhametov ABSTRACT. We consider the complexity of initial segments of computable linear orders. We prove that $\Sigma^0_2$initial segments of computable linear orders contain in total all computable linear orders without the greatest elements and all $\Sigma^0_2$degrees. 
16:50  A nonuniqueness theorem for jumps of principal ideals SPEAKER: unknown ABSTRACT. We show that for every degree u REA in 0', there is a pair a_0,a_1 of distinct r.e. degrees such that (a_0)' = u = (a_1)', and such that the set {x' : x <= a_0}, which consists of all jumps of sets Turingbelow a_0, is equal to the corresponding set {x' : x <= a_1}. This defeats certain approaches to proving the rigidity of the r.e. degrees. 
17:10  Every nonzero honest elementary degree has the cupping property SPEAKER: Paul Shafer ABSTRACT. If a < b are elements of a lattice, then we say that a cups to b if there is a c < b such that a + c = b. Kristiansen proves that if a < b in the lattice of honest elementary degrees and a is significantly above 0 (that is, there is a function elementary in a that majorizes every elementary function), then a cups to b. We improve this result by relaxing the restriction that a is significantly above 0 to simply that a is nonzero: if a and b are honest elementary degrees with 0 < a < b, then a cups to b. This answers a question of Kristiansen. 
17:30  Degree spectra of relations on a cone SPEAKER: Matthew HarrisonTrainor ABSTRACT. We consider structures $\mathcal{A}$ with an additional relation $R$. We say that two relations $R$ and $S$ on structures $\mathcal{A}$ and $\mathcal{B}$ respectively have the same (relativised) degree spectrum if, for sets $C$ on a cone above \textbf{d}, \[ \{R^{\tilde{\mathcal{A}}} \oplus C : \tilde{\mathcal{A}} \cong \mathcal{A} \text{ and } \tilde{\mathcal{A}} \leq_T C \} = \{S^{\tilde{\mathcal{B}}} \oplus C : \tilde{\mathcal{B}} \cong \mathcal{B} \text{ and } \tilde{\mathcal{B}} \leq_T C \}. \] Using determinacy, these degree spectra are partially ordered. Many classes of degrees which relativise, such as the $\Sigma^0_\alpha$ degrees or $\alpha$CEA degrees, are degree spectra. This is a notion which captures solely the modeltheoretic properties of the relation $R$. We will advocate for the naturality of this viewpoint by recasting existing results in this new language, giving new results, and putting forward new questions. Existing results of Harizanov in show that there are two minimal degree spectra, the computable sets and the c.e.\ sets. Ash and Knight considered whether Harizanov's results could be generalised. We give a partial positive answer by showing that any degree spectrum which contains a non$\Delta^0_2$ degree contains all of the 2CEA degrees. We also give an example of two incomparable degree spectra. 
17:50  $\Delta_2^0$spectra of linear orderings SPEAKER: Andrey Frolov ABSTRACT. In \cite{nonlown}, for any $n\ge 2$, it was constructed a linear ordering $L$ such that the spectrum $Sp(L)$ contains exactly all nonlow$_n$ degrees. Recall, the {\it spectrum} of a linear ordering $L$ is the class $Sp(L) = \{\deg_T(R) \mid R \cong L\}$. R. Miller \cite{Miller} constructed a linear ordering whose $\Delta_2^0$spectrum contains exactly all nonlow$_0$ $\Delta_2^0$degrees, i.e., all nonzero $\Delta_2^0$degrees. The {\it $\Delta_2^0$spectrum} of linear ordering $L$ is the class $Sp(L)^{\Delta_2^0} = \{\deg_T(R) \in \Delta_2^0 \mid R \cong L\} = Sp(L) \cap \Delta_2^0$. The author \cite{Fr1} constructed a linear ordering whose $\Delta_2^0$spectrum contains exactly all nonlow$_1$ $\Delta_2^0$degrees. In \cite{nonlown}, for any $n\ge 2$, it was constructed a linear ordering $L$ such that $Sp(L)$ contains exactly all high$_n$ degrees. Also in \cite{nonlown} it was remarked that there does not exist a linear orderings $L$ such that $Sp(L)$ is exactly all high$_n$ degrees for $n \in \{0, 1\}$. \begin{theorem} There exists a linear ordering $L$ such that $Sp^{\Delta_2^0}(L) = \{\mathbf{0}'\}$. In other words, $\Delta_2^0$spectrum of $L$ contains exactly all high$_0$ $\Delta_2^0$degrees. \end{theorem} \begin{theorem} There exists a linear ordering whose $\Delta_2^0$spectrum contains exactly all high$_1$ $\Delta_2^0$degrees. \end{theorem} \begin{thebibliography}{9} \bibitem{Fr1} {\scshape A.~Frolov}, {\itshape $\Delta_2^0$copies of linear orderings}, {\bfseries\itshape Algebra and Logic}, vol.~45 (2006), no.~3, pp.~201209 (in english), pp.~6975 (in russian). \bibitem{nonlown} {\scshape A.~Frolov, V.~Harizanov, I.~Kalimullin, O.~Kudinov, R.~Miller}, {\itshape Spectra of high$_n$ and nonlow$_n$ degrees}, {\bfseries\itshape Journal of Logic and Computation}, vol.~22 (2012), no.~4, pp.~745754. \bibitem{Miller} R.~Miller, {\scshape R.~Miller}, {\itshape The $\Delta_2^0$ spectrum of a linear ordering}, {\bfseries\itshape Journal of Symbolic Logic}, vol.~66 (2001), no.~2, pp.~470486. \end{thebibliography} 
18:10  Degree spectra of structures under $\Sigma_n$equivalence. SPEAKER: Pavel Semukhin ABSTRACT. The properties of degree spectra of countable structures have been studied extensively in computable model theory. Recently Andrews and Miller [1] introduced and studied a notion of the degree spectra of a theory which is defined as DegSp(T) = {Deg(M)  M is a model of T}. In particular, they constructed a theory whose spectrum is equal to a nondegenerate union of two cones, which is known to be impossible for a degree spectrum of a structure. In our work we consider an analogous question for $\Sigma_n$spectrum of a structure. We say two structures A and B are $\Sigma_n$equivalent, if they satisfy the same $\Sigma_n$sentences. Let A be a countable structure. The $\Sigma_n$spectrum of A is defined as the set {Deg(B)  B is $\Sigma_n$equivalent to A}$. The construction from [1] actually implies that there is a structure $A$ such that $\Sigma_2$spectrum of A is equal to a nondegenerate union of two cones. We show that this result does not hold anymore if we replace $\Sigma_2$equivalence by $\Sigma_1$equivalence. Theorem. Let A be a countable structure. Then $\Sigma_1$spectrum of A cannot be equal to a nondegenerate union of two cones. We also discuss other properties of $\Sigma_n$spectra and related open question. [1] Uri Andrews, Joseph S. Miller, Spectra of theories and structures, to appear in the Proceedings of the American Mathematical Society. 
16:30  Effective results on the asymptotic behavior of nonexpansive iterations SPEAKER: Laurentiu Leustean ABSTRACT. This talk reports on an application of proof mining to the asymptotic behavior of Ishikawa iterations for nonexpansive mappings \cite{Leu14,Leu10}. {\em Proof mining} is a paradigm of research concerned with the extraction, using prooftheoretic methods, of finitary content from mathematical proofs. This research direction can be related to Terence Tao's proposal \cite{Tao07} of {\em hard analysis}, based on finitary arguments, instead of the infinitary ones from {\em soft analysis}. We present uniform effective rates of asymptotic regularity for the Ishikawa iteration associated to nonexpansive selfmappings of convex subsets of uniformly convex Busemann geodesic space. We show that these results are obtained by a logical analysis of an asymptotic regularity proof due to Tan and Xu \cite{TanXu93}, consisting of two main steps: the first one with a classical proof, analyzed using the combination of monotone functional interpretation and negative translation, while the second one has a constructive proof, analyzed more directly using monotone modified realizability. As a consequence, our results are guaranteed by a combination of logical metatheorems for classical and semiintuitionistic systems, proved by Gerhardy and Kohlenbach \cite{GerKoh06,GerKoh08} for different classes of spaces and adapted to uniformly convex Busemann spaces in \cite{Leu14}. \begin{thebibliography}{10} \bibitem{GerKoh06} {\scshape P. Gerhardy, U. Kohlenbach}, {\itshape Strongly uniform bounds from semiconstructive proofs}, {\bfseries\itshape Annals of Pure and Applied Logic}, vol.~141 (2006), pp.~89107. \bibitem{GerKoh08} {\scshape P. Gerhardy, U. Kohlenbach}, {\itshape General logical metatheorems for functional analysis}, {\bfseries\itshape Transactions of the American Mathematical Society}, vol.~360 (2008), pp.~26152660. \bibitem{Leu10} {\scshape L. Leu\c{s}tean}, {\itshape Nonexpansive iterations in uniformly convex $W$hyperbolic spaces}, {\bfseries\itshape Nonlinear Analysis and Optimization I: Nonlinear Analysis} (A. Leizarowitz, B. S. Mordukhovich, I. Shafrir, A. Zaslavski, editors), Amer. Math. Soc., Providence, RI, 2010, pp.~193209. \bibitem{Leu14} {\scshape L. Leu\c{s}tean}, {\itshape An application of proof mining to nonlinear iterations}, {\bfseries\itshape arXiv:1203.1432v1 [math.FA]}, 2012; accepted for publication in Annals of Pure and Applied Logic. \bibitem{TanXu93} {\scshape K.K. Tan, H.K. Xu}, {\itshape Approximating fixed points of nonexpansive mappings by the Ishikawa iteration process}, {\bfseries\itshape J. Math. Anal. Appl.}, vol.~178 (1993), pp.~301308. \bibitem{Tao07} {\scshape T. Tao}, {\itshape Soft analysis, hard analysis, and the finite convergence principle}, 2007, available on terrytao.wordpress.com/2007/05/23/soft//analysishardanalysisandthefiniteconvergenceprinciple/. \end{thebibliography} 
16:50  Pi_1 induction axioms vs Pi 1 induction rules 
17:10  Reverse mathematics of WQOs and Noetherian spaces SPEAKER: Alberto Marcone ABSTRACT. This work in progress is joint with Emanuele Frittaion, Matthew Hendtlass, Paul Shafer, and Jeroen Van der Meeren. If $(Q,{\leq_Q})$ is a quasiorder we can equip $Q$ with several topologies. We are interested in the Alexandroff topology $A(Q)$ (the closed sets are exactly the downward closed subsets of $Q$) and the upper topology $u(Q)$ (the downward closures of finite subsets of $Q$ are a basis for the closed sets). $A(Q)$ and $u(Q)$ are (except in trivial situations) not $T_1$, yet they reflect several features of the quasiorder. For example, $(Q,{\leq_Q})$ is a well quasiorder (WQO: wellfounded and with no infinite antichains) if and only if $A(Q)$ is Noetherian (all open sets are compact or, equivalently, there is no strictly descending chain of closed sets). Moreover, if $(Q,{\leq_Q})$ is WQO then $u(Q)$ is Noetherian. Given the quasiorder $(Q,{\leq_Q})$, we consider two natural quasiorders on the powerset $\mathcal{P}(Q)$: \begin{align*} A \leq^\flat B \iff & \forall a \in A\, \exists b \in B\, a \leq_Q b; \\ A \leq^\sharp B \iff & \forall b \in B\, \exists a \in A\, a \leq_Q b. \end{align*} We write $\mathcal{P}^\flat(Q)$ and $\mathcal{P}^\sharp(Q)$ for the resulting quasiorders, and $\mathcal{P}_f^\flat(Q)$ and $\mathcal{P}_f^\sharp(Q)$ for their restrictions to the collection of finite subsets of $Q$. GoubaultLarrecq proved that if $(Q,{\leq_Q})$ is WQO then $u(\mathcal{P}^\flat(Q))$ and $u(\mathcal{P}_f^\sharp (Q))$ are Noetherian, even though $\mathcal{P}^\flat(Q)$ and $\mathcal{P}_f^\sharp (Q)$ are not always WQOs. We study these theorems and some of their consequences from the viewpoint of reverse mathematics, proving for example: \begin{itemize} \item over $\mathsf{RCA}_0$, $\mathsf{ACA}_0$ is equivalent to each of \lq\lq if $(Q,{\leq_Q})$ is WQO then $u(\mathcal{P}^\flat(Q))$ is Noetherian\rq\rq, and \lq\lq if $(Q,{\leq_Q})$ is WQO then $A(\mathcal{P}_f^\flat(Q))$ is Noetherian\rq\rq; \item $\mathsf{ACA}_0$ proves \lq\lq if $(Q,{\leq_Q})$ is WQO then $u(\mathcal{P}_f^\sharp(Q))$ is Noetherian\rq\rq, yet $\mathsf{WKL}_0$ does not. \end{itemize} 
17:30  A characterization for diagonalizedout objects SPEAKER: Saeed Salehi ABSTRACT. Cantor's Diagonal Argument came out of his third proof for the uncountability of the set of real numbers (see e.g. \cite{franks}). Unlike the first and second proofs, the diagonal argument can also show the nonequinumerosity of a set with its powerset. In modern terms the proof is as follows: for a function $F\!:\!A\!\rightarrow\!\mathscr{P}(A)$, where $\mathscr{P}(A)\!=\!\{B\mid B\subseteq A\}$ is the powerset of $A$, the antidiagonal set $D_F=\{a\!\in\!A\mid a\not\in F(a)\}$ is not in the range of $F$ because if it were, say $D_F=F(\alpha)$, then $\alpha\!\in\!D_F\leftrightarrow \alpha\not\in F(\alpha)\leftrightarrow\alpha\not\in D_F$ contradiction. This argument shows up also in Russell's Paradox, the set of sets which do not contain themselves, $R=\{x\mid x\not\in x\}$, and in Turing's nonrecursivelyenumerable set $\overline{K}=\{n\in \mathbb{N}\mid n\not\in W_n\}$ where $W_n$ is the domain of the $n^{\rm th}$ recursive function $\varphi_n$ (i.e., $W_n=\{x\!\in\!\mathbb{N}\mid \exists y: \varphi_n(x)=y\}$) by which one can show the algorithmic unsolvability of the halting problem (of a given algorithm on a given input). There are, in fact, many other instances of the diagonal arguments in wide areas of mathematics from logic and set theory to computability theory and theory of computational complexity. In this talk, we examine this argument in more detail and discuss some other proofs (e.g. \cite{raja1,raja2}) of Cantor's theorem (on the nonequinumerosity of a set with its powerset). By introducing a generalized diagonal argument, we show that all other proofs should fit in this generalized form, which is roughly as follows: for a function $g:A\rightarrow A$ the generalized antidiagonal set $D_F^g=\{g(a)\mid g(a)\not\in F(a) \}$ is not in the range of $F$ because if it were, say $D_F^g=F(\alpha)$, then $g(\alpha)\in D_F^g\leftrightarrow g(\alpha)\not\in F(\alpha) \leftrightarrow g(\alpha)\not\in D_F^g$ contradiction. For the argument to go through, the function $g$ should satisfy some conditions; and we will prove that every subset of $A$ (say $B\subseteq A$) that is not in the range of $F$ (for all $a\in A$, $B\not=F(a)$ holds) should somehow be in this generalized antidiagonal form ($B\cap g[A]=D_F^g$) for some suitable function $g$ which satisfies those conditions; cf. \cite{dekker,horowitz}. We will argue that this provides a characterization for diagonal proofs and indeed characterizes the objects whose existence are proved by a kind of diagonal(izing out) argument. \bibitem{dekker}{\scshape Jacob C. E. Dekker}, {\itshape Productive Sets}, {\bfseries\itshape Transactions of the American Mathematical Society}, vol.~78 (1955), no.~1, pp.~129149. \bibitem{franks}{\scshape John Franks}, {\itshape Cantor's Other Proofs that $\mathbb{R}$ is Uncountable}, {\bfseries\itshape Mathematics Magazine}, vol.~83 (2010), no.~4, pp.~283289. \bibitem{horowitz}{\scshape Bruce M. Horowitz}, {\itshape Sets Completely Creative via Recursive Permutations}, {\bfseries\itshape Zeitschrift f\"{u}r Mathematische Logik und Grundlagen der Mathematik}, vol.~24 (1978), no.~2530, pp.~445452. \bibitem{raja1}{\scshape Natarajan Raja}, {\itshape A NegationFree Proof of Cantor's Theorem}, {\bfseries\itshape Notre Dame Journal of Formal Logic}, vol.~46 (2005), no.~2, pp.~231233. \bibitem{raja2}{\scshape Natarajan Raja}, {\itshape Yet Another Proof of Cantor's Theorem}, {\bfseries\itshape Dimensions of Logical Concepts} (JeanYves B\'{a}ziau and Alexandre CostaLeite, editors), Cole\c{c}\~{a}o CLE: Volume 54, Campinas, Brazil, 2009, pp.~209217. 
17:50  Some applications of the Arithmetized Completeness Theorem to secondorder arithmetic SPEAKER: Tin Lok Wong ABSTRACT. Goedel's Completeness Theorem is one of the most fundamental results in mathematical logic. When formalized in arithmetic, it is often referred to as the Arithmetized Completeness Theorem (ACT). The ACT is a surprisingly powerful machinery for constructing nonstandard models of arithmetic. For instance, it has been known [1, 2] that "all possible kinds" of extensions of a model of Peano arithmetic can, in a sense, be realized using the ACT. We find new applications of the ACT in the context of secondorder arithmetic. These include an alternative proof of Harrington's theorem [3] that WKL0 is Pi11conservative over RCA0. [1] Kenneth Mc Aloon, Completeness theorems, incompleteness theorems and models of arithmetic, Transactions of the American Mathematical Society, vol. 239 (1978), pp. 253277. [2] James H. Schmerl, End extensions of models of arithmetic, Notre Dame Journal of Formal Logic, vol. 33 (1992), no. 2, pp. 216219. [3] Stephen G. Simpson, Subsystems of Second Order Arithmetic, Perspectives in Logic, Cambridge University Press, 2009. 
18:10  Some properties of Intuitionistic Set Theory with the principle UP. SPEAKER: Alexey Vladimirov ABSTRACT. Some properties of Intuitionistic Set Theory with the principle UP. Let ZFI2C be usual intuitionistic ZermeloFraenkel set theory in twosorted language (where sort 0 is for natural numbers, and sort 1 is for sets). Axioms and rules of the system are: all usual axioms and rules of intuitionistic predicate logic,intuitionistic system of arithmetic,and all usual proper axioms and schemes of ZermeloFraenkel set theory for variables of sort 1,namely, axioms of Extensionality, Infinity, Pair, Union, Power set, Infinity, and schemes: Separation, Transfinite Induction as Regularity, and Collection as Substitution. It is wellknown that both ZFI2C and ZFI2C+DCS(where DCS is a wellknown principle Double Complements of Sets) have some important effectivity properties: disjunction property, numerical existence property (but not full existence property!) and also that the Markov Rule,the Church Rule,and the Uniformization Rule are admissible in it. Such reach collection of properties shows that these theories are sufficiently constructive theories. On the other hand, ZFI2C+ DCS contains the classical theory ZFI2C = ZFI2C+LEM) in the sense of Godel negative translation. Moreover, a lot of important mathematical reasons may be formalized in ZFI2C+DCS, so,we can formalize and decide in it a lot of informal problems about transformation of a classical reason into intuitionistical proof and extraction of some exact description of a mathematical object from some proof of it`s existence. So, the theory ZFI2C+DCS can be considered as a basic system of Intuitionistic Set Theory. We can extend it by a some wellknown intuitionistic principles, such that Markov Principle M, Extended Church Principle ECT, and the Principle UP. It is wellknown that both theories ZFI2C+DCS+M+ECT, and ZFI2C+DCS+M has the same effectivity properties as ZFI2C+DCS. It is known also that ZFI2C+DCS+M+ECT is conservative over the theory ZFI2C+DCS+M w.r.t. the class A.E.N. of all AEformulae over arithmetical negative (in the usual sense). We also prove that ZFI2C+M+ ECT is conservative over the theory ZFI2C+M. The Principle UP is a wellknown specifical intuitionistic principle. It claims that we cannot define effectivly nontrivialfunction from sets to natural numbers.It has been studed in intuitionistic type theory very closely. In the article we prove that ZFI2C+ DCS+ M+ CT+UP is conservative over the theory ZFI2C+DCS+M w.r.t. the same class A.E.N. Of course, we also prove that ZFI2C+M+ECT is conservative over the theory ZFI2C+M w.r.t. of the same class A.E.N. We also prove that theories ZFI2C+DCS+M+CT+UP, ZFI2C+DCS+M+UP, ZFI2C+ DCS+ UP, and ZFI2C+UP have the same effectivity properties as ZFI2C and ZFI2C+DCS. 
16:30  The complexity of computably enumerable graphs SPEAKER: Luca San Mauro ABSTRACT. In recent literature, the theory of computably enumerable equivalence relations (ceers) has been widely investigated (see, for instance, [1], [2]). One of the most fruitful approaches is to study them considering the degree structure generated by the following reducibility: Given two ceers R and S, we say that R is reducible to S (R<S) if there is a computable function f s.t., for every x,y, xRy iff f(x)Sf(y). In this talk, we propose to make use of this reducibility within a more general context than that of ceers, namely in the study of (simply undirected) c.e. graphs. Our presentation is divided in two parts. Firstly, we focus on computable graphs. While the theory of computable equivalence relations is quite trivial [1], in this context the situation is more complicate. We provide a partial characterization for the computable case. Secondly, we move to universal graphs. We offer a natural, yet not trivial, example of an universal graph U. More generally, recall that there is a unique random graph RG s.t. every countable graph G can be embedded as an induced subgraph of RG ([3]). This fact depends on a specific property (*) of RG (see [3]) for the definition of (*). Hence, it is natural to ask for some analogue of (*) in our context  specially after noticing that (*) fails for U. We discuss several candidates for this role. [1] U. Andrews, S. Lempp, J. S. Miller, K. M. Ng, L. San Mauro, A. Sorbi, Universal computably enumerable equivalence relations, Journal of Symbolic Logic, to appear [2] S. Gao, P. Gerdes, Computably Enumerable Equivalence Relations, Studia Logica, February 2001, Volume 67, Issue 1, pp 2759 vol.~67 (2001), no.~1, pp.2759. [3] P. Cameron, The random graph, The Mathematics of Paul Erd\"os, II (2nd ed.)} (R. L. Graham, J. Nešetřil and S. Butler, ed.), Springer, Publisher's address, 2013, pp.353378. 
16:50  The order dimensions of degree structures SPEAKER: Kojiro Higuchi ABSTRACT. We investigate the order dimensions of several degree structures such as Turing degree structure. It may be nice if we can decompose a given degree structure into "simpler" partial orders naturally defined for the structure. Indeed, it is known that every partial order is embeddable into the product order of a family of linear orders. The order dimension of a given partial order is defined as the least cardinality of such a family. Thus, the order dimension of a degree structure tells us how many linear orders at least we should have so that the degree structure is embeddable into the product order of those linear orders. The concept "order dimension" was introduced by Dushnik and Miller in 1941, and it is also called DushnikMiller dimension. As our main results on the order dimensions of degree structures, this talk includes the following results: the order dimension of Turing degree structure is uncountable and at most the cardinality of the continuum; the order dimension of Muchnik degree structure is the cardinality of the continuum; and the order dimension of Medvedev degree structure is lying between the cardinality of the continuum and the cardinality of the power set of the continuum. 
17:10  Computable numberings in Ershov hierarchy SPEAKER: Sergey Ospichev ABSTRACT. The talk will cover some recent results about computable numberings in Ershov hierarchy 
17:30  Daviestrees in infinite combinatorics SPEAKER: Daniel Tamas Soukup ABSTRACT. Daviestrees are special sequences of countable elementary submodels which played important roles in generalizing arguments using the Continuum Hypothesis to pure ZFC proofs. The most notable application of this technique is probably Jackson and Mauldin's solution to the Steinhaus tiling problem. The aim of this talk is to introduce Daviestrees and to point out several new applications in infinite combinatorics. Such include simple proofs to the following results: the plane is the union of n+2 "clouds" provided that the continuum is at most aleph_n; every uncountably chromatic graph contains kconnected uncountably chromatic subgraphs for each finite k (both results are due to Komjath). Our belief is that Daviestrees did not get their well deserved attention despite the fact that they provide an easily applicable tool for logicians and set theorists. 
17:50  A descriptive set theoretical axiomatization of the Mathias model. SPEAKER: Wojciech Stadnicki ABSTRACT. We investigate a series of axioms, which capture the combinatorial core of the Mathias model. These axioms are formulated in terms of games with Borel sets and functions, without explicitly refering to forcing. In this way we derive a descriptive set theoretical axiomatization of the Mathias model. We consider some properties of this model, in particular values of cardinal coefficients. We derive them directly from our axioms. Although we concentrate on the Mathias model, our methods are more general. One can produce an analogous axiomatization of other models obtained by the iteration of suitably definable proper forcing. 
18:10  Restricting Martin's axiom to a ccc ground model SPEAKER: Miha Habič ABSTRACT. We introduce a variant of Martin's axiom, called the grounded Martin's axiom or grMA. This principle asserts that the universe is a ccc forcing extension and that MA holds for posets from the ground model. The new axiom, which emerges naturally from the analysis of the SolovayTennenbaum proof of the consistency of MA, is shown to have many of the desirable properties of the weaker fragments of MA. In particular, we show that grMA is consistent with a singular continuum and also that it is consistent with the left side of Cichoń's diagram collapsing to omega_1. We also show that grMA is better behaved than MA when adding generic reals. Specifically, grMA is preserved under adding a Cohen real and holds after adding a random real to a model of MA. 
16:30  Elementary epimorphisms between models of set theory SPEAKER: unknown ABSTRACT. An elementary epimorphism $f : M \rightarrow N$ (between modeltheoretic structures in some language) is a homomorphism such that, for every formula $\phi$ in the language with parameters $n_1, \ldots , n_k$ from $N$ true in $N$, there are $f$preimages $m_1, \ldots , m_k$ of the $n_i$'s such that $\phi(m_1, \ldots , m_k)$ holds in $M$. Here we investigate elementary epimorphisms between models of set theory. We show that the only $\Pi_1$elementary epimorphisms between models of ZF are isomorphisms. In contrast, there are nontrivial $\Sigma_1$elementary epimorphisms, and nontrivial (full) elementary epimorphisms between models of ZFC$^$ (ZFC without Power Set). Furthermore, we study the inverse system induced by the last example, and its inverse limit. Inverse limits do not always exist, and even when they do they might not be the entire thread class, but in this case it is. 
16:50  Generalized Ellentuck spaces and initial Tukey chains of nonppoints SPEAKER: Natasha Dobrinen ABSTRACT. The generic ultrafilter $\mathcal{G}_2$ forced by the partial ordering $\mathcal{P}(\omega\times\omega)/(\mathrm{Fin}\times\mathrm{Fin})$ is a nonppoint which is also not a Fubini product of ppoints, but is a RudinKeisler immediate successor of its projected Ramsey ultrafilter. In \cite{BDR}, it was shown that $\mathcal{G}_2\not\ge_T[\omega_1]^{<\omega}$, and hence is below the maximum Tukey type for ultrafilters, yet it is not basically generated. In \cite{D}, we show that, in fact, $\mathcal{G}_2$ is a Tukey immediate successor of its projected Ramsey ultrafilter, and moreover, the projected Ramsey ultrafilter is the only nonprincipal ultrafilter with Tukey type strictly below that of $\mathcal{G}_2$. This is done by showing that $\mathcal{P}(\omega\times\omega)/(\mathrm{Fin}\times\mathrm{Fin})$ contains a dense subset which in fact forms a topological Ramsey space and then proving a Ramseyclassification theorem for equivalence relations on fronts. Moreover, we generalize this to show that for all $2\le k<\omega$, $\mathcal{P}(\omega^k)/\mathrm{Fin}^{\otimes k}$ is forcing equivalent to a new topological Ramsey space $\mathcal{E}_k$ which is a generalization of the Ellentuck space. The generic ultrafilters $\mathcal{G}_k$ are nonppoints which have exactly $k$ Tukey predecessors, as well as exactly $k$ RudinKeisler predecessors. [BDR] Andreas Blass, Natasha Dobrinen, Dilip Raghavan, The next best thing to a ppint, Submitted. [D] Natasha Dobrinen, High dimensional Ellentuck spaces and initial chains in the Tukey structure of nonppoints, Submitted.

17:10  Coanalytic ideals on $\omega$ SPEAKER: Konstantinos Beros ABSTRACT. We consider a variant of the RudinKeisler order for ideals on $\omega$ and prove the existence of a complete coanalytic ideal with respect this order. The key tool is a parameterization of all coanalytic ideals. We obtain this parameterization via a method which yields a simple proof of Hjorth's 1996 theorem on the existence of a complete coanalytic equivalence relation. Unlike Hjorth's proof, ours does not rely on the use of the effective theory specific to $\Pi^1_1$ sets and thus generalizes under PD to other projective classes. 
17:30  Budding Trees SPEAKER: Sheila Miller ABSTRACT. We define budding trees, show that they form a topological Ramsey space, and discuss applications. 
17:50  Finite Inseparability of Elementary Theories Based on Connection SPEAKER: HsingChien Tsai ABSTRACT. Consider a firstorder language L. For any Lformula alpha, let #alpha stand for the Gödel number of alpha. An Ltheory T is finitely inseparable if and only if there is a recursive function f such that for any two disjoint recursively enumerable sets A and B such that {#alpha: alpha is a valid sentence in L} is included in A and {#alpha: alpha is an Lsentence refuted by some finite model of T} is included in B, f(a, b)does not belong to A union B, where a and b are indices of A and B respectively. It is easy to see that finite inseparability implies undecidability and the former is strictly stronger than the latter. Let C be a binary predicate and I will show the finite inseparability of the theory axiomatized by the following three axioms: (1) For all x (Cxx); (2) For all x, for all y(if Cxy, then Cyx); (3) For all x, for all y(if(Cxy and not x=y), then for some z(Cxz and not Cyz)). Making use of the said result, I will also show the finite inseparability of the theory axiomatized by (1), (2), (4) For all x, for all y (if for all z(Cxz iff Cyz), then x=y) and (5) For any formula alpha, if there is some x such that alpha, then there is some y such that for all z(Cyz iff there is some u such that alpha and Cuz). The foregoing theory contains exactly the mereological part and the quasiBoolean part of Clarke’s system. There is still one more part of Clarke’s system, that is, the quasitopological part. It is still unknown whether the full Clarke’s system is finitely inseparable or not. However, such a system does have finite models and some of them are of a peculiar kind. Based on this observation, I conjecture that the full Clarke’s system is also finitely inseparable. 
16:30  On various strengthenings of the notion of indivisibility SPEAKER: Nadav Meir ABSTRACT. We say a structure M in a first order language L is indivisible if for every colouring of its universe M in two colours, there is a monochromatic substructure M′ ⊆ M such that M′ ≅ M. Additionally, we say that M is symmetrically indivisible if M′ can be chosen to be symmetrically embedded in M (That is, every automorphism of M′ can be can be extended to an automorphism of M), and that M is elementarily indivisible if M′ can be chosen to be an elementary substructure. The notion of indivisibility is a longstudied subject. We will present these strengthenings of the notion, examples and some basic properties. We will define a new "product" of structures which preserves these notions along with other nice properties, and use it to answer some questions presented in [HKO11] regarding the properties and interaction between these notions. In particular: Does elementary indivisibility imply symmetric indivisibility? Is an elementarily indivisible structure neccesarily homogeneous? If M is symmetrically indivisible and L_{0}⊆L, is M reduced to L_{0 }symmetrically indivisible? [HKO11] Assaf Hasson, Menachem Kojman and Alf Onshuus, On symmetric indivisibility of countable structures, Model Theoretic Methods in Finite Combinatorics, AMS, 2011, pp.417–452. 
16:50  An ordinal rank characterising when Forth suffices SPEAKER: Roger Villemaire ABSTRACT. This talk will present a necessary and sufficient condition for Cantor's Forth construction to yield an onto mapping in terms of a new ordinal rank. We will emphasise that the rank is derived from a combination of a smallest and a greatest fixpoint (of monotone operators). We will also highlight the existence of homogeneous structures for all possible countable ordinal ranks, with a construction using unions of wreath powers. 
17:10  Extreme amenability of precompact expansions of countably categorical structures SPEAKER: Alexandre Ivanov ABSTRACT. A group $G$ is called {\bf amenable} if every $G$flow (i.e. a compact Hausdorff space along with a continuous Gaction) supports an invariant Borel probability measure. If every $G$flow has a fixed point then we say that $G$ is {\bf extremely amenable}. Let $M$ be a relational countably categorical structure which is a Fra\"{i}ss\'{e} limit of a Fra\"{i}ss\'{e} class $\mathcal{K}$. To see whether $Aut(M)$ is amenable one usually looks for an expansion $M^*$ of $M$ so that $M^*$ is a Fra\"{i}ss\'{e} structure with extremely amenable $Aut(M^* )$. Moreover it is usually assumed that $M^*$ is a {\bf precompact} expansion of $M$, i.e. every member of $\mathcal{K}$ has finitely many expansions in $Age(M^* )$. Some theorems of O.Angel, A.Kechris, R.Lyone and A.Zucker describe amenability of $Aut(M)$ in this situation. It is a basic question in the subject if there is a countably categorical structure $M$ with amenable automorphism group which does not have expansions as above. We connect this material with the property of existence of nice enumerations, introduced by G.Ahlbrandt and M.Ziegler in 1986. We also give some interesting examples of countably categorical structures $M$ so that $Aut(M)$ is amenable, but $M$ does not have order expansions with extremely amenable automorphism groups. 
17:30  Weak Beth definability property for finite variable fragments. SPEAKER: unknown ABSTRACT. Theorem. Let n > 2. The nvariable fragment of firstorder logic does not have the weak Beth definability property (wBDP). Moreover, there are a theory and a strong implicit definition of a unary relation D for this theory such that there is no explicit definition for D even in the nvariable fragment with infinite conjunctions and disjunctions, not even if we restrict the models to the finite ones. Neither the theory nor the implicit definition use substitution of variables. Failure of wBDP for n = 4 was not known, failure for n greater than 4 was proved by Ian Hodkinson, and for n = 3 by Andras Simon. The present proof is considerably simpler than theirs. Beth definability property fails for the 2variable fragment L2, and it holds for the nvariable fragment if we restrict the sizes of the models to < n + 2 (for all n greater than 1). We conjecture that wBDP holds for L2. If so, L2 is a natural logic distinguishing Beth definability property from wBDP. 
17:50  Nonmonotonic extensions of the weak Kleene clone with constants SPEAKER: Jose MartinezFernandez ABSTRACT. A clone on a set $A$ is a set of finitary functions on $A$ that includes the projection functions and is closed for composition. It is called a clone with constants when it contains all the constant functions on $A$. Every truthfunctional propositional language determines the clone generated by the interpretation of its operator symbols. If we consider propositional languages interpreted with a threevalued truthfunctional scheme, the clones generated by the weak and strong Kleene operators are specially interesting, because Kleene logics have been applied to the study of several fields, like partial predicates, semantical paradoxes, vagueness, the semantics of programming languages, etc. The clone with constants generated by the weak Kleene propositional operators and the constant functions will be called the weak Kleene clone and analogously for the strong Kleene clone. It is well known that the strong Kleene clone coincides with the clone of threevalued functions monotonic on the order of information (i.e., the partial order on ${0,1,2}$ determined by $2\leq 0$, $2\leq 1$). The aim of this paper is to determine all the clones that are extensions of the weak Kleene clone but are not included in the strong Kleene clone. Equivalently, this amounts to the characterization of all the clones that can be obtained when we add to the weak Kleene clone a set of functions that include some function nonmonotonic on the order of information. Using Jablonskij's theorem that determines all threevalued maximal clones and Lau's theorem that characterizes all the threevalued submaximal clones (see \cite{Lau}, II5 and II14), it is easy to check that only two maximal clones ($C_{2}$ and $U_{2}$) and three submaximal clones (one of them being the strong Kleene clone) contain the weak Kleene clone. The paper will determine completely all the clones in the interval between the weak Kleene clone and $U_{2}$ and all the clones between the weak Kleene clone and $C_{2}$ that are not contained in the strong Kleene clone. 
18:10  A sheaf model of randomness SPEAKER: Alex Simpson ABSTRACT. In this talk I will present some properties of the universe of sets from the perspective of a particular sheaf topos, which I call the random topos. This is a boolean topos, hence a model of classical set theory, whose properties make it a natural home for developing a version of probability theory based on random elements. An important feature of the topos is a fundamental notion of independence. This gives rise to a canonical definition of random element: an element (e.g., from the interval [0,1]) is defined to be random if it is contained in all measure 1 subsets that are indpendent of it. This definition can be used to support the development of theories of probability and measure, in which all sets are measurable (though not necessarily Lebesgue measurable), and measures are kappaadditive for any aleph, kappa. (Of course the Axiom of Choice fails, though Dependent Choice holds.) The above results closely mirror work of van Lambalgen from 1992. However, our approach differs from his in two main respects. The first is that our model is a sheaf topos built over a site of probability spaces. Because of this, statements about randomness get translated, by KripkeJoyal semantics in the topos, into statements in standard (Kolmogorovstyle) probability theory. Second, the notion of independence that we use can be understood prior to and separately from the definition of randomness. Independence in our sense corresponds roughly to "no information in common''. In contrast, van Lambalgen's notion of independence has a definition of randomness built into it. 
16:30  A Defense of Information Economy Principle SPEAKER: Hao Cheng Fu ABSTRACT. In our ordinary life it is inevitable for everyone has to adjust one's own belief state in light of new information when the new information is inconsistent with his belief state. Some philosophers such as Quine and AGM (Alchourrόn et al.) suggested that the loss of information value should be minimized as possible whenever one confronts the inconsistency and the principle in belief revision theory is usually socalled information economy principle (IEP for short). Furthermore, Gärdenfors has constructed a model who recommended the idea of epistemic entrenchment to this model to explain why IEP works. But Rott casted some doubts on IEP due to the postulates of epitemic entrenchment proposed by Gärdenfors sometimes failed to realize the features of nonmonotonic reasoning, i.e. it is possible that one might keep the less entrenched beliefs rather than the more ones in the process of belief change. In this paper, I want to present a gametheoretic framework to reconstruct the notion of epistemic entrenchment to avoid the challenges from Rott and prove that IEP is still available to be the norm to estimate the process of belief change. 
16:50  Prospects for a Naive Theory of Classes SPEAKER: Harvey Lederman ABSTRACT. We examine the prospects for a na\"ive theory of classes, in which full ``na\"ive'' comprehension and an extensionality rule are maintained by weakening the background logic. Without extensionality, proving na\"ive comprehension consistent is formally analogous to proving na\"ive truth consistent, and in recent years much progress has been made on the latter question. But there is no natural analog for extensionality in the case of truth, so the question arises whether these logics for reasoning about truth can also be shown consistent with a form of extensionality. In a series of papers, and in his 2006 book (\cite{brady2006}), Ross Brady has presented various theories of na\"ive classes. We begin by providing a simpler, more accessible version of Brady's proof of the consistency of these theories. Our new presentation of Brady then makes it easy to see how Brady's result can be generalized to apply to certain logics which have a modallike semantics given using fourvalued, as opposed to threevalued worlds. (These include some logics from \cite{bacon2013}.) These ``new'' logics have a significant advantage over Brady's original: they validate a weakening rule (indeed, a weakening axiom) for a noncontraposable conditional. Since these laws are crucial if the conditional is to be used for restricted quantification, this is a substantial improvement. Still, we do not think even these logics are satisfactory. The noncontraposable conditional which validates weakening in these logics is not the conditional of the extensionality rule. But there's strong intuitive motivation for the conditional in the extensionality rule to validate weakening. Otherwise, there will be ``sets'' which contain everything, but which are not extensionally equivalent. While Brady's logics (and the fourvalued generalizations) deliver a form of extensionality, in the absence of weakening the formal rule does not capture the intuitive notion of extensionality. 
17:10  On the logical use of implicit contradictions SPEAKER: Antonio Vincenzi ABSTRACT. Some positive applications of the counterexamples of Robinson property on the characterization of Interpolation and Compactness properties 
17:30  Definable topological dynamics and real Lie groups SPEAKER: Grzegorz Jagiella ABSTRACT. Methods of topological dynamics have been introduced to model theory by Newelski and since then saw further development in that field by other authors. Given a model $M$ with all types over $M$ definable and a definable group $G$, we consider the category of definable flows. This category has a universal object $S_G(M)$, the space of types in $G$ over $M$. It is shown that the Ellis semigroup of this flow is isomorphic to $S_G(M)$ itself. It can be considered as a modeltheoretic equivalent to $\beta G$, the large compactification of $G$. In the talk I will describe the results from my paper that give a description of definable topological dynamics of a large class of groups interpretable in an $o$minimal expansion of the field of reals along with their universal covers interpreted in a certain twosorted structure. The results provide a wide range of counterexamples to a question by Newelski whether the Ellis group of the universal definable $G$flow is isomorphic to $G/G^{00}$ and generalize methods from used by Gismatullin, Penazzi and Pillay that provided a particular counterexample. 
17:50  Topologies on Polish structures SPEAKER: Jan Dobrowolski ABSTRACT. A Polish structure is a pair $(X,G)$, where $G$ is a Polish group acting faithfully on a set $X$ so that the stabilizers of all singletons are closed subgroups of $G$ (this definition comes from K. Krupiński). Notice that, in the above definition, it is not required that $X$ is a topological space. I will discuss some issues concerning existence of topologies on $X$ satysfying some natural conditions. Special attention will be given to the case in which $X$ carries a structure of a group (i. e., $(X,G)$ is a Polish group structure). 
18:10  Explosiveness, Model Existence, and Incompatible Paraconsistencies SPEAKER: JuiLin Lee ABSTRACT. In this talk we present that the general concept of formal inconsistencies can be welldeveloped for any given semantics $\models$ (no matter it is truth functional or not). Note that the concept negation is not a necessary part in our treatment. In this theory of formal inconsistencies, there are two important concepts, model existence property (i.e., w.r.t.~the given inconsistency, every consistent set has a model with respect to $\models$) and explosiveness property (i.e., w.r.t.~the given inconsistency, every inconsistent set is also absolutely inconsistent). Now given a semantics $\models$, it will generate a set of inconsistencies, say, $Ins_{\models} =\{I_i,\dots\}$. If a $\models$sound proof system $L$ has both model existence property and explosiveness for some inconsistency $I\in Ins_{\models}$, then all inconsistencies in $Ins_{\models}$ are provably equivalent in $L$. \par Then it is natural to ask, for the classical semantics, whether there are incompactible paraconsistencies in the following sense, i.e., are there two inconsistencies $I_1, I_2$ (generated from classical semantics) such that there are classically sound proof systems $L_1, L_2$ such that in $L_1$ it has $I_1$ model existence and $I_2$ explosiveness but not $I_1$ explosiveness and not $I_2$ model existence. And in $L_2$ it has $I_2$ model existence and $I_1$ explosiveness but not $I_2$ explosiveness and not $I_1$ model existence. We will prove that the answer is positive, which shows that there are incompatible paraconsistencies. 
19:00  VSL Public Lecture: Gödel in Vienna SPEAKER: Karl Sigmund 