ABSTRACT. Multi-agents 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 network-formation 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 multi-agent games. For example, in network-formation 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.

ABSTRACT. Backward Induction (BI) is the basic solution concept for finite games with perfect information. It is the procedure to find out all the subgame-perfect 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 Extensive-Form 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.

ABSTRACT. The enumeration degrees are an upper semi-lattice 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 long-standing 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, K-pairs, 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 K-pairs is still first order definable. They investigated maximal K-pairs and showed that within the local structure the total enumeration degrees are first order definable as the least upper bounds of maximal K-pairs.

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.

ABSTRACT. We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter 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 zero-reachability 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 zero-reaching 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 zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching 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.

ABSTRACT. Ground Tree Rewrite Systems with State are known to have an undecidable control state reachability problem. Taking inspiration from the recent introduction of scope-bounded multi-stack 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 scope-bounded multi-stack pushdown systems, we show --- via reductions to and from reset Petri-nets --- that these systems have an Ackermann-complete control state reachability problem. However, reachability of a regular set of trees remains undecidable.

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 w-iterations (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, higher-order functions which are best handled with abstract interpretation or type systems.

We demonstrate this by generalising our type-and-effect systems to object-oriented programs and higher-order functions.

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 first-order 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 first-order 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.

ABSTRACT. Bisimulation up-to 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 up-to 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 up-to 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.

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.

ABSTRACT. We consider two-player non zero-sum 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, mean-payoff, and discounted sum. Moreover we show that it is possible to synthesize such strategy profiles that are finite-memory 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 mean-payoff measures. Our solutions rely on new results for zero-sum quantitative games with lexicographic objectives that are interesting on their own right.

ABSTRACT. We investigate the existence of certain types of equilibria (Nash, epsilon-Nash, subgame perfect, epsilon-subgame perfect) in infinite sequential games with real-valued payoff functions depending on the class of payoff functions (continuous, upper semi-continuous, Borel) and whether the game is zero-sum. 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.

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 non-trivial property of elliptic curves: the existence of an isomorphism between a curve and its Picard group of divisors.

ABSTRACT. The integration of the generate-and-test paradigm and semi-rings for the aggregation of results provides a parallel programming framework for large scale data-intensive applications. The so-called 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 divide-and-conquer 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.

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 re-using 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, re-using most of the existing proofs.

ABSTRACT. We report on a formalization of ordinals and cardinals in Isabelle/HOL. A main challenge we faced was the inability of higher-order 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.

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.

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 H-closure Theorem. H-closure 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 while-programs, and was originally proved from the classical Ramsey Theorem, then intuitionistically, but using a intuitionistic version of Ramsey Theorem different from our one. Our long-term goal is to extract effective bounds for the while-programs from the proof of Termination Theorem, and our new intuitionistic version of Ramsey Theorem is designed for this goal.

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.

ABSTRACT. This paper discusses the method of formative rules for first-order rewriting, which was previously defined for a class of higher-order rewriting. Dual to the well-known 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 higher-order definition, we can obtain significant improvements in the first-order setting, with or without types.

ABSTRACT. Monotone algebras are frequently utilized to generate reduction orders in automated termination- and complexity-proofs. 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 non-linear polynomial interpretations over various domains, including the reals.

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.

ABSTRACT. One recurring pattern in strategic reasoning consists in constructing a strategy for one game while playing another, auxiliary game on the side. Ehrenfeucht-Fraisse 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 meta-games.

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: game-theoretic 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 model-checking (GTS) and proofs (DL) procedures. We show how these restrictions can be derived from preference profiles of bounded-rational 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.

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 anti-coordination games played on graphs. Hereby, new links between social network theory, game theory and dynamic ‘epistemic’ logic are drawn.

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 state-of-the-art 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 so-called 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].

ABSTRACT. We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the Kneser-Lovasz 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 Kneser-Lovasz Theorem. On the other hand for the cases $k=2,3$ (for which combinatorial proofs of the Kneser-Lovasz 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 Kneser-Lovasz theorem.

ABSTRACT. Incremental SAT solving under assumptions, introduced in Minisat, is in wide use. However, Minisat's algorithm for incremental SAT solving under assumptions has two main drawbacks which hinder performance considerably. First, it is not compliant with the highly effective and commonly used preprocessor SatELite. Second, all the assumptions are left in the formula, rather than being represented as unit clauses, propagated, and eliminated. Two previous attempts to overcome these problems solve either the first or the second of them, but not both. This paper remedies this situation by proposing a comprehensive solution for incremental SAT solving under assumptions, where SatELite is applied and all the assumptions are propagated. Our algorithm outperforms existing approaches over publicly available instances generated by a prominent industrial application in hardware validation.

ABSTRACT. Portfolio approach for parallel SAT solvers is known as the standard parallelization technique. In portfolio, diversification is one of the important factors in order to enable workers (solvers) to conduct a vast search. The diversification is implemented by setting different parameters for each worker in the state-of-the-art parallel portfolio SAT solvers. However, existing diversification can be insufficient because the combination of the parameters is limited, in which two or more workers can search same spaces. For this issue, we propose a novel diversification technique, called community branching. In this method, we assign a different set (or sets) of variables (called a community) to each worker and force them to select these variables as decision variables in early decision levels. In this manner, we can avoid overlaps of search spaces between the workers more intentionally than the existing method. We create a graph, where a vertex is corresponds to a variable and an edge stands for relations in a same clause, and we apply a modularity-based community detection algorithm to it. The variables in a community have strong relationships, and a distributed search for different communities can benefit the whole search. Experimental results shot that we could speedup the existing parallel SAT solvers with our proposal.

ABSTRACT. (Tentative) In this paper, we present a simple parallel version of Glucose that uses a lazy policy to exchange clauses between cores. By working on the clause exchange policy, we ensure that in the context of many cores, the large number of incoming clauses will not degrade each core performances.

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 second-order logic with a new fixed-point-like 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 quasi-weak cost automata, as well as results about converting two-way alternating cost automata to one-way alternating cost automata.

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.

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 non-redundant monotone DNFs are dual. It is known that non-DUAL, the complementary problem to DUAL, is in GC(log² 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 non-DUAL is in GC(log² n,LOGSPACE).

In this paper we prove this conjecture and actually place the non-DUAL problem into the complexity class GC(log² n,TC⁰) which is a subclass of GC(log² n,LOGSPACE). We here refer to the logtime-uniform version of TC⁰, 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 non-DUAL that requires to guess O(log² n) bits. We then proceed by a logical analysis of this algorithm, allowing us to formulate its deterministic part in FO(COUNT).

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 two-player 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 second-order logic, for instance in the work on algorithmic meta theorems.

As the main logical result of this paper we develop decomposition- or splitter-theorems for the modal $\mu$-calculus in the style of Feferman-Vaught 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$ model-checking is fixed-parameter tractable on various classes of transition systems such as transition systems of bounded directed path width and bounded Kelly-width. To the best of our knowledge, these are among the first FPT-results for $L_\mu$ that do not follow immediately from tractability of monadic second-order logic.

ABSTRACT. We consider the two-variable fragment of first-order 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 NExpTime-complete.

ABSTRACT. We present the first method for reasoning about temporal logic properties of higher-order, infinite-data 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 type-and-effect 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 type-and-effect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higher-order software, as well as modular strategies for procedural programs.

ABSTRACT. Starting with an algorithm to turn lists into full trees which uses non-obvious 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 non-uniform inductive types which parallel numerical representations in a style advertised by Okasaki, and a small amount of dependent types.

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 so-called Univalence Axiom, which allows us to treat isomorphic types as if there were equal. 

Quillen's homotopical algebra, instead, provides a category-theoretic 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.

ABSTRACT. We introduce a novel resource analysis for typed term rewrite systems based on a potential-based 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 well-typed, then their exists a polynomial interpretation that orients R. For this we suitable adapt the standard notion of polynomial interpretations to the typed setting.

ABSTRACT. In this talk we introduce a game semantics for conditional logic. We
define a game for every inference between conditionals. A winning
strategy for the first player can be transformed into a proof of the
inference in system P, which is the standard inference system for
conditional logic. Conversely a proof in system P yields a winning
strategy for the first player. A winning strategy for the second
player can be transformed into a countermodel to the inference in the
standard order semantics of conditional logic. Conversely a
countermodel in the order semantics yields a winning strategy for the
second player. Combining these results we obtain a new, more
constructive, proof of strong completeness for conditional logic with
respect to its order semantics.

ABSTRACT. Dialogical Logic as a game-theoretic 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.

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.

ABSTRACT. Henkin (1961) enriched first-order logic with so-called 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 first-order formulas with branching quantifiers results in a logic which is strictly stronger than ordinary first-order logic.

In the first part of my presentation I will quickly review various formalisms which develop Henkin's ideas. One of them is Independence-Friendly 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 game-theoretical 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 win-lose 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 model-theoretical 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 first-order 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.~1--16.

\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.~169--183.

\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.~571--589.

\bibitem{MSS} {\scshape A. I. Mann, G. Sandu and M. Sevenster}, {\bfseries\itshape Independence-Friendly Logic: A Game-Theoretic 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.~618--631.

\end{thebibliography}

ABSTRACT. The roots of UD-randomness 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 UD-randomness is very weak. While every Schnorr random real is UD-random, the class of UD-random 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 UD-random reals and the relationships between UD-randomness and other randomness notions.

This work is joint with Wesley Calvert.

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.

ABSTRACT. When working with measurable flows, it is sometimes convenient to choose a countable cross-section and to reduce a problem of interest to a similar question for the action induced by the flow on this cross-section. In some cases, one wants to impose additional restrictions on the cross-section, usually by restricting possible distances between points within each orbit.

Historically, cross-sections 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 cross-section 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 cross-sections that are regular on all orbits without exceptions, and methods of ergodic theory, which tend to produce cross-sections 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 cross-section with only two different distances between adjacent points?

The talk will provide an overview of these and other results concerning the existence of regular cross-sections, 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.

ABSTRACT. Logic has been called the "calculus of computer science" - and yet, while any physics student is required to take several semesters of calculus, the same cannot be said about logic and students of computer science. Despite the great and burgeoning activity in logic-related topics in computer science, there has been very little interest, in North America at least, in developing a strong logic component in the undergraduate curriculum. Meanwhile, in other parts of the world, departments have set up specialized degree programs on logical methods and CS. This special session, organized under the auspices of the ASL's Committee on Logic Education, aims to explore the role of logic in the computer science curriculum. How are computer scientists trained in logic, if at all? What regional differences are there, and why? Is a greater emphasis on logic in the computer science undergraduate curriculum warranted, both from the point of view of training for research in CS and from the point of view of training for industry jobs? What should an ideal "Logic for Computer Science" course look like?

Byron Cook believes that, in the rush to create engineers and scientists, we have lost sight of the fact that an education should be broad and place emphasis on principles rather than specific skills such as Javascript. Logic is the perfect topic in this setting, as it has application in both humanities and science, and fosters a discussion about mechanics while not requiring a significant amount of technical overhead.

The Association for Computing Machinery has just chartered a new Special Interest Group on Logic and Computation (SIGLOG). Education is one of the prime concerns of this new SIG and one of the activities on the SIG's education committee will be to advocate for a greater presence of logic in the curriculum. Prakash Panangaden discusses the aims of the new SIG with particular emphasis on its educational mission.

Nicole Schweikardt will report on experiences with designing an undergraduate introductory course on logic in computer science at Goethe-University Frankfurt.

The University of Technology Vienna participates in a European Masters program in computational logic and has just started a doctoral program in Logical Methods in Computer Science. Alexander Leitsch describes these initiatives and considers lessons other departments can draw from the Vienna experience.

Presentations will be followed by a panel discussion. Materials will be available on the Committee on Logic Education website at http://ucalgary.ca/aslcle/.

ABSTRACT. Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanation for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size.

As our main contribution we obtain combinatorial characterisations of these hardness measures. Our characterisations are both in terms of Prover-Delayer games and of sets of partial assignments with some consistency strength. These unified characterisations allow elegant proofs of relations between the different hardness measures. In particular, we obtain a generalised version of Atserias and Dalmau's result on the relation between resolution width and space from (J. Comput. Syst. Sci. 2008). Our results do not only hold for unsatisfiable instances, but also transfer to the satisfiable case, for which little is known regarding hardness measures.

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, model-checking, 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.  Production-quality 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 interpretation-based tools. Examples of abstractions will be provided, from semantics to typing, grammars to safety, reachability to potential/definite termination, numerical to protein-protein 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.

ABSTRACT. Machine-checked proofs are becoming ever-larger, 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 widely-used in the seL4 verification stack, and report on its strengths and limitations.

ABSTRACT. Historically, the LCF tradition of interactive theorem proving was tied to the read-eval-print loop, with sequential and synchronous evaluation of prover commands given on the command-line. This user-interface technology was adequate when R. Milner introduced his LCF proof assistant in the 1970-ies, but it severely limits the potential of current multicore hardware and advanced IDE front-ends.

Isabelle/PIDE breaks this loop and retrofits the read-eval-print phases into an asynchronous model of document-oriented 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 front-end perspective on the proof document, while making adequate use of the CPU resources on multicore hardware on the back-end.

Recent refinements of Isabelle/PIDE provide an explicit concept of asynchronous print functions over existing proof states. This allows to integrate long-running or potentially non-terminating tools into the document-model. Applications range from traditional proof state output (which may consume substantial time in interactive development) to automated provers and dis-provers 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 find-theorems). Thus the Prover IDE provides continuous proof processing, augmented by add-on tools that help the user to continue writing proofs.

ABSTRACT. This paper introduces Clide, a collaborative web interface for the Isabelle theorem prover. The interface allows a document-oriented 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.

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 F-omega with positive recursive type definitions, which we analyze. We also prove type preservation for S.

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 "Q-logic of P-terms'' and Ppoly which intuitively denotes the "predicative polymorphism" extension of P.

These results suggest a new approach to the study of the meta-theory of PTSs, by examination of the relationships between different calculi and "predicative extensions" which allow more expressiveness with equivalent logical strength.

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 non-nested (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 multi-step 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.

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 second-order logic. Based on a non-definability result for a class of partial orders, an example is given of a non-characterizable class of revision operators. This appears to be the first non-characterizability result in belief revision.

ABSTRACT. Our main goal in this paper is to give game semantics for various non-classical logics, and observe how non-classical logical elements change the verification game.

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 Q-resolution, which forms the foundation of learning in modern search-based QBF solvers, is exponentially inferior in proof length to its extended variants: long-distance Q-resolution (LQ-resolution) and Q-resolution with resolution over universal literals (QU-resolution). The relative proof power between LQ-resolution and QU-resolution, 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 LQ-resolution proofs in contrast to their exponential Q-resolution counterparts.

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 first-order 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 non-rigid 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.

ABSTRACT. I want to present a three-valued 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 Liar-like 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.

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 Graph-Calculus 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)

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 PSPACE-complete.

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 many-relational modal language with independent relations, having the so-called \emph{presburger constraints}, which can express both integer and rational grading. Demri and Lugiez show that the satisfiability for the PML language is PSPACE-complete, 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 results---from polynomial to PSPACE---for a range of description logics, syntactic analogs of fragments of GGML, are obtained (Y., 2012, 2013).

In this talk we consider many-relational 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.

ABSTRACT. We define the notion of fuzzy bisimulation for the standard Godel modal logic and prove the corresponding Hennessy-Milner style theorem.

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 `well-connectedness' 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 straight-forward.

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.

ABSTRACT. On the basis of dynamic model of self-reference statements the variant of multiple-valued logic describing external operations of such statements is considered. It is noted that for formulations and self-reference 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 four-group V . It suggests that the truth space for values of self-reference statements is described by quaternion algebra H.

ABSTRACT. G\"{o}del 3-valued logic G3 is the strongest of the G\"{o}del many-valued logics introduced in [1]. Although the Routley-Meyer semantics (RM-semantics) 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 RM-semantics 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 RM-semantics for G3 once this logic has been axiomatized as an extension of B$_{+}$ (cf. [2], [3]).

ABSTRACT. The depth relevance condition (drc) is a strengthening of the variable-sharing 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 non-trivial 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.

ABSTRACT. This work builds on the well-known 0-1 law for the asymptotic probabilities of first-order 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 0-1 law hold in some non-trivial extensions of first-order logic (e.g., with fixed point operators) but fail in others, notably in most natural fragments of monadic second-order (MSO) and even for modal logic formulae, in terms of frame validity. The question we study here is how to characterise -- axiomatically or model-theoretically -- 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 well-defined. The set of almost sure validities in the finite of a given logical language is a well-defined 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 non-existence (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.

ABSTRACT. This paper extends Reynolds' separation logical system for pointer while program verification to second-order 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.

ABSTRACT. We prove that the determinacy of Gale-Stewart games whose winning sets are infinitary rational relations accepted by 2-tape Büchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart 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 non-effective, in these games. We prove the same results for Gale-Stewart games with winning sets accepted by real-time 1-counter Büchi automata, then extending previous results obtained about these games.

(1) There exists a 2-tape Büchi automaton (respectively, a real-time 1-counter 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 2-tape Büchi automaton (respectively, a real-time 1-counter 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 2-tape Büchi automata (respectively, of real-time 1-counter 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))$.

ABSTRACT. We prove that $T_{NC^1}$, the true universal first-order 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 NW-generators are hard for $T_{PV}$, the true universal theory in the language containing names for all p-time algorithms.

\begin{thebibliography}{10}

\bibitem{cite1} {\scshape Jan Kraj\'{i}\v{c}ek}, {\itshape On the proof complexity of the Nisan-Wigderson generator based on a hard NP$\cap$coNP function}, {\bfseries\itshape Journal of Mathematical Logic}, vol.~11 (1), 2011, pp.~11--27.

\end{thebibliography}

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.

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 so-called 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.

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 14-01-00376), and by the Grants Council (under RF President) for State Aid of Leading Scientific Schools (grant NSh-860.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.~105--115.

\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.~51--67.

\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.~215--231.

\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.~179--187.

\end{thebibliography}

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.~1--14.

\end{thebibliography}

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.

ABSTRACT. In Diagonally Non-Computable Functions and Bi-Immunity, Carl Jockusch and Andrew Lewis-Pye proved that every DNC function computes a bi-immune set. They asked whether every DNC function computes an effectively bi-immune set. Several attempts have been made to solve this problem in the last few years. We construct a DNC function that computes no effectively bi-immune set, thereby answering their question in the negative. We obtain a few corollaries that illustrate how our technique can be applied more broadly.

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.

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 Martin-Lö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 1-generic 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.

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.

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 Turing-below 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.

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 non-zero: if a and b are honest elementary degrees with 0 < a < b, then a cups to b. This answers a question of Kristiansen.

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 model-theoretic 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 2-CEA degrees. We also give an example of two incomparable degree spectra.

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 non-low$_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.~201--209 (in english), pp.~69--75 (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.~745--754.

\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.~470--486. \end{thebibliography}

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 non-degenerate 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 non-degenerate 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 non-degenerate 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.

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 proof-theoretic 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 self-mappings 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 semi-intuitionistic 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 semi-constructive proofs}, {\bfseries\itshape Annals of Pure and Applied Logic}, vol.~141 (2006), pp.~89--107.

\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.~2615--2660.

\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.~193--209.

\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.~301--308.

\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-//analysis-hard-analysis-and-the-finite-convergence-principle/.

\end{thebibliography}

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 quasi-order 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 quasi-order. For example, $(Q,{\leq_Q})$ is a well quasi-order (WQO: well-founded 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 quasi-order $(Q,{\leq_Q})$, we consider two natural quasi-orders 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 quasi-orders, and $\mathcal{P}_f^\flat(Q)$ and $\mathcal{P}_f^\sharp(Q)$ for their restrictions to the collection of finite subsets of $Q$.

Goubault-Larrecq 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}

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 non-equinumerosity 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 anti-diagonal 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 non-recursively-enumerable 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 non-equinumerosity 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 anti-diagonal 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 anti-diagonal 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.~129--149.

\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.~283--289.

\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.~25--30, pp.~445--452.

\bibitem{raja1}{\scshape Natarajan Raja}, {\itshape A Negation-Free Proof of Cantor's Theorem}, {\bfseries\itshape Notre Dame Journal of Formal Logic}, vol.~46 (2005), no.~2, pp.~231--233.

\bibitem{raja2}{\scshape Natarajan Raja}, {\itshape Yet Another Proof of Cantor's Theorem}, {\bfseries\itshape Dimensions of Logical Concepts} (Jean-Yves B\'{a}ziau and Alexandre Costa-Leite, editors), Cole\c{c}\~{a}o CLE: Volume 54, Campinas, Brazil, 2009, pp.~209--217.

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 second-order arithmetic. These include an alternative proof of Harrington's theorem [3] that WKL0 is Pi11-conservative over RCA0.

[1] Kenneth Mc Aloon, Completeness theorems, incompleteness theorems and models of arithmetic, Transactions of the American Mathematical Society, vol. 239 (1978), pp. 253-277.

[2] James H. Schmerl, End extensions of models of arithmetic, Notre Dame Journal of Formal Logic, vol. 33 (1992), no. 2, pp. 216-219.

[3] Stephen G. Simpson, Subsystems of Second Order Arithmetic, Perspectives in Logic, Cambridge University Press, 2009.

ABSTRACT. Some properties of Intuitionistic Set Theory with the principle UP.

Let ZFI2C be usual intuitionistic Zermelo-Fraenkel set theory in two-sorted 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 Zermelo-Fraenkel 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 well-known that both ZFI2C and ZFI2C+DCS(where DCS is a well-known 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 well-known intuitionistic principles, such that Markov Principle M, Extended Church Principle ECT, and the Principle UP.

It is well-known 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 AE-formulae 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 well-known specifical intuitionistic principle. It claims that we cannot define effectivly non-trivialfunction 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.

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 27-59 vol.~67 (2001), no.~1, pp.27--59.

[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.353--378.

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 Dushnik-Miller 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.

ABSTRACT. The talk will cover some recent results about computable numberings in Ershov hierarchy

ABSTRACT. Davies-trees 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 Davies-trees 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 k-connected uncountably chromatic subgraphs for each finite k (both results are due to Komjath).

Our belief is that Davies-trees did not get their well deserved attention despite the fact that they provide an easily applicable tool for logicians and set theorists.

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.

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 Solovay-Tennenbaum 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.

ABSTRACT. An elementary epimorphism $f : M \rightarrow N$ (between model-theoretic 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$-pre-images $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 non-trivial $\Sigma_1$-elementary epimorphisms, and non-trivial (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.

ABSTRACT. The generic ultrafilter $\mathcal{G}_2$ forced by the partial ordering $\mathcal{P}(\omega\times\omega)/(\mathrm{Fin}\times\mathrm{Fin})$ is a non-p-point which is also not a Fubini product of p-points, but is a Rudin-Keisler 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 Ramsey-classification 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 non-p-points which have exactly $k$ Tukey predecessors, as well as exactly $k$ Rudin-Keisler predecessors.

 [BDR] Andreas Blass, Natasha Dobrinen, Dilip Raghavan, The next best thing to a p-pint, Submitted.

[D] Natasha Dobrinen, High dimensional Ellentuck spaces and initial chains in the Tukey structure of non-p-points, Submitted.

ABSTRACT. We consider a variant of the Rudin-Keisler order for ideals on $\omega$ and prove the existence of a complete co-analytic ideal with respect this order. The key tool is a parameterization of all co-analytic ideals. We obtain this parameterization via a method which yields a simple proof of Hjorth's 1996 theorem on the existence of a complete co-analytic 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.

ABSTRACT. We define budding trees, show that they form a topological Ramsey space, and discuss applications.

ABSTRACT. Consider a first-order language L. For any L-formula alpha, let #alpha stand for the Gödel number of alpha. An L-theory 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 L-sentence 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 quasi-Boolean part of Clarke’s system. There is still one more part of Clarke’s system, that is, the quasi-topological 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.

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 long-studied 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₀⊆L, is M reduced to L₀ 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.

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.

ABSTRACT. A group $G$ is called {\bf amenable} if every $G$-flow (i.e. a compact Hausdorff space along with a continuous G-action) 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.

ABSTRACT. Theorem. Let n > 2. The n-variable fragment of first-order 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 n-variable 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 2-variable fragment L2, and it holds for the n-variable 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.

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 truth-functional propositional language determines the clone generated by the interpretation of its operator symbols. If we consider propositional languages interpreted with a three-valued truth-functional 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 three-valued 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 non-monotonic on the order of information. Using Jablonskij's theorem that determines all three-valued maximal clones and Lau's theorem that characterizes all the three-valued 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.

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 kappa-additive 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 Kripke-Joyal semantics in the topos, into statements in standard (Kolmogorov-style) 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.

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 so-called 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 game-theoretic 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.

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 modal-like semantics given using four-valued, as opposed to three-valued 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 non-contraposable 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 non-contraposable 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 four-valued generalizations) deliver a form of extensionality, in the absence of weakening the formal rule does not capture the intuitive notion of extensionality.

ABSTRACT. Some positive applications of the counterexamples of Robinson property on the characterization of Interpolation and Compactness properties

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 model-theoretic 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 two-sorted 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.

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).

ABSTRACT. In this talk we present that the general concept of formal inconsistencies can be well-developed 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.