Logikseminariet Stockholm/Uppsala hösten 2002 och våren 2003

Seminarieledare: Per Martin-Löf (Stockholm), Erik Palmgren, Viggo Stoltenberg-Hansen (Uppsala)

Vårterminen 2003

2 juni

13.00–14.00

Johan Strömqvist

Ekvivalenta formuleringar av urvalsaxiomet, speciellt i algebra

Sammanfattning: Urvalsaxiomet formulerades av Zermelo 1904 med ändamålet att visa den av Cantor formulerade välordningsprincipen, den princip som säger att varje mängd kan välordnas. Det är ett av mängdlärans axiom och har likt Euklides parallellpostulat fått utstå en hel del kritik för att inte vara av ``uppenbar natur''; kritiken har främst riktats mot axiomets icke konstruktiva natur. Urvalsaxiomet, Zorns lemma och välordningsprincipen är sedan länge kända ekvivalenta former inom mängdläran men fortfarande dyker det upp nya ekvivalenta former inom olika grenar av matematiken. Inom algebra, till exempel, så impliceras urvalsaxiomet både av att ``varje kommutativ ring med etta har ett äkta maximalt ideal'' och att ''varje vektorrum har en bas'', vilket visades av Hodge 1979 respektive Blass 1984. Den sistnämnda implikationen kommer vi att bevisa under seminariet. Omvändningen av dessa båda utsagor är kända sedan länge. Vi kommer också att titta lite närmare på ordinaltal, såsom von Neumann definierade dem, och beskriva något informellt hur dessa utgör ryggraden bland mängder.

Måndagen den 2 juni 2003 kl 13.00 - 14.00 Johan Strömqvist presenterar sitt examensarbete "Ekvivalenta formuleringar av urvalsaxiomet, speciellt i algebra". Handledare: Bo Stenström Plats: sal 16, hus 5, Kräftriket


21 maj 2003

10.00–11.45, Sal 16, hus 5, Kräftriket

Per Martin-Löf

Are the objects of propositional attitudes propositions in the sense of propositional and predicate logic?


7 maj 2003

Onsdag 7 maj, kl 10.30-12.15 (Obs! Tid och lokal) Sal 2144, MIC, Polacksbacken, Uppsala

Erik Palmgren

Predikativa kategorier och intern logik


22 april 2003

Tisdag den 22 april, kl. 10.30, OBS: DAG och TID!! Sal 2244 MIC, Polacksbacken, Uppsala.

Marko Djordjevic

On the finite submodel property

Abstract: A result giving a new (it seems) sort of first-order sentence without finite models will be presented. This leads us into looking at the so called finite submodel. A first-order theory T has the finite submodel property if, for any model M of T, any sentence in T is true in a finite substructure of M. It is known that all smoothly approximable structures and the random structure have the finite submodel property. I will, in a context wider than this, present both positive results (conditions which imply the finite submodel property) and negative results (examples without it).


9 april 2003

Onsdagen den 9 april kl. 10.00-11.45 i sal 16, hus 5, Kräftriket.

Jens Brage

A classical tableau calculus


2 april

Onsdag 2 april, kl. 10.30 (OBS Tid och lokal!), Sal 2244, MIC, Polacksbacken, Uppsala

Nicola Gambino (Cambridge)

Sheaf interpretations for constructive set theories.

Abstract: Constructive Set Theory is concerned with the study of axiom systems supporting the development of constructive mathematics in a set-theoretical framework. On the one hand, constructive set theories and Martin-Löf dependent type theories are very similar since they both reject the assumption of "fully impredicative" principles, such as the power-set axiom. On the other hand, they are very different because of the distinctive peculiarities of set theory and type theory.
After introducing Constructive Set Theory and explaining its connection with Dependent Type Theory, I will develop sheaf interpretations for constructive set theories. These interpretations can be seen as the constructive counterpart of the forcing technique for classical set theory. Sheaf interpretations offer indeed a general technique that can be applied to establish proof-theoretical results concerning constructive systems.
In the final part of the talk, I will present first applications of sheaf interpretations and discuss how this technique could be transferred in Dependent Type Theory.


26 mars 2003

Onsdag 26 mars, kl. 13.15, Matematiska institutionens seminarierum 3513 (plan 5, hus 3) MIC, Polacksbacken, Uppsala.

Luigi Santocanale

An Interpolation Theorem in the Theory of Circular Proofs

ABSTRACT: A mu-calculus is a propositional logic with fixed point operators mu and nu. For example, given a propositional formula t(x) whose interpretation is a monotone function f: L -> L on a complete lattice, two new formulas mux.t(x) and nux.t(x) are created to denote the least and the greatest fixed point of f, respectively. The operations mu and nu are analogous to quantifiers, and classes Sn and Pn of propositional formulas (or mu-terms) are defined as follows: S0 = P0 is the class of propositional formulas without applications of fixed point operations; Sn+1 is the closure of Sn and Pn under the operation mu and substitution; Pn+1 is the closure of Sn and Pn under the operation nu and substitution. In this talk I will show how we can use tools from proof theory to prove the following fact: let t in Pn + 1 and s in Sn + 1 be two mu-terms in the signature of lattice theory; if for all interpretations on a complete lattice the relation |t| <= |s| holds, then we can find a mu-term r such that: 1) for every interpretation |t| <= |r| and |r| <= |s|, 2) r belongs to the closure of Sn and Pn under the operation of substitution. The proofs we consider are winning strategies in games of the form G -> H, well known from the semantics of linear logic; G and H are parity games. The game G -> H can have cycles and the winning strategies as well; the proofs that we consider are therefore circular.


19 mars 2003

Onsdag 19 mars, kl. 10.00 i sal 16, hus 5, Kräftriket.

Johan Granström

Imperative lambda calculus

Abstract: Imperative Lambda Calculus (ILC) is a bridge between functional and mainstream programming languages. Johan Granström will discuss methods of interpreting ILC in dependent type theory.


5 mars 2003

Onsdag 5 mars, kl. 13.15 (OBS Tid!) Matematiska institutionens seminarierum 3513 (plan 5, hus 3), MIC, Polacksbacken, Uppsala

Benno van den Berg (Utrecht)

Inductive types, ex/reg-completions, and realizability


19 februari 2003

Matematiska institutionens seminarierum 3513 (plan 5, hus 3) MIC, Polacksbacken, Uppsala.

Erik Palmgren

Constructive completions of ordered sets, groups and fields II


5 februari 2003

kl. 13.00, Matematiska institutionens seminarierum 3513 (plan 5, hus 3) MIC, Polacksbacken, Uppsala. OBS Ny tid och lokal!

Erik Palmgren

Constructive completions of ordered sets, groups and fields

Abstract: The constructive real numbers are known to verify only a weakened form of the axioms for total order. We examine two kinds of completions of such orders. For arbitrary dense orders these are Dedekind cuts. For (nonarchimedean) ordered groups and fields, we consider so-called Cauchy cuts. As always, there is the problem how to represent the collection of cuts as a set in type theory. We show how this can be done using provable choice principles, in particular a generalisation of dependent choice.


29 januari 2003

Onsdagen 29 januari kl 10.00-11.45 Sal 16, hus 5, Kräftriket, Stockholm.

Jesper Carlström

Descriptive Definitions in Type Theory

Abstract: Descriptive definitions are very common in mathematics: you prove there is a unique x satisfying P(x) and then give that x a name. For instance, it is common to define a^{-1} as `the x such that ax=1 and xa=1'.
In most logical systems, however, we do not have support for descriptive definitions but only explicit ones. There are several known ways to interpret descriptive definitions by eliminating them, but these interpretations are unsatisfactory in several respects, as I will show.
I will give a very direct interpretation in type theory by translating a modified version of Sören Stenlund's natural deduction-style system for first order intuitionistic logic with descriptors.


Höstterminen 2002

11 december 2002

Onsdagen den 11 december kl. 10.30 i sal 2:315, Mic, Polacksbacken, Uppsala.

Viggo Stoltenberg-Hansen

An effective domain representation of $C^1[0,1]$.

Abstract: We present a construction, due to A. Edalat and A. Lieutier, of an effective Scott domain $D$ with the property that $C^1[0,1]$ is topologically embedded into the maximal elements of $D$.


4 december 2002

Onsdag 4 december kl 10.30--12.15, sal 2:315, MIC, Polacksbacken, Uppsala.

Alexander Shen (Moscow, right now in Uppsala)

Self-similar aperiodic tilings

Abstract: A tiling problem requires to tile the plane with tiles, (squares with some pattern on them) if there are finite number of tile types and local rules that describe legal tilings. The classic theorem (Berger, Robinson) says that there is a tile set (the set of tiles and rules) that has only aperiodic tilings. This seems rather counterintuitive since translation-invariant rules force non-invariant tilings. We try to explain the underlying reason representing Berger-Robinson construction as a kind of self-similarity argument.


27 november 2002

Onsdagen den 27 november kl. 10.00-11.45 i sal 16, hus 5, Kräftriket, Stockholms Universitet

Per Martin-Löf

Inference vs. consequence


20 november 2002

Onsdagen den 20 november kl. 13.15 i sal 2:245, Mic, Polacksbacken, Uppsala

Jonas Eliasson

Ultrasheaves and double negation (cont.)


13 november 2002

Onsdagen den 13 november kl. 10.00 i sal 16 hus 5, Kräftriket, Stockholm

Sara Negri (Helsingfors)

Permutability of rules in lattice theory


6 november 2002

6 november 10.30 i sal 2315, MIC, Polacksbacken, Uppsala

Jonas Eliasson

Ultrasheaves and Double Negation

Abstract: The talk will be devoted to proving that the topos of ultrasheaves is (equivalent to) the double negation subtopos of Moerdijk's topos (a joint work with S. Awodey). All necessary concepts will be introduced in the talk.


23 oktober 2002

Onsdagen den 23 oktober kl. 10.30 i sal 2:315, MIC, Polacksbacken, Uppsala

Lars-Åke Lindahl

PRIMES is in P (Referat av en artikel av M. Agrawal, N. Kayal, N. Saxena)


16 oktober 2002

Onsdagen den 16 oktober kl. 10.30 i sal 2:315, MIC, Polacksbacken,Uppsala

Thierry Coquand

A calculus of dependently typed records


9 oktober 2002

Onsdagen den 9 oktober kl. 10.30 i sal 2:315 MIC, Polacksbacken, Uppsala

Alexander Rabinovich (Tel Aviv University, Israel)

Composition Methods

Abstract: Composition Theorems are tools which reduce sentences about a complex structure to sentences about its parts. A seminal example of such a result is the Feferman-Vaught Theorem (1959) which reduces the first-order theory of generalized products to the first order theory of its factors and the monadic second-order theory of index structure. In this talk I explain (1) a definition of a generalized sum of structure and (2) a composition theorem for first-order logic over the generalized sum. Some applications of the composition theorem to definability will be provided which replace game (or inductive) arguments by transparent reductions.


2 oktober 2002

Onsdagen den 2 oktober kl. 10.00-11.45 i sal 16, hus 5, Kräftriket.

Per Martin-Löf

Are rules valid in virtue of meaning or is meaning determined by rules?


25 septembet 2002

25 september 10.30 i sal 2315, MIC, Polacksbacken, Uppsala

Jonas Eliasson

Sheaves and Ultrasheaves II

Abstract. I will continue with some of the proofs left out in the first talk. I will also sketch the proof that the topos of ultrasheaves is equivalent to the double negation subtopos of the topos of sheaves on filters.


18 september 2002

18 september 10.30 i sal 2315, MIC, Polacksbacken, Uppsala

Jonas Eliasson

Sheaves and Ultrasheaves

Abstract: Given a set S and an ultrafilter (I,U) we can form the ultrapower S^I/U of S over (I,U). But what happens when you vary the ultrafilter U? An answer to this question has been given by Andreas Blass in the study of ultrafilters under the Rudin-Keisler ordering. In this talk I will show how these varied ultrapowers can be seen as ultrasheaves, i.e. sheaves on the category of ultrafilters.
I will introduce the collection of ultrasheaves (a topos) and show how it relates to the ultrapowers. I will explain how this arose from the constructive sheaf model of nonstandard arithmetic introduced by Ieke Moerdijk, and show how the topos can be used to model nonstandard set theory. No knowledge of topos theory will be assumed.


28 augusti 2002

28 augusti 10.30 i sal 2315, MIC, Polacksbacken, Uppsala.

Erik Palmgren

Well-founded choices, maximal points and complete orders

Abstract: We present a generalisation of the familiar dependent choice principle from natural numbers to W-types, as a theorem of Martin-Löf type theory. It is then used to show predicative set-representability of

  1. the points of a formal topology, whose points are all maximal,
  2. the Dedekind cuts in dense unbounded linear orders.



Maintainer: Brandon Doherty, brandon.doherty@math.su.se