Wednesday, 9 May
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Sam Sanders, Ghent University
Reuniting the antipodes: bringing together Constructive and Nonstandard Analysis
Abstract: In the Sixties, Errett Bishop introduced Constructive Analysis, a redevelopment of classical Mathematics based
on the fundamental notions of `algorithm' and `proof', inspired by the BHK (Brouwer-Heyting-Kolmogorov) interpretation.
Constructive Reverse Mathematics (CRM) is a spin-off from Harvey Friedman's famous `Reverse Mathematics' program,
based on Constructive Analysis.
Bishop famously derided Nonstandard Analysis for its lack of computational meaning. In this talk, we introduce `Ω-invariance':
a simple and elegant definition of `finite procedure' in (classical) Nonstandard Analysis. Using an intuitive interpretation, we
obtain many results from CRM, thus showing that Ω-invariance is quite close to Bishop's notion of algorithm. We suggest a
possible application of Ω-invariance to Per Martin-Löf's famous Type Theory, in light of its recent interpretation using homotopy.
Wednesday, 25 April
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Henrik Forssell, Oslo
Recovering theories from their models
Abstract: Given a theory T and its category of models and homomorphisms Mod(T), is it possible to recover T from Mod(T) (up to some suitable notion of equivalence)? A positive answer for regular theories was given by Makkai who showed that the classifying topos of a regular theory - from which the theory can be recovered - can be represented as filtered colimit preserving functors from Mod(T) to the category SET of sets and functions. Moving to coherent (and classical first-order theories), however, it becomes necessary to equip Mod(T) with some extra structure. While Makkai uses structure based on ultra-products for this case, it is possible to equip Mod(T) with a natural topology and represent the classifying topos of T as equivariant sheaves on the resulting topological category (or groupoid, considering just the isomorphisms). This forms the basis of an extension of Stone duality to first-order theories, and allows for the application of topos-theoretic techniques to e.g. give a topological characterization of the definable subclasses of Mod(T).
Wednesday, 18 April
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Juha Kontinen, Helsinki
Axiomatizing first-order consequences in dependence logic
Abstract: Dependence Logic, introduced by Jouko Väänänen in 2007, is a new logic incorporating the concept of dependence into first-order logic. The expressive power of dependence logic coincides with that of existential second-order logic In the past few years, dependence logic has grown into a new framework in which various notions of dependence and independence can be formalized. The high expressive power of dependence logic has a consequence that dependence logic in full generality cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized. We give an explicit axiomatization and prove the respective Completeness Theorem. This is joint work with Jouko Väänänen.
Wednesday, 21 March
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Hajime Ishihara (Japan Advanced Institute of Science and Technology)
Some Conservative Extension Results of Classical Logic over Intuitionistic Logic
Wednesday, 7 March
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Erik Palmgren
What is an internal setoid model of dependent type theory?
Abstract: Standard models of dependent type theory, such as categories with attributes, use semantics
based on the category of sets. It seems to be an unresolved question how to best formulate such
semantics using the category of setoids instead, and how to do this internally to type theory it self.
We discuss some proposals for solutions and possible generalizations to other categories of interpretation.
Wednesday, 29 February
10:00 - 11:45, room 16, building 5, Kräftriket, Stockholm.
Peter Schuster (Leeds)
A Proof Pattern in Algebra
Abstract: Many a concrete theorem of abstract algebra admits a short and elegant proof by contradiction but with Zorn's Lemma. A few of these theorems have recently turned out to follow in a direct and elementary way from Raoult's Principle of Open Induction, a little known equivalent of Zorn's Lemma. A proof of the latter kind typically follows a certain pattern, and may be extracted from a proof of the former sort. If the theorem has finite input data, then a finite order carries the required instance of induction, which thus is provable by fairly elementary means. Basic proof theory suffices to eliminate the decidability assumptions one may have to make en route. The tree one can grow alongside the induction encodes an algorithm which computes the desired output data. We will discuss all this along the lines of some typical examples.
Friday, 24 February
13:15 - 15:00, room 16, building 5, Kräftriket, Stockholm. (Note time and day!)
Mohammad Jabbari (SU)
Algebraic Theories and Algebraic Categories
Abstract: Algebra is a subject dealing with variables, operations and equations. This viewpoint - present in the Tarski-Birkhoff's tradition in universal algebra - was the scene before the birth of categorical logic in F. W. Lawvere's 1963 thesis. In his thesis, among other things, he objectified algebraic "theories" as special kind of categories and algebraic structures as special set-valued functors on them. He learned to do universal algebra by category theory! This was the start of a fruitful line of discoveries which culminated in the creation of (elementary) topos theory by Lawvere and M. Tierney in late 1970.
At about the same time, an alternative categorical approach to general algebra emerged out of the collective efforts of some homological algebraists (Godement, Huber, Eilenberg, Beck, ...) which centers around the notion of "monads (triples)". Among other intuitions, this machinery enables us to grasp the algebraic part of an arbitrary category. This approach later found applications in descent theory and computer science. The highpoint of this area is Beck's monadicity theorem.
This seminar is divided into three parts. At first we review some of Lawvere's ideas in algebraic theories and state his characterization theorem for algebraic categories. Then we shortly describe the monadic approach to algebra. Finally we state some theorems about the equivalences between these three approaches into algebraic categories.
Main References.
[1] Lawvere, F. W., "Functorial semantics of algebraic theories", PhD Thesis, Columbia, 1963.
[2] Adamek, J., et al., "Algebraic Theories - A Categorical Introduction to General Algebra", Cambridge University Press, 2011.
Wednesday, 15 February
10:00-11:45, room 16, building 5, Kräftriket, Stockholm
Martin Blomgren (KTH)
Essentially small categories
Abstract. To each small category it is possible to associate a homotopy type. This is done through the nerve functor; via this functor it is thus possible to transport homotopy notions from simplicial sets (or topological spaces) to the category of small categories.
In this talk we introduce the notion of essentially small categories;
such a category, albeit "big", allows for a nerve construction -- an essentially small category has a small subcategory that serves as a
good homotopy approximation for its ambient category; we give several
concrete examples of "big" but essentially small categories and their homotopy types. We also explain how to do categorical homotopy theory
on "big" categories in general.
Wednesday, 8 February
10:00-11:45, room 16, building 5, Kräftriket, Stockholm
Christian Espíndola (SU)
Categorical methods in model theory
Abstract. In this talk we will discuss applications of methods in
categorical logic to model theory, which was the theme of my undergraduate
thesis. In the first part we will expose Joyal's categorical proof of
Gödel's completeness theorem for first order classical logic, which is
based on a series of unpublished lectures in Montréal in 1978. The proof
makes use of functorial semantics, as introduced by Lawvere, to translate
into categorical language the existing proof of completeness. In the second
part we will make use of Joyal's constructions and explain how they can be
adapted to give categorical proofs of Löwenheim-Skolem theorem and of the
criterion known as Vaught's test, which gives sufficient conditions for a
first order theory to be complete. We will also comment on the constructive
aspects of the categorical proofs, as well as to what extent they can
dispense with choice principles.
Wednesday, 1 February
10:00-11:45, room 16, building 5, Kräftriket, Stockholm
Dag Prawitz
Gentzen's 2nd consistency proof
and normalization of natural deductions in 1st order arithmetic
Wednesday, 25 January
10:00-11:45, room 16, building 5, Kräftriket, Stockholm
Håkon Robbestad Gylterud (SU)
Symmetric Containers
Abstract. This talk is based on my Master Thesis. I will give a brief introduction to the notion of a container and how to differentiate them, as defined in [1] and [2]. This yields combinatorial information from the process of differentiation (a la combinatorial species). Then I show how a more general notion, called symmetric containers, contains anti-derivatives of many containers.
References
[1] Michael Abbott, Thorsten Altenkirch and Neil Ghani (2005). Containers: constructing strictly positive types, Theoretical Computer Science 342(1), 3 - 27.
[2] Michael Abbott, Thorsten Altenkirch, Neil Ghani and
Conor Mcbride (2008), ¶ for data: Differentiating data structures.
Wednesday, 18 January
10:00-11:45, room 16, building 5, Kräftriket, Stockholm
Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand
Approaching topology constructively via apartness
Abstract: In 2000, Luminita Vita and I began investigating axioms for a constructive theory of apartness between points and sets, and between sets and sets, as a possible constructive approach to topology. The culmination of this work came last October, with the publication of the monograph [3], in which we lay down what we believe to be the defnitive axioms for (pre-)apartness and then develop the theory, with particular application to (quasi-)uniform spaces. Our development uses points, and is therefore in the style and spirit of Bishop's original constructive approach to analysis [1, 2]. As with analysis, so with topology: once the "right" axioms are used, the theory allows in a natural, if technically nontrivial, way (with one exception). In this talk I shall present the axioms for apartness and uniform spaces, and discuss various aspects of the resulting theory, paying particular attention to the connections between various types of continuity of functions.
References
[1] E. Bishop, Foundations of Constructive Analysis, McGraw-Hill, New York 1967.
[2] E. Bishop and D.S. Bridges, Constructive Analysis, Grundlehren der Math. Wissenschaften 279, Springer Verlag, Heidelberg, 1985.
[3] D.S. Bridges and L. Vita, Apartness and Uniformity: A Constructive
Development, in: CiE series "Theory and Applications of Computability",
Springer Verlag, Heidelberg, 2011.
Minisymposium on categorification and foundations of mathematics and quantum theory
Room 16, building 5, Kräftriket, Stockholm.
9:15- 10:05: Bas Spitters (Radboud University, Nijmegen)
Bohrification: Topos theory and quantum theory
Abstract. Bohrification associates to a (unital) C*-algebra
10:15 - 11:05: Thierry Coquand (Göteborg)
About the Kan simplicial set model of type theory
11:15 - 12:05: Volodymyr Mazorchuk (Uppsala)
2-categories, 2-representations and applications
Abstract. In this talk I plan to explain what a 2-category is, how 2-categories appear in algebra and topology, how one can study them, in particular, how one constructs 2-representations of 2-categories, and, finally, how all this can be applied.
13:30 - 14:20: Erik Palmgren (Stockholm)
Proof-relevance of families of setoids and identity in type theory
Abstract. Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result is shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed.
14:30 - 15:20: Nils Anders Danielsson (Göteborg)
Bag equality via a proof-relevant membership relation.
Abstract. Two lists are "bag equal" if they are permutations of each other, i.e. if they contain the same elements, with the same multiplicity, but perhaps not in the same order. I will describe how one can define bag equality as the presence of bijections between sets of membership proofs. This definition has some nice properties:
Wednesday 23 November
10.00-12.00, in room 16, building 5, KrŠftriket.
Dag Westerståhl
Logical constants and logical consequence
Abstract: I will first briefly overview the problem of logical constants (what is it
that makes a symbol logical?) and some approaches to it, in particular the
invariance approach originating with Tarski. Then I present some recent joint work
with Denis Bonnay on a new approach: Given an interpreted language and
a set of logical constants, Tarski's semantic definition of logical
consequence
yields a consequence relation. But given a consequence relation, is there a
natural way to extract from it a set of logical constants? I compare two
ways
of doing so, one purely syntactical, based on the idea that an expression is
logical if it is essential to the validity of at least one inference, and
one
semantical, based on the idea that an expression is logical if its
interpretation
is fully determined by the rules for its use. To describe these methods,
Galois
connections between consequence relations, sets of symbols, and sets of
interpretations (all ordered under inclusion) play an important role.
Wednesday, 12 and 19 October
10:15-12:00, room 16, building 5, Kräftriket, Stockholm
Erik Palmgren
Voevodsky's foundations - type-theoretic background and the univalence axiom
Abstract: This talk is the second in a series around Voevodsky's proposal for a novel foundations of mathematics based on notions from homotopy theory. We shall here present some background in Martin-Löf type theory, in particular pertaining to the identity types which are central to the approach, giving the notion of path. Furthermore the Univalence Axiom and its consequences are discussed. If time permits we also start presenting Voevodsky's standard model of type theory extended with this axiom.
Wednesday, 28 September
10:15-12:00, room 16, building 5, Kräftriket, Stockholm
Torsten Ekedahl
Voevodsky's foundations - homotopy and categorical background
Abstract: I will give some background in homotopy and category theory that should aid in understanding Voevodsky's proposed approach to the foundations of type theory. This includes how groupoids and n-groupoids appear naturally as a framework for equality when one wants to retain as much information as possible but also how homotopy and in particular homotopy coherence comes into the picture.
January 25, 2012, Erik Palmgren. Email: palmgren (at) math (dot) su (dot) se