Colloquium Logicum 2014

4-6 September 2014
Munich, Germany

The Colloquium Logicum is organized every two years by the DVMLG, which is the German association of logicians in mathematics, philosophy and theoretical computer science.

In 2014 the conference will take place in Munich at the Universität der Bundeswehr München, Neubiberg, in the vicinity of Munich.

The conference will cover the whole range of mathematical logic and the foundations of the exact sciences, in particular, logic in philosophy, computer science and artificial intelligence.

Besides the regular scientific programme it is planned to include a PhD Colloquium with invited presentations of excellent recent PhD graduates.

The programme committee invites the submission of abstracts of papers of all fields of research covered by the DVMLG. Abstracts should have between 100 and 500 words and are to be submitted via the EasyChair submission page (see information on the right-hand side). Authors of papers will be notified about acceptance soon after that.

Conference Venue, Accommodation, Directions, Dinner

Regular participants need to organize their own accommodation!

Invited Speakers

PhD Colloquium Speakers

Programme Committee




We acknowledge generous support from the following organisations:

Local Organizing Team

Vasco Brattka (Chair), Birgit Elbl, Guido Gherardi,
Peter Hertling, Gisela Krommes, Tahina Rakotoniaina, Christoph Spandl.


Institute for Theoretical Computer Science, Mathematics and OR
Faculty of Computer Science
Universität der Bundeswehr München
Werner-Heisenberg-Weg 39
85577 Neubiberg, Germany

Conference Photo

Some CL 2014 Participants


This schedule might be subject to minor changes!

You can import this ICAL Calendar Link into your own calendar.

  • Audimax: Building 33, Room No. 0161
  • Lecture Hall: Building 33, Room No. 0101
  • Abstracts of Keynote Lectures

    • Matthias Aschenbrenner. The model theory of transseries

      Abstract: Transseries were introduced in the 1980s by the analyst Écalle in his work on Hilbert's 16th Problem, and also, independently, by the model theorists Dahn and Göring in their work around Tarski's problem on real exponentiation. They naturally arise as asymptotic expansions for germs of functions definable in certain o-minimal structures. Since the late 1990s, van den Dries and myself, later joined by van der Hoeven, have pursued a program to understand the model theoretic aspects of this intricate but fascinating mathematical object. In last few months we were able to make a significant step forward, and established a quantifier elimination theorem for the differential field of transseries in a natural language. My goal for this talk is to introduce transseries and to explain our recent work.

    • Manuel Bodirsky. Reconstructing countably categorical structures from their polymorphism clones

      Abstract: Two countably categorical countable structures have isomorphic topological automorphism groups if and only if they are first-order bi-interpretable, by a theorem of Ahlbrandt and Ziegler. For surprisingly many structures we can replace the topological automorphism group by the (abstract) automorphism group and the statement remains valid. In this talk I will discuss to which degree we can recover a countably categorical structure from its endomorphism monoid, or its polymorphism clone, instead of its automorphism group. Two countably categorical countable structures have isomorphic topological clones if and only if they are primitive positive bi-interpretable. We suspect that also here, we can typically replace the topological clone by the (abstract) clone and the statement remains valid, and show this for the situation where one of the structures is the Rado graph.

      Joint work with Michael Pinsker and Andras Pongracz

    • Stefania Centrone. Proofs without detours: a retrospective perspective

      Abstract: I will present and discuss some interesting aspects of Bernard Bolzano's reflections on the notion of "rigorous proof".

    • Victoria Gitman. Choice schemes for Kelley-Morse set theory

      Abstract: The defining feature of the second-order Kelley-Morse (KM) set theory is that its class comprehension scheme includes all second-order assertions. The full choice scheme includes, for every second-order formula $\phi$, the assertion that if for every set $x$, there is a class $Y$ such that $\phi(x,Y)$ holds, then there is a single class $Z$ that has among its slices a witnessing class for every $x$. The choice scheme can be stratified by formula complexity and has obvious set-sized variants. Choice schemes for KM were first studied by Mostowski and Marek. They have been considered in the context of nonstandard set theory and more recently in analyzing class forcing extensions. I will show that even the weakest choice scheme, namely choice for omega and formulas with no second-order quantifiers, is already independent of KM. This provides an interesting contrast with the situation in second-order arithmetic, where $Z_2$, the analogue of KM, proves all instances of $\Sigma^1_2$ choice, but the choice scheme may fail at the $\Sigma^1_3$ level. I will also show that the full choice scheme does not follow from the set-sized version. Finally, I will argue that KM+, which is KM together with the choice scheme, is a more robust theory than KM because it is preserved by ultrapowers of the universe and proves that second-order complexity classes are closed under first-order quantification, while it is consistent that ultrapowers of KM models fail to even satisfy KM and that in a model of KM, second-order complexity classes can fail to be closed under even bounded first-order quantification. This is joint work with Joel David Hamkins and Thomas Johnstone.

    • Fairouz Kamareddine. Computerising mathematical text, debugging proof assistants and object versus meta level

      Abstract: Mathematical texts can be computerised in many ways that capture differing amounts of the mathematical meaning. At one end, there is document imag- ing, which captures the arrangement of black marks on paper, while at the other end there are proof assistants (e.g., Mizar, Isabelle, Coq, etc.), which capture the full mathematical meaning and have proofs expressed in a formal foundation of mathematics. In between, there are computer typesetting systems (e.g., LATEX and Presentation MathML) and semantically oriented systems (e.g., Content MathML, OpenMath, OMDoc, etc.). In this talk we advocate a style of computerisation of mathematical texts which is flexible enough to connect the different approaches to computerisation, which allows various degrees of formalisation, and which is compatible with different logical frameworks (e.g., set theory, category theory, type theory, etc.) and proof systems. The basic idea is to allow a man-machine collaboration which weaves human input with machine computation at every step in the way. We propose that the huge step from informal mathematics to fully formalised mathematics be divided into smaller steps, each of which is a fully developed method in which human input is minimal. We also propose a method based on constraint generation and solving to debug proof assistants written in SML and reflect on the need and limitation of mixing the object and metalevel.

    • Anca Muscholl. Distributed synthesis

      Abstract: Synthesis is about constructing systems that behave correctly w.r.t. to a given specification. Synthesizing distributed systems is an attractive goal, since such systems are notoriously difficult to get right. Unfortunately, there are very few known decidable frameworks for distributed synthesis. We will discuss one such framework, stated in the rendez-vous model of Zielonka automata. In this setting, synthesis is decidable for all omega-regular local specifications, under the restriction that the communication graph of the system is acyclic.

    • Olivier Roy. The logic of obligations as weakest permissions

      Abstract: This will be a talk about deontic logic. This is the logic of obligations and permissions. I will introduce a new understanding of these deontic modals. I call it the logic of "obligation as weakest permission." In this logic obligations and permissions provide, respectively, necessary and sufficient conditions for an action to be legal. I will argue for the philosophical plausibility of this view, present its non-normal modal logic, as well as a cut-free hypersequent calculus for it, and show how it can be extended and applied to practical norms in decision and game theory. This is join work with Albert Anglberger (LMU Munich) and Norbert Gratzl (LMU Munich)

    • Daniel Turetsky. Algorithmic Randomness and the Turing Degrees

      Abstract: Algorithmic randomness uses the tools of computability theory to analyze the question, "When is an infinite binary sequence random?". Several different definitions of a random sequence are studied, with the most common being Martin-Löf randomness. Randomness has a rich interaction with the Turing degrees of more classical computability theory, in particular with the c.e. degrees and the PA degrees. For example, if a random cannot compute $0'$ (or equivalently, cannot compute a PA degree), then every c.e. set which it can compute is $K$-trivial, which means that randomness considers it useless as an oracle; despite being non-computable, it has no derandomization power. The covering problem asks if this can be reversed: is every $K$-trivial computable from a random that does not compute $0'$? I will review the appropriate definitions and discuss the covering problem and similar questions. I will also discuss the proof of the covering problem and how it touches on the interaction of algorithmic randomness and effective analysis.

    Abstracts of PhD Colloquium Lectures

    • Dominik Adolf. The core model induction

      Abstract: The core model induction, originally introduced by Hugh Woodin, is a versatile method to compute lower bounds for the consistency strength of extension of ZFC. We hope to introduce the basic concepts and discuss some recent developmenmts.

    • Marcos Cramer. The Naproche system: Proof-checking mathematical texts in controlled natural language

      Abstract: We have developed a controlled natural language (CNL) – i.e. a subset of a natural language defined through a formal grammar – for writing mathematical texts. The Naproche system can check the correctness of mathematical proofs written in this CNL. In this talk we will highlight some interesting logical and linguistic problems that had to be solved in the development of the Naproche CNL and the Naproche system: The system uses a formalism from the linguistic theory of presuppositions in order to work with potentially undefined terms, and can handle dynamic quantification, including the phenomenon of implicit dynamic function introduction, which had previously not been discussed in the literature.

    • Tomer Kotek. Definability of Combinatorial Functions

      Abstract: In recent years there has been growing interest in graph polynomials, functions from graphs to polynomial rings which are invariant to isomorphism. Graph polynomials encode information about the input graphs e.g. in their evaluations, coefficients, degree and roots. Many researchers studied specific graph polynomials such as the chromatic polynomial, the Tutte polynomial, the interlace polynomial or the matching polynomial. In this talk a unified logical framework for graph polynomials will be presented. Using this framework, the definability of graph polynomials which count generalized colorings will be compared with with that of graph polynomials defined as subset expansions. A method of showing non-definability of graph polynomials using connection matrices will be discussed. Applications of this method to non-definability proofs of graph classes will be presented.

    • Davide Rinaldi. Formal Topology, Information Systems and Finite Density

      Abstract: Scott introduced Information Systems to make available a simpler and constructive presentation of algebraic domains. We propose here an alternative description, based on Sambin's Formal Topology, and we investigate the status of the corresponding Kleene-Kreisel density theorem, stating that total ideals are dense in the finitely generated partial ideals of a given type. By means of general tools in formal topology, we give a finite and constructive version of it for non-flat domains.

    Abstracts of Contributed Talks

    • Geghard Bedrosian and Frederik Herzberg. Ultraproduct construction of representative utility functions with infinite-dimensional domain

      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 finite-dimensional 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 Kirman--Sondermann (1972) correspondence). However, since the decision problems of macroeconomic theory are typically infinite-dimensional, 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 superstructur eover $W\cup\mathbb{R}$, obtained by a bounded ultrapower construction with respect to the Kirman--Sondermann ultrafilter.

    • Alexander Carstensen Block. The Modal Logic of Symmetric Extensions

      Abstract: Symmetric forcing was first used by Paul Cohen to show the independence of the Axiom of Choice from $\mathsf{ZF}$. It is a modification of the method of forcing, a flexible set theoretic model construction assigning to a given (countable transitive) model of $\mathsf{ZF}$ outer models, called generic extensions, each of which is "generated" from a single new object. The forcing method itself is unsuitable for establishing the independence of the Axiom of Choice from $\mathsf{ZF}$, since every generic extension of a $\mathsf{ZFC}$-model also satisfies the Axiom of Choice.
      So instead Cohen used symmetric forcing, considering symmetric submodels of generic extensions instead of actual generic extensions. Symmetric submodels are obtained by deleting objects whose descriptions (in terms of the so-called forcing language) are not sufficiently stable under a certain group action. This process may remove well-orderings of sets still present, thereby breaking the axiom of choice.
      We refer to symmetric submodels of generic extensions in short as symmetric extensions. A central property of symmetric extensions (and generic extensions as well) is that truth in them can be expressed in the ground model one starts with. More precisely for every first-order sentence $\varphi$ in the language of set theory there is a first-order sentence $\varphi^*$ in the language of set theory such that for any (countable transitive) $\mathsf{ZF}$-model $M$ we have that $M \models \varphi^*$ iff for any symmetric extension $N$ of $M$: $N$ satisfies $\varphi$.

      Using this fact we can give a correspondence between formulas in the basic modal language and first-order sentences in the language of set theory as follows. A translation is a map assigning proposition letters to sentences in the language of set theory. We can extend any translation $T$ to an interpretation $\underline{T}$ assigning formulas in the basic modal language to first-order sentences in the language of set theory by recursively setting:
      (1) $\underline{T}(p) := T(p)$ for any proposition letter $p$;
      (2) $\underline{T}(\bot) := (0=1)$;
      (3) $\underline{T}(A+B) := \underline{T}(A) + \underline{T}(B)$ for any logical connective $+$;
      (4) $\underline{T}(\Box A) := [\underline{T}(A)]^*$
      With this we can define the ZF-provable modal logic MLS of symmetric forcing by setting $MLS := \{A \mid ZF$ proves $\underline{T}(A)$ for any translation $T\}$

      This definition is analogous to the definitions of the corresponding modal logic of forcing as introduced and investigated by Joel Hamkins and Benedikt Löwe in [1]. Using an adaptation of their methods we show that MLS = S4.2 and therefore that MLS coincides with the modal logic of forcing.

      1. JOEL D. HAMKINS, BENEDIKT LÖWE, The modal logic of forcing. Transactions of the American Mathematical Society, vol. 360 (2008), no. 4, pp. 1793-1817

    • Vasco Brattka, Guido Gherardi and Rupert Hölzl. Probabilistic computability and choice

      Abstract: The aim of this talk is to give an overview of the systematic investigation we have carried out onto the field of randomized algorithms for real numbers. In particular, the notions of Las Vegas and probabilistic computability for infinite sequences are presented. As case studies we analyze the problems of computing Nash equilibria and solutions to the intermediate value theorem.

      See the arXiv version for more details.

    • Yong Cheng, Sy-David Friedman and Joel David Hamkins. Large cardinals need not be large in HOD

      Abstract: We prove that large cardinals need not generally exhibit their large cardinal nature in HOD. For example, a supercompact cardinal \kappa need not be weakly compact in HOD, and there can be a proper class of supercompact cardinals in V, none of them weakly compact in HOD, with no supercompact cardinals in HOD. Similar results hold for many other types of large cardinals, such as measurable and strong cardinals.

    • Merlin Carl. Algorithmic Randomness for Infinitary Machines

      Abstract: During the last decade, a number of machine models of transfinite computability have been proposed and studied, such as Infinite Time Turing Machines, Infinite Time Register Machines and Ordinal Turing Machines. We consider algorithmic randomness for machine models of infinitary computations. We show that a theorem of Sacks, according to which a real $x$ is computable from a randomly chosen real with positive probability iff it is recursive holds for many of these models, but is independent from $ZFC$ for ordinal Turing machines. Furthermore, we define an analogue of Martin-Löf-randomness for Infinite Time Register Machines and show that some classical results like van Lambalgen's theorem continue to hold.

    • Bernhard Fisseni. What makes stories similar? – Some Empirical and Formal Results

      Abstract: We present a survey of the results and findings of the research project *What makes stories similar?* funded by the John Templeton Foundation from October 2011 to May 2015.

      The research project *What makes stories similar?* funded by the John Templeton Foundation from October 2011 to May 2015 and coordinated by Benedikt Löwe as principal investigator aimed at providing a discussion of similarity for narratives. Guided by its eponymous question and based on Löwe's previous research on comparability and (in)compatibility of formal frameworks, the project aimed to find out whether there are structural (rather than presentational) properties that contribute or even define story similarity, whether they can be expressed in formal representation systems, and how such representations can be empirically tested.

    • Walter Hoering. A Formalism allowing Non-deterministic Strategies

      Abstract: Turing and Feferman have shown, how to interpret and use Gödel's incompleteness theorem in a positive way - i.e. as a tool to construct progressions of recursively enumerable theories. These theories work with constructive ordinals and are either effectively realizable and recursively enumerable, therefore Gödel-extendible, using as they do, only effective rules and only a recursively enumerable part of the constructive ordinals, or they reach beyond he effective, using some version of the omega-rule or a non-trivial section of the constructive ordinals. If one deals with these progressions, one can work within a conventional system or abandon it fore another one, which may be stronger. This unconditioned and permanent capacity for choice is beyond the capacities of a conventional formal system. At this point we cannot but ask for the difference between the capacities of a human being and the possibilities of a conventional formal system. The answer is quite simple: the difference lies in the freedom of man, in his capacity for random choice. So we come to look for a new kind of formal system featuring this capacity. We construct a new kind of formal system, the non-deterministic systems which have non-determinism built in in a presumably novel way. It seems to go beyond the recursively enumerable. We call a system non-deterministic, if it can take a random input or alternately also a deterministic input at the same place. Some of these systems are capable of strengthening themselves indefinitely by dint of their own strength, just as Baron Münchhausen pulled himself and the horse upon which he was riding out of a pernicious swamp just by pulling up his own tuft of hair. Therefore we propose the name of Münchhausen-Systems for this kind of system. Another adventure of the Baron was that, riding on a canon ball, he suddenly decided to change direction by jumping onto another canon ball approaching from the opposite direction. Also this story will have a counterpart here. Only that the rather pedestrian analogue of the Baron's instantaneous resolution, a random generator, will be used to create an infinite sequence of natural numbers and thereby of systems. Turing in his conception of a device, later to be called Turing machine, dealt with linear computation, proceeding without branching:. "There is only one way to go on, straight ahead". Housewives and artisans know: If I do one thing, I will have to skip something other. It is this kind of inescapable choice between many alternatives, which we model in our systems. Our subject is computability, deducibility if free, non-determined decisions are allowed to intervene an infinite number of times: "There are always many directions to go on" In our Münchhausen Systems (M-systems for short) we always face the alternative: to stay where we are and to continue working in the present surrounding - or - to change into a new environment. If one is interested in evaluating sets like O, Kleene's constructive ordinals, or B the set of recursive well-founded trees one deals with positive inductive definitions I.e. with productive sets - to which M-Systems can be applied.

    • Mirjana Ilic and Branislav Boricic. Is t really needed in formulating sequent calculi for relevant logics?

      Abstract: The first Gentzen calculi for distributive relevant logics were presented in the late 1960's and early 1970's, when Dunn published Gentzen system for positive relevant logic, and Minc formulated the Gentzen system for positive relevant logic with necessity. In those calculi, an empty left-hand side, in the left premise of the cut rule can lead to irrelevance (the modal fallacy would be derivable, then). There are two ways to prevent the inference of the modal fallacy in those calculi. However in both of them, the constant t, which is not the part of the standard language for relevant logics, is needed. Giambrone and Brady also followed those ideas in formulating the sequent calculi for RW+ and RW, confirming the need for t in those logics, also. However, it has been shown recently, that it is possible to obtain the cut--free sequent calculus for RW without the help of t. We present the sequent calculus GRW of RW. The calculus GRW is with right-handed sequents, based on unsigned formulae, unlike Brady's calculus L'RW of RW, which is based on single-conclusion sequents with signed formulae. The calculus GRW has a much neater presentation, although the proof that it is cut--free is somewhat more complex.

    • Franziska Jahnke. Definable Henselian Valuations

      Abstract: In a henselian valued field, many arithmetic or algebraic questions can be reduced, via the henselian valuation, to simpler questions about the value group and the residue field. By the celebrated Ax-Kochen/Ershov Principle, in fact, if the residue characteristic is 0, `everything' can be so reduced: the 1st-order theory of a henselian valued field (as a valued field) is fully determined by the 1st-order theory of its value group (as an ordered abelian group) and of its residue field (as a pure field). Conversely, in many cases, a henselian valuation is so intrinsic to a field that it is itself encoded in the arithmetic of the field, i.e. its valuation ring is a 1st-order parameter-free definable subset of the field (in the language of rings). In this talk, we investigate the question when a henselian valued field admits such a non-trivial 0-definable henselian valuation. Clearly, separably or real closed fields admit no non-trivial definable valuations, and, by the work of Prestel and Ziegler, there are further examples of henselian valued fields which do not admit a 0-definable non-trivial henselian valuation. We give conditions on the residue field which ensure the existence of a parameter-free definiton. Using recent work of Prestel, we deduce that in every case discussed in the talk the formula can be found to be either existential-universal or universal-existential.

      The material presented includes joint work with both Jochen Koenigsmann and Arno Fehm.

    • Yurii Khomskii. Suslin proper forcing and regularity properties

      Abstract: Recently, in joint work with Vera Fischer and Sy Friedman, we obtained a number of new results separating regularity properties on the $\Delta^1_3$, $\Sigma^1_3$ and $\Delta^1_4$ levels of the projective hierarchy. In this talk I will present some of the methods we used to obtain these results, focusing on the concept of "Suslin/Suslin+ proper forcing", a strengthening of Shelah's concept of proper forcing which only works for easily definable forcing notions, and which was a crucial technical ingredient in our proofs.

    • Takayuki Kihara and Arno Pauly. Point degree spectra of represented spaces

      Abstract: We introduce the point spectrum of a represented spaces as a substructure of the Medvedev degrees. The point spectrum is closely linked to isomorphism type of a space w.r.t. countably continuous maps, and via this, also with the dimension. Through this new connection between descriptive set theory and degree theory (as part of computability theory) we can answer several open questions. As a result on the way, we prove that any admissible represented space with an effectively fiber-compact representation is already computably metrizable.

    • Giorgio Laguzzi. Roslanowski and Spinas dichotomies

      Abstract: (the talk is bases on joint works with Yurii Khomskii and Wolfgang Wohofsky)

      We investigate two tree forcings for adding infinitely often equal reals: the full splitting Miller forcing $\mathbb{FM}$, introduced by Roslanowski in [1], and the infinitely often equal trees forcing $\mathbb{IE}$, implicitly introduced by Spinas in [2]. We prove results about Marczewski-type regularity properties associated with these forcings as well as dichotomy properties on $\mathbf{\Delta}^1_2$ and $\mathbf{\Sigma}^1_2$ levels, with a particular emphasis on a parallel with the Baire property. Furthermore, we prove that our dichotomies hold for all projective sets in Solovay's model, and that the use of an inaccessible is necessary for both. Finally we also investigate the Marczewski-type ideals related to $\mathbb{FM}$ and $\mathbb{IE}$, proving some results of orthogonality with other tree forcings ideals.
      [1] A. Roslanowski, On game ideals, Colloq. Math., 59(2):159-168, 1990.
      [2] O. Spinas, Perfect set theorems, Fund. Math., 201(2):179-195, 2008.

    • Javier Legris. Existential Graphs as a Framework for Introducing Logical Constants and Logical Systems

      Abstract: Charles S. Peirce conceived his diagrammatic logic of the Existential Graphs (EGs) as the best formulation of logical systems, according to his iconic conception of logic and his idea of “exact logic”. Consequently they constituted a general methodology for the mathematical treatment of deduction based on notions from topology. Thus, the EGs open a fully new direction in symbolic logic. Peirce formulated different diagrammatic systems for the EGs that have been intensively studied and expanded in the last years.
      In this paper a new interpretation of Peirce’s EGs is introduced by applying them as a framework for defining logical constants and logical systems. This interpretation is coherent with the idea of the ‘productive ambiguity’ of diagrammatic representation implied in Peirce’s own conception. Diagrams are open to different interpretations because of their purely structural nature. Furthermore, this interpretation attempts to build up a bridge between Peirce’s EGs and the current perspective in logic of Structural Reasoning. According to this, EGs could be properly understood as a kind of Structural Reasoning, in the sense used by Peter Schroeder-Heister and originated in Gerhard Gentzen’s ideas. Instead of using sequent style systems, the EGs can be used in order to formulate general properties of deduction and to define logical concepts. Instead of combinatorial analysis and recursion (as in the case of sequent systems), EGs can be studied by topology. In this sense, the EGs can be interpreted as an account of logical structures. More specifically, the ‘scroll’ formulated by Peirce in early formulations of the EGs will be used to express an implication structure.
      The main claims of the paper can be summarized as follows: (1) diagrams can be used in two different senses: (a) as an intuitive way to express the nature of deduction in terms of diagrams, (b) as a mathematical tool to characterize logical constants of different logic systems. (2) The theory for formulating logic systems evolves from a coherent philosophical perspective, so that there is a clear correspondence between logical theory (including a topological framework) and philosophical theory (the iconic nature of deduction). (3) The philosophical theory does not make deduction and logical concepts dependent on ordinary language.

    • Philipp Lücke. Infinite fields with free automorphism groups

      Abstract: Shelah proved that a free group of uncountable rank is not isomorphic to the automorphism group of a countable first-order structure. In contrast, Just, Shelah and Thomas showed that it is consistent with the axioms of set theory that there is a field of cardinality $\aleph_1$ whose automorphism group is a free group of rank $2^{\aleph_1}$. Motivated by this result, they ask whether there always is a field of cardinality $\aleph_1$ whose automorphism group is a free group of rank greater than $\aleph_1$.
      I will present joint work with Saharon Shelah that shows that the free group of rank $2^\kappa$ is isomorphic to the automorphism group of a field of cardinality $\kappa$ whenever $\kappa$ is a cardinal satisfying $\kappa=\kappa^{\aleph_0}$. The techniques developed in the proof of this statement also show that the existence of a cardinal $\kappa$ of uncountable cofinality with the property that there is no field of cardinality $\kappa$ whose automorphism group is a free group of rank greater than $\kappa$ implies the existence of large cardinals in certain inner models.

    • Roman Murawski. Philosophy of logic and mathematics in Warsaw School (the case of Tarski and Mostowski)

      Abstract: The aim of the talk is to analyze main trends and tendencies, main standpoints and views in the philosophical reflection on mathematics and logic in Warsaw School between the wars. This was the time of intensive development of mathematics (Polish Mathematical School) and of logic (Warsaw Logical School, Lvov-Warsaw Philosophical School) in Poland. Hence a natural question arises whether this development of mathematics and logic was accompanied by philosophical reflection on those disciplines, whether the researches were founded on and stimulated by certain fixed philosophical presuppositions. On the other hand philosophy of mathematics and logic is based on and uses certain results of metamathematics, of the foundations of mathematics and of logic. Did logical achievements influence the philosophical reflection? The philosophical views of main logicians and mathematician (among them of Tarski and Mostowski) will be presented and analyzed. We come to the conclusion that Polish logicians and mathematicians being convinced of the importance of philosophical problems and knowing quite well the current philosophical trends treated logic and mathematics as autonomous disciplines independent of philosophical reflection on them, independent of any philosophical presuppositions. Therefore they sharply separated mathematical and logical research practice and philosophical discussions concerning logic and mathematics. Philosophical views and opinions were treated as “private” matter that should not influence the mathematical and metamathematical investigations. On the contrary, in the latter all correct methods could and should be used. This “methodological Platonism” enabled Polish logicians and mathematicians to work in various areas without being preoccupied by philosophical dogmas. In controversial cases, as for example in the case of the axiom of choice in set theory, their attitude can be characterized as neutral – without making any philosophical declarations they simply considered and studied various mathematical consequences of both accepting and rejecting the controversial principles and investigated their role in mathematics.

    • Hugo Nobrega. Obtaining Weihrauch-complete functions and relations from sets of real numbers

      Abstract: We report on research that connects the theory of Weihrauch degrees to the descriptive set theory of classes of functions.
      Among other previously known results, functions $f_n$ for each natural number $n$ and a relation $R$ had already been found which characterize the Baire class $n$ functions and the class of functions preserving $\mathbf{\Sigma}^0_2$ under preimages, respectively, in the sense that a given function is in one of the mentioned classes if and only if it is Weihrauch-reducible to the corresponding function or relation.

      In this talk, we show that functions characterizing the Baire class $\alpha$ functions can be obtained by a general construction applied to any Wadge-complete set for $\mathbf{\Sigma}^0_\alpha$, for all $\alpha < \omega_1$, and show that the $f_n$ functions are special cases of this construction.
      Furthermore, we show that relations characterizing the classes of functions with a certain type of partition property related to the famous Jayne-Rogers theorem --- namely, for each $\alpha < \omega_1$, the class of functions whose domain can be partitioned into countably many $\mathbf{\Pi}^0_\alpha$ sets such that the function restricted to each set in the partition is continuous --- can also be obtained by another general construction applied to any Wadge-complete set for $\mathbf{\Sigma}^0_\alpha$.
      In particular, using the Jayne-Rogers theorem we show that $R$ can also be seen as a special case of this construction.

    • Edoardo Rivello. Revision without Choice

      Abstract: Revision sequences were introduced in 1982 by Herzberger and Gupta (independently) as a mathematical tool in developing what is since then known as "The revision theory of Truth". Later, the same tool was applied to other areas of logic and philosophy, like the theory of definitions, the analysis of circular concepts, the theory of rational belief, and others. In the original and informal presentation of the theory, the revision sequences are ordinal-length sequences, namely operations defined on the proper class of all ordinal numbers. However, it is a common feature of most revision theories proposed in the literature the fact that the same theory can be obtained by quantifying over the class of all limit-length revision sequences, so providing a formalisation of the theory in ZFC. Further, for a given theory, by an application of the Lowenheim-Skolem theorem, McGee’s theorem establishes an upper bound for the length of the revision sequences we need to quantify over.

      McGee's theorem and analogous or related results, are usually proved by invoking some amount of the Axiom of Choice, in the form of the Lowenheim-Skolem theorem or in another. In this talk I will present a general method for reproving such results without using any form of the Axiom of Choice. The method applies to a wide range of revision theories encompassing Harzberger's, Gupta's and Belnap's original ones.

      The talk is based on the following recent works (preprints available on
      E. Rivello, Stability-Dependent Revision, submitted, 2013.
      E. Rivello, Revision without the Axiom of Choice, submitted, 2014.

    • Carsten Rösnick. On Type-2 Complexity of Some Operators in Geometry, Topology and Analysis

      Abstract: This talk will be about my yet-to-be-finished PhD thesis. In my thesis I analyze the computational complexity of some operators in geometry and analysis based on earlier work of Ko and Friedman (1981/84, 1991), Chou and Ko (1995, 2005), Brattka et al (1999, 2003), Labhalla et al (2001), Zhao and Müller (2008), Kawamura and Cook (2011), and others. Examples of operators include binary set union, intersection and projection, as well as integration, differentiation, reciprocals $f \mapsto 1/f$ and inverses $f \mapsto f^{-1}$. These, and more, operators are realized (in the TTE-sense/"Weihrauch model") on oracle Turing machines where their realizers are type-2 functionals, i.e. functionals $\phi$ of form $\mathbb{N}^{\mathbb{N}} \times \mathbb{N} \to \mathbb{N}$.

      In order to speak about computations, we first have to introduce representations for spaces like the class of all closed subsets of $\mathbb{R}^n$, or the class of continuous, smooth or analytic functions. Usually, there is more than one "natural" choice of representation, but as it will turn out, most of the ones we will see are polytime equivalent---thus, from the perspective of complexity, it does not matter which one we choose when devising the complexity of operators. This in a sense even proves the complexity bounds for operators to be 'robust'. However, obviously not all representations turn out to be polytime equivalent: For example, there are three quite natural representations in the realm of closed sets which are not polytime equivalent; the first two because of the difficulty to get global information out of local information, the second two due to the need to add additional data.

      Having settled the question about some representations and their relations, we turn to operators: the projection for sets, as well as integration and function inversion for continuous functions. Projection proves to be polytime if restricted to convex compact sets; while the lack of convexity links it to $P$ vs $NP$ in the discrete world. Integration is known to map polytime functions to polytime ones when restricted to analytic functions, but over smooth functions it is not polytime---just like for continuous functions. So, in a sense, smoothness does not help from a complexity point of view. This gap between polytime over analytic and exptime over smooth functions can be quantified in terms of the Gevrey level (loosening the bounds on the growth of analytic functions depending on said level)---which we will do. It turns out that the complexity of integration depends exponentially on this level. We will also take a look at a third operator, function inversion $f \mapsto f^{-1}$, sufficient preconditions for this operator to be at least computable, and the barriers to surpass due to its linkage to the existence of one way functions and one way permutations.

    • Sam Sanders. Computing with infinitesimals

      Abstract: See PDF document.

    • Ralf Schindler, Sandra Uhlenbrock and W. Hugh Woodin. Producing Iterable Models with Woodin Cardinals from Optimal Determinacy Hypotheses

      Abstract: Projective determinacy is the statement that for certain infinite games, where the winning condition is projective, there is always a winning strategy for one of the two players. It has many nice consequences which are not decided by ZFC alone, e.g. that every projective set of reals is Lebesgue measurable. An old so far unpublished result by W. Hugh Woodin is that one can derive specific countable iterable models with Woodin cardinals from this assumption. Work by Itay Neeman shows the converse direction, i.e. projective determinacy is in fact equivalent to the existence of such models. These results connect the areas of inner model theory and descriptive set theory. We will give an overview of the relevant topics in both fields and, if time allows, sketch a proof of Woodin's result.

    • Peter Schuster and Davide Rinaldi. Eliminating Krull's Lemma for Horn Clauses

      Abstract: In the language of rings we consider implications from a finite conjunction to a finite disjunction of atomic formulas. It is well-known that one can characterise algebraically when such implication can be proved for (commutative) rings and for integral domains, respectively. By interpolation, we extend this characterisation to the provability of such implications for reduced rings: i.e., rings in which only 0 is nilpotent. Scott entailment relations are particulary suited for proving those characterisations. From the mono-conclusion case one can read off a syntactical proof that the theory of integral domains is conservative for Horn clauses over the theory of reduced rings. This allows to eliminate Krull's Lemma, the appropriate incarnation of Zorn's Lemma, from many a "short and elegant'' proof in commutative algebra that works by reduction modulo a generic prime ideal. With only little effort, the approach above can be carried over from the case of integral domains over reduced rings to the case of local rings over rings: just replace ideals by filters, and "is zero'' by "is invertible''. With hardly more effort one can also deal with occurrences of mixed predicates in the antecedent. All proofs on the meta-level are constructive and elementary. Within the given theories, however, it is irrelevant whether one thinks provability in terms of classical or intuitionistic logic: all formulas under consideration are geometric implications. In competition with related results from dynamical algebra, we eliminate also the condition that every integral domain or local ring be non-trivial, and thus avoid to speak of absurdity. This opens up the possibility to step down from classical logic not only to intuitionistic but also to minimal logic.

    • Johannes Stern. A New Norm for Truth and the Modal Logics of Axiomatic Theories of Truth

      Abstract: Due to a seminal result by Solovay it is well known that the modal logic $GL$ is the modal logic of the natural provability predicate of $PA$ in $PA$. In other words $GL$ expresses exactly the modal properties of the natural provability predicate of $PA$. At least in principle one could try determining the modal logic of other sentential predicates of an arithmetic theory or an extension thereof. In particular it seems interesting to look for the modal logic of the truth predicate of various axiomatic theories of truth. While this question is interesting in its own right we shall focus on its philosophical relevance and argue that such an investigation leads to a new norm for theories of reflexive truth.
      We argue for this this claim by discussing the recent arithmetic completeness result by Czarniecki and Zdanowski. Czarnecki and Zdanowski show that the normal modal logic $KDD_C$, which extends the basic normal modal logic $K$ by the modal principles $$\begin{align*} (D)&&\Box\phi\rightarrow\Diamond\phi&&\\ (D_C)&&\Diamond\phi\rightarrow\Box\phi&& \end{align*}$$ is the modal logic of the truth predicate of symmetric theories of truth (although Czarnecki and Zdanowski do not mention this fact). A theory of truth is called symmetric if and only if the truth predicate commutes with all boolean connectives and is closed under the rules of T-introduction and T-elimination. The ingenious strategy employed by Czarnecki and Zdanowski in showing the arithmetic completeness of $KDD_C$ with respect to symmetric theories of truth is to show that $KDD_C$ is the maximal normal modal logic that can be consistently extended by the relevant modal instances of the diagonal lemma. Since $KDD_C$ is sound with respect to symmetric theories of truth it then must be the modal logic of the truth predicate of symmetric theories of truth.

      The observation that $KDD_C$ is a maximal modal logic lead us to proposing the following new norm for reflexive theories of truth: The modal logic of the truth predicate of reflexive theories of truth ought to be maximal (in the sense of Czarnecki and Zdanowski).

      We argue that this norm should replace the naive desiderata that all T-biconditionals ought to be derivable, which, however, cannot be satisfied in classical and consistent theories of truth. We then illustrate and discuss the consequences of adopting such a norm and also point to certain limitations.

    • Elena Tatievskaya. Symbol and Rule: Cassirer’s treatment of Kant’s Schematism

      Abstract: Cassirer (The Philosophy of Symbolic Forms (1923-1929)) regards cognition as symbolizing that follows rules. Such rules are embodied in systems of meaning invariants used to order objects and govern scientific as well as pre-scientific cognition, language and art. Cassirer compares symbols with Kant’s transcendental schemata that mediate between categories and sensible appearances and uses the terms “schema” and “rule” as interchangeable. Hence it may be asked what the rule-like function of the schema consists in and whether this notion therefore could help to clarify Cassirer’s concept of a symbol and of how rules of symbolizing work.
      I argue that transcendental schemata can be regarded as belonging to the rules of understanding that allow of judging. Using Krausser’s definition of the topological structure of the intuition of time („Kant’s Schematism of the Categories and the Problem of Pattern Recognition“, Synthese 33, 1976, 175-192) which presupposes the relations of simultaneity and following between different elements of a sensibly intuited manifold I propose to represent principles of pure understanding and so-called “schema-judgments” or “criteria” that connect schemata with categories in such a way that the principles define possible antecedents of the propositions that fix such criteria. The consequents of such propositions involve the expression of the form of the judgment that becomes possible due to the application of the schema. Thus a transcendental schema works as a rule according to which the category represented by the schema defines some logical property of the judgment that concerns the apprehended object. Such a property could be the quantity, quality, form or modality of the judgment.
      If we take for example the categories of quantity and consider the number as “Anzahl” of the elements of a sensibly given manifold of which some property is predicated in a judgment the general principle of the axioms of intuition that requires that all intuitions be extensive quantities can be formulated in the form “Either an appearance differs from other appearances simultaneous with it insofar as they in their turn are not simultaneous with each other or some appearances of the given manifold differ with respect to their simultaneity from the other ones or the given manifold contains no appearances that are not simultaneous with at least one of its elements”. Then the proposition that represents the schema of e.g. the category of plurality is “If a given manifold contains an appearance that is simultaneous with only some of the other appearances and differs with respect to simultaneity from the remaining ones a certain property can be predicated of some of the appearances of the manifold”.
      Cassirer’s symbol functions analogously to a schema representing a category since it orders objects due to its ability to represent a system of meaning invariants which in its turn determines the rule-like role of the symbol. The cognition is not restricted to the formation of judgments but involves the production of symbols of different kinds.

    • Gregory Wheeler. Beware of B

      Abstract: No epistemic logic should include the Brouwersche schema, (B), as (B) and (K) yield a pair of known schemas (Chellas 1980) which I dub the BUM schemas. BUMs are a disaster for epistemic logics in general, although BUMs are not problematic for provability logics, which suggests that (B) points out a sharp distinction between (regular) epistemic logics and logics of provability. To mark the distinction, and to preserve Brouwer’s good name, I propose epistemic logicians hereafter refer to (B) as the Blog Schema. Finally, with the downfall of (B) joining the ranks of (5) (Hintikka 1962) and (4) (Williamson 2000), hints of a new case against regular systems of epistemic logic comes into view: (K) does not play well with other modal schemas.

    • Gunnar Wilken and Andreas Weiermann. Goodstein sequences for prominent ordinals up to the ordinal of $\Pi^1_1-CA_0$

      Abstract: We present a smooth approach to generate Goodstein principles which are true but unprovable in theories of iterated inductive definitions, $ID_n$, and eventually the theory $\Pi^1_1-CA_0$. This work was published in the Annals of Pure and Applied Logic in 2013.