Michael Makkai: Notions of identity for and in higher dimensional categories.

FOLDS, first-order logic with dependent sorts, provides a general concept of identity (examples of which are: isomorphism for classical structures, equivalence for categories, biequivalence for bicategories, etc.) for categorical structures, by (1) re-coding the structures in question as L- structures: SET-valued functors from a well-chosen FOLDS signature (a 1-way, finitary category) L, and (2) deploying the general concept of L-equivalence, defined uniformly for all FOLDS signatures L. This is the notion of identity for a specific kind of a higher structure, say bicategory, mentioned in the title.

On the other hand, internally in a bicategory, we talk about equivalence of objects (0-cells), and also of 1-cells, and even of diagrams indexed by a fixed bicategory, as the “right” notion of identity. It turns out that FOLDS equivalence helps to give a simple uniform way of defining internal identity valid in a wide variety of cases. FOLDS equivalence as the notion of identity for higher structures is the main topic of my 1995 – unpublished but available on my web-site – monograph on FOLDS. The material for FOLDS equivalence used for identity internally in higher structures, examples and certain general facts, is unpublished, and some of it needs polishing, although I am ready to soon provide notes and give lectures, rather technical lectures and notes at that, on the subject.

The right initial context for the general theory of FOLDS equivalence “in and for” higher structures is one that eliminates usual syntax completely, It is based on the consideration of classes (I use PHI as a variable denoting a class in question) of X -augmented L-structures, for varying FOLDS signatures L and augmentation types X; X here is a finite SET-valued functor on L; and an augmented structure is a functor M:L-->SET (L-structure), together with an augmentation (natural transformation) a:X-->M . The only condition imposed on PHI is that it be invariant under L-equivalence (which is defined naturally for augmented structures as well). The context described is one familiar in model-theoretic- logic, where a formula – any formula in any logic such as first-order, second order, etc – is replaced by the class of augmented structures satisfying it; the above X is the (context-organized) set of (typed by dependent sorts) free variables in the formula. I would like to call this the Lindstroem context for FOLDS. Originally introduced by Per Lindstroem for ordinary classical one-sorted logic, Lindstroem's context for model-theoretic logic gives rise to his (once?) celebrated (but nowadays quite forgotten ...?) theorem characterizing first-order logic “from above”. It turns out that Lindstroem's theorem has a smooth, even elegant, generalization to FOLDS, with a proof that is a careful, but quite straightforward, lifting Lindstroem's proof, by replacing the uniform classical notion of isomorphism – accepted exclusively as the right notion of identity for structures in model-theoretic logic – by FOLDS L-equivalence, for varying FOLDS signatures L.

Let me note that the Lindstroem theorem for FOLDS and its proof are quite independent from the main meta-theorem for FOLDS ( let me call it the invariance theorem) which asserts, roughly and slightly more weakly than necessary, that, up to logical equivalence, the first-order (multi-sorted) statements over L (as a plain multisorted signature) that are invariant under FOLDS equivalence are exactly the ones formulated in the FOLDS syntax over L: see the 1995 monograph. On the other hand, similarly to the invariance theorem, the FOLDS-version of the Lindstroem theorem is a demonstration of the tight relation of the FOLDS concept of identity and the FOLDS syntax. One is reminded of the Leibnizian definition of identity: two things are identical if and only if they satisfy the same meaningfully applicable properties.

Benno van den Berg: Effective Kan fibrations in simplicial sets.

Homotopy type theory started in earnest when Voevodsky formulated his univalence axiom and showed that the category of simplicial sets hosts a model of type theory in which this axiom holds. After he made these contributions, people wondered to which extent this model can be developed in a constructive metatheory and can be exploited for computational purposes. Some serious obstacles were found and in response many researchers switched to cubical sets and started working on "cubical type theories". In joint work with Eric Faber I have developed an approach which seeks to circumvent the obstructions for developing a simplicial sets model for homotopy type theory in a constructive fashion. In this talk I will try to give some idea of how we try to do this, what we have achieved thus far and how our project compares to related ones by Gambino, Henry, Szumilo and Sattler.

Jouko Väänänen: The Strategic Balance of Games in Logic.

Truth, consistency and elementary equivalence can all be characterised in terms of games, namely the so-called evaluation game, the model-existence game, and the Ehrenfeucht-Fraısse game. We point out the great affinity of these games to each other and call this phenomenon the strategic balance in logic. The three games penetrate into the heart of logic. Their mathematical interpretations and elaborations lead us into the deepest questions of mathematical logic, especially model theory and set theory. They provide tools for understanding central questions of philosophical logic such as intuitionistic, modal and other non-classical logic. They have become indispensable in theoretical computer science modelling interaction and complexity.

Jiří Rosický: Towards a point free model theory.

Traditional model theory uses signatures and formulas to specify structures and their morphisms. Shelah introduced abstract elementary classes using signatures but no formulas. Instead, structures and morphisms are governed by abstract properties. Makkai and Paré defined accessible categories as a framework for model theory without signatures and without underlying sets. Every accessible category can be equipped with underlying sets and formulas but it can be done in many ways. My aim is to present some advantages of this "point-free" approach. In particular, cardinalities of underlying sets are replaced by internal sizes. Among others, stable independence will be made point-free.

Jeremy Avigad: Methodology and metaphysics in Dedekind's theory of ideals.

Philosophical questions don't often intrude on a mathematician's workday, but occasionally questions arise as to whether some fundamental new way of doing things is justified, appropriate, or desirable. When that happens, there are two models as to how mathematics ought to proceed: according to the first, such questions should be adjudicated on the basis of broad reflection on the nature and meaning of mathematics, and according to the second, they should be adjudicated purely in terms of mathematical utility. Stewart Shapiro has described these models as "philosophy first'" and "philosophy last, if at all."

In this talk, I'll use the work of the nineteenth-century mathematician Richard Dedekind to show that philosophical and mathematical questions cannot always be so cleanly separated. Dedekind's mathematical innovations include early uses of infinitary, set-theoretic language; uses of non-constructive reasoning; axiomatic and algebraic characterization of structures; and a focus on properties that can be characterized in terms of mappings between them. These innovations are so far-reaching that it is hard not to attribute them to a fundamentally different conception of what it means to do mathematics. And yet Dedekind's writings make it clear that they were designed with distinctly mathematical problems and goals in mind.

I will focus, in particular, on the history of Dedekind's theory of ideals. Between 1871 and 1895, Dedekind published four versions of the theory; paying attention to this evolution, and to the contrasts with a rival approach by Kronecker, can help us understand some of the attitudes and goals that are fundamental to modern mathematics.

Michael Shulman: The derivator of setoids.

Can homotopy theory be developed in constructive mathematics, or even in ZF set theory without the axiom of choice? Recent work inspired by homotopy type theory has yielded two constructive homotopy theories (simplicial sets and equivariant cubical sets) that are classically equivalent to that of spaces, but it is unknown if they are constructively equivalent to each other. If they are not, then which one is correct? Or are they both correct, or both incorrect? What do these questions even mean?

I will propose one criterion for the correctness of a constructive homotopy theory of spaces: as a derivator, it should be the free cocompletion of a point. (A derivator is an enhancement of the homotopy category that remains 1-categorical, but can still express universal properties of this sort.) Then I will give some evidence that any such homotopy theory must have the curious property that its 1-truncation contains, not only sets, but also setoids. Specifically, the ex/lex completion of the category of sets defines a derivator that satisfies a relative version of the aforementioned universal property; thus it should be a localization of any derivator satisfying the absolute condition. This suggests that either setoids are an unavoidable aspect of constructive homotopy theory, or the criterion needs to be modified.