September 11: Amar Hadzihasanovic: Functional interpretations and categorical models of nonstandard arithmetic
16.00--17.00
Abstract: Recently, van den Berg, Briseid and Safarik introduced nonstandard Dialectica [4], a functional interpretation that is capable of eliminating instances of familiar principles of nonstandard arithmetic - including overspill, underspill, and generalisations to higher types - from proofs. We show that, under few metatheoretical assumptions, the properties of this interpretation are mirrored by first order logic in a constructive sheaf model of nonstandard arithmetic due to Moerdijk [2], later developed by Palmgren [3].
The categorical analysis suggests how one can obtain nonstandard Dialectica from a variant of the Diller-Nahm interpretion with two different kinds of quantifiers (with and without computational meaning), similar to Hernest’s light Dialectica interpretation [1], by weakening the computational content of the existential quantifiers. Finally, we draw some new connections between nonstandard principles, and principles that are rejected by strict constructivism.
References
[1] M.-D. Hernest. Light functional interpretation. In Computer science logic, pages 477–492. Springer, 2005.
[2] I. Moerdijk. A model for intuitionistic non-standard arithmetic. Annals of Pure and Applied Logic, 73(1):37–51, 1995.
[3] E. Palmgren. Developments in constructive nonstandard analysis. Bulletin of Symbolic Logic, pages 233–272, 1998.
[4] B. van den Berg, E. Briseid, and P. Safarik. A functional interpretation for nonstandard arithmetic. Annals of Pure and Applied Logic, 2012.

October 16, 2013: Luca Spada: General affine adjunctions, Nullstellensätze, and dualities
13.00--14.00
Abstract: In classical algebraic geometry, one studies the solutions sets over an algebraically closed field K of systems of equations between polynomials in n variables with coefficients in K. In fact, there is a (contravariant) Galois connection between subsets of K^n and of the polynomial ring K[x_1,...,k_n]. The first aim of this talk is to show how the above generalises to any equationally definable class of algebras. Further, we will show that the classical Galois connection just described can always be made functorial, and thus lifted to a dual adjunction between the category of "affine sets" with their "polynomially definable" maps, and the category defined by the objects in the variety and their homomorphisms. This general adjunction, together with its induced duality between the full subcategories on the fixed objects, provides a link between Birkhoff's subdirect representation theorem, Hilbert's Nullstellensatz and topological dualities in the style of Marshall Stone for varieties of algebras. We show how several dualities of this sort, such as Stone duality for Boolean algebras, Priestley duality for distributive lattices, Gelfand duality for real C*-algebras, Pontryagin duality for locally compact abelian groups can be perfectly framed in this picture. Finally, we perform the last step in the abstraction and land in a general categorical framework which encompasses an even larger number of dualities, being able to give an account of, e.g., Galois theory of field extensions and the adjoint connection between subgroups of the fundamental group of a path-connected and semi-locally simply connected topological space and its path-connected covering spaces.

October 16, 2013: Fabio Pasquali: Sheaves and Cauchy-complete Categories in Doctrines
14.15--15.15
Abstract: It has been Walters who firstly noted the link between the notion of sheaf and that of Lawvere Cauchy-completeness. In particular he proved that the topos of sheaves on a site (C,J) is equivalent to the bicategory of symmetric Cauchy-complete Rel(C,J)-categories, where Rel(C,J) is a suitable category of relations. We give a different, purely syntactical, proof of the equivalence discovered by Walters. We comment on some new classes of examples.

October 16, 2013: Eyvind Briseid: On functional interpretations for systems of nonstandard arithmetic
15.45--16.45
Abstract: We will present work on functional interpretations for systems of both classical and constructive nonstandard arithmetic, inspired by Nelson's Internal Set Theory (IST). These results allow one to extract computable bounds and realizers from certain nonstandard proofs, and also show conservativity of nonstandard systems over standard ones. In this talk we will consider extensions of the soundness theorem for the nonstandard functional interpretation to weaker systems with only restricted forms of induction, and also to stronger systems with a form of Weak König's Lemma added.

January 29, 2014: Jouko Väänänen: Multiverse set theory and absolutely undecidable propositions
17:00--18:00
Abstract: For a time Goedel contemplated the idea that there could be absolutely undecidable propositions, on which set theory bifurcates into two (or more) different systems. Although Goedel later abandoned this idea, we try to make sense of this ``bifurcation". We present a multiverse approach to set theory allowing for the possibility that some propositions are neither true nor false for the reason that they are true in some of the parallel universes and false in others.

March 27, 2014: Lev Beklemishev: Positive Provability Logic -- for Uniform Reflection Principles
16:00--17:00
Abstract: We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant `true' by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and $\omega$, where $\omega$ corresponds to the full uniform reflection schema, whereas $n<\omega$ corresponds to its restriction to arithmetical $\Pi_{n+1}$-formulas. This calculus is shown to be complete w.r.t.\ a suitable class of finite Kripke models and to be decidable in polynomial time.

April 23, 2014: Thierry Coquand: Constructive mathematics and univalent foundation
16:00--17:00
Abstract: We describe some extensions of dependent type theory suggested by the univalent foundation program of Voevodsky. These extensions should be useful for representing mathematics in type theory. In particular, the axiom of univalence can be seen as a strong form of extensionality. We can also express a new existential quantification which is closer to intuitionistic quantification, which satisfies the axiom of description. All these extensions can be explained constructively.