Proof interpretations are tools in mathematical logic with a wide range of applications: consistency results, independence results, and extraction of computational content from proofs, just to name a few. They are usually applied only in the context of logic or arithmetic. There is the dream of applying them even to set theory. Now the dream is fulfilled with a novel proof interpretation: Krivine's classical realisability. In this talk I present my personal digest of Krivine's classical realisability and one of its main applications to set theory: set theory ZF plus the statement "there is a set S between N (the set of natural numbers) and R (the set of real numbers) not equinumerous to its cartesian square S x S" is a consistent theory where both the axiom of choice and the continuum hypothesis fail. As a corollary we get two classical and celebrated results: ZF does not prove the axiom of choice nor the continuum hypothesis. This is a short, simple, and sweet talk, focusing on the ideas and setting aside technicalities.

* INRIA Paris-Rocquencourt, pi.r2, Univ Paris Diderot, Sorbonne Paris Cite, F-78153 Le Chesnay, France. Financially supported by the French Fondation Sciences Mathematiques de Paris.

A guarded recursive definition is one where the recursion variable only occurs in positions guarded by a delay operator. In this talk I will present a new model of guarded recursion and motivate it using two different examples: first as a model for computations with coinductive types such as streams, and second as a model of a metalanguage useful for defining models of programming languages with higher-order store. The model is a simple presheaf model (over the ordered natural numbers) and I will describe the computational intuition. If I have time I will describe work in progress on constructing models of intentional type theory with guarded recursion. Most of the talk describes joint work with Lars Birkedal, Kristian Stoevring and Jan Schwinghammer published at LICS 2011.

Modern software tends to undergo frequent requirement changes and typically is deployed in many different scenarios. This poses significant challenges to formal software verification, because it is not feasible to verify a software product from scratch after each change. It is essential to perform verification in a modular fashion instead. The goal must be to reuse not merely software artifacts, but also specification and verification effort. In our setting code reuse is realized by delta-oriented programming, an approach where a core program is gradually transformed by code "deltas" each of which corresponds to a product feature. The delta-oriented paradigm is then extended to contract-based formal specifications and to verification proofs. As a next step towards modular verification we transpose Liskov's behavioural subtyping principle to the delta world. Finally, based on the resulting theory, we perform a syntactic analysis of contract deltas that permits to automatically factor out those parts of a verification proof that stays valid after applying a code delta. This is achieved by a novel verification paradigma called "abstract symbolic execution."

We present a novel coalgebraic formulation of infinite extensive games. We define both the game trees and the strategy profiles by possibly infinite systems of corecursive equations. Certain strategy profiles are proved to be subgame perfect equilibria using a novel proof principle of predicate coinduction which is shown to be sound by reducing it to Kozen's metric coinduction. We characterize all subgame perfect equilibria for the dollar auction game. The economically interesting feature is that in order to prove these results we do not need to rely on continuity assumptions on the payoffs which amount to discounting the future. In particular, we prove a form of one-deviation principle without any such assumptions. This suggests that coalgebra supports a more adequate treatment of infinite-horizon models in game theory and economics. I will also sketch the possibilities that this (and more generalized) mathematics opens up for reflexive economics, which takes it serious that modeling in social science takes place within the modeled system and that essentially depends on self-referential paradoxes and corecursion and similar mathematical constructions. This opens the door to a proper treatment of the Lucas critique, evolutionary, institutional, agend based, computational, numerical economics, econometrics of non experimental data, money, value theory, political economics and management theory and also to a unification and cross fertilization between systems sociology, computer science and biology.

The computability of functions by Pour-El and Richards requires that Sequential Computability and Effective Continuity. So, a computable function must be continuous. The theory of Walsh series is based on the Fine metric, which is stronger than Euclidean metric. A function is Fine continuous if and only if it is continuous at dyadic irrationals and right continuous at dyadic rationals. So, Rademach functions and Walsh functions are fine continuous. The Fine computability is defined by means of the Fine topology instead of the Euclidean topology.

The fixed point property on tree-like Banach spaces
A Banach space $X$ is said to have the fixed point property if for every weakly compact convex set $K\subseteq X$ and every non-expansive $T:K\to K$ (i.e. $\|Tx-Ty\|\leq \|x-y\|$ for all $x,y\in K$), the map $T$ has a fixed point. This property is closely related to the geometry of the space under consideration. If the geometry of the space is "nice", i.e. if $X$ possesses normal structure, then $X$ has the fixed point property. On the other hand, a space without normal structure may fail this property (e.g. the space $L_1$) or it may enjoy this property (e.g. the space $c_0$).
In this lecture we will consider the important class of separable Banach spaces not containing $\ell_1$ with non-separable dual. Our purpose is to study these spaces with respect to the fixed point property. In particular, after discussing some known members of this class, we will present a Banach space belonging to the class under consideration which has the fixed point property even though it does not possess normal structure.

Non-principal ultrafilters, program extraction and higher order reverse mathematics
Abstract: We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher order arithmetic. Let (U) be the statement that a non-principal ultrafilter on N exists and let ACA_0^w be the higher order extension of ACA_0. We show that ACA_0^w + (U) is Pi¹_2-conservative over ACA_0^w and thus that ACA_0^w + (U) is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly \Pi¹_2 statement \forall f \exists g A(f,g) in ACA_0^w + (U) a realizing term in G"odel's system T can be extracted. This means that one can extract a term t\in T, such that \forall f A(f,t(f)).

Descriptive complexity is a bridge between complexity theory and logic. It asks for the logic resources that are necessary to define the computational resources such as time, space or the amount of hardware that are necessary to decide a property. Horn and Krom logic have their origins in propositional logic. Some researchers extend them to second logic, named SO-HORN and SO-KROM logic. We define revised and extended versions of these logics and get some results. We show that SO-HORN$^r$ and ($\exists$)SO-KROM$^r$ capture P and NL on ordered structures, respectively, and both SO-EHORN and $\Pi^{1}_{1}$-KROM capture co-NP. 

November 4, 2011 at 15:00 in S2|15-201
Jaime Gaspar
Goedel functional interpretation

Abstract: We give a quantitative version of a strong nonlinear ergodic theorem for (a class of possibly even discontinuous) selfmappings of an arbitrary subset of a Hilbert space due to R.~Wittmann and outline how the existence of uniform bounds in such quantitative formulations of ergodic theorems can be proved by means of a general logical metatheorem. In particular these bounds depend neither on the operator nor on the initial point. Furthermore, we extract such uniform bounds in our quantitative formulation of Wittmann's theorem, implicitly using the proof-theoretic techniques on which the metatheorem is based. However, we present our result and its proof in analytic terms without any reference to logic as such. Our bounds turn out to involve nested iterations of relatively low computational complexity. While in theory these kind of iterations ought to be expected, so far this seems to be the first occurrence of such a nested use observed in practice. October 28, 2011 at 13:30 in S2|15-201

Abstract: Every nonempty open set in a computable metric space contains a computable point. In contrast, the Non-Basis Theorem asserts that a nonempty co-c.e. closed set in Cantor space (hence, even in the real line) can avoid any computable points. Recent exciting progress in Computable Analysis naturally raises the question whether Non-Basis Theorems exist for connected co-c.e. closed sets. In this talk, we show global and local non-computability results concerning connectivity, local connectivity, simply connectivity, and contractibility for planar continua.

Since then many other aperiodic tile sets have been found, not only on the discrete plane, but also on the continuous plane (the most famous being probably Penrose's "kite and darts" set of two tiles). 
In this talk, I will describe yet another construction of an aperiodic tile set. Although the resulting tile set will produce tilings quite similar to those of Robinson's (an infinite hierarchical structure of embedded  squares) the local constraints will be presented in a (hopefully) more natural way: we will start from simple geometrical figures and organize them step by step by adding new rules progressively to enforce the global structure.

At the seminar we will discuss the origins, basic ideas and notions of
synthetic topology, and some proofs. Depending on time, we'll speak about the logical and computational aspects of the theory.

Abstract: Hillam's theorem gives a characterisation of the convergence of fixed point iterations. We present a quantitative version of Hillam's theorem where we give an explicit rate of metastability (a kind of "finitary rate of convergence") for the fixed point iteration. We explain how this result is obtained by methods of proof theory used in the proof mining program, called functional interpretations, which extract computational content from proofs.

February 11, 2011 at 14:00 in S2|15-201
Alexander Kartzow
First-order logic on generalisations of pushdown graphs

Abstract: In their search for a topological characterization of relatively (i.e. oracle-) computable relations (aka multivalued functions), Brattka and Hertling (1994) have considered two notions: weak continuity (which is weaker than relative computability) and strong continuity (which is stronger than relative computability). Based on the Henkin quantifier, we propose a notion of uniform continuity and explore its relations to weak/strong continuity as well as to relative computability.

Abstract: It is known that determinacy of infinite games characterize many subsystems of second order arithmetic.

In this talk, we treat relatively stronger systems, beyond so-called "big five systems", and consider the possibility of determinacy as a tool to investigate strong systems of second order arithmetic.

We observe that the notion of nowhere density is essentially the earlier stability theoretic notion of superflatness, introduced by Podewski and Ziegler in 1978. With this, we show that for a subgraph-closed class C of (not necessarily finite) graphs, the following are equivalent:

1) C is nowhere dense
2) C is stable
3) C is dependent

The result can be generalised to classes of coloured digraphs. It fails if C is not subgraph-closed. For arbitrary graph classes, dependence is the most general notion, generalising both nowhere density and stability, as well as (locally) bounded clique-width. 

This is joint work with Hans Adler.

     MAX(f) = sup_{0<x<1} f(x) ,      INT(f) = int_0¹ f(t) dt .

It has been shown by Friedman and Ko (1982) that for the restricted an be approximated up to an error 2^{-n} on polynomial-space in n. In above's framework of computation, each computable real function f : [0,1] -> R is essentially represented as a type-2 function (in the sense of Weihrauch), mapping a rational sequence to a rational sequence, i.e., f \in (N->Q) -> (N->Q). This enables us to discuss the computational complexity of a real-valued function on classical Turing machines with oracle access. Here, a TM M computing f is presented with an oracle phi \in (N->Q) for x in [0,1] and a precision n in N, such that M produces the output M^\phi(n) \in Q with 

     |M^\phi(n) - f(x)| < 2^{-n}.  

When it comes to the computation of the functionals MAX and INT, the encoding of an input for a Turing machine becomes even more critical: Instead of representing an x \in [0,1] by a fast converging sequence \phi \in (N->Q), we now have to encode a continuous real-valued function f : [0,1] -> R. The first goal of this thesis is to devise, compare and explore different ways of accessing an unknown continuous real function via black-box queries that model the actual computation of f as supported by certified numerics like interval arithmetic or the iRRAM. Building on this, the second goal of this Master's Thesis is to determine the query complexity of the MAX-functional with respect to different protocols. In combination with an complexity analysis of the protocols themselves, this should yield more explicit quantitative and parameterized both upper and lower bounds (compared to those presented in the beginning) on the complexity of MAX (and INT).

Computation with infinitely presented groups

Abstract: We give an overview of the current methods for computing with a class of infinitely presented groups, the so-called finitely $L$-presented groups. Theses infinite presentations generalize finite presentations and they allow interesting applications. In particular, our methods allow to compute the lower central series quotients and the Dwyer quotients of the Schur muliplier.

Computable fields and their algebraic closures

Abstract: We present recent results about computable fields F, especially those algebraic over their prime subfields, and embeddings of them into their algebraic closures.  The discussion begins with the basic definitions and a review of Rabin's Theorem, and continues with more exact computability-theoretic comparisons, by Steiner and by the speaker, among the set of irreducible polynomials in F[X], the set of polynomials there with roots in F, and the image of F within computable presentations of its algebraic closure.  Finally, we will discuss the Blum-Shub-Smale model of computation on the real numbers, and explain how it changes the array of tools available for examination of these questions.     back to the top of the page

Proof interpretations with truth

This is based on a joint work with Paulo Oliva.     back to the top of the page

The monotone completeness theorem in constructive reverse

We give a logical principle which is stronger than LPO, and show that it is equivalent to the statement:

(1) Every bounded monotone sequence of real numbers is a Cauchy sequence without modulus.

We also give a function existence axiom which is weaker than the number-number choice for Pi⁰_1 formulas, and show that it is equivalent to the statement:

(2) Every Cauchy sequence without modulus is a Cauchy sequence with modulus.

 Therefore MCT is divided into the logical statement (1), the function existence statement (2), and the Cauchy completeness of the reals which is constructively provable without countable choice.

back to the top of the page

Finite axiomatization of quasivarieties of relational structures

On the expressive CNF formulas of bounded Tree- and Clique-Width

Abstract: We study the expressive power of certain families of polynomials over a field K. The latter are defined via Boolean formulas in conjunctive normal form. We attach in a natural way a graph to such a formula and study the resulting polynomial families when certain parameters of that graph like tree- and clique-width are assumed to bounded.     back to the top of the page

Exakte reelle Arithmetik - reelle Zahlen aus der Sicht der Informatik

Implementierungen dieses Berechenbarkeitsbegriffes werden oft als "exakte reelle Arithmetik" bezeichnet; Basis ist dabei in der Regel eine Intervallarithmetik mit mehrfach genauen Zahlen, ergänzt um eine automatisierte Genauigkeitssteuerung. Damit sind numerische Algorithmen möglich, die in der endlichen Welt der double-precision-Zahlen nicht sinnvoll wären. 

Slash and completeness 

Abstract: Gödel's incompleteness theorems gave a fatal blow in Hilbert's program. Despite this, there were some attempts to salvage the program. One of them, by Hilbert himself, was to add omega-rule (if A(n) is provable for each fixed n, then "for all n, A(n)" is provable) to Peano arithmetic. This rule evades Gödel's incompleteness and gives a complete arithmetical theory.   Proof interpretations are proof-theoretic tools to prove consistency results, conservation results, closure under rules and to extract computational content from proofs. The slash is a very simple toy case of a proof interpretation. However, the omega-rule boosts the slash, resulting in some interesting applications. We will talk about one of them: a very simple proof of the completeness of Peano arithmetic plus omega-rule.     back to the top of the page

 Martin Otto, TU Darmstadt
Acyclicity in hypergraph covers and applications 

Abstract: Which degrees of acyclicity can be achieved in FINITE hypergraph covers? While actual acyclicity can always be had in generally infinite unfoldings, finite covers can only guarantee certain bounded forms of acyclicity at best.   I want to discuss new constructions of weakly N-acyclic covers (joint work with Vince Barany and Georg Gottlob, Oxford) and N-acyclic covers with a view to their use in the finite model theory of guarded logics.     back to the top of the page

Expressiveness and Computational Complexity of Euclidean Quantum Logic 

Abstract: Quantum logic generalizes, and in dimension one coincides with, Boolean logic. The satisfiability problem of quantum logic formulas is shown NP-complete in dimension two. We then extend these considerations to three and higher-dimensional Euclidean spaces R^d and C^d. For fixed d>2, quantum satisfiability turns out polytime-equivalent to the real feasibility of a multivariate quartic polynomial equation: a well-known problem lying (probably strictly) between NP and PSPACE. We finally investigate the problem over INdefinite finite dimensions and relate it to the real feasibility of quartic NONcommutative *-polynomial equations.     back to the top of the page

 Comparison of Complexity over the Real vs. Complex Numbers 

Abstract: We compare the complexity of certain problems over the reals with their corresponding versions over the complex numbers. We argue in particular that the problem of deciding whether a system of (real) polynomial equations has a real solution is strictly harder than asking for a complex solution, since it cannot be solved by a complex BSS-machine.   On the other side we describe a family of problems, whose real versions are in the model of algebraic decision trees strictly easier than its complex versions.   For this end we prove a new lower bound for the decision complexity of a closed algebraic set X in C^n in terms of the sum of its (compactly supported) Betti numbers b_c(W), which is for the first time better than logarithmic in b_c(W). 

back to the top of the page

 Topology in computable analysis 

Abstract: Computable Analysis studies computability over the real numbers and related spaces. Since computable functions are continuous in some sense, topology plays an important role in this theory. The cartesian closed category QCB of quotients of countably based topological spaces turns out to be an appropriate category for modelling the topological aspects of higher type computation.

In this talk, we discuss topological properties of the Kleene-Kreisel continuous functionals and their surprising relationship to an open problem in exact real-number computation. This problem is whether two approaches in functional programming on higher type computability over the reals coincide.

We show that the sequential topology on the space N^(N^N), which is the space of Kleene-Kreisel continuous functionals of type 2, is neither zero-dimensional nor regular. Moreover, we establish non-regularity of further function spaces formed in the cartesian closed category of sequential spaces. This is one of the categories from which QCB inherits its cartesian closed structure.     back to the top of the page

 Sequential game theory: a formal and abstract approach 

Abstract: In a game from game theory, a Nash equilibrium (NE) is a combination of one strategy per agent such that no agent can increase his payoff by unilaterally changing his strategy. Kuhn proved that all (tree-like) sequential games have NE. Osborne and Rubinstein abstracted over these games and Kuhn's result: they proved a *sufficient* condition on agent *preferences* for all games to have NE. I will present a *necessary and sufficient* condition, thus accounting for the game-theoretic frameworks that were left aside. The proof is *formalised* using Coq, and contrary to usual game theory it adopts an inductive approach to trees for definitions and proofs. By rephrasing a few game-theoretic concepts, by ignoring useless ones, and by characterising the proof-theoretic strength of Kuhn's/Osborne and Rubinstein's development, the talk also intends to clarifies sequential game theory.

Then I will sketch an alternative proof. Both proofs so far pre-process the preferences by topological sorting, which is surprising since it decreases the number of NE. Finally I will sketch two other proofs that pre-process the preferences only by transitive closure. The four proofs are all constructive and by induction, and I will compare them when seen as algorithms. The four proofs also constitute diverse viewpoints on the same concepts, the trial of diverse techniques against the same problem, and reusable techniques for similar structures. 

back to the top of the page

 Proof interpretations with truth 

Abstract: Proof interpretations are proof-theoretic tools to extract computational content (such as computable choice functions) from proofs. In some cases this only works (at least without strengthening the theories involved) for proofs of theorems of a particular logical form, but we wish to extract computational content from proofs of arbitrary theorems. Interpretations with truth have been developed to cope with this. We present two new methods on how to do hardwire truth and apply them to new proof interpretations.

In a first part we make a brief introduction to proof interpretations and the extraction of computational content from proofs. Then in a second part we present our two methods. Finally in a third part we apply them in some case studies.

This is joint work with Paulo Oliva.     back to the top of the page

 Real Computation with Least Discrete Advice: A Complexity Theory of Nonuniform Computability 

Abstract: It is folklore particularly in numerical and computer sciences that, instead of solving some general problem f:A->B, additional structural information about the input x in A (that is any kind of promise that x belongs to a certain subset A' of A) should be taken advantage of. Some examples from real number computation show that such discrete advice can even make the difference between computability and uncomputability. We turn this into a both topological and combinatorial complexity theory of information, investigating for several practical problems how much advice is necessary and sufficient to render them computable. Specifically, finding a nontrivial solution to a homogeneous linear equation A*x=0 for a given singular real NxN-matrix A is possible when knowing rank(A)=0,1,...,N-1; and we show this to be best possible. Similarly, diagonalizing (i.e. finding a BASIS of eigenvectors of) a given real symmetric NxN-matrix is possible when knowing the number of distinct eigenvalues: an integer between 1 and N (the latter corresponding to the nondegenerate case). And again we show that N-fold (i.e. roughly log N bits of) additional information is indeed necessary in order to render this problem (continuous and) computable; whereas for finding SOME SINGLE eigenvector of A, providing the truncated binary logarithm of the least-dimensional eigenspace of A--i.e. Theta(log N)-fold advice--is sufficient and optimal.     back to the top of the page

Effective Descriptive Set Theory and Applications in Analysis 

Abstract: Descriptive Set theory is the area of mathematics which studies the structure of definable sets in separable and complete metric spaces. A central part of this area is Effective Descriptive Set Theory (for shortness Effective Theory) which uses ideas from Logic and in particular from Recursion Theory. This area provides a deeper understanding of the subject and has applications in Analysis. We begin this lecture with a brief summary of the basic concepts and we give a new approach to Effective Theory which yields some surprising results. Then we present some connections with General Topology; all theorems we talk about involve notions from both areas. Finally we give some results in Banach space Theory. Here all theorems involve only classic (i.e., non-effective) notions but still Effective Theory is essential for their proof.     back to the top of the page

Ionads: a generalised notion of topological space

Acyclicity in hypergraph covers

On the Computational Content of Bolzano-Weierstraß

Abstract: We will apply the methods developed in the field of 'proof mining' to the Bolzano-Weierstraß theorem BW and calibrate the computational contribution of using this theorem in a proof of a combinatorial statement. Using a simple proof based on weak König's lemma and arithmetical comprehension we provide an explicit solution of the Gödel functional interpretation as well as the monotone functional interpretation of BW for the product space \prod_i \in N [-k_i, k_i] for a given sequence of rational numbers (k_i) \subseteq Q (with the standard product metric). In fact, we will use it to get optimal program and bound extraction theorems for proofs based on fixed instances of BW, i.e. for BW applied to fixed sequences in \prod_i \in N [-k_i, k_i].     back to the top of the page

Logics with Rank Operators

Abstract: It is a long-standing open problem in descriptive complexity theory whether there is a logic that expresses exactly the polynomial-time decidable properties of unordered structures. It has been known since the early 90s that fixed-point logic with counting (FPC) is not sufficient and there have been several proposals for more expressive logics. Taking our inspiration from recent results that show that natural linear-algebraic operations are not definable in FPC, we propose FPR - an extension of fixed-point logic with an operator for matrix rank. We show that this is strictly more expressive than FPC and can express the polynomial-time problems that have been shown to be inexpressible in FPC. We also show that FO+R, the extension of first-order logic with rank operators is surprisingly expressive. It can express some forms of transitive closure and, on ordered structures, captures the complexity classes ModpL.

In this talk, I will give the history and general background to the question and explain the context of the new results. I will also point to several interesting open problems. (Joint work with Martin Grohe, Bjarki Holm and Bastian Laubner).