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

To main page

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

To main page