The Stockholm Logic Seminar

Organisers: Erik Palmgren (chair), Peter LeFanu Lumsdaine, Per Martin-Löf (emeritus)

The regular seminar time is Wednesdays 10.00-11.45, and the usual location is room 16, building 5, Kräftriket (Roslagsvägen 101), Stockholm.

Spring 2016


May 4
10:00 - 11:45
TBA

TBA



March 23
10:00 - 11:45
Martín Escardó

TBA


March 16

No seminar this week due to the 27th Nordic Congress of Mathematician, March 16-20, Frescati.

March 9
10.00-11.45
Håkon Robbestad Gylterud

Strong collection, subset collection and the identity type

Abstract: Strong collection and subset collection are two axioms of constructive set theory. They are distinct from other set theoretical axioms in that they claim existence of certain sets, but do not characterise these sets precisely. Their constructive justification is closely tied to AczelÕs model of constructive set theory in type theory, and the notion of operation versus the notion of function. I will in this talk discuss these axioms in the context of a model where the interpretation of equality is the identity type. As it turns out, it is instructive to first consider the equivalents of these axioms for multisets.


February 24
10:00 - 11:45
Erik Palmgren

Categories with Families and FOLDS: functorial semantics vs standard semantics

Abstract: Every dependent first-order signature Sigma generates a free category with families F(Sigma). A model C of the Sigma-signature is a cwf morphism M from F(Sigma) to C. Such a morphism is uniquely determined by its values on the signature. We show that such morphisms can constructed by incrementally by induction on the signature. This shows that this functorial notion of model extends the usual non-dependent version of model of first-order signature.


February 17
10:00 - 11:45
Roussanka Loukanova

Gamma-Reduction in Type Theory of Acyclic Recursion

Abstract: I will introduce Moschovakis Type Theory of Acyclic Recursion (TTAR) by extending its reduction system. The extended TTAR has potentials for more efficient computational semantics of formal and natural languages. At first, I will present the original reduction calculus of TTAR, which reduces TTAR-terms to their canonical forms. The canonical forms of the terms determine the algorithms that compute their semantic denotations, and, in addition, the relation of algorithmically referential synonymy between TTAR-terms. The lambda-rule, which is the most important rule of the reduction calculus of TTAR, strictly preserves the algorithmic structure of the reduced terms. However, in its original, general formulation, the lambda-rule may result in superfluous lambda abstractions in some parts of the terms. In the second part of the talk, I introduce the gamma-rule, which extends the reduction calculus of TTAR and its referential synonymy to gamma-reduction calculus and gamma-synonymy, respectively. The gamma-rule is useful for simplifying terms. It reduces superfluous lambda-abstraction and corresponding functional applications in the terms, while retaining the major algorithmic structure of the terms.

February 3
10:00 - 11:45
Johan van Benthem, Universiteit van Amsterdam

Dynamic-Epistemic Logic, Information and Tracking

Abstract: We review basics of dynamic-epistemic logics for agent attitudes of knowledge and belief, plus stepwise effects of events leading to information and belief change. Then, we introduce more fine-grained neighborhood models for 'evidence', and their richer set of attitudes and dynamic events. Next, we study how dynamics at one 'zoom level' can, or cannot, track the dynamics at another level, using natural inter-level maps. Finally, we discuss a total logical picture of how information functions.

References:

J. van Benthem, 2011, Logical Dynamics of Information and Interaction, Cambridge University Press, Cambridge UK.

--, 2015, 'Tracking Information', in K. Bimbó, ed., Mike Dunn on Logic and Information, Outstanding Contributions to Logic, Springer, Dordrecht.

January 20
10:00 - 11:45
Per Martin-Löf

The two interpretations of natural deduction: how do they fit together?


Fall 2015


December 9
10:00 - 11:45
Michael Makkai, McGill

FOLDS equivalences as the basis of a general theory of identity for concepts in higher dimensional categories, part 2


December 2
10:00 - 11:45
Michael Makkai, McGill

FOLDS equivalences as the basis of a general theory of identity for concepts in higher dimensional categories, part 1.

Abstract (for part 1 and 2): 1. The theory of abstract sets is based on a formal language that is given within FOLDS, first-order logic with dependent sorts. Abstract set theory was introduced in an informal manner by F. W. Lawvere in Section 2 of his 1976 paper ÒVariable quantities and variable structures in topoiÓ. Lawvere used his informal, but very informative description of abstract set theory for the purposes of topos theory. In 2003, and then in a more detailed manner in 2013, I introduced the formalization I will talk about here. It is more directly set-theoretical than topos theory, which is based on the language of categories. The structuralist imperative, stated by Bourbaki as an explicit requirement on any concept of structure, a special case of which is that Òan abstract set has no external properties save its cardinalityÓ (Lawvere), appears, necessarily in the absence of a formal language, as a desideratum in Lawvere's exposition. The main result of my work is that in the new formalization, the structuralist imperative becomes a provable general fact, in the form that any concept formulated in the dependent-typed language of abstract sets is invariant under isomorphism.

I will use the opportunity of abstract sets to introduce, albeit only in an informal way, the general syntax of FOLDS.

2. I introduced FOLDS in 1995 in the monograph ÒFirst Order Logic with Dependent Sorts with Applications to Category TheoryÓ (available on my web-site both in its originally typed and also in a TEXed version). In the paper ÒTowards a Categorical Foundation of MathematicsÓ, published in 1998, but written at the same time as the monograph in 1995, I gave a descriptive outline of the theory. The syntax is explained both symbolic-logically, and by using tools of categorical logic. The main reason why I came out with FOLDS is that I found that there is a notion generalizing isomorphism Ð called FOLDS equivalence -- for structures for a FOLDS language such that:1) many (all?) notions of equivalence used in higher- dimensional categories coincide with appropriate instances of the FOLDS equivalence, and 2) first-order properties of structures in general are invariant under FOLDS equivalence if and only if they are equivalently formulatable in the FOLDS syntax. My main application of FOLDS is a statement of the universe of the so-called multitopic categories; see The Multitopic Category of All Multitopic Categories on my web-site, in both the 1999 and the corrected 2004 versions. In the talk, I will necessarily be rather informal about the subject, with suggestive examples rather than precise general definitions.


November 25
10:00 - 11:45
Dag Westerståhl

The meaning of ▢ and other logical constants

Abstract: We study the extent to which logical consequence relations in a language L determine the meaning of the logical constants of L. For example: Do the laws of classical logical consequence in first-order logic fix the meaning of ∀? Carnap asked this question in 1943 about the connectives in classical propositional logic (and implicitly answered it). In [1], we extended this result to first-order logic, and to the framework of possible worlds semantics. In this talk, which is about work in progress, I consider the same question for some intensional logics. First, there are two simple observations on the interpretation of the connectives in intuitionistic propositional logic, in the setting of Kripke semantics. Then I focus on modal logic. Roughly, what range of interpretations of ▢ do various (normal) modal logics allow? Some results and some open issues will be presented. This is joint work with Denis Bonnay.

[1] D. Bonnay and D. Westerståhl, `Compositionality solves Carnap's Problem', Erkenntnis 80 (4), 2015 (online first).

November 18
10:00 - 11:45
Andrew Swan, Leeds

Identity types in Algebraic Model Structures

Abstract: The original Bezem-Coquand-Huber cubical set model promised to give a constructive model of homotopy type theory. However, in its original form there was a notable shortcoming: one of the definitional equalities usually included in type theory, the J computation rule was absent. One way to fix this is to use an alternative definition of identity type in which we keep track more carefully of degenerate paths. The new identity type has a nice presentation in the setting of algebraic model structures. To model identity types what we need is very good path objects: a factorisation of each diagonal as a trivial cofibration followed by a fibration. I'll show a general way to create very good path objects from path objects in the weaker sense of factorisations of diagonals as weak equivalence followed by fibration, and that under certain reasonable conditions on an ams this can be carried out "stably and functorially" allowing us to satisfy the Garner-van den Berg notion of "stable functorial choice of diagonal factorisation." I'll use these ideas to show that in particular cubical sets with Kan fibrations satisfy Garner and van den Berg's notion of homotopy theoretic model of identity types. In this way we get a constructive proof that cubical sets model intensional type theory including all definitional equalities, dealing with coherence issues directly without using universes or local universes and retaining any propositions from the original BCH model, including univalence.


October 28
10:00 - 11:45
Eric Finster, Eric Finster, EPFL Lausanne

Towards an Opetopic Type Theory

Abstract: The realization that dependent type theory has a higher categorical interpretation where types are coherent higher groupoids has been a major development in the field. However, while internally types exhibit coherent structure provided by their identity types, type theory itself still lacks any mechanism for describing more general coherent objects. In particular, it has no means of describing higher equivalence relations (i.e. internal higher groupoid objects) or coherent diagrams of types (functors into the universe). Much work has focused on the search for reasonable internal notion of simplicial types to remedy this problem, but to date no simple solution has been found. In this talk, motivated by recent progress in formalizing the Baez-Dolan opetopic definition of higher categories in type theory, I will present an alternative approach to coherence based on opetopes. The theory of opetopes is based on the theory of polynomial functors, also known as as W-types or containers in the type theory literature, and thus fits naturally with concepts already familiar from logic and computer science. I will sketch a type theory extended with syntax for manipulating opetopic expressions a explain how this leads to a quite general logical theory of coherence.


October 14
10:00 - 11:45
Peter LeFanu Lumsdaine

Equivalences of (models of) type theories, continued

Abstract: Continuing from last week's seminar, I will go into the details of the logical structure in the models in spans and span-equivalences. I will also lay out some more abstract nonsense about categories of contextual categories, and use this to give applications of the span-equivalences model to the "homotopy theory of homotopy type theory".

October 7
10:00 - 11:45
Peter LeFanu Lumsdaine

Equivalences of (models of) type theories

Abstract: (joint work with Chris Kapulkin) I will present a new model of type theory in "span-equivalences" over a given model, based on the model in spans or basic pairs (as given by Simone Tonelli and by Mike Shulman). This "span-equivalences" model provides a useful technical tool for reasoning about equivalence between models of type theories. I will describe (at least) two applications: firstly, that once the interpretation of contexts, types, and terms has been fixed, the interpretation of the rest of type theory is determined up to equivalence; and secondly, a presentation of the "homotopy theory of models of type theory". This is work in progress, and suggestions of further applications are very welcome!

September 16
10:00 - 11:45 in room 22, building 5, Kräftriket, Stockholm. (Note unusual location!)

Valentin Goranko

Logics for visual-epistemic reasoning in multi-agent systems

Abstract. In this talk I will present a logical framework for multi-agent visual-epistemic reasoning, where each agent receives visual information from the environment via mobile camera with a given angle of vision in the plane. The agents can thus observe their surroundings and each other and can reason about each other's observation abilities and knowledge derived from these observations. I will introduce suitable logical languages for formalising such reasoning, involving atomic formulae stating what agents can see, multi-agent epistemic operators, as well as dynamic operators reflecting the ability of agents (or, their cameras) to move and turn around. I will then introduce several different types of models for these languages and will discuss their expressiveness and some essential validities. Lastly, I will discuss some basic model-theoretic problems arising in this framework that open up new directions of study, relating logic, geometry and graph theory.

This talk is partly based on a recent joint work with Olivier Gasquet (Univ. Paul Sabatier, IRIT, Toulouse) and Francois Schwarzentruber (ENS Rennes).


September 9
10:00 - 11:45
Raazesh Sainudiin, University of Canterbury, Christchurch, N.Z.

An Interval Tree Arithmetic for Computationally Amenable Operations with Maps in Some Metric Spaces

Abstract: I will spend the first part of the talk on an introduction to interval analysis (for general maths audience). In the second part of the talk I will introduce an arithmetic with planar binary trees that are used to represent maps and show how this is used to solve some concrete real-world problems, including nonparametric density estimation, dynamic air-traffic representation, tighter range enclosures of interval-valued functions that can be expressed via finitely many real arithmetic operations, and simulation from challenging densities in up to 10 dimensions.

References:

http://tinyurl.com/oxrgse4

http://tinyurl.com/pakpny9

http://dx.doi.org/10.1145/2414416.2414422

http://arc.aiaa.org/doi/abs/10.2514/1.I010015


September 2
10.00-11.45

Erik Palmgren

Progress report on formalizing categories with attributes in type theory, part 2

Abstract: This talk is a follow up of the talks by Peter Lumsdaine and myself respectively, last term on this subject. A complete formalization in Coq of bounded categories with attributes and structures for type theory with one universe, has since then been achieved. We indicate how a setoid model of type theory is constructed via the use of a formalized model of CZF.


August 26
10.00-11.45

Per Martin-Löf

Spreads, repetitive structures, and functional causal models


Monday, July 6

Makoto Fujiwara, JAIST

Constructive provability versus uniform provability in classical computable mathematics

Abstract: So-called elementary analysis EL is two-sorted intuitionistic arithmetic, which serves as system to formalize constructive mathematics. In this talk, we show that for any Pi^1_2 formula T of some syntactical form, T is provable in EL if and only of T is uniformly provable in classical variant RCA of EL. It is remarkable that all of our proofs are constructive, namely, they are just explicit syntactic translations. Since a large number of existence theorems are formalized as Pi^1_2 formula T of the form, under the agreement that constructive provability is identical with provability in EL, it suggests the constructive equivalence (from a meta-perspective) between constructive provability and classical uniform provability in RCA for practical existence theorems.


Friday, July 3
15:00 - 16:00, in room 306, building 6, Kräftriket,

Ulrik Buchholtz, Carnegie-Mellon University

Weak dependent type theories

Abstract: I'll discuss ongoing work on formulating proof-theoretically weak dependent type theories (of strength polytime and primitive recursive) that permit some higher type and large eliminations. Motivations include constructive reverse mathematics and eventually also a weak homotopy type theory.

Spring 2015


June 3
10.00-11.45

Erik Palmgren

Progress report on formalizing categories with attributes in type theory

Abstract: This talk is a complement to the talk by Peter LeFanu Lumsdaine earlier this term on a joint project with him and Håkon Gylterud.



May 27
10.00-11.45

Chris Kapulkin, University of Western Ontario

Type theory and locally cartesian closed quasicategories

Abstract: Let T be a dependent type theory admitting the rules for Pi-, Sigma-, and Id- types, and let C(T) be its syntactic category, that is, the category whose objects are contexts and whose morphisms are (sequences of) terms. This category is naturally equipped with a class of syntactically defined weak equivalences and as such presents some quasicategory. It is then natural to ask what can we say about this quasicategory. After explaining the necessary background, I will show a proof that the quasicategories arising this way are locally cartesian closed. This answers the question posed by Andre Joyal in his talk at the Oberwolfach mini-workshop on HoTT in 2011.



May 20
10.00-11.45

Christian Espíndola

Completeness of infinitary intuitionistic logics

Abstract: In this talk I will present the second half of my thesis, which relies on classical assumptions and is meant to be a counterpart for the constructive content of the first half. We will define formal systems for infinitary intuitionistic logics and prove completeness theorems in terms of a natural infinitary Kripke semantics, both in the propositional case and the first-order case. The metatheory will be ZFC plus the existence of weakly compact cardinals, a large cardinal assumption that will also be proved to be necessary for the completeness results to hold. We will also review some applications and consequences of these results.


May 6
10.00-11.45

Peter LeFanu Lumsdaine

Martin Hofmann's conservativity theorems

Abstract: Two notable conservativity results in dependent type theory are due to Martin Hofmann: the conservativity of the logical framework presentation of a type theory, and the conservativity of extensional type theory over intensional type theory with extensionality axioms.

I will discuss these two theorems, and the general status of conservativity results in dependent type theory.

This will be an entirely expository talk.


April 29
10.00-11.45

Steve Awodey, Carnegie Mellon University

Cubical Homotopy Type Theory

Abstract: In this work-in-progress talk, I will analyse the cubical model of homotopy type theory of Coquand et al. in functorial terms, making a few modifications along the way. The basic category of cubical sets used is presheaves on the free cartesian category on a bipointed object, i.e. the Lawvere theory of bipointed objects. The presheaf category is the classifying topos for strictly bipointed objects.

The Kan extension property familiar from algebraic topology is shown to be exactly what is required to model the Identity-elimination rule of Martin-Löf, and the closure of Kan objects under function spaces is ensured constructively by Coquand's uniformity condition, re-analysed as the existence of a certain natural transformation making natural choices of Kan fillers. A universe of Kan objects is given in the style of the recent Ònatural modelsÓ construction, based on ideas of Lumsdaine-Warren and Voevodsky.


April 22
10.00-11.45

Peter Aczel, Manchester University

On the Consistency Problem for Quine's New Foundations, NF

Abstract: In 1937 Quine introduced an interesting, rather unusual, set theory called New Foundations - NF for short. Since then the consistency of NF has been an open problem. And the problem remains open today. But there has been considerable progress in our understanding of the problem. In particular NF was shown, by Specker in 1962, to be equiconsistent with a certain theory, TST^+ of simple types. Moreover Randall Holmes, who has been a long-term investigator of the problem, claims to have solved the problem by showing that TST^+ is indeed consistent. But the working manuscripts available on his web page that describe his possible proofs are not easy to understand - at least not by me.

In my talk I will introduce TST^+ and its possible models and discuss some of the interesting ideas, that I have understood, that Holmes uses in one of his possible proofs.


April 15
10.00-11.45

Maarten McKubre-Jordens, University of Canterbury, NZ

Mathematics in Contradiction

Abstract: Advances in paraconsistent logics have begun attracting the attention of the mathematics community. Motivations for the development of these logics are wide-ranging: expressiveness of language; a more principled approach to implication; robustness of formal theories in the face of (local) contradiction; founding naive intuitions; and more. In this accessible survey talk, we outline what paraconsistency is, why one might use it to do mathematics, discuss some of the triumphs of and challenges to doing mathematics paraconsistently, and present some recent results in both foundations and applications. Applying such logics within mathematics gives insight into the nature of proof, teases apart some subtleties that are not often recognized, and gives new responses to old problems. It will turn out that despite the relative weakness of these logics, long chains of mathematical reasoning can be carried out. Moreover, in handling contradictions more carefully, paraconsistent proofs often bring out subtle differences between proofs that are often overlooked - not all proofs are created equal, even when truth (or falsity!) is preserved.


March 11
10.00-11.45

Henrik Forssell

Constructive completeness (continued)

Abstract: We give an analysis of some long-established constructive completeness results in terms of categorical logic and pre-sheaf and sheaf semantics, and add some new results in this area which flow from the analysis. Several completeness theorems are derived without the assumption that equality of non-logical symbols in the language can be decided. This is joint work with Christian Espíndola. The talk summarizes and continues some of the previous presentations by Espíndola and Forssell on the subject.

February 25
10.00-11.45

Peter LeFanu Lumsdaine

Progress report: formalising semantics of type theory in type theory.


February 4
10.00-11.45

Per Martin-Löf

Invariance of causal space-time (cont.).


January 28
10.00-11.45

Per Martin-Löf

Invariance of causal space-time


January 21
10.00-11.45

Benno van den Berg, ILLC, Amsterdam

Recent results around a nonstandard functional interpretation

Abstract: In recent work with Eyvind Briseid and Pavol Safarik we defined functional interpretations for systems for nonstandard arithmetic. We used these interpretations to prove conservation and term extraction results. In the talk I will explain the nonstandard functional interpretation could have been found without aiming for a proof-theoretic analysis of nonstandard systems, but rather by modifying certain ideas for refined term extraction. I will also discuss recent developments.


January 14
10.00-11.45

Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand

Morse Set Theory as a Foundation for Constructive Mathematics

Abstract: In the northern autumn of 1972, I came across A.P. Morse's little book `A Theory of Sets', and became absorbed by the idea of carrying through a constructive development of set theory (CMST) along the same lines, in which everything was expressed in a kind of pseudocode governed by strict rules of language and notation. Such a development would seem to be particularly suitable for proof-checking and for the extraction of programs from proofs. Chapter 1 of my D.Phil. thesis (Oxford, 1974) contained the fruits of my labours to that stage. After that, despite a brief foray into CMST for a conference paper in 1986, my plan to develop the set theory in greater depth was shelved until taken up again late last year.

In this talk I sketch some of the salient features of this updated development of CMST, paying particular attention to where it deviates from Morse's classical theory and to those results of the latter that are essentially nonconstructive


Fall 2014


December 17
10.00-11.45

Christian Espíndola

Beth models for intuitionistic logic

Abstract: The semantics of possible worlds for intuitionistic logic gives rise to Kripke models and its variant, Beth models. Although both semantics can be shown to be complete, we will see that the later has advantages over the former in the sense that with a weaker metatheory, they describe a wider variety of categorical models. In particular, we will discuss how to build, for every model in a Grothendieck topos, an elementarily equivalent Beth model, as well as the constructive aspects and applications of this.


10 December
10.00-11.45

Erkki Luuk

A type-theoretical approach to Universal Grammar

Abstract: The idea of Universal Grammar as the hypothetical linguistic structure shared by all human languages harkens back at least to the 13th century. The best known modern elaborations of the idea are due to Chomsky (e.g. 1970, 1981, 1995). Following a devastating critique from theoretical (e.g. Jackendoff 2002), typological (e.g. Evans & Levinson 2009) and field (e.g. Everett 2005) linguistics, these elaborations, the idea of Universal Grammar itself and the more general idea of language universals stand untenable and are largely abandoned. The talk will show how to tackle the hypothetical structure of Universal Grammar using dependent type theory in a framework very different from the Chomskyan ones.


3 December
10.00-11.45

Peter LeFanu Lumsdaine

The coherence problem for dependent type theory

Abstract: Coherence constructions are a vexing technical hurdle which most models of dependent type theory, especially homotopical ones, have to tackle in some way. I will explain what the basic problem of coherence is, and survey the main known approaches to overcoming it, including the constructions of Hofmann,Voevodsky/Hofmann - Streicher, Lumsdaine - Warren, and Curien - Garner - Hofmann.


26 November
10.00-11.45

Antti Kuusisto, Stockholm University

Uniform one-dimensional fragment of first-order logic

Abstract: In this talk we first briefly survey recent research on complexity and expressivity of weak fragments of first-order logic. Such fragments include, e.g., guarded fragments and two-variable systems. We then discuss the recently introduced uniform one-dimensional fragment (UF1), which generalizes the standard two-variable fragment in a way that leads to the possibility of defining non-trivial properties of relations of arbitrary arities. The increased expressivity does not lead to an increase in complexity: we show that UF1 is NEXPTIME-complete. The work presented is joint work with Emanuel Kieronski and Lauri Hella.


5 November
10.00-11.45

Peter Dybjer, Chalmers/Gothenburg University

Game semantics and normalization by evaluation

Abstract: We show that Hyland and Ong's game semantics for PCF can be presented using normalization by evaluation (nbe). We use the bijective correspondence between innocent well-bracketed strategies and PCF Böhm trees, and show how operations on PCF Böhm trees, such as composition, can be computed lazily and simply by nbe. The usual equations characteristic of games follow from the nbe construction without reference to the game-theoretic machinery. As an illustration, we give a Haskell program computing the application of innocent strategies.

This is joint work with Pierre Clairambault, CNRS and ENS Lyon.


22 October
10.00-11.45

Valentin Goranko, Stockholm University

On the theories of almost sure validities in the finite in some fragments of monadic second-order logic

Abstract: This work stems from the well-known 0-1 law for the asymptotic probabilities of first-order definable properties of finite graphs (in general, relational structures). Fagin's proof of this result is based on a transfer between almost sure properties in finite graphs and true properties of the countable random graph (aka, Rado graph). Both the transfer theorem and the 0-1 law hold in some non-trivial extensions of first-order logic (e.g., with fixed point operators) but fail in others, notably in most natural fragments of monadic second-order (MSO). The main problem of this study is to characterise, axiomatically or model-theoretically, the set of almost surely valid in the finite formulae of MSO, i.e. those with asymptotic probability 1. The set of almost sure validities in the finite of any given logical language (where truth on finite structures is well-defined) is a well-defined logical theory, containing all logical validities of that language and closed under all sound finitary rules of inference. Beyond that, little is known about these theories in cases where the transfer theorem fails. The talk will begin with a brief introduction to asymptotic probabilities and almost surely true properties of finite graphs, the 0-1 laws for first-order logic and in some extensions of it, and their relationship with the respective logical theories of infinite random graphs. Then I will focus on the almost sure theories in modal logic and in the Sigma^1_1 and Pi^1_1 fragments of MSO on binary relational structures, aiming at obtaining explicit logical characterisations of these theories. I will present such partial characterisations in terms of characteristic formulae stating almost sure existence ( Sigma^1_1) or non-existence (for Pi^1_1) of bounded morphisms to special target finite graphs. Identifying explicitly the set of target finite graphs that generate almost surely valid characteristic formulae seems a quite challenging problem, to which we so far only provide some partial answers and conjectures.


21 October
Extra type theory seminar
10.00-11.45

Ali Assaf, INRIA and École Polytechnique, Paris

Embedding logics in the lambda-Pi calculus modulo rewriting

Abstract: The lambda-Pi calculus modulo is an extension of the lambda-Pi calculus with rewrite rules. Using the Curry-Howard correspondence, it can be used as a logical framework to define logics and express proofs in those logics in a way that preserves the reduction semantics. I will show how we embed various theories such as the calculus of constructions and simple type theory in the lambda-Pi calculus modulo rewriting and consider the soundness and completeness of these embeddings.


15 October
SMC Colloquium, 15.15-16.15, Oskar Klein lecture hall, AlbaNova

Michael Rathjen, Leeds

Is Cantor's continuum problem still open?

Abstract: The continuum hypothesis, CH, asserts that an infinite set of reals is either countable or of the same size as the entire continuum (so nothing exists in between). Cantor couldn't determine the truth or falsity of CH. The quest for its status became enshrined in Hilbert's famous 1900 list, earning it a first place. Hilbert announced a proof of CH in his 1925 talk "On the Infinite" which arguably inspired Gödel to find a model of set theory that validates CH. With the work of Cohen in the 1960s, many people were convinced that CH was now a settled problem as all essential facts about it were deeply understood. This situation, however, did not convince everybody (e.g. Gödel). The last 20 years or so have seen a resurgence of the problem in modern set theory, in particular in the work of Woodin. In the first part of the talk, I plan to survey the most important known facts about CH. This will be followed by relating some of the modern attempts at finding new axioms to settle CH. Their justifications are partly based on technical results but also tend to be highly speculative and often come enmeshed with essentially philosophical arguments. Finally I shall consider a specific proposal by Solomon Feferman to clarify the nature of CH. He has advocated an account of the set-theoretic universe which allows him to distinguish between definite and indefinite mathematical problems. His way of formally regimenting this informal distinction is by employing intuitionistic logic for domains for which one is a potentialist and reserving classical logic for domains for which one is an actualist. This framework allowed him to state a precise conjecture about CH, which has now been proved. I plan to indicate a rough sketch of the proof.


1 October
10.00-11.45

Jacopo Emmenegger

A weak factorization system between type theory and homotopy theory

Abstract: Gambino and Garner have proved that the rules of the identity type in Martin-Löf type theory imply the existence of a weak factorization system in the syntactic category, known as the identity type w.f.s. We present a generalization of this result to a category satisfying four axioms reminiscent of the rules of Martin-Löf type theory, and show that it applies also to the category of small groupoids and to that one of topological spaces, giving back the weak factorization systems generated by Grothendieck fibrations and by Hurewicz fibrations, respectively. The categorical setting also highlights a close connection between Paulin-Mohring rules for the identity type and the identity type w.f.s. Some familiarity with dependent type theory and basic homotopy theory will be assumed.

24 September
10.00-11.45

Jiri Rosicky, Brno

Towards categorical model theory

Abstract: We will explain how abstract elementary classes are situated among accessible categories and how model theory can be extended from the former to the latter. In particular, we will deal with categoricity, saturation, Galois types and tameness.


17 September
10.00-11.45

Aarne Ranta, Göteborg

Machine Translation: Green, Yellow, and Red

Abstract: The main stream in machine translation is to build systems that are able to translate everything, but without any guarantees of quality. An alternative to this is systems that aim at precision but have limited coverage. Combining wide coverage with high precision is considered unrealistic. Most wide-coverage systems are based on statistics, whereas precision-oriented domain-specific systems are typically based on grammars, which guarantee translation equality by some kind of formal semantics.

This talk introduces a technique that combines wide coverage with high precision, by embedding a high-precision semantic grammar inside a wide-coverage syntactic grammar, which in turn is backed up by a chunking grammar. The system can thus reach good quality whenever the input matches the semantics; but if it doesn't, the user will still get a rough translation. The levels of confidence can be indicated by using colours, whence the title of the talk.

The talk will explain the main ideas in this technique, based on GF (Grammatical Framework) and also inspired by statistical methods (probabilistic grammars) and the Apertium system (chunk-based translation), boosted by freely available dictionaries (WordNet, Wiktionary), and built by a community of over 50 active developers. The current system covers 11 languages and is available both as a web service and as an Android application. (extended version of my talk at Vienna Summer of Logic, http://www.easychair.org/smart-program/VSL2014/NLSR-2014-07-18.html#talk:3396)


10 September
10.00-11.45

Peter LeFanu Lumsdaine

Introduction to HoTT, for logicians

Abstract: What is Homotopy Type Theory? Many things! It can be seen as (non-exhaustively):

I will survey all of these, with a focus on the second point: concepts such as truncatedness and connectedness, which are motivated by homotopy-theoretic models, but can already be expressed and developed in plain dependent type theory. (In this talk, I will assume some familiarity with dependent type theory.)

Spring 2014

11 June
10.00-11.45

Fredrik Nordvall Forsberg, University of Strathclyde

Inductive-inductive definitions in Intuitionistic Type Theory

Abstract: Martin-Löf's dependent type theory can be seen both as a foundational framework for constructive mathematics, and as a functional programming language with a very rich type system. Of course, we want this language to have a rich notion of data structure as well. I will describe one class of such data types, where a type A is formed inductively, simultaneously with a second type B : A -> Type which depend on it. Since both types are formed inductively, we call such definitions inductive-inductive definitions. Examples of inductive-inductive definitions -- e. g. sorted lists, Conway's Surreal numbers and the syntax of dependent type theory -- will be given, and their meta-theory discussed.

7 May
10.00-11.45

Henrik Forssell and Håkon R. Gylterud

Type theoretical databases

Abstract: We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. From a computer science perspective, the interesting point is that this category can be seen to represent tables in a natural way. Thus the category is a model for databases, a single mathematical structure in which all database schemas and instances (of a suitable, but sufficiently general form) are represented. The type theory then allows for the specification of database schemas and instances, the manipulation of the same with the usual type-theoretic operations, and the posing of queries. This is joint work with David I. Spivak (MIT).

9 April (two seminars !)
10.00-11.45
Justyna Grudzinska, Warsaw

Generalized Quantifiers on Dependent Types: A System for Anaphora

Abstract: We propose a system for the interpretation of anaphoric relationships between unbound pronouns and quantifiers. The main technical contribution of our proposal consists in combining generalized quantifiers with dependent types. Empirically, our system allows a uniform treatment of all types of unbound anaphora, including the notoriously difficult cases such as quantificational subordination, cumulative and branching continuations, and 'donkey anaphora'. [This is joint work with Marek Zawadowski.]

13.30-15.15

Marek Zawadowski, Warsaw

Equational Theories for Combinatorics and Geometry

Abstract: Monads, Lawvere Theories, and Operads provide different means to define algebraic structures in categories. Under some natural assumptions they present the same algebraic structures in the category Set. Symmetric operads were originally introduced to study the geometry of loop spaces, whereas analytic and polynomial monads were introduced to study enumerative combinatorics. They have been applied with a success to combinatorial problems related to higher-dimensional categories. In my talk I will discuss the subcategories of categories of monads (on Set) Lawvere theories, and operads (in Set) that correspond to various classes of equational theories relevant for combinatorics and geometry.

2 April

Jouko Väänänen, Helsinki

Dependence and independence: A logical approach

12 March

Henrik Forssell

Constructive completeness and exploding models

Abstract: We present a unifying categorical approach, based on Joyal's completeness theorem, that proves constructive completeness theorems for classical and intuitionistic first order logic, as well as for the coherent fragment. We show that the notion of exploding structure introduced by Veldman in 1976 is adequate for certain fragments of first-order logic and that Veldman's modified Kripke semantics arises, as a consequence, as the semantics of a suitable sheaf topos. The proof, as that of Veldman's, makes use of the fan theorem. This raises the question of how far one can get in proving completeness constructively but without using the fan theorem. We show that the disjunction-free fragment is constructively complete without appeal to the fan theorem, and also without placing restrictions on the decidability of the theories and the size of the language. Along the way we show how the completeness of Kripke semantics for the disjunction free fragment is equivalent, over IZF, to the Law of Excluded middle. (This is joint work with Christian Espíndola.)

5 March

Per Martin-Löf

Sample space-time

26 February

Per Martin-Löf

Dependence and causality

19 February

Erik Palmgren

On dependently typed first-order logic (cont.)

Abstract: Dependently typed (or sorted) first-order logics were introduced and studied by M. Makkai (1995), P. Aczel and N. Gambino (2006) and J.F. Belo (2008). Belo gave a completeness theorem for an intuitionistic version of such a logic with respect Kripke semantics. In this talk we consider a more general semantics based on categories with families. (This seminar is a continuation from September 18.)

29 January

Håkon Robbestad Gylterud

Univalent Multisets

Abstract: Multisets, like sets, consist of elements and the order of appearance of these elements is irrelevant. What distinguishes multisets from sets is the fact that number of occurrences of an element matters. In this talk I will show how one may capture this intuition in Martin-Löf Type Theory. First, I will present a technical result on the identity types of W-types in type theory (without the Univalence Axiom). In light of this result I will give an analysis of the underlying type of Aczel's model of Constructive Zermelo-Fraenkel set theory (CZF) in presence of the Univalence Axiom. The conclusion is that Aczel's type, considered with the identity type as equality, consist of iterative, transfinite multisets. I will also present an axiomatic approach to multisets - based on a "translation" of the axioms of CZF.

22 January

Peter LeFanu Lumsdaine, IAS, Princeton

Semi-simplicial sets, with an eye to type theory

Abstract: Simplicial sets give, classically, a wonderful model for homotopy theory, and a very satisfying interpretation of type theory. In constructive settings, however, this theory breaks down in several ways. One candidate for repairing it is to pass to *semi-simplicial sets* - structures like simplicial sets, but with only face operations, not degeneracies. These are in some ways harder to work with than simplicial sets, but constructively, they seem much better-behaved. I will show how to construct (classically) a right semi-model structure on semi-simplicial sets, and a resulting model of type theory; and I will discuss the issues involved in attempting to constructivise these results.

Fall 2013

18 December

Roy T Cook, University of Minnesota

There is No Paradox of Logical Validity

Abstract: A number of arguments have recently appeared (independently in work by Beall & Murzi, Shapiro, and Whittle) for the claim that the logical validity predicate, when added to Peano Arithmetic (PA), is inconsistent in much the same manner as the addition of an unrestricted truth predicate to PA leads to a contradiction. In this paper I show that there is no genuine paradox of logical validity. Along the way a number of rather important, rather more general, lessons arise, including: (i) Whether or not an operator is logical depends not only on what content that operator expresses, but the way that it expresses that content (e.g. as a predicate versus as a logical connective). (ii) Different paradoxes (or purported paradoxes) require different assumptions regarding the status of the principles involved (e.g. mere truth preservation versus logical validity). (iii) A previous analysis of the purported paradox, due to Jeffrey Ketland, fails to properly locate the root of fallacious reasoning involved (apportioning the blame equally to the assumption that PA is logically valid and to the assumption that the validity rules are themselves logically valid). As a result, there is no paradox of logical validity. More importantly, however, these observations lead to a number of novel, and important, insights into the nature of validity itself.

4 December

Christian Espíndola

The completeness of Kripke semantics in constructive reverse mathematics

Abstract: We will consider in intuitionistic set theory the completeness theorem with respect to Kripke semantics and analyze its strength from the point of view of constructive reverse mathematics. We will prove that, over intuitionistic Zermelo-Fraenkel set theory IZF, the strong completeness of the negative fragment of intuitionistic first order logic is equivalent, in the sense of interderivability, to (all instances of) the law of the excluded middle, and that the same result holds for the disjunction-free fragment. On the other hand, we will prove that the strong completeness of full intuitionistic first order logic is equivalent, over IZF, to (all instances of) the law of the excluded middle plus the Boolean prime ideal theorem. As a consequence, we will see that the generalization to arbitrary theories of Veldman's completeness theorem for modified Kripke semantics cannot be proved in IZF. Finally, we will mention aspects of a joint work in progress with Henrik Forssell on the categorical analysis of modified Kripke semantics and how it could be used to derive in IZF completeness proofs for the disjunction-free fragment.

6 November

Ali Enayat, Göteborg

Satisfaction classes: conservativity, interpretability, and speed-up

Abstract: This talk reports on joint work with Albert Visser (Utrecht). A full satisfaction class on a model M of PA (Peano arithmetic) is a subset S of M that decides the 'truth' of all arithmetical formulae with parameters in M (including those of nonstandard length, if M is nonstandard), while obeying the usual recursive Tarski conditions for a satisfaction predicate. I will present a robust technique for building a wide variety of full satisfaction classes using model-theoretic ideas. This model-theoretic construction lends itself to certain arithmetizations, which in turn can be employed to show that the conservativity of PA + "S is a full satisfaction class" over PA can be verified in Primitive Recursive Arithmetic. I will also comment on the ramifications of the aforementioned arithmetization on interpretability, and speed-up of PA + "S is a full satisfaction class" over PA.

30 October

Thierry Coquand, Göteborg

A model of Type Theory in cubical sets

Abstract: We present a model of Type Theory where a type is interpreted as a cubical set satisfying the Kan condition. This can be seen both as a refinement of Bishop's definition of a set as a collection with an equivalence relation and as a constructive version of Voevodsky's Kan simplicial set model. We use cubical sets with non ordered dimensions, and explain the connection with the notion of nominal sets. Finally, we show how to use this model to give a new explanation of the axiom of description.

23 October

Guillaume Brunerie, Nice

A type-theoretic definition of weak infinity-groupoids

Abstract: The notion of weak infinity-groupoid was originally developed by Grothendieck with the hope of providing an algebraic model for spaces up to homotopy. This notion has also recently come up in type theory with the proof by van den Berg, Garner and Lumsdaine that every type in dependent type theory has the structure of a weak infinity-groupoid (using the definition of Batanin-Leinster). In this talk I will present a type-theoretic definition of the notion of weak infinity-groupoid, equivalent to Grothendieck's definition, and prove that every type in dependent type theory is such a weak infinity-groupoid.

16 October

Henrik Forssell

Localic methods in constructive model theory

Abstract: We outline some preliminary investigations into using locale-theoretic methods in constructive model theory, methods springing from such results as the sheaf-theoretic representation and cover theorems of Joyal and Tierney and (formal) space valued completeness theorems of e.g. Coquand and Smith.

9 October

Dag Prawitz

Relations between Gentzen's and Heyting's approaches to meaning

18 September

Erik Palmgren

On dependently typed first-order logic

28 August

Per Martin-Löf

Truth of empirical propositions

Spring 2013

12 June

Mateus de Oliveira Oliveira

The parameterized complexity of equational logic

Abstract. We introduce a variant of equational logic in which sentences are pairs of the form (s=t, ω) where ω is an arbitrary ordering of the sub-terms appearing in s=t. To each ordered equation (s=t, ω) one may naturally associate a notion of width, and to each derivation of an ordered equation (s=t, ω) from a set of axioms E, one may naturally define a notion of depth. The width of such a derivation is defined as the width of the thickest ordered equation appearing in it. Our main result states that for any fixed set of axioms E and constants c and d one may determine whether a given ordered equation (s=t, ω) can be inferred from E in depth d and width c in time f (|E|, d, c)*|s = t|^O(c) . Additionally we will define the notion of b-bounded substitution. We say that a proof is b- bounded if every substitution rule used on it is b-bounded. We will show that one may determine whether (s=t, ω) follows from E via a b-bounded proof of depth d and width c in time f (|E|, d, c, b)|s = t|.

29 May

Simone Tonelli

Investigations into a model of type theory based on the concept of basic pair. (Presentation of MSc Thesis)

Abstract. he principal aim of this thesis is to explain a possible model of Per Martin-Löf's type theory based on the concept of Giovanni Sambin’s basic pair. This means to extend the concept of "set" in the easiest and most natural way: transforming it in a couple of sets and an arbitrary relations set between them, i.e. a basic pair. This reasoning will be applied to all the judgment forms and will give us an interpretation of Martin-Löf's type theory. Our purpose will be to find a model which satisfies this interpretation, and we will look for it following two different approaches. The first one is meant to remain inside the standard type theory constructing an internal model; the second one, arisen from some impasses reached in the development of the first attempt, is aimed at adding new type constructors at the standard theory, extending it and allowing us to create an external model. These new types, that we have denoted here with a star, have to be seen like an arbitrary relations set between two set of the same type without star. This extended theory will give us all the results needed in a natural way, and might be useful in different interpretations for further research.

A two day workshop 20-21 May

60th Parallel Workshop on Constructivism and Proof Theory

8 May

Douglas Bridges (University of Canterbury, Christchurch, New Zealand)

TBA in Constructive Theory of Apartness Spaces

Abstract. The theory of apartness spaces, a counterpart of the classical one of proximity spaces, provides one entry to a purely constructive (i.e. developed with intuitionistic logic and CZF set theory or ML type theory) study of topology. The canonical example of apartness spaces are metric spaces, locally convex spaces, and, more generally, uniform spaces. The general theory of apartness and its specialisation to uniform spaces has been studied extensively since 2000, and is expounded in detail in [1]. In this talk we first present the basic notions of apartness between sets and of uniform structures, and point out the connection between point-set apartness spaces and neighbourhood spaces. We then introduce u-neighbourhood structures, which lie somewhere between topological and uniform neighbourhood structures. It turns out that every reasonable apartness space $X$ has an associated apartness relation $\bowtie _{w}$ induced by a u-neighbourhood structure. Classically, that associated structure is induced by the unique totally bounded uniform structure that induces the original apartness on $X$. Although there is no possibility of proving, in general, that $\bowtie _{w}$ is induced constructively by a uniform structure, it is always induced by a u-neighbourhood structure. The mysterious `TBA' in the title of the talk derives from the fact that there is a natural definition of total boundedness for u-neighbourhood spaces, enabling us to examine the computationally useful notion of totally bounded apartness (TBA) outside the context of a uniform space. Reference [1] D.S. Bridges and L.S.V\^{\i}\c{t}\u{a}, Apartness and Uniformity: A Constructive Development, in: CiE series Theory and Applications of Computability", Springer Verlag, Heidelberg, 2011.

13 March

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.

27 February

Erik Palmgren

The Grothendieck construction and models for dependent types

13 February

Per Martin-Löf

Invariance under Isomorphism and Definability (continued)

6 February

Per Martin-Löf

Invariance under Isomorphism and Definability (continued)

30 January

Per Martin-Löf

Invariance under Isomorphism and Definability

23 January

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.

Fall 2012

12 December

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.

5 December

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.

28 November

Peter Schuster, Pure Mathematics, University of Leeds

When Irreducibles are Prime

Abstract: 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

21 November

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.

7 November

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.

26 September

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.

12 September

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.

Spring 2012

30 May

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.

9 May

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.

25 April

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).

18 April

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.

21 March

Hajime Ishihara (Japan Advanced Institute of Science and Technology)

Some Conservative Extension Results of Classical Logic over Intuitionistic Logic

7 March

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.

29 February

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.

15 February

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.

8 February

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.

1 February

Dag Prawitz

Gentzen's 2nd consistency proof and normalization of natural deductions in 1st order arithmetic

25 January

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.

18 January

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.

Fall 2011

December 12, 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

We will survey this technique, provide a short comparison with the related work by Isham and co-workers, which motivated Bohrification, and use sites and geometric logic to give a concrete external presentation of the internal locale. The points of this locale may be physically interpreted as (partial) measurement outcomes.

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:



23 November

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.

12 and 19 October

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.

28 September

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.

Seminars Spring 2011 and Earlier (The Stockholm-Uppsala Seminar)

Spring 2011

9-10 June
Symposium on Constructivity and Computability in Algebra, Analysis, Logic and Topology Uppsala, 9-10 June 2011.
17-18 March

Three lecture seminar series in theoretical computer science & mathematical logic

Containers, a mini-course

Prof. Neil Ghani, University of Strathclyde, UK

Summary: The semantics of data types within computer science is often given using initial algebra semantics. However, not all functors have initial algebras and even those that do often lack good properties. As a result, a number of formalisms have been invented to capture those functors which give rise to initial algebras with good properties. Containers are one such formalism and this series of talks concerns them. One of the pleasant features I will mention is the smooth generalisation of containers to indexed containers and then to inductive recursive definitions. I'll aim to make my talks accessible to those with an understanding of one of i) category theory; ii) type theory; or iii) functional programming.

All lectures will be given in room 2215, Polacksbacken (ITC), Lägerhyddsvägen 2, Uppsala (house 2, floor 2, room 215).

Fall 2010

November 11

Andrew Pitts, Cambridge

Structural Recursion with Locally Scoped Names

Abstract: I will discuss a new recursion principle for inductive data modulo alpha-equivalence of bound names that makes use of Odersky-style local names when recursing over bound names. It is inspired by the nominal sets notion of "alpha-structural recursion". The new approach provides a pure calculus of total functions that still adequately represents alpha-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. It arises from a new semantics of Odersky-style local names using nominal sets.


September 29

Ogawa Mizuhito, JAIST, Japan

Confluence of Term Rewriting Systems, brief history and recent progress

Abstract: Confluence and termination are two major target properties of rewrite systems. This talk briefly overviews the histroy of sufficient conditions for confluence of first-order term rewriting systems, and recent progress from our group will be introduced. (One appeared in IJCAR this July and another will come soon in IPL.)


September 8

Erik Palmgren

On the category of types with intensional identity


September 1

Per Martin-Löf

Contexts and cubical complexes


August 25

Johan Glimming

Towards Parametric Direcursion


August 25

Peter Dybjer, Chalmers

The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theory with Pi, Sigma, and Extensional Identity Types


Spring 2010

May 26

Johan Granström

Metamodelling in constructive type theory


May 19

Richard Garner

Ionads and constructive topology.

Abstract: Formal topology provides a way of defining topological structures within constructive type theory. However, the theory of formal topologies is more akin to that of locales than to that of topological spaces. The purpose of this talk is to discuss a way in which the theory of topological spaces could be embedded directly into constructive type theory; it employs a new notion---that of an ionad---which may be seen as a proof-relevant generalisation of the notion of topological space.


May 19

Douglas S Bridges

Constructive reverse mathematics

Abstract: Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Constructive reverse mathematics is reverse mathematics carried out in Bishop-style constructive math (BISH)---that is, using intuitionistic logic and, where necessary, constructive ZF set theory; see (Bridges and Vita 2006). There are two primary foci of constructive reverse mathematics: first, investigating which constructive principles are necessary to prove a given constructive theorem; secondly, investigating what non-constructive principles are necessary additions to BISH in order to prove a given non-constructive theorem. I will present work on constructive reverse mathematics, carried out with Josef Berger and Hannes Diener. The main theme of the talk is the connection between the antithesis of Specker's theorem, various continuity properties, versions of the fan theorem, and Ishihara's principle BD-N.

References


April 21

Anton Hedin

Vitali's covering theorem in constructive mathematics

Abstract: Vitali's covering Theorem states in its simplest form that if a closed interval I, in the real numbers, is (Vitali-) covered by a collection of open intervals V, then for every k>0 there is a finite subset F of V of pairwise disjoint intervals which cover all of I except a subset of measure less than k. We show that the Theorem fails in Bishop's constructive mathematics by giving a recursive counterexample. In fact it is equivalent to Weak Weak Kšnig's Lemma over BISH. Moreover we show that, under a reasonable interpretation of Vitali covering, the Theorem holds in the topology of reals in formal topology. The relation to the point-set result is explained via the concept of spatiality of formal topologies. The talk is based on joint work with Dr. Hannes Diener.


April 14

Per Martin-Löf

Spreads and choice sequences in type theory (cont.)


April 7

Per Martin-Löf

Spreads and choice sequences in type theory (cont.)


March 24

Per Martin-Löf

Spreads and choice sequences in type theory


March 17

Kim Solin

Applications of modified semirings

Abstract: In this talk I present some applications of semirings that have been modified to serve a particular purpose. These applications include reasoning about programs and reasoning about epistemic notions. I conclude by presenting two open problems.


February 3

Sten-Åke Tärnlund

P vs NP


Fall 2009

During Fall 2009 Institut Mittag-Leffler had a programme on Mathematical Logic: Set Theory and Model Theory. This replaced the logic seminar activity that term.

Academic year 2008/2009

List of seminars

Academic year 2007/2008

List of seminars

Earlier seminars

Earlier seminars see .

March 5, 2016, Erik Palmgren. Email: palmgren (at) math (dot) su (dot) se