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.

*TBA*

*TBA*

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

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

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

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

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

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

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

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

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

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

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

* 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".

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

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

*
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

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

** Per Martin-Löf**

* Spreads, repetitive structures, and functional causal models *

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

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

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

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

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

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

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

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

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

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

** Peter LeFanu Lumsdaine **

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

** Per Martin-Löf **

* Invariance of causal space-time (cont.). *

** Per Martin-Löf **

* Invariance of causal space-time *

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

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

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

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

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

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

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

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

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

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

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

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

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

** Peter LeFanu Lumsdaine**

* Introduction to HoTT, for logicians *

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

- - various new homotopy-theoretic models of (traditional) dependent type theory;
- - a complex of new concepts and definitions within (traditional) dependent type theory, motivated by these models;
- - new axioms (univalence, HIT), motivated by these models;
- - the use of DTT with these new axioms as a foundation for mathematics.

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

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

* 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.]

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

** Jouko Väänänen, ** Helsinki

* Dependence and independence: A logical approach *

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

** Per Martin-Löf **

* Sample space-time *

** Per Martin-Löf **

* Dependence and causality *

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

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

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

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

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

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

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

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

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

** Dag Prawitz **

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

** Erik Palmgren **

* On dependently typed first-order logic *

** Per Martin-Löf **

* Truth of empirical propositions *

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

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

60th Parallel Workshop on Constructivism and Proof Theory

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

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

** Erik Palmgren **

* The Grothendieck construction and models for dependent types *

** Per Martin-Löf **

* Invariance under Isomorphism and Definability (continued) *

** Per Martin-Löf **

* Invariance under Isomorphism and Definability (continued) *

**Per Martin-Löf **

* Invariance under Isomorphism and Definability *

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

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

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

**Peter Schuster,** Pure Mathematics, University of Leeds

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

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

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.

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

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

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

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

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

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

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

** Hajime Ishihara ** (Japan Advanced Institute of Science and Technology)

* Some Conservative Extension Results of Classical Logic over Intuitionistic Logic *

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

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

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.

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

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

**Dag Prawitz **

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

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

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

* Approaching topology constructively via apartness *

Abstract: In 2000, Luminita Vita and I began investigating axioms for a constructive theory of apartness between points and sets, and between sets and sets, as a possible constructive approach to topology. The culmination of this work came last October, with the publication of the monograph [3], in which we lay down what we believe to be the defnitive axioms for (pre-)apartness and then develop the theory, with particular application to (quasi-)uniform spaces. Our development uses points, and is therefore in the style and spirit of Bishop's original constructive approach to analysis [1, 2]. As with analysis, so with topology: once the "right" axioms are used, the theory allows in a natural, if technically nontrivial, way (with one exception). In this talk I shall present the axioms for apartness and uniform spaces, and discuss various aspects of the resulting theory, paying particular attention to the connections between various types of continuity of functions.

References

[1] E. Bishop, Foundations of Constructive Analysis, McGraw-Hill, New York 1967.

[2] E. Bishop and D.S. Bridges, Constructive Analysis, Grundlehren der Math. Wissenschaften 279, Springer Verlag, Heidelberg, 1985.

[3] D.S. Bridges and L. Vita, Apartness and Uniformity: A Constructive
Development, in: CiE series "Theory and Applications of Computability",
Springer Verlag, Heidelberg, 2011.

** Minisymposium on categorification and foundations
of mathematics and quantum theory **

Room 16, building 5, Kräftriket, Stockholm.

9:15- 10:05: ** Bas Spitters** (Radboud University, Nijmegen)

* Bohrification: Topos theory and quantum theory *

Abstract. Bohrification associates to a (unital) C*-algebra

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

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.

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

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

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

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.

- Lecture 1: Thursday, March 17, 10.15am
- Lecture 2: Thursday, March 17, 15.15pm
- Lecture 3: Friday, March 18, 15.15pm

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

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

**Erik Palmgren**

*On the category of types with intensional identity*

**Per Martin-Löf**

*Contexts and cubical complexes*

**Johan Glimming**

*Towards Parametric Direcursion*

**Peter Dybjer, ** Chalmers

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

**Johan Granström**

*Metamodelling in constructive type theory*

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

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

- J. Berger and D.S. Bridges, `A fan-theoretic equivalent of the antithesis of Specker's theorem', Proc. Koninklijke Nederlandse Akad. Weten. (Indag. Math., N.S.), 18(2), 195--202, 2007.
- D.S. Bridges and H. Diener, `The pseudocompactness of [0,1] is equivalent to the uniform continuity theorem', J. Symbolic Logic 72(4), 1379--1383, 2007.
- D.S. Bridges and L.S. Vita, Techniques of Constructive Analysis, Universitext, Springer-New-York, September 2006

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

**Per Martin-Löf**

*Spreads and choice sequences in type theory (cont.)*

**Per Martin-Löf**

*Spreads and choice sequences in type theory (cont.)*

**Per Martin-Löf**

*Spreads and choice sequences in type theory*

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

**Sten-Åke Tärnlund**

*P vs NP*

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