Rodney Downey, Algorithmic Randomness and Computability

School of Mathematics, Statistics and Computer Science
Victoria University
PO Box 600
Wellington
New Zealand

In these lectures, I will examine questions such as: what does it mean for a real to be random? what does it mean for one real to be more random than another? Does a real being random mean that it has high or low information content?

There has been amazing progress in this area in recent years through that work of many authors. I plan to cover the basic ideas behind the theory of algorithmic randomness (randomness means (i) not having rare properties (ii) having initial segments that are hard to compress and (iii) random means hard to predict, for example). I will then look at recent work clarifying the relationship between randomness and computational power, as well as the classification of reals by initial segment complexity. Finally I plan to look at the deep work on triviality and lowness with its important implications in classical computability.

Background material and details can be found in the references below.

Downey, R., Some Computability-Theoretical Aspects of Reals and Randomness, in The Notre Dame Lectures (P. Cholak, ed) Lecture Notes in Logic Vol. 18, Association for Symbolic Logic, 2005, 97-148.

Downey, R., Five Lectures on Algorithmic Randomness, to appear proceedings of Computational Prospects of Infinity World Scientific.

Downey, R., and D. Hirschfeldt, Algorithmic Randomness and Complexity, Springer-Verlag Monographs in Computer Science, to appear.

Downey, R., D. Hirschfeldt, A. Nies, and S. Terwijn, Calibrating randomness, to appear, Bulletin Symbolic Logic.

A. Nies, Computability and Randomness, to appear.

Ieke Moerdijk, Introduction to Algebraic Set Theory

The goal of this tutorial on Categorical Logic is to explain some of the recent developments in Algebraic Set Theory. This theory provides a general and flexible framework for constructing models of many kinds of set theories. It is based on the idea of viewing the cumulative hierarchy as a kind of algebraic structure, which is complete (in the sense of lattice theory) with respect to a certain a priori given notion of size. These algebraic structures are called ZF-algebras in the literature. Models of Intuitionistic Zermelo Fraenkel Set Theory (IZF) which were constructed using sheaves or realizability methods naturally arise in this context. Small adaptations of the ambient category where these algebraic structures live, or of the axioms for the notion of size, naturally lead to models of other set theories, such as Aczel's Constructive Set Theory CZF.

For references, you may wish to consult the website for algebraic set theory, http://www.phil.cmu.edu/projects/ast/

Boban Velickovic, Forcing Axioms

Forcing axioms are natural combinatorial statements which decide many of the questions undecided by the usual axioms ZFC of set theory. The study of these axioms was initiated in the late 1960s by Martin and Solovay who introduced Martin's Axiom, followed by the formulation of the Proper Forcing Axiom by Baumgartener and Shelah in the early 1980s and Martin's Maximum by Foreman, Magidor and Shelah in the mid-1980s. In the mid 1990s Woodin's work on P_max extensions established deep connections between forcing axioms and the theory of large cardinals and determinacy. Nevertheless, some of the key problems remained open. In 2003 Moore formulated the Mapping Reflection Principle (MRP) which seems to be the missing ingredient needed in order to resolve many of the remaining open problems in the subject and a number of important developments in the subject followed.

In this series of lectures we first survey the theory of forcing axioms and then present some recent results: Moore's work on MRP, my work with A. Caicedo on definable well-orderings of the reals, Viale's result that the Proper Forcing Axiom implies the Singular Cardinal Hypothesis, etc.

Samson Abramsky, Categorical Quantum Logic

We describe a novel approach to axiomatizing Quantum Mechanics in the setting of strongly compact closed categories. This axiomatization captures all the features which are significant for Quantum Information and Computation, and provides a basis for effective reasoning about quantum informatic processes. It can be presented in terms of a diagrammatic calculus which can be seen as a proof system for a logic, leading to a new perspective on what the right logical formulation for Quantum Mechanics should be.

Marat Arslanov, Problems of definability and structural differences among elementary theories of the Ershov difference hierarchy

Kazan State University
420008, Kazan, Russia
e-mail: Marat.Arslanov@ksu.ru

In my talk I will give a survey on the current state of the research on differences among elementary theories of the Ershov difference hierarchy, including a recent negative solution of well-known Downey's Conjecture on elementary equivalency of n- and m-c.e. degree structures for n,m>1 and n≠m.

Problems on definability of the relation "m-computably enumerable" in n-c.e. degree structures (n>m), and on m-c.e. degrees as Σ₁-substructures of n-c.e. degree structures will be also considered, including recent solutions of a number of open questions in this area. New open questions will be raised, and trends of the research development in this area will be discussed.

Harvey Friedman, Search for consequences

We will discuss some new examples of necessary uses of set theory with large cardinals that fit squarely into finite graph theory. We will also discuss prospects for the future.

Martin Goldstern, Applications of Mathematical Logic in Algebra: the lattice of clones

A clone on a set X is a family of finitary operations on X which contains all projections and is closed under substitution (composition), such as the family of term functions on any universal algebra. The set of all clones on a fixed set X forms a complete lattice, whose structure is rather complicated already for finite sets X.

I will discuss some old (1960s), intermediate and recent (2006) results about the structure (and more often: non-structure) of this lattice on infinite sets, as well as open questions. It turns out that methods and results from set theory (forcing, descriptive set theory, infinite combinatorics), as well as model theory are essential for this analysis.

Ehud Hrushovski, Model theory of valued fields

I will survey some of the developments in the subject, with emphasis on connections to abstract model theory and to geometry.

Jochen Koenigsmann, Axiomatizing Fields via Galois Theory

Grothendieck's program of "anabelian geometry" is designed to recover a field K from its absolute Galois group G_K:=Gal (K^s/K). This has been achieved, e.g., for the class of finitely generated fields, but it doesn't work in general. However, replacing G_K by G_K(x), the absolute Galois group of the rational function field K(x) over K, does the trick: almost all perfect fields K are determined up to isomorphism by G_K(x).

The model theoretic version of this theorem proves that K and G_K(x) are biinterpretable where we consider the field K in the usual first order language for rings, and where G_K(x) is understood as a structure in the language for profinite groups developed by Cherlin, van den Dries, Macintyre and Chatzidakis. We will also discuss the impact on decidability questions for fields like C(t) or F_p((t)).

Andrew Lewis, On constructing strong minimal covers

After giving an introduction to the splitting tree technique of minimal degree construction we shall discuss the generality of this approach and applications to the construction of strong minimal covers.

Antonio Montalban, Embeddability and decidability in the Turing Degrees.

One of the main goals of computability theory is to understand the shape of the structure of the Turing degrees. Two common ways of studying this is by looking at structures that can be embedded into the Turing Degrees and by looking a the decidability of the theory oft his structure varying the language or taking substructures. We describe the author's results in this area.

Erik Palmgren, Intuitionism, Bishop constructivism and point-free thinking

Department of Mathematics
Uppsala University

A consequence of the Heine-Borel theorem is that a point-wise continuous function on the closed unit interval is uniformly continuous. Brouwer incorporated this theorem into intuitionism by developing new mathematical axioms. Topology could then be developed using essentially the classical point-based theory. These axioms, incompatible with the interpretation of logic in terms of computable functions, were given up in the later development of constructive mathematics by the followers of Errett Bishop. Instead various techniques to provide necessary information about (local) uniformity were developed.

A parallel development was that within locale theory, where a point is a derived concept of the topology, while the notion of cover is basic. This made it possible to naturally extend the notion of being locally uniformly continuous to general maps between topological spaces. We show how the theory of Bishop and the point-free theory can be reconciled. The foundational problems of point-free topology are interesting from a predicativistic point of view, and have been addressed by many researchers since the mid 1980s. We discuss some recent developments in this area. We also discuss examples of point-free methods in measure theory.

Wolfram Pohlers, Iterations of ordinal operators

Westfälische Wilhelms-Universität Münster

An ordinal operator is a function mapping sets of ordinals to sets of ordinals. Iterations of ordinal operators play an important role in the ordinal analysis of impredicative theories. We define the iterations of an ordinal operator and give an example how iterated ordinal operators are used in ordinal analysis. Finally we discuss their importance ot the design of ordinal notation systems.

Ernest Schimmerling, Coherent sequences and threads

I will discuss results that connect forcing axioms such as PFA, core models and combinatorial principles such as Jensen's "square".

John Steel, Some correctness results for extender models

Every real in an iterable extender model M is ordinal definable, by the basic canonicity results for such models. However, it is not always the case tht M is sufficiently correct to satisfy the statement "every real is ordinal definable". We shall discuss this situation, and show that if M is sufficiently small, in that its extender sequence does not have extenders overlapping Woodin cardinals, then M satisfies the statement "there is a real from which every real is ordinal definable". The key to this result is an analysis of the extent to which such an M knows how to iterate itself. That analysis also has applications in the infinitary combinatorics of extender models. (Part of this work is joint with Ralf Schindler.)

William Tait, Cut-Elimination for Impredicative Systems of Second-Order Number Theory

The main content of the talk will be a quite simple proof of Takeuti's result, the eliminability of cuts in Π¹₁ Analysis with the Omega-Rule. The proof uses essentially only the well-known proof theory of predicative systems. Although we will obtain ordinal bounds on the length of cut-free proofs, the computations are simple and there will be no discussion of ordinal notations. I will discuss the possibility of extending the method of proof to stronger systems of analysis.

Frank Wagner, Amalgamation, fusion and collaps: Exotic fields and vector spaces

Modifying an old method of Fraisse for the construction of countable universal homogeneous structures, Ehud Hrushovski has developed a powerful tool to build exotic structures and geometries out of finitely generated substructures. His methods have recently been extended to constructions over a vector space over a finite field, and even over the rationals. This has in particular yielded a field of finite Morley rank of positive characteristic with a distinguished proper infinite additive subgroup, and a field of finite Morley rank of characteristic zero with a distinguished proper infinite multiplicative subgroup. The latter construction uses non-trivial results from algebraic geometry.

I shall survey the method, and sketch the proofs.

Noam Greenberg, Definability in the lower regions of the c.e. degrees

The nether regions of the c.e. degrees have yielded a variety of interesting classes (e.g., the array computable, almost deep, and K-trivial degrees). Using Ershov's difference hierarchy, we obtain a transfinite hierarchy of classes in the low₂ degrees. Two levels of this hierarchy are now known to be naturally definable, by appealing to embeddings of non-distributive lattices in initial segments. An application to higher computability theory will also be given.

Bjørn Kjos-Hanssen, Complex oscillations and the law of the iterated logarithm

Algorithmic randomness is most often studied in the setting of the Cantor space. However, it has also been considered for the space of continuous functions on the unit interval. There, the analogue of a Martin-Löf random real is a complex oscillation.

In response to a question of Fouché, we show that the law of the iterated logarithm holds almost everywhere for each complex oscillation. The main idea of the proof is to take advantage of Carathéodory's theorem on isomorphism of measure algebras.

Peter Hertling, Is the Mandelbrot set computable?

Institut für Theoretische Informatik und Mathematik
Fakultät für Informatik
Universität der Bundeswehr München
85577 Neubiberg
Germany

First, we discuss the question in the title shortly in the framework of the computation model by Blum, Shub and Smale. Then we turn to the Turing machine model and the computability notions studied in computable analysis. We show that the exterior of the Mandelbrot set, the boundary of the Mandelbrot set, and the hyperbolic components satisfy certain natural computability conditions. We conclude that the two-sided distance function of the Mandelbrot set is computable if the famous hyperbolicity conjecture is true. We also formulate the question whether the distance function of the Mandelbrot set is computable in terms of the escape time.

Joseph S. Miller, Lowness Notions, Measure and Domination

University of Connecticut

An oracle A is low for a given computability theoretic class if relativizing to A does not change the class. The oracles that are low for ML-randomness are a particularly interesting example. They were introduced by Zambella in 1990 and several characterizations were given in papers of Nies, Hirschfeldt, Stephan and others. Recently, Downey, Nies, Weber and Yu proved that every oracle low for weak 2-randomness is low for ML-randomness. We see that the reverse is also true.

This work is related to two domination properties introduced by Dobrinen and Simpson: almost everywhere domination and its uniform variant. Following up on work of Kjos-Hanssen, we explain how lowness properties relate to measure regularity properties and thus to domination properties. We can use this relationship to prove that the domination properties of Dobrinen and Simpson are equivalent.

Jan Reimann, The Metamathematics of Algorithmic Randomness

Ruprecht-Karls-Universitaet Heidelberg
Institut fuer Informatik
Im Neuenheimer Feld 294
69120 Heidelberg

We will discuss some recent work with Theodore Slaman (Berkeley) on the logical structure of random reals. By relativizing Martin-Löf's test concept to representations of measures one can define a notion of randomness with respect to arbitrary (probability) measures on Cantor space. Instead studying the properties of random reals with respect to Lebesgue measure, we can now study a "reverse" problem: Which properties of a real ensure randomness with respect to a reasonably well-behaved, e.g. non-atomic measure?

The investigation of this problem reveals interesting relations between the logical complexity of a real and its randomness properties. Furthermore, we will address the question whether these relations cannot be proved without transcending the theory they are formulated in (e.g. analysis).

Bakhadyr Khoussainov, Frank Stephan, Yue Yang, Computable Categoricity and Ershov Hierarchy

Let A be a structure. A computable presentation of A is a structure A' isomorphic to A such that the domain of A' is the set of natural numbers and the relations of A' are computable (= recursive). It is understood that all structures considered in the talk have computable presentations.

The main topic of this talk is the following question: given two computable presentations A' and A'' of A what is the complexity of the easiest isomorphism between these two presentations?

A structure is called Δ-0-2-categorical iff there is always an isomorphism between any two computable presentations which is limit-recursive, that is, computable relative to the halting problem as an oracle. A structure is called computably categorical iff there is always a computable, that is, recursive, isomorphism between any two computable presentations. In the present talk, an Ershov-type hierarchy is investigated between these two levels of categoricity.

Call the structure A Fn-categorical iff there is for any two computable presentations A' and A'' of A an isomorphism f from A' to A'' such that f is the limit of a uniformly recursive approximation a with f(x) = a(x,t) for almost all t and there are at most n numbers t with either t=0 or a(x,t) being different from a(x,t-1). Call A Gn-categorical iff there is for any two computable presentations A' and A'' an isomorphism f from A' to A'' such that its graph {(x,y): f(x) = y} is an n-r.e. set in the Ershov-hierarchy. That is, there is a uniform approximation a(x,y,t) to the graph such that for all pairs (x,y), a(x,y,0) = 0 and all but at most n positive natural numbers t satisfy a(x,y,t) = a(x,y,t-1). These notions can easily be generalized to recursive ordinals n.

One has the trivial implication that every computable categorical structure is Fn-categorical, every Fn-categorical structure is Gn-categorical and every Gn-categorical structure is Δ-0-2-categorical. The following results have been obtained.

Theorem 1. The hierarchy is proper, that is, for any recursive ordinal n there is a Fn-categorical structure which is not Gm-categorical for any m<n.

Theorem 2. Let A be the disjoint union of finite graphs with edge-relation R. (a) If there is a constant bound on the size of all involved finite graphs then (A,R) is G2-categorical. (b) The disjoint union of infinitely many singletons and infinitely many pairs of nodes with one connection is G2-categorical but not Fn-categorical for any n. (c) The disjoint union of all finite graphs in which every graph occurs infinitely often is not Gn-categorical for any recursive ordinal n. (d) Every disjoint union of finite graphs is Δ-0-2-categorical.

Theorem 3. If a Boolean algebra is Gn-categorical for a number n then it is already computable categorical. The same is true for linear orders.

Ulrich Berger, Strong normalisation via domain-theoretic computability predicates

It is well-known that intersection types on the one hand characterise the strongly normalisable lambda terms and on the other hand give rise to a syntactically defined domain model for the lambda calculus. Recently, Coquand and Spiwack combined and extended these facts to give criteria for strong normalisability for the lambda calculus with recursively defined constants, thus extending my previous domain-theoretic normalisation results. In the talk I will show that the normalisation proof can also be carried out in an abstract axiomatic setting where the computability predicates are indexed by the elements of a (not syntactically presented) domain.

Venanzio Capretta and Amy Felty, Higher Order Abstract Syntax in Type Theory

University of Ottawa
School of Information Technology and Engeneering

The use of higher-order abstract syntax is an important approach for the representation of binding constructs in encodings of languages and logics in a logical framework. Formal meta-reasoning about such object languages is a particular challenge. We present a mechanism for such reasoning, formalized in Coq, inspired by the Hybrid tool in Isabelle.

At the base level, we define a de Bruijn representation of terms with basic operations and a reasoning framework. At a higher level, we can represent languages and reason about them using higher-order syntax. We take advantage of Coq's constructive logic by formulating many definitions as Coq programs.

We illustrate the method on two examples: the untyped lambda calculus and quantified propositional logic. For each language, we can define recursion and induction principles that work directly on the higher-order syntax.

Work in progress consists in generalizing the tool to provide an implementation of higher-order universal algebra in type theory. It will allow to specify multi-sorted algebras with binding operations and automatically obtain algebras of terms over it together with higher-order recursion and induction principles. We plan to apply the method to the formalization of derivation systems with hypothetical judgements, using our tool in a two-level approach. We will also tackle the POPLmark challenge to test the practicality of our approach.

Reference
Venanzio Capretta and Amy Felty, Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq, draft paper available at http://www.science.uottawa.ca/~vcapr396/publications/lfmtp06.pdf
The files of the corresponding Coq development are available at http://www.science.uottawa.ca/~vcapr396/coq/lfmtp06_coq.html

John Harrison, Taking theorem proving mainstream

In recent years, theorem proving has made notable progress, with many impressive new applications both in formal verification and the formalization of pure mathematics. However, theorem proving is still the preserve of specialists, and has a reputation, not entirely undeserved, for being difficult and painful. We will discuss how we might bring forward the day when theorem proving becomes a mainstream activity for a much larger community of mathematicians and computer scientists.

Martin Hofmann (joint work with Christian Dax & Martin Lange), A proof system for the linear time mu-calculus

We present a simple sound and complete infinitary proof system for the linear time μ-calculus and then give two decision procedures for provability in the system, hence validity of formulas. One uses nondeterministic Büchi automata, the other one a generalisation of size-change termination analysis (SCT) known from functional programming.

Branimir Lambov, Exact and efficient computation over the real numbers

Floating point numbers have been used for a long time as the simple solution to the problem of efficiently using real numbers in computers. Most of the time they give us meaningful results, but since they such a crude representations of the theoretical objects they are used to replace, floating point computations are prone to cause difficult to detect problems.

As computers are becoming more and more powerful, it becomes increasingly feasible to use exact real computations, where real numbers are given by objects that are a mathematically precise representation of the real numbers and the functions that operate on them do not try to approximate the results, but exactly represent the operation of interest. Implementations of the concept exist, but they are very rarely used in practice, and even specialized tools such as Mathematica or MatLab do not offer this machinery.

This presentation will demonstrate an implementation of exact real arithmetic in C++ which attempts to solve the main problems that still make exact arithmetic unsuitable for wide use: the performance of exact computations and their ease of use. To make exact computations easy to use, one has to construct libraries in such a way that the behaviour of the objects that represent real numbers differs as little as possible from the behaviour of the floating point types available in the language. On the other hand, to make them efficient, one needs to introduce some unconventional behavour in (at least parts of) the user's programs. We will describe an implementation of an approach used to combine two different approaches to exact computability in one tool, where the user code has two levels of access to real numbers each complete with its own exact representation for every function provided by the library or implemented by the user, and which has all necessary machinery to easily permit very fast exact computations in an easy to use environment.

Andrew Pitts (joint work with Ranald Clouston), Names, Equations and Freshness

University of Cambridge

Although equational logic is perhaps a little tame compared with other branches of mathematical logic, it has proved very useful to several areas of computer science—especially in its "many-sorted" form. Here I focus on meta-logic and meta-programming, where sorts may represent the various syntactical data structures associated with a formal language. The syntax of such "object-level" languages, be they programming languages or formal logics, nearly always involves various kinds of name and various constructs that bind names to a particular scope. When describing the properties of such languages, we very often employ notions of "freshness" of a name with respect to a structure. Nominal Logic [Theoretical Computer Science 323(2004) 473-497] is a meta-logic that axiomatises the notion of freshness of names within first-oder logic. Recently Murdoch Gabbay and Aad Mathijssen have studied "nominal algebra". It is, roughly speaking, an equational part of nominal logic, in which one considers both equations and "freshnesses", conditioned by freshness assumptions. It seems to provide a natural way of expressing many meta-theoretical properties of syntax to do with meta-variables, substitution and quantification.

In this talk I will give a simplified presentation of this kind of nominal equational logic, emphasising its relationship to ordinary, many-sorted equational logic. The main result is a completeness theorem for nominal equational theories with respect to the nominal sets model (also known as the Schanuel topos). Unlike the completeness theorem for ordinary equational logic, this is a non-trivial result that sheds some light of the role of explicit versus implicit parameters in meta-mathematics.

Raf Cluckers (joint work with F. Loeser), b-minimality

École Normale Supérieure
Département de mathématiques et applications
45 rue d'Ulm
75230 Paris Cedex 05
France

We present joint work with F. Loeser on a new variant on the notion of minimality, generalizing o-minimality, p-minimaliy, and other notions. It is suited for all Henselian valued fields. In fact, the only ingredients are a notion of balls and points, the possibility of having auxiliary sorts, and some axioms using these notions. There is a plentitude of examples and there are promising expansions by nontrivial entire analytic functions. There is a dimension theory and Euler characteristics of the main sort relative to the auxiliary sorts can be studied. Henselian valued fields of char 0 are b-minimal in a natural language. Henselian valued fields in characteristic p are not b-minimal in this language: some expansion is needed but yet unknown.

Clifton Ealy (joint work with Alf Onshuus), Equivalence Relations and the Existence of a Notion of Independence

I will isolate several properties that one may reasonably demand of a notion of independence in models of a theory T. We show that the only obstacle to the existence of a notion satisfying these properties is the interpretability in models of T of arbitrarily long chains of equivalence relations. Alternatively, one may view this result as a characterization of non-rosiness in terms of equivalence relations.

Piotr Kowalski, Ax Theorem in arbitrary characteristic

pdf file of abstract

Assaf Hasson (joint work with Piotr Kowalski), Strongly minimal sets definable in expansions of RCF

pdf file of abstract

Sonia L'Innocente, Model Theory and Lie Algebras: Infinite dimensional representations over sl₂(K)

Department of Mathematics and Computer Science
University of Camerino
Camerino
Italy

pdf file of abstract

Tim Mellor, An Euler Characteristic for real closed valued fields

We highlight some ideas in the proof that real closed valued fields admit a strong Euler characteristic. One utilizes a link between the definable sets of a real closed valued field and the semi algebraic sets of an overfield. This allows the use of theorems from o-minimality.

Klaus Aehlig, Non-Interleaved Polymorphic Types and Iterated Inductive Definitions

Consider the following restriction of the polymorphically typed lambda calculus ("System F"). All quantifications are parameter free. In other words, in every universal type ∀α.τ, the quantified variable α is the only free variable in the scope τ of the quantification. This fragment characterises precisely the provably recursive functions of finitely iterated inductive definitions.

Andrey Bovykin, New results on unprovability and logical strength

Liverpool University
St.Petersburg Department of Steklov
Mathematical Institute

I shall present recent results on unprovability in Peano Arithmetic and on logical strength of infinitary ramseyan statements. In particular I shall discuss

• model-theoretic treatment of Infinitary Canonical Ramsey Theorem and Regressive Ramsey Theorem, using strong cuts in models of arithmetic;
• a reduction of logical strength of Ramsey Theorem for pairs to logical strength of some first-order theory (the density scheme) by a model-theoretic construction;
• an unprovable statement about the sine-function and a method of encoding Ramsey-theoretic statements in the language of dynamical systems;
• IΣ₂-unprovable statements about braids;
• exact unprovability results (threshold results).

Nicola Gambino, Sheaf models for constructive set theories

Université du Québec à Montréal

Constructive Zermelo-Frankel set theory (CZF) was introduced by Peter Aczel in order to provide a set-theoretical foundation for the development of Bishop's constructive mathematics.

I will describe sheaf models for CZF. These models provide a general tool to prove relative consistency and independence results, analogous to the classical method of forcing. Furthermore, I will show how these models fit into the framework of Joyal and Moerdijk's Algebraic Set Theory.

Joost Joosten, Lowerbounds in proof complexity

There exist various relations between lower bounds on lengths of proofs of a sequence of propositional tautologies and seperations of computational complexity classes. In this talk we shall see some non-trivial examples and some results on the lowerbounds involved. In particular, we shall see a relation where propsitional encodings of finite consistency statements play a crucial role.

Thomas Studer (joint work with Gerhard Jäger and Mathis Kretz), Cut-free systems for the propositional modal μ-calculus

Institut füur Informatik und angewandte Mathematik
Universität Bern
Neubrückstrasse 10
CH-3012 Bern
Switzerland

The propositional modal μ-calculus extends standard (multi-)modal propositional logic by operators for least and greatest fixed points of positive operators. We begin with setting up a very natural infinitary calculus for the propositional modal μ-calculus which we collapse to a finite cut-free system afterwards. We show soundness and completeness of both axiomatizations. Completeness is established by constructing a canonical counter-model to any non-provable formula using the method of saturated sequents. Soundness is a consequence of the small model property and well-known results about monotone operators.

Henry Towsner, Ordinal Analysis of Recursive Weak Compactness

We outline an approach to the ordinal analysis of systems at the strength of a recursively weakly compact ordinal (usually characterized as Kripke-Platek set theory with reflection on Π₃ formulas) using an ordinal notation system derived from the equivalent notion of 2-admissibility. The result is an ordinal notation system based on a notion of collapsing functions to ordinals and higher order infinitary rules whose premises range over all suitable transformations on derivations.

Natasha Dobrinen, Co-stationarity of the ground model, internal consistency, and new sequences

Kurt Gödel Research Center for Mathematical Logic
Währinger Strasse 25
1090 Wien
Austria

ps file of abstract

John Krueger, Some Consistency Results Related to Internal Approachability

I will sketch a proof that under suitable forcing axioms, various weakenings of internal approachability, namely internally unbounded, internally stationary, and internally club, are not equivalent.

Paul B. Larson, Martin's Maximum and definability in H(ℵ₂)

Department of Mathematics and Statistics
Miami University
Oxford, Ohio 45056
USA

We will discuss a coding method invented by Woodin which has been used to solve several problems in the study of H(ℵ₂), the collection of sets whose transitive closures have cardinality ℵ₁. In a paper appearing in 2000, we used this method to show that from a supercompact limit of supercompact cardinals one could force Martin's Maximum to hold while the P_max axiom (*) fails. Recently we modified that argument to prove a stronger fact, that Martin's Maximum is consistent with the existence of a wellordering of the reals definable in H(ℵ₂) without parameters, from the same large cardinal hypothesis. In doing so we give a much simpler proof of the original result.

Jordi Lopez-Abad (joint work with S. Todorcevic), Partial unconditionality and barriers

We survey a combinatorial framework for studying subsequences of a given sequence in a Banach space, with particular emphasis on weakly-null sequences. We base our presentation on the crucial notion of barrier introduced long time ago by Nash-Williams. In fact, one of the purposes of this work is to isolate the importance of studying mappings defined on barriersas a crucial step towards solving a given problem that involves sequences in Banach spaces. We focus our study on various forms of "partial unconditionality" present in arbitrary weakly-null sequences in Banach spaces. We give a general notion of partial unconditionality that covers most ofthe known cases such as, for example, Elton's near unconditionality, convex unconditionality, and Schreier unconditionality, but we also add some new cases.

Barbara Majcher-Iwanow, Polish group actions and admissible sets

University of Wroclaw

In the book "Classification and Orbit Equivalence Relations" G. Hjorth has introduced a kind of countable invariants for analysing orbits of G-actions on Polish spaces where G is a closed subgroup of S_∞. The method generalizes the Scott analysis of models. Using these ideas we study orbit equivalence relations inside admissible sets. For example we obtain appropriate versions of some results of M. Nadel on Scott sentences and admissible sets.

Our approach naturally leads us to some refinement of the notion of the canonical partition of a Polish G-space. It can be defined for any ordinal α (we call it the α-canonical partition).

Christian Rosendal, Classifying Borel transformations in Kakutani style

A classical problem of dynamics and ergodic theory dating back to Poincaré is to classify one-parameter flows up to some suitable notion of time change. One of the main tools in the ergodic theory part of this theory is a reduction of the problem to the notion of Kakutani equivalence of measure preserving automorphisms. In recent decades there has been an attempt to transfer the problems and techniques of ergodic theory into a purely descriptive setting and we will completely answer the analogue of Poincaré's question for Borel measurable one-parameter flows. We also present results on the much harder problem of classifying not necessarily injective Borel transformations up to a notion of kakutani equivalence.

Henk Barendregt, Gödel's legacy in computability

Goedel introduced, essentially via Term Rewriting Systems, the full class of computable functions for a practical purpose: the representability of provability in arithmetic. The way this was done was not optimal as the notion of partial computable function was missing and therefore no enumeration theorem could be given.

A second important legacy in his incompleteness paper is that provability is linked to computability and this is at present much applied in systems for computer mathematics.

Harvey Friedman, Gödel's legacy in mathematical philosophy

Gödel's definitive results and his essays leave us with a rich legacy of philosophical programs that promise to be subject to mathematical treatment. After surveying some of these, we focus attention on the program of circumventing his demonstrated impossibility of a consistency proof for mathematics by means of extramathematical concepts. This program has seen substantial progress through our new Concept Calculus.

John Steel, Gödel's legacy in set theory

In 1930-37, Kurt Gödel proved the first substantial theorems in the metamathematics of set theory.

Theorem 0.1 (Gödel 1931) If T is a consistent, axiomatizable extension of ZF, then T does not prove Con(T).

Theorem 0.2 (Gödel 1937) If ZF is consistent, then so is ZFC + GCH + "there is a Δ¹₂ wellorder of the reals".

We shall sketch how the themes present here have played out in the development of set theory.

Mark van Atten, Gödel's legacy in intuitionism

After a brief overview of the historical relations between Gödel and Brouwer as well as between Gödel and Heyting, the emphasis will shift to what Gödel's and Brouwer's approaches to the foundations of mathematics have in common