September 29: Sebastiaan Terwijn: Intervals in the Medvedev lattice
16.00--17.00
Abstract:
The Medvedev lattice is a structure from computability theory with ties to constructive logic. We will briefly describe this connection and the relation to structures such as the Turing degrees. We will then discuss structural properties of the Medvedev lattice, in particular, the size of its intervals. We show that every interval in the lattice is either finite, in which case it is isomorphic to a finite Boolean algebra, or contains an antichain of size 2^2^\aleph_0, the size of the lattice itself. We also prove that it is consistent that the lattice has chains of this size, and in fact that these big chains occur in every interval that has a big antichain. We also study embeddings of lattices and algebras. We show that large Boolean algebras can be embedded into the Medvedev lattice as upper semilattices, but that a Boolean algebra can be embedded as a lattice only if it is countable. Finally we discuss which of these results hold for the closely related Muchnik lattice.
To main page

October 13: Yuri Gurevich: Play to test
16.00--17.00
Abstract:
What's testing? Well, from some point of view, it is a game. Testing tasks can be viewed (and organized!) as games against nature. We introduce and study reachability games. Such games are ubiquitous. A single industrial test suite may involve many instances of a reachability game; hence the importance of optimal or near optimal strategies for reachability games. We find out when exactly optimal strategies exist for a given reachability game, and how to construct them.
To main page

October 27: Jouko Väänänen: Dependence Logic
16.00--17.00
Abstract:
n 1961 Henkin suggested a game theoretic semantics for first order logic and its extension by so called partially ordered quantifiers. It remained an open problem whether this extension and other similar logics could be given a compositional semantics. In 1997 Wilfrid Hodges made a breakthrough in this area by giving a compositional semantics for these logics. In his semantics satisfaction is defined as a relation between formulas and sets of assignments, rather than as a relation between formulas and individual assignments, as is customary in first order logic.
Based on this idea, we introduce Dependence Logic. This is an extension of first order logic, in which dependence of variables on each other is a basic atomic concept. We give an overview of this logic, its properties, and its applications, from database theory to set theory.
To main page

October 27: Wim Veldman: Perhaps the Intermediate Value Theorem and perhaps more
16.00--17.00
Abstract

November 24: Valentin Shehtman: On completeness and incompleteness in first-order modal logic.
16.00--17.00
Abstract:
We shall briefly describe the present nontrivial situation in semantics for first-order modal and superintuitionistic logics.
It can be characterized as a big gap: simply axiomatizable logics may have a complicated semantical description, and the other way round --- ``relatively simple" classes of frames may correspond to non-axiomatizable logics.
The following topics will be discussed: completeness and elementarity in standard Kripke semantics; generalizations of Kripke semantics -- from Kripke sheaves to simplicial semantics; alternatives to Kripke-type semantics.
To main page

December 15: Brian Semmes: Decomposing 2->3.
16.00--17.00
Abstract:
In this talk I will review the tree game and show how it can be calibrated to characterize various classes of functions on Baire space. I will review the "n->m" notation and sketch a game-theoretic proof of a structure theorem for the "2->3" class.
To main page

January 19, 2007: Tim Baarslag: Limitations of primitive recursive algorithms
16.00--17.00
Abstract:
Studying a primitive recursive definition of a mathematical function yields a corresponding primitive recursive algorithm in a straightforward way. We will review such primitive recursive algorithms from a computational point of view. We shall prove among other things that primitive recursive algorithms are very ineffective in terms of the number of steps they require. We will extend these results by broadening the class of `built-in' functions and by adding a scheme of minimization to consider partial recursive algorithms.
To main page

February 2, 2007: Rosalie Iemhoff: Skolemization and Herbrand's theorem
16.00--17.00
Abstract:
The Skolemization method stems from the intuition that proving a universally quantified statement is the same as proving the statement for an arbitrary object. The ``let x be an arbitrary number'' sentence that appears at the start of many a proof in which it is shown that ``for all x ...'', bears witness of this fact. Herbrand's theorem builds on this insight by showing that quantified statements are equiconsistent with propositional ones that can be obtained from the original statement in a canonical way. In the setting of constructive theories these methods fail to be sound and complete. In the talk I will present a variant of Skolemization that is sound and complete for constructive theories, and explain how it easily implies an analogue of Herbrand's theorem. After that I will discuss the implications of these results for various well-known constructive theories, and compare them to other results with a Skolemization flavour, like for example the Dialectica Interpretation.
To main page

February 16, 2007: Ronald de Wolf: Quantum proofs for classical theorems
16.00--17.00
Abstract:
In the last decade the theory of quantum mechanical computers has developed, and we now know that quantum computers can be exponentially faster than classical computers when solving certain problems (this probably includes factoring). A more recent and very different application of quantum computers is as a mathematical tool to prove or reprove theorems about *classical* computers. We will give four examples, from the areas of communication complexity, error-correcting codes, complexity classes, and matrix rigidity.
To main page

March 2, 2007: Juha Kontinen: Majority in logic and computation
16.00--17.00
Abstract:
The topic of the talk is descriptive complexity theory. The logarithmic, linear, and polynomial hierarchy have been characterized logically in terms of alternating universal and existential quantifiers. In this talk we consider the so-called counting extensions of these hierarchies. We show that these classes can be logically characterized in terms of majority quantifiers. We also discuss alternative characterizations of these classes in terms of threshold circuits and bounded arithmetics.
To main page

March 16, 2007: Juliette Kennedy: Square-like principles, Arithmetic and Model Theory
16.00--17.00
Abstract:
We present some independence results in the area of classical model theoretic embedding and isomorphism theorems, first considering the particular case of models of arithmetic. This is joint work with Saharon Shelah.
To main page

March 23, 2007: Andres Villaveces: Generic Predicates over Hilbert Spaces - (Continuous) Model Theory of Pairs
16.00--17.00
Abstract:
Expanding well-known structures with generic objects has led in the past to various important results and examples of simple theories (ACFA is perhaps the best known). I will present a generalization of a theorem of Chatzidakis and Pillay to continuous model theory, and two constructions of Hilbert spaces by generic predicates (in the continuous model theory sense). I will also present a result in the intersection between the model theory of Abstract Elementary Classes and Continuous Model Theory. This is joint work with Alexander Berenstein.
To main page

March 30, 2007: Roman Kossak: Forcing in models of arithmetic
16.00--17.00
Abstract:
Forcing is a useful tool for constructing undefinable inductive subsets of nonstandard models of PA. I will give a survey of applications. It will include Simpson’s theorem on expansions to prime models and its recent generalization by Schmerl; Milll’s theorem on limitations of the Mac Dowell-Specker theorem; connections with the Scott set problem, and the problem of constructing a rather classless recursively saturated model.
To main page

April 3, 2007: Yuri Gurevich: Why Sets?
16.00--17.00
Abstract:
Sets play a key role in foundations of mathematics. Why? To what extent is it an accident of history? Imagine that you have a chance to talk to mathematicians from a far away planet. Would their mathematics be set-based? What are the alternatives to the set-theoretic foundation of mathematics? Besides, set theory seems to play a significant role in computer science, in particular in database theory and formal methods. Is there a good justification for that? We discuss these and related issues.
To main page

Arithmetic Days: Models and Interpretations
Wednesday, April 4
Kromme Nieuwe Gracht 80: 1.02
10.00-17.00h
10.00-11.00 Kossak: Smorynski's projects
11.15-12.15 Ressayre: From model completeness to quantifier elimination in o-minimal expansions of the reals: an application of non standard methods
12.15-14.00 LUNCH
14.00-15.00 Kaye: Interpretations of arithmetic and set theory
15.00-15.30 TEA
15.30-16.30 Engstrom: Transplendent models: Omitting types in expansions
16.30-17.00 DISCUSSION

Thursday, April 5
Drift 21, 1.04
10.00-17.00.
10.00-11.00 Enayat: Automorphisms of models of arithmetic
11.15-12.15 Kennedy: Square principles and model theory
12.15-14.00 LUNCH
14.00-15.00 Visser: Local and Global Interpretability
15.00-15.30 TEA
15.30-17.00 FREE ACTIVITIES
19.00 DINNER

April 13, 2007: Bas Spitters: Computable sets: Located and overt locales
16.00--17.00
Abstract:
What is a computable set? One may call a bounded subset of the plane computable if it can be drawn at any resolution on a computer screen. Using the constructive approach to computability one naturally considers totally bounded subsets of the plane. We connect this notion with notions introduced in other frameworks.
A subset of a totally bounded set is again totally bounded iff it is located. Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in locale theory in a constructive, or topos theoretic, context. We show that the two notions are intimately connected. We propose a definition of located sublocale motivated by locatedness of subsets of metric spaces. A closed sublocale of a compact regular locale is located iff it is overt. Moreover, a closed subset of a complete metric space is Bishop compact --- that is, totally bounded and complete --- iff its localic completion is compact overt. The closure and the positive closure of a located sublocale coincide. For Baire space metric locatedness corresponds to having a decidable positivity predicate.
Finally, we show that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales.
We work constructively, predicatively and avoid the use of the axiom of countable choice. Consequently, all are results are valid in any (predicative) topos.
Joint work with Thierry Coquand
To main page

April 19, 2007: Lauri Hella: Constraint Satisfaction Problems and Quantifier Free Reductions
16.00--17.00
Abstract:
The class of Constraint Satisfaction Problems is an intensively studied subclass of NP. It bears relevance to a wide variety of disciplines, including molecular biology, electronic engineering, computer algebra and AI. All constraint satisfaction problems can be formulated as homomorphism problems. In the uniform case, two finite relational structures B and A are given as input, and the task is to determine whether there is a homomorphism from B to A. Our focus is on the non-uniform case, in which the target structure A is fixed. The corresponding problem is denoted by Csp(A), and the class of all such non-uniform constraint satisfaction problems is denoted by CSP. Well-known examples of CSP are graph coloring problems, and satisfiability problems.
A lively branch of CSP research is devoted to the so-called Dichotomy Conjecture: Every problem in CSP is either in PTIME or NP-complete. This conjecture was formulated by Feder and Vardi (93, 99), and it was inspired by dichotomy results that were already known for restricted classes of constraint satisfaction problems. A popular approach to the Dichotomy Conjecture is to use connections to universal algebra. The notion of polymorphism can be used to obtain polynomial time reductions between constraint satisfaction problems. It also leads to a notion of expressive power of a problem Csp(A) in terms of a closure operator on the set of relations on A.
We propose quantifier free reductions as another way of measuring the expressive power of constraint satisfaction problems. We write Csp(B) <_qf Csp(A) if there is a sequence P of quantifier free first-order formulas such that for all C, C is in Csp(B) if and only if P(C) isin Csp(A), where P(C) is the structure defined by P on C. In our main results we prove that there are problems which are complete for CSP with respect to quantifier free reductions. Here we say that Csp(A) is complete for CSP with respect to quantifier free reductions, if Csp(B) <_qf Csp(A) for every finite relational structure B. Similarly, we prove that there are Datalog definable problems in CSP which are complete for the class of all Datalog definable CSPs with respect to quantifier free reductions.
Joint work with Merlijn Sevenster
To main page

May 4, 2007: Ali Enayat: From fragments of arithmetic to large cardinals via Quine-Jensen set theory
16.00--17.00
Abstract:
The Quine-Jensen system NFU of set theory is obtained by allowing urelements in Quine's "New Foundations" system NF of set theory. The consistency of NF has remained an open question since its inception (1937), but Jensen's work (1968) shows that the strengthening of NFU with the axiom of infinity is equiconsistent with a weak fragment of Zermelo set theory. But that is not the end of the story.
In this talk we discuss recent work concerning the calibration of the consistency strength, as well as the interpretability-type, of various natural extensions of NFU. As we shall see, there is an unexpected, intimate relationship between NFU-style set theories and canonical systems of arithmetic and set theory. Some of the new results discussed in this talk have been obtained in collaboration with Robert Solovay.
To main page

May 18, 2007: Dimitri Hendriks: A calculus for deciding productivity of recursive stream definitions
16.00--17.00
Abstract:
Our work centers around the notion of `productivity' which is dual to termination, and originates from the paradigm of functional programming. Roughly, a program is productive if it continuously builds up a (potentially) infinite object that is canonical in the sense that it is in constructor normal form. The objective of our work is to analyze productivity of a restricted class of functional programs that yield streams, that is, infinite sequences, over some domain. In order to analyze the quantitative behaviour of recursive stream programs, we abstract from actual stream elements to what we call `pebbles'. In the calculus we have developed, the `pebble growth rate' of recursive stream functions, the components of recursive stream programs, is expressible. Employing these fine-grained means we are able to determine whether a recursive stream program `feeds itself' and enables a non-terminating computation whose output converges to a constructor normal form. In this way we obtain a decision algorithm for productivity on a large class of recursive stream definitions that, as easy examples, contains programs for the streams of Fibonacci numbers, and the Thue-Morse and Toeplitz sequences.
Joint work with Joerg Endrullis, Clemens Grabmayer, Ariya Isihara, and Jan Willem Klop.
To main page

June 1, 2007: Piet Rodenburg: Piecewise Initial Algebra Semantics
16.00--17.00
Abstract:
Data types - algebras modulo isomorphism, essentially - can be defined (specified) by equations: equations E define algebra A if A is the free algebra, on the empty set of generators, in the variety determined by E; possibly, and importantly, it may be that one has to define an expansion of A, and then reduce. People prefer to get long lists of equations and reductions in instalments; and then the question arises when two ways of piecing a specification together are equivalent.
Bergstra, Heering and Klint proposed an equivalence calculus, 'module algebra', in the early nineties. They defined a number of interpretations for this calculus; but they did not succeed in linking up with the form of algebraic specification just sketched.
In a paper to appear in the Journal of Logic and Algebraic Programming I managed this for about 90%. I will describe the approach taken there, and discuss its shortcomings.
To main page

June 11, 2007: Yuri Gurevich: Zero-one laws of discrete mathematics
16.00--17.00
Abstract:
The fraction of n-vertex graphs that are connected grows to 1 as n grows to infinity. In that sense almost all finite graphs are connected. Almost all graphs are also Hamiltonian, not 3-colorable, rigid, etc. Each of these results required a separate proof. Is there a general phenomenon behind results of that sort? It turns out that much depends on the logical form of the property in question. In particular, every first-order sentence is almost surely true or almost surely false on finite structures. This zero-one law for first-order logic was generalized to some richer logics. We will discuss the zero-one laws of finite model theory including a new geometric zero-one law of Bob Gilman, Alexei Myasnikov and the speaker.
To main page

June 15, 2007: Kamal Lodaya: Marking time
16.00--17.00
Abstract:
For applications in timed systems, temporal logic has been generalized to include measurement of duration. as examples, we have the "Metric tense logic" of Burgess (1984), "Metric temporal logic" of Koyman(1990), "Duration calculus" of Zhou, Hoare and Ravn (1991), "MTL" of Alur and Henzinger (1993), "Quantitative temporal logic" of Hirshfeld and Rabinovich (1999). In this talk we discuss the continuous and sampled semantics of these logics, as well as completeness and decidability issues.
To main page