Forthcoming speakers at the seminar this Spring include: Douglas S. Bridges (Canterbury, N.Z.), Sam Sanders (Munich).
Wednesday, 13 March
10.00 - 11.45, room 16, building 5, Kräftriket, Stockholm
André Porto (Universidade Federal de Goiás, Brazil)
Rules, Equations and Infinity in Wittgenstein
Abstract: Our presentation will address Wittgenstein's construal of different kinds of mathematical statements, such as singular and general equations, with special attention to his handling of the notion of infinity. We will argue for a close proximity between his proposals and those of Category Theory. We will also pay close attention to the differences between his elucidations and the ones offered by contemporary Intuitionism.
Wednesday, 27 February
10.00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Erik Palmgren
The Grothendieck construction and models for dependent types
Wednesday, 13 February
9.00 - 11.00, room 16, building 5, Kräftriket, Stockholm
Per Martin-Löf
Invariance under Isomorphism and Definability (continued)
Wednesday, 6 February
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Per Martin-Löf
Invariance under Isomorphism and Definability (continued)
Wednesday, 30 January
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Per Martin-Löf
Invariance under Isomorphism and Definability
Wednesday, 23 January
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Christian Espíndola
On Glivenko theorems for intermediate predicate logics
Abstract: We will expose a simple proof-theoretic argument showing that Glivenko's theorem for propositional logic and its version for predicate logic follow as an easy consequence of the deduction theorem, from which we will show with the same elementary arguments some Glivenko-type theorems relating intermediate logics between intuitionistic and classical logic. We will consider two schemata, the double negation shift (DNS) and the one consisting of instances of the principle of excluded middle for sentences (REM). We will prove that both schematas combined derive classical logic, while each one of them provides a strictly weaker intermediate logic, and neither of them is derivable from the other. We will show that over every intermediate logic there exists a maximal intermediate logic for which Glivenko's theorem holds, and also deduce two characterizations of DNS, as the weaker (with respect to derivability) schema that added to REM derives classical logic and as the strongest (with respect to derivability) schema among the ¬¬-stable ones.
Wednesday, 12 December
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Håkon Robbestad Gylterud
The partiality monad and its algebras
Abstract: In this talk I will give a description of the partiallity monad, its
implementation in Martin-Löf type theory, and talk about my current
research into its properties.
The partiality monad is an attempt to give an abstract descriptions of
what a computation is, using categorical language. From any monad we can
construct its Kleisli category, and in the case of the partiallity monad
the Kleisli category models partial, computable functions.
I have begun an investigation into how this monad can be used to describe
some aspects of computability in Martin-Löf type theory. I will relate this
to other approaches to constructive computability theory (in particular
Richman's "Church's thesis without tears"), and talk about the algebras for
this monad and their connections to domain theory.
Wednesday, 5 December
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Allard M. Tamminga, Bayreuth and Groningen
Correspondence analysis for many-valued logics (joint work with Barteld Kooi)
Abstract:
Taking our inspiration from modal correspondence theory, we present the idea of correspondence analysis for many-valued logics. As a benchmark case, we study truth-functional extensions of the Logic of Paradox (LP). First, we characterize each of the possible truth table entries for unary and binary operators that could be added to LP by an inference scheme. Second, we define a class of natural deduction systems on the basis of these characterizing inference schemes and a natural deduction system for LP. Third, we show that each of the resulting natural deduction systems is sound and complete with respect to its particular semantics.
Wednesday, 28 November
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Peter Schuster, Pure Mathematics, University of Leeds
When Irreducibles are PrimeAbstract: Many an indirect proof with Zorn's Lemma has recently allowed for being turned upside down into a direct proof with Raoult's Open Induction; case studies pertain to commutative rings [1] and Banach algebras [2]. Under sufficiently concrete circumstances this may even yield a constructive proof without any form of the Axiom of Choice. To prepare the ground for a more systematic treatment we now classify the cases that can be found in mathematical practice by way of representative proof patterns. To start with we distill, and prove by Open Induction, a generalised form of the contrapositive of the Separation Lemma or Prime Ideal Theorem that is ascribed to Lindenbaum, Krull, Stone, and Tarski. Our version subsumes not only instances from diverse branches of abstract algebra but also a Henkin-style completeness proof for first-order logic. By recurrence to a theorem of McCoy, Fuchs, and Schmidt on irreducible ideals we further shed light on why prime ideals occur --- and why transfinite methods. (This is joint work in progress with D. Rinaldi, Munich, and is partially based on joint work with N. Gambino, Palermo, and F. Ciraulo, Padua.)
[1] P. Schuster, Induction in algebra: a first case study. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 2012, Dubrovnik, Croatia. IEEE Computer Society Publications (2012) 581-585
[2] M. Hendtlass, P. Schuster, A direct proof of Wiener's theorem. In: S.B. Cooper, A. Dawar, B. Loewe, eds., How the World Computes. Turing Centenary Conference and 8th Conference on Computability in Europe, CiE 2012, Cambridge, UK, June 2012, Proceedings. Springer, Berlin and Heidelberg. Lect. Notes Comput. Sci. 7318 (2012) 294-303
Wednesday, 21 November
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Tero Tulenheimo, University of Lille
Classical Negation and Game-Theoretical Semantics
Abstract:
Typical applications of Hintikka's game-theoretical semantics (GTS) give
rise to semantic attributes --- truth, falsity --- expressible in the
\Sigma^1_1 fragment of second-order logic. Actually a much more general
notion of semantic attribute is motivated by strategic considerations.
When identifying such a generalization, the notion of classical negation
plays a crucial role. We study two languages, L_1 and L_2, in both of
which two negation signs are available: \neg and \sim. The latter is the
usual GTS negation which transposes the players' roles, while the former
will be interpreted via the notion of {\it mode}. Logic L_1 extends IF
logic; \neg behaves as classical negation in L_1. Logic L_2 extends L_1
and it is shown to capture the \Sigma^2_1 fragment of third-order logic.
Consequently the classical negation remains inexpressible in L_2.
Thursday, 8 November
13:00 - 14.45, room 306, building 6, Kräftriket, Stockholm (Note: time and place)
Henrik Forssell, University of Oslo
Title: Simplicial databases
Abstract: We consider a database model based on (finite) simplicial complexes rather than relations. A brief introduction to the relational model is given for logicians not familiar with it. We thereafter describe how simplicial complexes can be used to model both database schemas and instances. This allows us to collect schemas and instances over them into one structure, which we relate to the notions of display map and comprehension category.
Wednesday, 7 November
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Benno van den Berg, Utrecht University
Title: Predicative toposes
Abstract: Topos theory is a very successful chapter in the categorical analysis of logic. Elementary toposes are categorical models of higher-order intuitionistic arithmetic and provide a framework for almost all interpretations of this theory, such as realizability, Kripke , topological and sheaf models. The notion of a topos is impredicative, however, and therefore its internal logic is much stronger than what most constructivists are willing to use in their work. Indeed, most constructivists want their work to be formalisable in weaker predicative systems like Martin-Lof's type theory and Peter Aczel's constructive set theory CZF. A predicative topos should be a topos-like structure whose internal logic has the same strength as these theories. I will explain what the difficulties are in coming up with a good notion of predicative topos, discuss two possible axiomatisations (very closely related), explain why I like these and then discuss their basic properties.
Wednesday, 26 September
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Erik Palmgren
Survey of notions of models for dependent type theories
Abstract: The notion of a model of Martin-Löf type theory, or more general dependent type theories, is fairly complicated
and exists in several versions. We give a survey of some of the most important ones.
Wednesday, 12 September
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Peter Dybjer (Chalmers)
Tests, games, and Martin-Löf's meaning explanations for intuitionistic type theory
Abstract: In this talk I shall argue that program testing provides the basis for constructive mathematical truth. This point of view leads to an alternative presentation of Martin-Löf's meaning explanations for intuitionistic type theory, where the judgements of type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. In particular, we get a new interpretation of hypothetical judgments, since tests for such judgments need methods for generating inputs. We sketch a "test manual" for intuitionistic type theory which employs concepts from game semantics, for example, input generation corresponds to opponent's moves in a game. In order to test a typing judgement we simultaneously play a strategy generated by a type and a strategy generated by a term, where the correct moves for the strategy of the term are determined dynamically by playing the strategy of the type.
The talk is on joint work in progress with Pierre Clairambault, Cambridge.
Wednesday, 30 May
10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm
Dag Westerståhl
Compositionality in context
Abstract: The standard notion of compositionality is well understood, and the formal framework of Hodges (2001) allows precise treatment of various features of compositionality. The issue in this talk is how context-dependence, i.e. cases where semantic values are assigned to syntactic expressions *in contexts*. Contexts here can be assignments, utterance situations (or features thereof s.a. speakers, times, locations, possible worlds,...), standards of precision, etc., or various aspects of linguistic context. Currying the context argument results in a function taking only expressions as arguments, and one question concerns the relation between compositionality of the curried function and that of the uncurried one. Another question is the relation between a compositional semantics and one given by a standard inductive truth definition. The background to these questions is linguistic, but in this talk I focus on the mathematical details.
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.
December 7, 2012, Erik Palmgren. Email: palmgren (at) math (dot) su (dot) se