Seminarieledare: Per Martin-Löf (Stockholm), Erik Palmgren, Viggo Stoltenberg-Hansen (Uppsala)
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
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?
Onsdag 7 maj, kl 10.30-12.15 (Obs! Tid och lokal) Sal 2144, MIC, Polacksbacken, Uppsala
Erik Palmgren
Predikativa kategorier och intern logik
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).
Onsdagen den 9 april kl. 10.00-11.45 i sal 16, hus 5, Kräftriket.
Jens Brage
A classical tableau calculus
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.
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.
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.
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
Matematiska institutionens seminarierum 3513 (plan 5, hus 3) MIC, Polacksbacken, Uppsala.
Erik Palmgren
Constructive completions of ordered sets, groups and fields II
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.
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.
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$.
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.
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
Onsdagen den 20 november kl. 13.15 i sal 2:245, Mic, Polacksbacken, Uppsala
Jonas Eliasson
Ultrasheaves and double negation (cont.)
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 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.
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)
Onsdagen den 16 oktober kl. 10.30 i sal 2:315, MIC, Polacksbacken,Uppsala
Thierry Coquand
A calculus of dependently typed records
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.
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 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 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 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
Maintainer: Brandon Doherty, brandon.doherty@math.su.se