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 ﬁrst 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 diﬀerent kinds of quantiﬁers (with and
without computational meaning), similar to Hernest’s light Dialectica interpretation [1],
by weakening the computational content of the existential quantiﬁers.
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.

To main page

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.

To main page

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.

To main page

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.

To main page

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.

To main page

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.

To main page

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.

To main page

To main page