View: session overviewtalk overviewside by side with other conferences
08:45  Welcome Address by the Rector SPEAKER: Sabine Seidler 
08:50  Welcome Address by the Organizers SPEAKER: Matthias Baaz 
08:55  VSL Opening SPEAKER: Dana Scott 
09:15  VSL Keynote Talk: Computational Ideas and the Theory of Evolution SPEAKER: Christos Papadimitriou ABSTRACT. Covertly computational insights have influenced the Theory of Evolution from the very start. I shall discuss recent work on some central problems in Evolution that was inspired and informed by computational ideas. Considerations about the performance of genetic algorithms led to a novel theory of the role of sex in Evolution based on the concept of mixability, the population genetic equations describing the evolution of a species can be reinterpreted as a repeated game between genes played through the multiplicative update algorithm, while a theorem on satisfiability can shed light on the emergence of complex adaptations. 
11:00  Tutorial on Stategic and Extensive Games 1 SPEAKER: Krzysztof Apt 
12:00  Applications of admissible computability SPEAKER: Noam Greenberg ABSTRACT. Admissible computability is an extension of traditional computability theory to ordinals beyond the finite ones. I will discuss two manifestations of admissible computability in the study of effective randomness and in the study of effective properties of uncountable structures. 
14:30  The DNA of logic and games. SPEAKER: Johan Van Benthem ABSTRACT. Logic and games are entangled in delicate ways. Logics {\bf of} games are used to analyze how players reason and act in a game. I will discuss dynamicepistemic logics that analyze various phases of play in this mode. But one can also study logic {\bf as} games, casting major logical notions as gametheoretic concepts. The two perspectives create a circle, or double helix if you will, of contacts all around. I will address this entanglement, and the issues to which it gives rise (\cite{vB}). 
15:15  Dependence and independence  a logical approach SPEAKER: Jouko Väänänen ABSTRACT. I will give an overview of dependence logic, the goal of which is to establish a basic logical theory of dependence and independence underlying seemingly unrelated subjects such as game theory, causality, random variables, database theory, experimental science, the theory of social choice, Mendelian genetics, etc. There is an abundance of new results in this field demonstrating a remarkable convergence. The concepts of (in)dependence in the different fields of humanities and sciences have surprisingly much in common and a common logic is starting to emerge. 
14:30  Pregeometries and definable groups SPEAKER: Pantelis Eleftheriou ABSTRACT. We will describe a program for analyzing groups and sets definable in certain pairs (R, P). Examples include: (1) R is an ominimal ordered group and P is a real closed field with bounded domain (joint work with Peterzil) (2) R is an ominimal structure and P is a dense elementary substructure of R (work in progress with Hieronymi) In each of these cases, a relevant notion of a pregeometry and genericity is used. 
15:15  Quasiminimal structures and excellence SPEAKER: Meeri Kesala ABSTRACT. A structure $M$ is quasiminimal if every definable subset of $M$ is either countable or cocountable. The field of complex numbers is a strongly minimal structure and hence quasiminimal, but if we add the natural exponential function, the quasiminimality of the structure becomes an open problem. Boris Zilber defined the nonelementary framework of \textit{quasiminimal excellent classes} in 2005 in order to show that his class of \textit{pseudoexponential fields} is uncountably categorical. He conjectured that the unique pseudoexponential field of cardinality $2^{\aleph_0}$ fitting into this framework is isomorphic to the complex numbers with exponentiation. A key property for the categoricity of quasiminimal excellent classes was the technical axiom of excellence, which was adopted from Shelah’s work for excellent sentences in $L_{\omega_1\omega}$. However, the original proof of the categoricity of pseudoexponential fields turned out to have a gap and the problem lay in sh! owing that the excellence axiom holds. In the paper \textit{Quasiminimal structures and excellence}\cite{cite1} we fill the gap in the proof with a surprising result: the excellence axiom is actually redundant in the framework of quasiminimal excellent classes. This result elegantly combines methods from classification theory that were generalized to different nonelementary frameworks by a group of people. These methods have a combinatorial core idea that is independent of the compactness of first order logic. We also study whether other quasiminimal structures fit into this uncountably categorical framework. The paper strengthens the belief that nonelementary methods can provide effective tools to analyse structures that are out of reach for traditional modeltheoretic methods. Different frameworks have been suggested and the methods refined and there are many interesting paths in the ongoing research. The paper is joint work of Martin Bays, Bradd Hart, Tapani Hyttinen, MK and Jonathan Kirby. 
14:30  Uniform and nonuniform reducibilities of algebraic structures SPEAKER: Iskander Kalimullin ABSTRACT. The talk will be devoted to various versions of algorithmic reducibility notion between algebraic structures. In particular, the reducibilities under Turing operetors, enumeration operators, and under $\Sigma$formulas will be considered. Several constructions of jump inversion where these reducibilities do not coincide. Furthermore, the $\Sigma$reducibility between the direct sums of cyclic pgroups will be studied in detail. 
15:15  Randomness in the Weihrauch degrees SPEAKER: Rupert Hölzl ABSTRACT. . 
14:30  Inductive Proofs & the Knowledge They Represent SPEAKER: Michael Detlefsen ABSTRACT. Proofs by mathematical induction seem to require certain interdependencies between the instances of the generalizations they prove. The character and significance of these interdependencies will be the main subject of this talk. 
15:15  Decidable languages for knowledge representation and inductive definitions: From Datalog to Datalog+/ SPEAKER: Georg Gottlob ABSTRACT. Datalog is a language based on functionfree Horn clauses used to inductively define new relations from finite relational structures. Datalog has many nice computational and logical properties. For example, Datalog captures PTIME on ordered structures, which means that evaluating fixed Datalog programs (i.e. rule sets) over finite structures is in PTIME and, moreover, every PTIMEproperty on ordered structures can be expressed as a Datalog program (see [1] for a survey). After giving a short overview of Datalog we argue that this formalism has certain shortcomings and is not ideal for knowledge representation, in particular, for inductive ontological knowledge representation and reasoning. We consequently introduce Datalog+/ which is a new framework for tractable ontology querying, and for a variety of other applications. Datalog+/ extends plain Datalog by features such as existentially quantified rule heads, negative constraints, and equalities in rule heads, and, at the same time, restricts the rule syntax so as to achieve decidability and tractability. In particular, we discuss three paradigms ensuring decidability: chase termination, guardedness, and stickiness, which were introduced and studied in [2, 3, 4, 5]. [1] Dantsin, E.; Eiter, T.; Georg, G.; and Voronkov, A. 2001. Complexity and expressive power of logic programming. ACM Computing Surveys 33(3):374425. [2] Cali, A.; Gottlob, G.; and Kifer, M. 2013. Taming the innite chase: Query answering under expressive relational constraints. Journal of Articial Intelligence Research 48:115174. [3] Cali, A.; Gottlob, G.; and Lukasiewicz, T. 2012. A general Datalogbased frame work for tractable query answering over ontologies. Journal of Web Semantics 14:5783. [4] Cali, A.; Gottlob, G.; and Pieris, A. 2012. Towards more expressive ontology languages: The query answering problem. Artificial Intelligence 193:87128. [5] Gottlob, G.; Manna, M.; and Pieris, A. 2013. Combining decidability paradigms for existential rules. Theory and Practice of Logic Programming 13(45):877892. 
16:30  Natural deduction for intuitionistic differential linear logic SPEAKER: Mattia Petrolo ABSTRACT. Recent investigations in denotational semantics led Ehrhard to define a new model of lambdacalculus and linear logic called finiteness spaces. In finiteness spaces, types are interpreted as topological vector spaces, lambdaterms and (via the CurryHoward correspondence) intuitionistic proofs are interpreted as analytic functions in topological vector spaces. However, analytic functions are infinitely differentiable, thus the question arise whether differentiation can be defined as a meaningful syntactic operation. A positive answer from a computational perspective is given by differential lambda$calculus, an extension of lambdacalculus in which the operations of differentiation and Taylor expansion of a lambdaterm are definable. One of the interests of differential lambdacalculus lies in the analogy that can be drawn between the usual notion of differentiation (i.e. linearity in mathematical sense) and its computational meaning (i.e. linearity in computational sense). It turns out that differentiation and the actual infinite operation involved in Taylor expansion makes sense also in a purely logical setting. The right syntax is provided by differential linear logic (DiLL) and analyzed in terms of differential interaction nets by T. Ehrhard and L. Regnier (2006). DiLL is an extension of LL characterized by three new rules dealing with the ! modality: cocontraction, codereliction, and coweakening. The latter rules are called "costructural" and, in a onesided sequent calculus setting, can be considered as symmetric duals of the ?rules. Costructural rules give a logical status to differentiation. In this paper, we introduce a natural deduction system for intuitionistic DiLL. We show normalization and, as corollaries, subformula, separability and introduction form properties for this system. Its relationships with the natural deduction systems for intuitionistic logic are discussed. 
16:50  An outline of intuitionistic epistemic logic SPEAKER: Tudor Protopopescu ABSTRACT. We outline an intuitionistic view of knowledge which maintains the BrouwerHeytingKolmogorov semantics and is consistent with Williamson's suggestion that intuitionistic knowledge is the result of verification and that verifications do not necessarily yield strict proofs. On this view, A > KA is valid and KA > A is not. The former expresses the constructivity of truth, while the latter demands that verifications yield strict proofs. Unlike in the classical case where Classical Knowledge ==> Classical Truth intuitionistically Intuitionistic Truth ==> Intuitionistic Knowledge. Consequently we show that KA > A is a distinctly classical principle, too strong as the intuitionistic truth condition for knowledge, ``false is not known,''which can be more adequately expressed by e.g., ~(KA & ~A) or, equivalently, ~(K⊥). We construct a system of intuitionistic epistemic logic: IEL = intuitionistic logic IPC + K(A>B)>(KA>KB) + (A>KA) + ~(K⊥) provide a Kripke semantics for it and prove IEL soundness, completeness and the disjunction property. IEL can be embedded into an extension of S4, S4V, via the Godel embedding ``box every subformula.'' S4V is a bimodal classical logic consisting of the rules and axioms of S4 for [] and D for K, with the connecting axiom []A > KA. The soundess of the embedding is proved. Within the framework of IEL, the knowability paradox is resolved in a constructive manner. Namely, the standard ChurchFitch proof reduces the intuitionistic knowability principle A > <>KA to A > ~~KA, which is an IELtheorem. Hence the knowability paradox in the domain of IEL disappears since neither of these principles are intuitionistically controversial. We argue that previous attempts to analyze the paradox were insufficiently intuitionistic. 
17:10  Some properties related to the existence property in intermediate predicate logics SPEAKER: NobuYuki Suzuki ABSTRACT. We discuss relationships between the existence property (EP) and its weak variants in intermediate predicate logics. In [2], we provided a negative answer to Ono's problem P52 in intermediate predicate logics (Does EP imply the disjunction property? [1]), and presented some related results. To solve the problem, we considered two variants of EP in superintuitionistic predicate logics, and used them to construct counterexamples in intermediate logics. One variant is an extreme EP; namely, for every \exists xA(x), L  \exists xA(x) implies that there exists a fresh individual variable v such that L  A(v). This property is so extreme that none of intermediate predicate logics has it. However, if we restrict \exists xA(x) to a sentence, EP implies this property, which we call the sentential existence property (sEP). Another one is a weak variant of EP; an intermediate predicate logic L is said to have the weak existence property (wEP), if for every \exists xA(x) that contains no free variables other than v_1, ..., v_n, L  \exists xA(x) implies L  A(v_1)\vee...\vee A(v_n). Then, it is easy to see that EP implies wEP, and wEP implies sEP. In the present talk, we show that the converses of these implications do not hold in intermediate predicate logics. [1] H. Ono, Some problems in intermediate predicate logics, Reports on Mathematical Logic, vol. 21 (1987), pp.5567. [2] N.Y. Suzuki, A negative solution to Ono's problem P52: Existence and disjunction properties in intermediate predicate logics, submitted. 
17:30  On Hallden complete modal logics determined by homogeneous frames SPEAKER: Zofia Kostrzycka ABSTRACT. For several normal modal logics we construct countable many their normal extensions, which are Hallden complete, as well as uncountable many, which are not. Our approach to this task is purely semantic. 
17:50  A universal diagonal schema by fixedpoints and Yablo’s paradox SPEAKER: Ahmad Karimi ABSTRACT. In 1906, Russell [5] showed that all the known settheoretic paradoxes (till then) had a common form. In 1969, Lawvere [3] used the language of category theory to achieve a deeper unication, embracing not only the settheoretic paradoxes but incompleteness phenomena as well. To be precise, Lawvere gave a common form to Cantor's theorem about power sets, Russell's paradox, Tarski's theorem on the undefinability of truth, and Godel's first incompleteness theorem. In 2003, Yanofsky [7] extended Lawvere's ideas using straightforward settheoretic language and proposed a universal schema for diagonalization based on Cantor's theorem. In this universal schema for diagonalization, the existence of a certain (diagonalizedout and contradictory) object implies the existence of a fixedpoint for a certain function. He showed how selfreferential paradoxes, incompleteness, and fixedpoint theorems all emerge from the single generalized form of Cantor's theorem. Yanofsky extended Lawvere's analysis to include the Liar paradox, the paradoxes of Grelling and Richard, Turing's halting problem, an oracle version of the P=?NP problem, time travel paradoxes, Parikh sentences, Lob's Paradox and Rice's theorem. In this talk, we fit more theorems in the universal schema of diagonalization, such as Euclid's theorem on the infinitude of the primes, and new proofs of Boolos [1] for Cantor's theorem on the nonequinumerosity of a set with its powerset. We also show the existence of Ackermannlike functions (which dominate a given set of functions such as primitive recursive functions) using the schema. Furthermore, we formalize a reading of Yablo's paradox [6], the most challenging paradox in the recent years, in the framework of Linear Temporal Logic (LTL [2]) and the diagonal schema, and show how Yablo's paradox involves circularity by presenting it in the framework of LTL. All in all, we turn Yablo's paradox into a genuine mathematico logical theorem. This is the first time that Yablo's paradox becomes a (new) theorem in mathematics and logic. We also show that Priest's [4] inclosure schema can fit in our universal diagonal/fixedpoint schema. The inclosure schema was used by Priest for arguing for the selfreferentiality of Yablo's sequence of sentences, in which no sentence directly refers to itself but the whole sequence does so.
[1] George Boolos, Constructing Cantorian Counterexamples, Journal of Philosophical Logic, vol. 26 (1997), no. 3, pp. 237239. [2] Fred Kroger & Stephan Merz, Temporal Logic and State Systems, EATCS Texts in Theoretical Computer Science, Springer, 2008. [3] F. William Lawvere, Diagonal arguments and cartesian closed categories, Category theory, homology theory and their applications II (Seattle Research Center of the Battelle Memorial Institute), LNM 92, Springer, Berlin, 1969, pp. 134145. [4] Graham Priest, Yablo’s Paradox, Analysis, vol. 57 (1997), no. 4, pp. 236242. [5] Bertrand Russell, On some difficulties in the theory of transfinite numbers and order types, Proceedings of the London Mathematical Society, vol. s24 (1907), no. 1, pp. 2953. [6] Stephen Yablo, Paradox without SelfReference, Analysis, vol. 53 (1993), no. 4, pp. 251252. [7] Noson S. Yanofsky, A Universal Approach to SelfReferential Paradoxes, Incompleteness and Fixed Points, Bulletin of Symbolic Logic, vol. 9 (2003), no. 3, pp. 362386. 
18:10  Canonical extensions and prime filter completions of poset expansions. SPEAKER: unknown ABSTRACT. The algebraic models of substructural logics are residuated ordered algebras [2]. Embedding a residuated ordered algebra into a complete algebra of the same class has many applications in logic, e.g., the canonical extension is used to obtain relational semantics for nonclassical logics [1]. The underlying sets of the algebraic structures of interest are often partially ordered. The canonical extensions of posets have been studied in [1, 2]. Upon closer inspection it can be seen that the completions in [1] and [2] are generally different. Both use a construction, first appearing in [3], based on a Galois connection between sets of filters and ideals, however, the choice of filters differs. We investigate the construction from [3] for various choices of filters and ideals, consider the extension of operations defined on the posets and focus on some specific properties of completions obtained via this construction. Next we present a construction for completions of posets that makes use of the prime filters of the posets. We show that the completion obtained via this second construction is isomorphic to the former for a particular choice of filters. 
16:30  On the compactness theorem in many valued logics SPEAKER: Hovhannes Bolibekyan ABSTRACT. Nowadays manyvalued logics occupy new areas of computer science. Being extensively used in various areas, theoretical investigations of different properties in such logics is a challenging area of research [1]. Firstly it worths mentioning that axiomatic systems for many valued logics are not well developed. Secondly many notions are not naturally extended in many valued logics from already existing analogues of classical or other "welldeveloped" non classical logics. One of the key properties to characterize first order logic is compactness. We formulate an analogue of classical compactness theorem for arbitrary Nvalued logic. To prove it overloading operators are constructed. 
16:50  Formalizing vagueness as a doxastic, relational concept SPEAKER: Thomas Benda ABSTRACT. Descriptions and statements about the physical world often involve vague predicates, e.g., "x is red". It has become a common procedure to assign vague predicates intermediate truth values that are real numbers between 0 and 1. However, there is no satisfactory account what it means to be true to a given degree, which leaves doxastic degrees as the only option. Furthermore, real numbers provide an almost absurd accuracy as well as a natural metric, where in fact we want to state no more than, say, that x is rather red than not, perhaps redder or less red than some y. That suggests considering vagueness as a relational notion. A thereby established vagueness relation is a partial order. Advantages of a relational account of vagueness are that vague predicates form a comparatively weak structure without metric and that the wellknown problem of higherorder vagueness vanishes. There is no reason not to implement doxastic degrees on the object language level. Furthermore, with the practice of evaluating vague predicates, relational vagueness should be allowed to depend on perception and epistemic as well as pragmatic context and hence be nonextensional. To set up a requisite formal language, we enclose vagueness predicates in quotation marks and perform their assessment with a background in mind which provides epistemic and pragmatic context. Thus a ternary predicate is introduced, B'Ax''Ay'b, read "I believe, with background b, Ax to at least as high a degree as Ay". Given background b, believing Ax with absolute confidence is formalized as B'Ax''0=0'b. Such a formalization may be applied to conferring values to physical magnitudes which uses approximations and error bars. "The value of a is v" would then be vague as much as "x is red", acknowledging a fuzzy nature of experimental, particularly, macroscopic physics. 
17:10  Two Formalisms for a Logic of Generalized Truth Values SPEAKER: Oleg Grigoriev ABSTRACT. This report concerns to the problem of constructing tableaubased proof procedure for a logic of generalized truth values. We propose two different tableaustyle formalisation for a logic which captures a syntactical analogue of semantic logical consequence relation. One of them is more or less 'traditional' and resembles tableau systems for relevant logic FDE. Another one is appropriate for designing a proof search procedure and based on well known KE formalism. 
17:30  Characterising Logics through their Admissible Rules SPEAKER: Jeroen Goudsmit ABSTRACT. The admissible rules of a logic are those rules under which the set of its theorems are closed. Many nonclassical logics have interesting admissible rules, and these admissible rules carry quite a bit of information. In fact, some logics can even be completely characterised by way of their admissible rules. Consider the lattice of intermediate logics, that is, the lattice of consistent extensions of propositional intuitionistic logic. The disjunction property is an example of an admissible rule. It is wellknown that there are continuum many logics among that lattice that enjoy the disjunction property, Medvedev’s logic and Kreisel–Putnam logic to name but two. It was shown by Maksimova that Medvedev’s logic can be characterised as the maximal intermediate logic above Kreisel–Putnam logic with the disjunction property. The intuitionistic propositional logic itself can also be characterised as the maximal intermediate logic that admits a particular set of rules, as has been independently confirmed by Skura and Iemhoff. The rules they employed arose independently in the work of Citkin and Visser. These rules can be stratified in natural way with respect to admissibility in the logics of bounded branching, also known as the Gabbay–de Jongh logics. We will present a characterisation of each of these logics as being the maximal intermediate logic admitting a particular strata of the aforementioned rules. 
17:50  Models for the probabilistic sequent calculus SPEAKER: Marija Boricic ABSTRACT. The usual approach to treating the probability of a sentence leads to a kind of polymodal logic with iterated (or not iterated) probability operators over formulae (see [3]). On the other hand, there were some papers dealing with probabilistic form of inference rules (see [1], [2] and [4]). The sequent calculi present a particular mode of deduction relation analysis. The combination of these concepts, the sentence probability and the deduction relation formalized in a sequent calculus, makes it possible to build up sequent calculus probabilized  the system {\bf LKprob}. Sequents in {\bf LKprob} are of the form $\Gamma\vdash_a^b\Delta$, meaning that 'the probability of provability of $\Gamma\vdash\Delta$ is in interval $[a,b] \cap I$', where $I$ is a finite subset of reals $[0,1]$. Let $\text{\rm Seq}$ be the set of all sequents of the form $\Gamma\vdash\Delta$. A model for {\bf LKprob} is any mapping $p: \text{\rm Seq} \to [0,1]$ satisfying: \it (i) \rm $p(A\vdash A)=1$, for any formula $A$; \it (ii) \rm if $p(AB\vdash )=1$, then $p( \vdash AB)=p( \vdash A)+p( \vdash B)$, for any formulas $A$ and $B$; \it (iii) \rm if sequents $\Gamma\vdash\Delta$ and $\Pi\vdash\Lambda$ are equivalent in $\text{\bf LK}$, in sense that there are proofs for both sequents $\bigwedge \Gamma \rightarrow \bigvee \Delta \vdash \bigwedge \Pi \rightarrow \bigvee \Lambda$ and $\bigwedge \Pi \rightarrow \bigvee \Lambda\vdash \bigwedge \Gamma \rightarrow \bigvee \Delta $ in $\mathbf{LK}$, then $p(\Gamma\vdash\Delta)=p(\Pi\vdash\Lambda)$. We prove that our probabilistic sequent calculus {\bf LKprob} is sound and complete with respect to the models just described. \begin{thebibliography}{10} \bibitem{cite1} {\scshape A. M. Frisch, P. Haddawy}, {\itshape Anytime deduction for probabilistic logic}, {\bfseries\itshape Artificial Intelligence}, vol.~69 (1993), pp.~93122. \bibitem{cite2} {\scshape T. Hailperin}, {\itshape Probability logic}, {\bfseries\itshape Notre Dame Journal of Formal Logic}, vol.~25 (1984), pp.~198212. \bibitem{cite3} {\scshape Z. Ognjanovi\'c, M. Ra\v skovi\'c, Z. Markovi\'c}, {\itshape Probability logics}, {\bfseries\itshape Logic in Computer Science}, Zbornik radova 12 (20), Z. Ognjanovi\'c (ed.), Mathematical Institute SANU, Belgrade, 2009, pp. ~35111. \bibitem{cite4} {\scshape C. G. Wagner}, {\itshape Modus tollens probabilized}, {\bfseries\itshape British Journal for the Philosophy of Science}, vol.~54(4) (2004), pp.~747–753. \end{thebibliography} 
18:10  Displaytype calculi for non classical logics SPEAKER: Sabine Frittella ABSTRACT. The proposed talk gives a general outline of a line of research aimed at providing a wide array of logics (spanning from dynamic logics to monotone modal logic through substructural logics) with display type proof systems which in particular enjoy a uniform strategy for cut elimination. We generalize display calculi in two directions: by explicitly allowing different types, and by dropping the full display property. The generalisation to a multitype environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth prooftheoretic treatment of multimodal and dynamic logics. The generalisation to a setting in which the full display property is not required makes it possible to account for logics, such as monotone modal logic, which admit connectives which are neither adjoints nor residuals. 
16:30  Complexity bounds for Multiagent Justification Logic SPEAKER: Antonis Achilleos ABSTRACT. We investigate the complexity of systems of Multiagent Justification Logic with interacting justifications (see [1]). The system we study has n agents, each based on some (singleagent) justification logic (we consider J, J4, JD, JD4, JT, LP) and a transitive, irreflexive binary relation, C. Each agent i has its own set of axioms, depending on the logic it is based on. If iCj, then we include axiom t:i φ > t:j φ (we do not include VVerification as in [1]). Finally, it has a sufficient amount of propositional axioms and an axiomatically appropriate constant specification, which is in P. Traditionally, to establish upper complexity bounds for satisfiability for Justification Logic, we use a set of tableau rules to generate a branch and then we run the ∗calculus on it. A similar system for (diamondfree) modal logic was studied in [2]. We adjust appropriately the tableau for the corresponding system in [2] and the ∗calculus can be run locally for every prefix, so we can use the same methods as in [2] to establish upper bounds. On the other hand, we can see that if we replace [i] by x:i in a diamondfree modal formula (for all i), then the new formula is satisfiable iff the old one was. Thus, we can prove the same complexity bounds as in [2]  with the exception that where satisfiability for a modal logic is in NP, the corresponding justification logic has its satisfiability in the second level of the polynomial hierarchy. [1] Antonis Achilleos, Complexity jumps in Multiagent Justification Logic with interacting justifications, Under submission [2] ____ Modal logics with hard diamondfree fragments, Under submission 
16:50  The relation between the graphs structures and proof complexity of corresponding Tseitin graph tautologies SPEAKER: Armen Mnatsakanyan ABSTRACT. We describe two sufficient properties of graphs Gn on n vertices such that the formulas based on them have exponential Resolution proof steps. The network style graphs of Tseitins formulas and graphs of Urquhart are examples of graphs with mentioned properties. If at least one of these properties is not valid for any graph, then the corresponding formula has polynomial bounded resolution refutation. 
17:10  The algorithmic complexity of decomposability in fragments of firstorder logic SPEAKER: Denis Ponomaryov ABSTRACT. We consider the decomposability problem for finite theories, i.e. the problem to decide whether a theory can be represented as a union of two (or several) theories sharing a given set of signature symbols. The algorithmic complexity of this problem has been studied in various calculi, ranging from firstorder logic to classical propositional and Description Logics. The results suggested that the complexity of decomposability coincides with the complexity of entailment in the underlying logic. Although this observation was not too surprising, a general method for proving this claim was missing. We describe a method of proving that the complexity of deciding decomposability coincides with the complexity of entailment in fragments of firstorder logic. We illustrate this method by showing the complexity of decomposability in signature fragments of firstorder logic, i.e. those which are obtained by putting restrictions on signature. 
17:30  Type equations and second order logic SPEAKER: Paolo Pistone ABSTRACT. The aim of this talk is to propose a constructive understanding of second order logic: it is argued that a better grasp of the functional content of the comprehension rule comes from the consideration of inference rules independently of logical correctness; the situation is analogous to that of computation, whose proper functional description imposes to consider non terminating (i.e. “wrong”) algorithms. The CurryHoward correspondence allows indeed a shift from the question of provability (within a formal system) to that of typability for pure lambda terms, representing for instance recursive functions. By relying on wellknown results on type inference, an equational description, independent of type systems, of the predicates required to build proofs of totality is presented: one no more focuses on what one can prove by means of a certain package of rules, but rather on what the rules needed to prove a certain formula must be like, at the level of their functional description. This might look a bit weird at first glance: by applying this technique it is possible, in principle, to construct second order proofs of totality for all partial recursive functions! The assumption that every system of type equations defines a set of types is indeed equivalent to a naive comprehension axiom. The focus on typability conditions exposes a different point of view on the phenomenon of incompleteness: the lack of the relevant “diagonal” or “limit ” proof is indeed explained by the lack of the relevant “diagonal” or “limit” predicates. On the other hand, on the basis of a characterization of the solvability of type equations by means of recursive techniques, it is conjectured that such a “naıve” approach to second order proofs is “complete” in the following sense: all total recursive functions are provably total in some consistent subsystem of the whole (violently inconsistent) system of equational types. 
17:50  An intuitive semantics for {Full Intuitionistic Linear Logic} SPEAKER: unknown ABSTRACT. This work describes an intuitive semantics in the style of Girard's wellknown cigarette vending machine for Full Intuitionistic Linear Logic. Full Intuitionistic Linear Logic (FILL) was introduced by Hyland and de Paiva [1] as arising from its categorical semantics, while hinting at its independent interest as a framework for forms of parallelism in Functional Programming. The systems FILL and its intuitionistic counterpart FIL[2] show that the constructive character of logical systems is not given by syntactic size restrictions on sequent calculus, but comes about by explaining connectives in terms of intensional constructions/operations/transformations on derivations of the system. This seems to us the central message of the BrouwerHeytingKolmogorov (BHK) interpretation and also of the CurryHoward isomorphism, which we take as guiding criteria for our mathematical logic investigations. This work also aims to explain to the mythical manonthe street what Full Intuitionistic Linear Logic is about. We were pressed on the point that, elegance of categorical constructions and esthetic criteria on proof systems notwithstanding, one should always be able to say what our logical operations mean in common words, when describing a new logical system like FILL. Initially we had no intuitive explanation for the multiplicative disjunction 'par', which now seems more understandable in terms of interactions with a 'stockkeeping' system. 
18:10  Argumentation Logic SPEAKER: unknown ABSTRACT. Born out of the need to formalize common sense in Articial Intelligence (AI), Ar gumentation Logic (AL) brings together the syllogistic roots of logic with recent argumentation theory from AI to propose a new logic based on argumentation. Argumentation Logic is purely proof theoretic dened via a criterium of acceptabil ity of arguments. Arguments in AL are sets of propositional formulae with the acceptability of an argument ensuring that the argument can defend against any other argument that is inconsistent with it, under a given propositional theory. AL can be linked to Natural Deduction allowing us to reformulate Propositional Logic (PL) in terms of argumentation and to show that, under certain conditions, AL and PL are equivalent. AL separates proofs into direct and indirect ones, the latter being through the use of a restricted form of Reductio ad Absurdum (RAA) where the (direct) derivation of the inconsistency must depend on the hypothesis posed when we apply the RAA rule. As such AL is able to isolate inconsistencies in the given theory and to behave agnostically to them. This gives AL as a conservative paraconsistent extension of PL that does not trivialize in the presence of inconsistency. The logic then captures in a single framework defeasible reasoning and its synthesis with the strict form of reasoning in classical logic. The interpretation of implication in AL is dierent from that of material implication, closer to that of default rules but where proof by contradiction can be applied with them. AL has recently formed the basis to formalize psychological theories of story comprehension. 
16:30  On the existential interpretability of structures SPEAKER: unknown ABSTRACT. We study the $\exists$interpretability of constructive structures of finite predicate signatures. This definition is motivated by a kind of effective interpretability of abstract databases and leads to a good natural translation of $\exists$queries. The following definition is a restricted variant of the standard wellknown definition of interpretability of structures: \smallskip \noindent{\bf Definition. } {\it Let $\mathfrak{A}_0$ and $\mathfrak{A}_1$ be two structures of finite predicate signatures and let $\langle P_1,\ldots, P_k\rangle$ be the signature of $\mathfrak{A}_0$. We say that $\mathfrak{A}_0$ has a $\exists$interpretation in $\mathfrak{A}_1$ if there exist \begin{itemize} \item $n\in\omega$ and a finite tuple of parameters $\bar p\in\mathfrak{A}_1$, \item $\exists$formula $U(\bar x,\bar y)$, $\bar x=n$, \item $\exists$formulas $E^+(\bar x_0,\bar x_1,\bar y)$ and $E^(\bar x_0,\bar x_1,\bar y)$ such that $\bar x_0=\bar x_1=n$, \item $\exists$formulas $P^+(\bar x_1,\ldots,\bar x_m,\bar y)$ and $P^(\bar x_1,\ldots,\bar x_m,\bar y)$, for each predicate symbol $P$ of the signature of $\mathfrak{A}_0$, where $m$ is the arity of $P$ with the property $\bar x_1=\cdots=\bar x_m=n$, \end{itemize} such that \begin{enumerate} \item The set $(U^{\mathfrak{A}_1}(\bar x))^2$ is a disjunct union of the sets $\{\langle\bar x_0,\bar x_1\rangle\mid \mathfrak{A}_1\models E^\varepsilon(\bar x_0,\bar x_1,\bar p)\}$, $\varepsilon\in\{+,\}$. \item For any $m$ary predicate symbol $P$ of the signature of $\mathfrak{A}_0$, the set $(U^{\mathfrak{A}_1}(\bar x))^m$ is a disjunct union of the sets $\{\langle\bar x_0,\ldots,\bar x_m\rangle\mid \mathfrak{A}_1\models P^\varepsilon(\bar x_0,\ldots,\bar x_m,\bar p)\}, \ \varepsilon\in\{+,\}$. \item Let $\widehat{P_i}=\{\langle\bar x_1,\ldots,\bar x_m\rangle\mid\mathfrak{A}_1\models P^+(x_1,\ldots,\bar x_m,\bar p)\}, \mbox{ äëÿ }i=1,\ldots,k$. Then the relation $E=\{\langle \bar x_0,\bar x_1\rangle\mid\mathfrak{A}_1\models E^+(\bar x_0,\bar x_1,\bar p)\}$ is a congruence on $\mathfrak{B}=\langle U^{\mathfrak{A}_1}(\bar x),\widehat{P}_1,\ldots,\widehat{P}_k\rangle$ and the quotient algebra $\mathfrak{B}/\!E$ is isomorphic to $\mathfrak{A}_0$. \end{enumerate} } \noindent{\bf Theorem. } {\it \begin{enumerate} \item The $\exists$interpretability generates an upper semilattice ${\mathcal L}_\exists$ in which computable structures form a principal ideal ${\mathcal L}^0_\exists$; in particular, there exists a universal computable structure, i.e., a computable structure that $\exists$interprets any computable structure. \item Any finite partial order is embeddable into ${\mathcal L}^0_\exists$. \end{enumerate} } 
16:50  The isomorphism problem for computable projective planes SPEAKER: Nurlan Kogabaev ABSTRACT. Computable presentations for projective planes are studied. We prove that the isomorphism problem is $\Sigma^1_1$complete for the following classes of projective planes: pappian projective planes, desarguesian projective planes, arbitrary projective planes. 
17:10  Coding graphs into fields SPEAKER: Russell Miller ABSTRACT. It is well established that the class of countable symmetric irreflexive graphs is complete in computable model theory: every countable structure in a finite language can be coded into a graph in such a way that the graph has the same spectrum, the same computable dimension, and the same categoricity spectrum as the original structure, and shares most other known computablemodeltheoretic properties of the original structure as well. In 2002, Hirschfeldt, Khoussainov, Shore, and Slinko collected related results and proved more, showing that many other classes of countable structures are complete in the same sense. On the other hand, classes such as linear orders, Boolean algebras, trees, and abelian groups are all known not to be complete in this way. We address the most obvious class for which this question was still open, by giving a coding of graphs into countable fields in such a way as to preserve all of these properties. 
17:30  Uniformization in the hereditarily finite list superstructure over the real exponential field SPEAKER: Svetlana Aleksandrova ABSTRACT. This work is concerned with the generalized computability theory, as well as properties of the real exponential field. To describe computability we use an approach via definability by Sigmaformulas in hereditarily finite superstructures, which was introduced in [1]. In particular, we establish the uniformization property for Sigmapredicates in the hereditarily finite list superstructure over the real exponential field. (See [2] for the structure's definition) We shall outline the proof of the following theorem. Theorem 1. For any Sigmapredicate P in the hereditarily finite list superstructure over the real exponential field exists a Sigmafunction f such that its domain dom(f)={x: exists y P(x,y)} and its graph G(f) is a subset of P. As a corollary we obtain existence of an universal Sigmafunction in the same structure. 1. Ershov, Yu. L. (1996). Definability and Computability, Consultants Bureau, New YorkLondonMoscow. 2. Goncharov, S. S. and Sviridenko, D. I. (1985). Sigmaprogramming (Russian), Vychisl. Sist. 107, pp. 329. 
17:50  Dynamic logic on approximation spaces SPEAKER: Alexey Stukachev ABSTRACT. We present recent results on a version of dynamic logic suitable to describe properties of approximation spaces, with the set of finite elements considered as a structure (typical example is the set of rational numbers within the set of real numbers). We consider the case when this structure generates on a whole approximation space an induced structure in a way definable in dynamic logic. We apply this general technique to approximation spaces from effective model theory and HFcomputability. 
18:10  On limitwise monotonic reducibility of Σ^0_2sets. SPEAKER: Damir Zainetdinov ABSTRACT. One of the directions of research in modern computability theory focus on studying properties of limitwise monotonic functions and limitwise monotonic sets. We prove the existence of incomparable Σ^0_2sets relative to limitwise monotonic reducibility and there is no maximal element in the class of all lmdegrees of Σ^0_2sets. Moreover, we prove that every countable partial order can be embedded into the class of all lmdegrees of Σ^0_2sets. 
16:30  Relativized universal numberings SPEAKER: unknown ABSTRACT. We study the greatest under reduction computable numberings of families of sets which are uniformly computably enumerable relative to an arbitrary oracle. 
16:50  Ideals without minimal numberings in the Rogers semilattice SPEAKER: Assylbek Issakhov ABSTRACT. It is well known many infinite families of c.e. sets whose Rogers semilattice contains an ideal without minimal elements, for instance, the family of all c.e. sets, \cite{Ers}. Moreover, there exists a computable family of c.e. sets whose Rogers semilattice has no minimal elements at all, \cite{Bad2}. In opposite to the case of the families of c.e. sets, for every computable numbering $\alpha$ of an infinite family $\mathfrak F$ of computable functions, there is a Friedberg numbering of $\mathfrak F$ which is reducible to $\alpha$, \cite{Ers}. This means that the Rogers semilattice of any computable family of total functions from level 1 of the arithmetical hierarchy contains no ideal without minimal elements. We study computable families of total functions of any level of the KleeneMostowski hierarchy above level 1 and try to find elementary properties of Rogers semilattices that are different from the properties of Rogers semilattices for the families of computable functions. \begin{theorem}\label{th1} For every n, there exists a $\Sigma^0_{n+2}$computable family of total functions whose Rogers semilattice contains an ideal without minimal elements. \end{theorem} Note that every Rogers semilattice of a $\Sigma^0_{n+2}$computable family $\mathfrak F$ contains the least element if $\mathfrak F$ is finite, \cite{Ers}, and infinitely many minimal elements, otherwise, \cite{BG}. Theorem \ref{th1} is based on the following criterion that extends the criterion for minimal numbering from \cite{Bad2}. \begin{theorem} Let $\alpha$ be a numbering of an arbitrary set $\mathcal S$. Then there is no minimal numbering of $\mathcal S$ that is reducible to $\alpha$ if and only if, for every c.e. set $W$, if $\alpha (W)=S$ then there exists a c.e. set $V$ such that $\alpha (V)=\mathcal S$ and, for every positive equivalence $\varepsilon$, either $\varepsilon\upharpoonright W\nsubseteq \theta_{\alpha}$ or $W\nsubseteq [V]_{\varepsilon}$. \end{theorem} \begin{thebibliography}{100} \bibitem{Ers} {\scshape Yu. L. Ershov}, {\bfseries\itshape Theory of numberings}, Nauka, Moscow, 1977 (in Russian). \bibitem{Bad2} {\scshape S. A. Badaev}, {\itshape On minimal enumerations}, {\bfseries\itshape Siberian Adv. Math.}, vol. 2 (1992), no. 1, pp. 130. \bibitem{BG} {\scshape S. A. Badaev and S. S. Goncharov}, {\itshape Rogers semilattices of families of arithmetic sets}, {\bfseries\itshape Algebra and Logic}, vol. 40 (2001), no. 5, pp. 283291. \end{thebibliography} 
17:10  Computable numberings in Analytical Hierarchy SPEAKER: Marina Dorzhieva ABSTRACT. We investigate minimal enumerations in analytical hierarchy. One of the most important minimal numberings is Friedbergs numbering. Owings showed that there is no Pi^1_1computable Friedberg enumeration of all Pi^1_1sets using metarecursion theory. This result is obtained in classic computability theory for higher levels of analytical hierarchy. 
17:30  Definability of 0' in the structure of $\omega$enumeration degrees SPEAKER: Andrey Sariev ABSTRACT. In this paper we find a first order formula which defines the first jump of the least element in the structure of the $\omega$enumeration degrees. 
17:50  Embedding the omegaenumeration degrees into the Muchnik degrees generated by spectra of structures SPEAKER: Stefan Vatev ABSTRACT. For an infinite sequence of sets $\mathscr{R} = \{R_n\}_{n\in\omega}$ and a set $X$, we write $\mathscr{R}\leq_{c.e.} X$ if for every $n$, $R_n$ is computably enumerable in $X^{(n)}$, uniformly in $n$. Soskov \cite{omegadegrees} considered the following redicibility between sequences of sets \[\mathscr{R} \leq_\omega \mathscr{P}\mbox{ iff }(\forall X \subseteq \mathbb{N})[\mathscr{P} \leq_{c.e.} X\ \Rightarrow\ \mathscr{R}\leq_{c.e.} X].\] This reducibility naturally induces an equivalence relation, whose equivalence classes are called $\omega$enumeration degrees. They form an upper semilattice, which have been extensively studied by a number of researchers in Sofia University over the past decade. In this talk we discuss how to encode an infinite sequence of sets $\mathscr{R}$ into a single countable structure $\mathcal{N}_{\mathscr{R}}$, preferably in a finite language, such that the Turing degree spectrum of $\mathcal{N}_{\mathscr{R}}$ is the set \[Sp(\mathcal{N}_{\mathscr{R}}) = \{d_T(X) \mid \mathscr{R} \mbox{ is c.e. in }X\}.\] We present two such methods. The first one was studied by Soskov \cite{soskov} and is based on the socalled Marker's extensions \cite{marker}. The other approach is based on the idea of coding each set $R_n$ by a sequence of pairs of computable structures \cite{pairsrecstr}. We conclude that for any two infinite sequences of sets $\mathscr{R}$ and $\mathscr{P}$ we can build countable structures $\mathcal{N}_{\mathscr{R}}$ and $\mathcal{N}_{\mathscr{P}}$ such that \[\mathscr{R} \leq_\omega \mathscr{P}\ \iff\ Sp(\mathcal{N}_{\mathscr{P}}) \subseteq Sp(\mathcal{N}_{\mathscr{R}}).\] In other words, the $\omega$enumeration degrees are embeddable into the Muchnik degrees generated by spectra of structures. 
18:10  Limitwise monotonic sets of reals SPEAKER: unknown ABSTRACT. We extend the limitwise monotonicity notion to the case of arbitrary computable linear ordering to get a set which is limitwise monotonic precisely in the noncomputable degrees. Also we get a series of connected nonuniformity results to obtain new examples of nonuniformly equivalent families of computable sets with the same enumeration degree spectrum. 
16:30  An Intuitionistic Interpretation of Classical Implication SPEAKER: unknown ABSTRACT. A connection between the classical and the Heyting's logic is given by the Glivenko's Theorem: for every propositional formula $A$, $A$ is classically provable iff $\neg\neg A$ is provable intuitionistically. \rm This theorem can be understood as a possible way of intuitionistic interpretation of the classical reasoning. Embedding of the implicative fragment of classical logic into the implicative fragment of the Heyting's logic was considered by J. P. Seldin [3] and L. C. Pereira, E. H. Haeusler, V. G. Costa, W. Sanz [2]. Seldin's interpretation essentially depends on the presence of conjunction, but the second one is obtained in the pure language of implication. Here we define, in spirit of Kolmogorov's interpretation, a mapping of the pure implicational propositional language enabling to prove the corresponding result. Let $p_1,\dots,p_n$ be a list of all propositional letters occurring in formula $A\to B$ and $q$ any propositional letter not occurring in $A\to B$. Then the image $b(A\to B)$ of $A\to B$ is defined inductively as follows: $b(p)=(p\to q)\to q$, for each $p\in\{p_1,\dots,p_n\}$, and $b(A\to B)=b(A)\to b(B)$. Namely, $b(A\to B)$ is obtained by replacing each occurrence of a propositional letter $p$ in $A\to B$ by $(p\to q)\to q$, where $q$ is a new letter. {\bf Embedding Lemma.} \emph{For every propositional implicational formula $A$, $A$ is provable in classical logic iff $b(A)$ is provable in Heyting logic.} This is a part of our paper [1] dealing with an alternative approach to normalization of the implicative fragment of classical logic. \begin{thebibliography}{10} \bibitem{cite1} {\scshape B. Bori\v ci\'c, M. Ili\'c}, {\itshape An Alternative Normalization of the Implicative Fragment of Classical Logic}, \rm (to appear). \bibitem{cite2} {\scshape L. C. Pereira, E. H. Haeusler, V. G. Costa, W. Sanz}, {\itshape A new normalization strategy for the implicational fragment of classical propositional logic}, {\bfseries\itshape Studia Logica}, vol. 96 (2010), no. 1, pp. 95108. \bibitem{cite3} {\scshape J. P. Seldin}, {\itshape Normalization and excluded middle I}, {\bfseries\itshape Studia Logica}, vol. 48 (1989), no. 2, pp. 193217. \end{thebibliography} 
16:50  Predicate Glivenko theorems and substructural aspects of negative translations SPEAKER: unknown ABSTRACT. In [1], the second author has developed a prooftheoretic approach to Glivenko theorems for substructural propositional logics. In the present talk, by using the same techniques, we will extend them for substructural predicate logics. It will be pointed out that in this extension, the following double negation shift scheme (DNS) plays an essential role. (DNS): \forall x \neg \neg \varphi(x) \rightarrow \neg \neg \forall x \varphi(x)$ Among others, the following is shown, where QFLe and QFLe$^{\dagger}$ are predicate extensions of FLe and FLe$^{\dagger}$, respectively (see [1]). The Glivenko theorem holds for QFLe$^{\dagger}$ +(DNS) relative to classical predicate logic. Moreover, this logic is the weakest one among predicate logics over QFLe for which the Glivenko theorem holds relative to classical predicate logic. Then we will study negative translations of substructural predicate logics by using the same approach. We introduce a negative translation, called extended Kuroda translation and over QFLe it will be shown that standard negative translations like Kolmogorov translation and G\"odelGentzen translation are equivalent to our extended Kuroda translation. Thus, we will give a clearer unified understanding of these negative translations by substructural point of view. 
17:10  Adding a Conditional to Kripke's Theory of Truth SPEAKER: Lorenzo Rossi ABSTRACT. I address the lack of expressiveness of Kripke's theory of truth (over arithmetic) along the lines suggested by H. Field, namely equipping it with a primitive, nontrivial conditional. However, I focus my attention on computationally simple methods to interpret a primitive conditional. I provide an inductive construction and define a corresponding monotone operator that improves on Kripke's construction and show some nice features. 
17:30  Constructive completeness and Joyal's theorem SPEAKER: Henrik Forssell ABSTRACT. We present a unifying, categorical approach to several constructive completeness theorems for intuitionistic (and classical) firstorder theories, as well for theories in certain fragments of firstorder logic, based on a theorem by A. Joyal [Thm 6.3.5, Makkai and Reyes, 1977]. We show that the notion of exploding (Tarski) model introduced by W. Veldman [Veldman 1976] is adequate for certain fragments of firstorder logic (as well as for classical firstorder logic) and that Veldman's modified Kripke semantics arises, as a consequence, as semantics in a suitable sheaf topos. In the process we give an alternative proof of Veldman's completeness theorem, and note the equivalence of this theorem with the Fan Theorem. Finally, we show that the disjunctionfree fragment is constructively complete with respect to modified Kripke semantics without appeal to the Fan Theorem, as well as without appeal to decidable axiomatizability and size restrictions on the language. This is joint work with Christian Espindola. 
17:50  Algorithmicalgebraic canonicity for mucalculi SPEAKER: Andrew Craig ABSTRACT. The correspondence and completeness of logics with fixed point operators has been the subject of recent research (see~\cite{BezHod:TCS},~\cite{muALBA}). These works aim to develop a Sahlqvistlike theory for their respective fixed point settings. That is, they identify classes of formulas which are preserved under canonical extensions and have firstorder frame correspondents. We prove that the members of a certain class of intuitionistic muformulas are \emph{canonical}, in the sense of~\cite{BezHod:TCS}. When projected onto the classical case, our class of canonical muformulas subsumes the class described in~\cite{BezHod:TCS}. Our methods use a variation of the algorithm ALBA (Ackermann Lemma Based Algorithm) developed in~\cite{DistMLALBA}. We show that all muinequalities that can be successfully processed by our algorithm, $\mu^*$ALBA, are canonical. Formulas are interpreted on a bounded distributive lattice $\A$ with additional operations. The canonical extension of $\A$, denoted $\A^\delta$, is a complete lattice in which the completely joinirreducible elements ($\jty(\A^\delta)$) are joindense, and the completely meetirreducible elements ($\mty(\A^\delta)$) are meetdense. An \emph{admissible valuation} takes all propositional variables to elements of $\A$. The algorithm aims to ``purify'' an inequality $\alpha \leq \beta$ by rewriting it as a (set of) pure (quasi)inequalities. A pure quasiinequality has no occurrences of propositional variables; only special variables whose interpretations range over $\jty(\A^\delta) \cup \mty(\A^\delta)$ are present. The fact that admissible and ordinary validity coincide for pure inequalities is the lynchpin for proving canonicity. The proof of the soundness of the rules of the algorithm $\mu^*$ALBA rests on the ordertopological properties of formulas (term functions) of the $\mu$calculus. 
18:10  ProofTheoretic Analysis of Brouwer's Argument of the Bar Induction SPEAKER: Ryota Akiyoshi ABSTRACT. ¥begin{document} ¥thispagestyle{empty} %% BEGIN INSERTING YOUR ABSTRACT DIRECTLY BELOW; %% SEE INSTRUCTIONS (1), (2), (3), and (4) FOR PROPER FORMATS ¥NP ¥absauth{Ryota Akiyoshi} ¥meettitle{ProofTheoretic Analysis of Brouwer's Argument of the Bar Induction} ¥affil{Faculty of Letters, Kyoto University, Yoshidahonmachi, Sakyo Ward, Kyoto Prefecture 6068501, Japan} ¥meetemail{georg.logic@gmail.com} In a series of papers, Brouwer had developed intuitionistic analysis, in particular the theory of choice sequences. An important theorem called the ``fan theorem" plays an essential role in the development of it. The fan theorem was derived from another stronger theorem called the ``bar induction", which is an induction principle on a wellfounded tree. We refer to [4,5] as standard references of Brouwer's intuitionistic analysis. Brouwer's argument in [1] contains a controversial assumption on canonical proofs of some formula. In many cases, constructive mathematicians have assumed the bar induction as axiom, hence the assumption has not been examined by them. In this talk, we sketch an approach of Brouwer's argument via infinitary proof theory. We point out that there is a close similarity between Brouwer's argument and Buchholz' method of the $¥Omega$rule ([2,3]). In particular, Brouwer's argument in [1] seems very close to Buchholz' embedding theorem of the (transfinite) induction axiom of $ID_{1}$ in [2], which is a theory of noniterated inductive definition. By comparing these two arguments, we give a natural explanation of why Brouwer needed the assumption. Our conclusion is that Brouwer supposed the assumption in order to avoid the impredicativity or a vicious circle which is essentially the same as one in the $¥Omega$rule for $ID_{1}$. In other words, the impredicativity can be explained in a very clear way from the view point of the $¥Omega$rule. Moreover, Brouwer's argument can be formulated in a mathematically precise way by the $¥Omega$rule. Therefore, we conclude that his introduction of the assumption is mathematically wellmotivated. If time is permitting, we suggest how to carry out this idea in a mathematical way. ¥begin{thebibliography}{10} ¥bibitem{B1} {¥scshape Luitzen Egbertus Jan Brouwer}, {¥itshape ¥"{U}ber Definitionsbereiche von Funktionen}, {¥bfseries¥itshape Mathematische Annalen}, vol.~97, 1927, pp.~6075. ¥bibitem{B2} {¥scshape Wilfried Buchholz}, {¥itshape The $¥Omega_{¥mu +1}$Rule}, in {¥bfseries¥itshape Iterated Inductive Definitions and Subsystems of Analysis: Recent ProofTheoretical Studies}, LNM 897, 1981, pp.~188233. ¥bibitem{B3} {¥scshape Wilfried Buchholz}, {¥itshape Explaining the {G}entzen{T}akeuti reduction steps}, {¥bfseries¥itshape Archive for Mathematical Logic}, vol.~40, pp.~255272. ¥bibitem{D1} {¥scshape Michael A. E. Dummett}, {¥bfseries¥itshape Elements of Intuitionism}, 2nd edition, OUP, 2000. ¥bibitem{TvD} {¥scshape A. S. Troelstra and D. van Dalen}, {¥bfseries¥itshape Constructivism in Mathematics}, Vol.1, NorthHolland, 1988. %% 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}) ¥end{thebibliography} ¥vspace*{0.5¥baselineskip} % this space adjustment is usually necessary after a bibliography ¥end{document} 
16:30  On ExplicitImplicit Reflection Principles. SPEAKER: Elena Nogina ABSTRACT. Reflection principles based on provability predicates were introduced in the 1930s by Rosser and Turing, and later were explored by Feferman, Kreisel & Levi, Schmerl, Artёmov, Beklemishev and others. We study reflection principles of Peano Arithmetic based on both proof and provability predicates. We find a classification of these principles and establish their linear ordering with respect to their deductive strength in Peano Arithmetic. The proof essentially relies on the GödelLöbArtёmov logic GLA. 
16:50  Ordinal Notations and Fundamental Sequences in Caucal Hierarchy SPEAKER: Fedor Pakhomov ABSTRACT. The Caucal hierarchy of infinite graphs with colored edges is a wide class of graphs with decidable monadic theories[1]. Graphs from this hierarchy can be considered as structures with finite number of binary relations. It is known that the exact upper bound for order types of the wellorderings that lie in this class is ε0 [2]. Actually, any wellordering from Caucal hierarchy can be used as a constructive ordinal notation system. We investigate systems of fundamental sequences for that wellorderings and the corresponding fastgrowing hierarchies of computable functions. For a wellordering (A,<) we can determine a system of fundamental sequences λ[n] by a relation Cs(x,y) such that Cs(α, β) <=> α is a limit point of < A and β = α[n], for some n. Our principal result is that for a wellordering with a pair of Schmidtcoherent fundamental sequences (A,<,Cs1,Cs2) from Caucal hierarchy the corresponding fastgrowing hierarchies fα1(x) and fα2(x) are equivalent in the following sense: for all α < β we have fβ1(n) > fα2(n) and fβ1(n) > fα2(n), for all large enough n (Schmidtcoherence is a classical condition that implies that functions from fastgrowing hierarchy are strictly increasing [3]). We show that any two wellorderings with Schmidtcoherent systems of fundamental sequences from Caucal hierarchy of the same order type < ω^ω give rise to the equivalent fastgrowing hierarchies. We also prove that it is possible to extend a graph with a wellordering from Caucal hierarchy by a Schmidtcoheren system of fundamental sequences for the wellordering in such a way that the resulting graph will lie in Caucal hierarchy. [1] Didier Caucal, On Infinite Terms Having a Decidable Monadic Theory, Mathematical Foundations of Computer Science 2002 (Diks, Krzysztof and Rytter, Wojciech), vol. 2420, Springer Berlin Heidelberg, 2002, pp. 165–176. [2] Braud Laurent, Arnaud Carayol, Linear Orders in the Pushdown Hierarchy, Lecture Notes in Computer Science (Samson Abramsky, et.al. eds.), vol. 6199, Springer Berlin Heidelberg, 2010, pp. 88–99. [3] Diana Schmidt, Builtup Systems of Fundamental Sequences and Hierarchies of NumberTheoretic Functions, Archive for Mathematical Logic, vol. 18 (1976), pp. 47–53. 
17:10  The maximal order type of the trees with the gapembeddability relation SPEAKER: Jeroen Van der Meeren ABSTRACT. In 1985, Harvey Friedman introduced a new kind of embeddability relation between finite labeled rooted trees, namely the gapembeddability relation. Under this embeddability relation, the set of finite rooted trees with labels bounded by a fixed natural number n is a wellpartialordering. The wellpartialorderedness of these trees (if we put a universal quantifier in front) gives rise to a statement not provable in Pi11CA_0. There are still some open questions left about these famous wellpartialorderings. For example, what is the maximal order type of these sets of trees with the gapembeddability relation? The maximal order type of a wellpartialordering is an important characteristic of that wellpartialordering and it captures in some sense its strength. In this talk, I will discuss some new recent developments concerning this topic. 
17:30  Computational reverse mathematics and foundational analysis SPEAKER: Benedict Eastaugh ABSTRACT. Reverse mathematics studies which natural subsystems of second order arithmetic are equivalent to key theorems of ordinary or nonsettheoretic mathematics. The main philosophical application of reverse mathematics proposed thus far is foundational analysis, which explores the limits of various weak foundations for mathematics in a formally precise manner. Richard Shore [1, 2] proposes an alternative framework in which to conduct reverse mathematics, called computational reverse mathematics. The formal content of his proposal amounts to restricting our attention to omegamodels of RCA0 when we prove implications and equivalences in reverse mathematics. Despite some attractive features, computational reverse mathematics is inappropriate for foundational analysis, for two major reasons. Firstly, the computable entailment relation employed in computational reverse mathematics does not preserve justification for all of the relevant foundational theories, particularly a partial realisation of Hilbert’s programme due to Simpson [3]. Secondly, computable entailment is a Pi^1_1complete relation, and hence employing it commits one to theoretical resources which outstrip those acceptable to the stronger foundational programmes such as predicativism and predicative reductionism. This argument can be formalised within second order arithmetic, making it accessible to partisans of foundational frameworks such as predicativism. In doing so we show that the existence of the set of sentences which are computably entailed is equivalent over ACA0 to Pi^1_1 comprehension. [1] Shore, R. A., Reverse Mathematics: The Playground of Logic, The Bulletin of Symbolic Logic, vol. 16 (2010), no. 3, pp. 378–402. [2] Shore, R. A., Reverse mathematics, countable and uncountable: a computational approach, Effective Mathematics of the Uncountable, Lecture Notes in Logic, (D. Hirschfeldt, N. Greenberg, J. D. Hamkins, and R. Miller, editors), ASL and Cambridge University Press, Cambridge, 2013, pp. 150–163. [3] Simpson, S G., Partial realizations of Hilbert’s program, The Journal of Symbolic Logic, vol. 53 (1988), pp. 349–363. 
17:50  Semantic completeness of first order theories in constructive reverse mathematics SPEAKER: Christian Espindola ABSTRACT. We introduce a general notion of semantic structure for firstorder theories, covering a variety of constructions such as Tarski and Kripke semantics, and prove that, over Zermelo Fraenkel set theory (ZF), the completeness of such semantics is equivalent to the Boolean Prime Ideal theorem (BPI). In particular, we deduce that the completeness of that type of semantics for nonclassical theories is unprovable in intuitionistic Zermelo Fraenkel set theory IZF. Using results of Joyal and McCarty, we conclude also that the completeness of Kripke semantics is equivalent, over IZF, to the Law of Excluded Middle plus BPI. By results from Banaschewski and Bhutani, none of these two principles imply each other, and so this gives the exact strength of Kripke completeness theorem in the sense of constructive reverse mathematics. 
18:10  Reverse Mathematics, more explicitly SPEAKER: Sam Sanders ABSTRACT. The program Reverse Mathematics can be viewed as a classification of theorems of ordinary mathematics from the point of view of computability. Working in Kohlenbach’s higherorder Reverse Mathematics, we study an alternative classification of theorems of ordinary mathematics, namely based on the central tenet of Feferman’s Explicit Mathematics that a proof of existence of an object is converted into a procedure to compute said object. Nonstandard Analysis is used in an essential way. Our preliminary classification gives rise to the Explicit Mathematics theme (EMT). Intuitively speaking, the EMT states a standard object with certain properties can be computed by a functional if and only if this object merely exists classically with the same nonstandard properties. Besides theorems of classical mathematics, we also consider intuitionistic objects, like the fan functional.

16:30  A computability approach to three hierarchies SPEAKER: Linda Brown Westrick ABSTRACT. We analyze the computable part of three hierarchies from analysis and set theory. The hierarchies are those induced by the CantorBendixson rank, the differentiability rank of Kechris and Woodin, and the Denjoy rank. Our goal is to identify the descriptive complexity of the initial segments of these hierarchies. For example, we show that for each recursive ordinal alpha>0, the set of Turing indices of computable C[0,1] functions that are differentiable with rank at most alpha is Pi_{2alpha+1}complete. Similar results hold for the other hierarchies. Underlying of all the results is a combinatorial theorem about trees. We will present the theorem and its connection to the results. 
16:50  A generalization of Solovay's Sigmaconstruction with application to intermediate models SPEAKER: Vladimir Kanovei ABSTRACT. A Sigmaconstruction of Solovay is extended to the case of intermediate sets which are not necessarily subsets of the ground model, with a more transparent description of the resulting forcing notion than in a classical paper of Grigorieff. As an application, we prove that, for a given name t (not necessarily a name of a subset of the ground model), the set of all sets of the form t[G] (the Ginterpretation of t), G being generic over the ground model, is Borel. This result was first established by Zapletal by a descriptive set theoretic argument. 
17:10  A new lower bound for the length of the hierarchy of norms SPEAKER: Alexander Block ABSTRACT. A norm is a surjective function from the Baire space R onto an ordinal. Given two norms φ, ψ we write φ ≤_N ψ if φ continuously reduces to ψ. Then ≤_N is a preordering and so passing to the set of corresponding equivalence classes yields a partial order, the hierarchy of norms. Assuming the axiom of determinacy (AD) the hierarchy of norms is a wellorder. The length Σ of the hierarchy of norms was investigated by Löwe in [1]; he determined that Σ ≥ Θ^2 (where Θ := {α  There is a surjection from R onto α}). In his talk "Multiplication in the hierarchy of norms", given at the ASL 2011 North American Meeting in Berkeley, Löwe presented a binary operation × on the hierarchy of norms such that for wellchosen norms φ, ψ the ordinal rank of φ×ψ in the hierarchy of norms is at least as big as the product of the ordinal ranks of φ and ψ, which implies that Σ is closed under ordinal multiplication and so Σ ≥ Θ^ω. In this talk I will note that in fact for wellchosen norms φ, ψ the ordinal rank of φ×ψ is exactly the product of the ranks of φ and ψ with an intermediate factor of ω_1. Furthermore using a stratification of the hierarchy of norms into initial segments closed under the ×operation I will show that Σ ≥ Θ^(Θ^Θ). [1] BENEDIKT LÖWE, The length of the full hierarchy of norms, Rendiconti del Seminario Matematico dell'Università e del Politecnico di Torino, vol. 63 (2005), no. 2, pp. 161168. 
17:30  Unraveling $\Sigma^0_\alpha(\Pi^1_1)$Determinacy SPEAKER: Sherwood Hachtman ABSTRACT. In parallel with the Borel hierarchy, one can define the levels $\Sigma^0_{\alpha}(\Pi^1_1)$ ($\alpha <\omega_1$) of the Boreloncoanalytic hierarchy by starting with $\Pi^1_1$ in place of the class $\Delta^0_1$ of clopen sets. In this talk, we consider the consistency strength of determinacy for infinite perfectinformation games with payoff in $\Sigma^0_\alpha(\Pi^1_1)$. This has been computed exactly for $\alpha = 0, 1$, by Martin, Harrington, and J. Simms. For $\alpha > 1$, dual results of Steel~\cite{Steel} and Neeman~\cite{Neeman} have shown the strength to reside within a very narrow range in the region of a measurable cardinal $\kappa$ of largest possible Mitchell order $o(\kappa)$. However, an exact equiconsistency had yet to be isolated. We have recently completed work pinpointing the determinacy strength of levels of the Borel hierarchy of the form $\Sigma^0_{1+\alpha+3}$, showing a levelbylevel correspondence between these and a family of natural $\Pi_1$ reflection principles. Combining our techniques with those of \cite{Neeman} and \cite{Steel}, we can characterize the strength of $\Sigma^0_{1+\alpha+3}(\Pi^1_1)$DET in terms of inner models with measurable cardinals. In particular, $\Sigma^0_4(\Pi^1_1)$DET is equivalent to the existence of a mouse satisfying $(\exists \kappa) o(\kappa)=\kappa^{++}$ plus the schema that each true $\Pi_1$ statement with parameters in $P^2(\kappa)$ reflects to an admissible set containing $P(\kappa)$. We will also discuss progress on calculating the strength of $\Sigma^0_2(\Pi^1_1)$DET, relating this to Mitchell's hierarchy of weak repeat point measures. 
17:50  Determinacy of Refinements to the Difference Hierarchy of Coanalytic sets SPEAKER: Chris Le Sueur ABSTRACT. It is quite wellknown result of Martin that the existence of a measurable cardinal is enough to prove the determinacy of all boldface Pi^1_1 sets. The argument nicely modifies to get the determinacy of all lightface Pi^1_1 sets from the existence of O^sharp. With this argument in mind, I will discuss how the technique has been pushed since then to get more determinacy in the difference hierarchy of Pi^1_1 sets, including a family of new determinacy results following from sharplike hypotheses. To achieve this I will also demonstrate a generalised notion of computability suitable for defining the lightface Borel hierarchy in uncountable spaces. 
18:10  On proof complexities of strong equal modal tautologies. SPEAKER: Hakob Nalbandyan ABSTRACT. By analogy with the notions of determinative conjuncts in CPL, we introduce the same notion for modal tautologies. On the base of introduced modal determinative conjuncts we introduce the notion of strong equality for modal tautologies and compare different measures of proof complexity (size, steps, space and width) for them in some proof systems of MPL. We prove that 1) in some proof systems the strong equal modal tautologies have the same proof complexities and 2) there are such proof systems, in which some measures of proof complexities for strong equal modal tautologies are the same, the other measures differ from each other only by the sizes of tautologies. 
16:30  Reducts of simple (noncollapsed) FraisseHrushovski constructions SPEAKER: Omer Mermelstein ABSTRACT. FraisseHrushovski constructions were first introduced by Hrushovski as a method for constructing strongly minimal sets that do not fit within Zilber's trichotomy conjecture. The construction can be seen as a twostep process where first a rank $\omega$ structure is constructed from a countable amalgamation class, using a variation of a Fraisse limit construction, and then the structure is ``collapsed'' to a strongly minimal substructure. In this talk we acquaint ourselves with the rank $\omega$, noncollapsed version of the construction and its associated combinatorial geometry, and provide a general method of showing that one simple FraisseHrushovski construction is a (proper) reduct of another FraisseHrushovski construction. 
16:50  On Jonsson sets and some their properties. SPEAKER: Aibat Yeshkeyev ABSTRACT. Our interest is to obtain a new information on the modeltheoretic properties of the Jonsson theories and the structure of their classes of models. To date, the best studied of the perfect Jonsson theory and their classes of existentially closed models. In this thesis, we consider a new approach to the study of Jonsson theories. We will work with special subsets of the semantic model of fixed Jonsson theory or of some Jonsson fragment of an arbitrary complete theory. We introduce the notion of Jonsson set as the corresponding closure of some existential formula in the semantic model. Using of the Jonsson sets we consider such properties as a stability, a categoricity and a similarity of relevant models and theories related to these sets. 
17:10  Ultraproduct construction of representative utility functions with infinitedimensional domain SPEAKER: Geghard Bedrosian ABSTRACT. This paper applies model theory to macroeconomic theory. In mathematical models of macroeconomic theory, the hypothesis of a "representative agent" is ubiquitous, but the search for a rigorous justification has so far been unsuccessful and was ultimately abandoned until very recently. Herzberg (2010) constructed a representative utility function for finitedimensional social decision problems, based on an bounded ultrapower construction over the reals, with respect to the ultrafilter induced by the underlying social choice function (via the KirmanSondermann (1972) correspondence). However, since the decision problems of macroeconomic theory are typically infinitedimensional, Herzberg's original result is insufficient for many applications. We therefore generalise his result by allowing the social alternatives to belong to a general reflexive Banach space W; in addition to known results from convex analysis, our proof uses a nonstandard enlargement of the superstructure over the union of W with the reals, obtained by a bounded ultrapower construction with respect to the KirmanSondermann ultrafilter. 
17:30  An axiomatic approach to modelling of orders of magnitude SPEAKER: unknown ABSTRACT. %% FIRST RENAME THIS FILE \documentclass[bsl,meeting]{asl} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %TCIDATA{OutputFilter=Latex.dll} %TCIDATA{Version=5.50.0.2890} %TCIDATA{} %TCIDATA{BibliographyScheme=Manual} %TCIDATA{LastRevised=Monday, April 07, 2014 19:30:57} %TCIDATA{} %\documentclass[10pt,a4paper]{asl} \usepackage[latin1]{inputenc} \usepackage{amsmath} \usepackage{amsfonts} \usepackage{amssymb} \begin{document} \end{document}\AbstractsOn \pagestyle{plain} \def\urladdr#1{\endgraf\noindent{\it URL Address}: {\tt #1}.} \newcommand{\NP}{} \input{tcilatex} \begin{document} \thispagestyle{empty} %% BEGIN INSERTING YOUR ABSTRACT DIRECTLY BELOW; %% SEE INSTRUCTIONS (1), (2), (3), and (4) FOR PROPER FORMATS \NP \absauth{Bruno Dinis, Imme van den Berg} \meettitle{An axiomatic approach to modelling of orders of magnitude} % First author's affiliation \affil{CMAF, University of Lisbon,Faculdade de Ciências Universidade de Lisboa Campo Grande, Edifício C6, Gabinete 6.2.18 P1749016 Lisboa , Portugal} \meetemail{bruno.salsa@gmail.com} % % Second author's affiliation \affil{Mathematics Department, University of Évora, Colégio Luís António Verney Rua Romão Ramalho, 59 7000671 Évora, Portugal} \meetemail{ivdb@uevora.pt} %% INSERT TEXT OF ABSTRACT DIRECTLY BELOW Many arguments deal informally with orders of magnitude of numbers. If one tries to maintain the intrinsic vagueness of orders of magnitude  they should be bounded, but stable under at least some additions , they cannot be formalized with ordinary real numbers, due to the Archimedean property and Dedekind completion. Still there is the functional approach through Oh's and oh's and more generally Van der Corput's neutrices\cite{vdcorput60}, both have some operational shortcomings. Nonstandard Analysis disposes of a natural example of order of magnitude: the (external) set of infinitesimals is bounded and closed under addition% \cite{koudjetithese}\cite{koudjetivandenberg}. Adopting the terminology of Van der Corput, we call a \emph{neutrix} an additive convex subgroup of the nonstandard reals. An \emph{external number} is the settheoretic sum of a nonstandard real and a neutrix. The external numbers capture the imprecise boundaries of informal orders of magnitude and permit algebraic operations which go beyond the calculus of the Oh's and oh's\cite{dinisberg}. This external calculus is based more on semigroup operations than group operations, but happens to be fairly operational in concrete cases and allows for total order with a generalized form of Dedekind completion\cite% {dinisberg2}. Based on joint work with Imme van den Berg, we discuss an axiomatics for the calculus of neutrices and external numbers, trying to do justice to the vagueness of orders of magnitude. In particular we consider foundational problems which appear due to the fact that some axioms are necessarily of second order, and the fact that the external calculus exceeds existing foundations for external sets\cite{kanoveireeken1}. \begin{thebibliography}{9} %% INSERT YOUR BIBLIOGRAPHIC ENTRIES HERE; %% SEE (4) BELOW FOR PROPER FORMAT. %% EACH ENTRY MUST BEGIN WITH \bibitem{citation key} %% \bibitem{vdcorput60} J.G. van der Corput, \textit{Neutrix calculus, neutrices and distributions}, MRC Tecnical Summary Report. University of Wisconsin, 1960. \bibitem{dinisberg} B. Dinis, I. P. van den Berg,\textit{\ Algebraic properties of external numbers}, J. Logic and Analysis 3:9 (2011) 130. \bibitem{dinisberg2} B. Dinis, I. P. van den Berg, \textit{On structures with two semigroup operations }(to appear) \bibitem{kanoveireeken1} V. Kanovei, M. Reeken, Nonstandard Analysis, axiomatically, Springer Monographs in Mathematics (2004). \bibitem{koudjetithese} F. Koudjeti, Elements of External Calculus with an aplication to Mathematical Finance, PhD thesis, Labyrinth publications, Capelle a/d IJssel, The Netherlands (1995). \bibitem{koudjetivandenberg} F. Koudjeti and I.P. van den Berg. Neutrices, external numbers and external calculus, in Nonstandard Analysis in Practice, p. 145170. F. and M. Diener eds., Springer Universitext, 1995. %% IF THERE ARE NO ENTRIES %% DELETE THE LINE ABOVE (\begin{thebibliography}{20}) %% AND THE LINE BELOW (\end{thebibliography}) \end{thebibliography} \vspace*{0.5\baselineskip} % this space adjustment is usually necessary after a bibliography \end{document} 
17:50  Elementary numerosities and measures. SPEAKER: Emanuele Bottazzi ABSTRACT. Generalizing the notion of numerosity, introduced in [1], we say that a function n from the powerset of a given set Ω is an elementary numerosity if it satisfies the properties 1. the range of n is the nonnegative part of a nonarchimedean field F that extends R; 2. n({x}) = 1 for every x ∈ Ω ; 3. n(A ∪ B) = n(A) + n(B) whenever A and B are disjoint. We have shown that every nonatomic finitely additive or sigmaadditive measure is obtained from an elementary numerosity by taking its ratio to a unit. The proof of this theorem relies in showing that, given a nonatomic finitely additive or sigma additive measure over Ω, there exists a suitable ultrafilter on Ω such that the elementary numerosity of a set can be defined as the equivalence class of a particular real Ω sequence. A proof can also be obtained from Theorem 1 of [2], by an argument of saturation. This result allowed to improve nonstandard models of probability, first studied in [3], that overcome some limitations of the conditional probability; further research aims towards models that avoid the BorelKolmogorov paradox. For this reasons, we do believe that this topic could be of particular interest not only to mathematicians but also to philosophers. [1] V. Benci, M. Di Nasso, Numerosities of labelled sets: a new way of counting, Advances in Mathematics, vol. 173 (2003), pp. 50–67. [2] C.W. Henson, On the nonstandard representation of measures, Transactions of the American Mathematical Society, vol. 172 (1972), pp. 437–446. [3] V. Benci, L. Horsten, S. Wenmackers, NonArchimedean probability, Milan Journal of Mathematics (to appear), arXiv:1106.1524. 
16:30  Differential Galois theory in the class of formally real fields. SPEAKER: Quentin Brouette ABSTRACT. Inside the class of formally real fields, we study strongly normal extensions as defined in chap. VI, [Kol]. Fix L/K a strongly normal extension of formally real differential fields such that the subfield C_K of constant elements of K is real closed. Let U be a saturated model of the theory of closed ordered differential fields containing L (see [Sin]), U is real closed and for i^2=1, U(i) is a model of DCF_0. We denote gal(L/K) the group of differential Kautomorphisms of L and Gal(L/K):=gal(<L, C_U> / <K, C_U>). Theorem 1. The group Gal(L/K), respectively gal(L/K), is isomorphic to a definable group G in the real closed field C_U, respectively C_K. Under the hypothesis that K is relatively algebraically closed in L, we prove that given any u\in L\setminus K, there exists \sigma\in Gal(L/K) such that \sigma(u)\neq u. Let K\subseteq E\subseteq L be an intermediate differential field extension. As the elements of Gal(E/K) are not supposed to respect the order induced on <E,C_U> by the one of U, they do not need to have an extension in Gal(L/K). Therefore, we do not get a 11 Galois correspondence like in the classical case where C_K is algebraically closed (see [Pil]). Let Aut(L/K) denote the subgroup of elements of Gal(L/K) that are increasing, let \eta:G\rightarrow Gal(L/K) denote a group isomorphism given by Theorem 1 and < L,C_U>^r be the real closure of <L,C_U> in U. Proposition 2. Let G_0 be a definable subgroup of G. There is a finite tuple \bar d\in <L,C_\U>^r such that \eta(G_0)\cap Aut(L/K) is isomorphic (as a group) to Aut(L(\bar d)/K(\bar d)).
Bibliography [Kol] E. R. Kolchin, Differential algebra and algebraic groups, Pure and Applied Mathematics, Vol. 54. Academic Press, New YorkLondon, 1973. xviii+446 pp. [Pil] A. Pillay, Differential Galois Theory I, Illinois Journal of Mathematics, vol.42 (1998), no.4, pp.978699. [Sin] M. Singer, The model theory of ordered differential fields, Journal of Symbolic Logic, 43 (1978), no.1, pp.8291.

16:50  Around ndependent fields SPEAKER: Nadja Hempel ABSTRACT. The notion of ndependent theories introduced by Shelah is a natural generalization of dependent or more frequently called NIP theories. They form a proper hierarchy of first order theories in which the case n equals to 1 coincides which NIP theories. In my talk, I give an overview about algebraic extensions of fields defined in structures with certain properties (superstable, stable, NIP, etc.). For instance, infinite NIP fields of positive characteristic are known to be ArtinSchreier closed. I extend this result to the wider class of infinite ndependent fields for any natural number n and present some applications to valued fields defined in this setting. Secondly, I show that nonseparable closed pseudoalgebraically closed (PAC) fields have the nindependence property for all natural numbers n which is already known for the independence property (n equal to 1) due to Duret. Hence, nonseparable closed PAC fields lie outside of the hierarchy of ndependent fields. 
17:10  Some remarks on $\aleph_0$categorical weakly circularly minimal structures SPEAKER: Beibut Kulpeshov ABSTRACT. \documentclass[bsl,meeting]{asl}\AbstractsOn \pagestyle{plain}\def\urladdr#1{\endgraf\noindent{\it URL Address}: {\tt #1}.}\newcommand{\NP}{}% \usepackage{verbatim}\begin{document}\thispagestyle{empty}% % BEGIN INSERTING YOUR ABSTRACT DIRECTLY BELOW; % % SEE INSTRUCTIONS (1), (2), (3), and (4) FOR PROPER FORMATS\NP \absauth{Beibut Kulpeshov} \meettitle{Some remarks on $\aleph_0$categorical weakly circularly minimal structures} \affil{Department of Information Systems and Mathematical Modelling, International Information Technology University, 34 A Manas str./8 A Zhandosov str., 050040, Almaty, Kazakhstan} \meetemail{b.kulpeshov@iitu.kz} The notion of {\it circular minimality} has been introduced and originally studied by D.~Macpherson and C.~Steinhorn in \cite{mac}. Here we continue studying the notion of {\it weak circular minimality} being its generalisation. A {\it circular} order relation is described by a ternary relation $K$ satisfying the following conditions:\\ (co1) $\forall x\forall y \forall z (K(x,y,z)\to K(y,z,x));$\\ (co2) $\forall x\forall y \forall z (K(x,y,z)\land K(y,x,z) \Leftrightarrow x=y \lor y=z \lor z=x);$\\ (co3) $\forall x\forall y \forall z(K(x,y,z)\to \forall t[K(x,y,t) \lor K(t,y,z)]);$\\ (co4) $\forall x\forall y \forall z (K(x,y,z)\lor K(y,x,z))$. A set $A$ of a circularly ordered structure $M$ is said to be {\it convex} if for any $a, b\in A$ the following holds: for any $c\in M$ with $K(a,c,b)$ we have $c\in A$ or for any $c\in M$ with $K(b,c,a)$ we have $c\in A$. A circularly ordered structure $M=\langle M, K, \ldots \rangle$ is {\it weakly circularly minimal} if any definable (with parameters) subset of $M$ is a finite union of convex sets \cite{km}. Any weakly ominimal structure is weakly circularly minimal, but the inverse is not true in general. Some of interesting examples of weakly circularly minimal structures that are not weakly ominimal were studied in \cite{km, kb30, ksm}. In \cite{km}\cite{ksm} $\aleph_0$categorical 1transitive weakly circularly minimal structures have been studied, and was obtained their description up to binarity. Here we discuss some properties of $\aleph_0$categorical weakly circularly minimal structures that are not 1transitive. In particular, we study a behaviour of 2formulas in such structures. \begin{thebibliography}{10} \bibitem{mac} H.D.~Macpherson, Ch.~Steinhorn, {\it On variants of ominimality}, {\bf Annals of Pure and Applied Logic}, 79 (1996), pp. 165209. \bibitem{km} B.Sh.~Kulpeshov, H.D.~Macpherson, {\it Minimality conditions on circularly ordered structures}, {\bf Mathematical Logic Quarterly}, 51 (2005), pp. 377399. \bibitem{kb30} B.Sh.~Kulpeshov, {\it On $\aleph_0$categorical weakly circularly minimal structures}, {\bf Mathematical Logic Quarterly}, 52 (2006), pp. 555574. \bibitem{ksm} B.Sh.~Kulpeshov, {\it Definable functions in the $\aleph_0$categorical weakly circularly minimal structures}, {\bf Siberian Mathematical Journal}, 50 (2009), pp. 282301. %% 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}) \end{thebibliography}\vspace*{0.5\baselineskip} % this space adjustment is usually necessary after a bibliography \end{document} 
17:30  Uniqueness of limit models in metric abstract elementary classes under categoricity and some consequences in domination and orthogonality of Galois types SPEAKER: unknown ABSTRACT. Abstract Elementary Classes (AECs) corresponds to an abstract framework for studying non first order axiomatizable classes of structures. Grossberg, VanDieren and Villaveces studied uniqueness of limit models as a weak notion of superstability in AECs. Hirvonen and Hyttinen gave an abstract setting similar to AECs to study classes of metric structures which are not axiomatizable in continuous logic, called Metric Abstract Elementary Classes (MAECs). In this work, we will talk about a study of a metric version of limit models as a weak version of superstability in categorical MAECs, and some consequences of uniqueness of limit models in domination, orthogonality and parallelism of Galois types. 
17:50  Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes SPEAKER: unknown ABSTRACT. We introduce the concept of a locally finite Abstract Elementary Class and develop the theory of excellence for such classes. From this we find a family of complete $L_{\omega_1,\omega}$ sentences $\phi^r$ such that $\phi^r$ is $r$excellent and $\phi^r$ homogeneously characterizes $\aleph_r$, improving results of Hjorth and LaskowskiShelah and answering a question of Souldatos. This provides the first example of an Abstract Elementary Class where the spectrum of cardinals on which amalgamation holds contains more than one interval. 
18:10  Computing the number of types of infinite tuples SPEAKER: Will Boney ABSTRACT. We show that the number of types of sequences of tuples of a fixed length can be calculated from the number of 1types and the length of the sequences. Specifically, if $\kappa \leq \lambda$, then $$\sup_{\M\ = \lambda} S^\kappa(M) = \left( \sup_{\M\ = \lambda} S^1(M) \right)^\kappa$$ We show that this holds for any abstract elementary class with $\lambda$ amalgamation%, but it is new for first order theories when $\kappa$ is infinite . No such calculation is possible for nonalgebraic types. We introduce a generalization of nonalgebraic types for which the same upper bound holds. We use this to answer a question of Shelah from [Sh:c]. 