## The Stockholm Logic Seminar

Organisers: Erik Palmgren and Per Martin-Löf (emeritus)

#### Spring 2013

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.

#### Fall 2012

Wednesday, 12 December

10:00 - 11.45, room 16, building 5, Kräftriket, Stockholm

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

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)

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.

#### Spring 2012

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

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

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

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.

#### 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

• the Kripke model, a presheaf topos, of its classical contexts;
• in this Kripke model a commutative C*-algebra, called the Bohrification
• the spectrum of the Bohrification as a locale internal in Kripke model.
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:

• Many bag equalities can be proved using a form of equational reasoning.
• The definition generalises easily to arbitrary unary containers, including types with infinite values, such as streams.
• By using a small variant of the definition one gets set equality instead, i.e. equality where neither multiplicity nor order matters. Other variations give the subset and subbag preorders. Many preservation properties?such as "the list monad's bind operation preserves bag equality"?can be proved uniformly for all these relations at once, thus avoiding proof duplication.
• The definition works well in mechanised proofs.

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.