Workshop

Workshop
Friday, October 6th
Sala riunioni (2° piano)
Department of Computer Science

09:30   Thomas Streicher - An Effective Version of the Spectral Theorem
10:20   Hajime Ishihara - The Hahn-Banach theorem, constructively revisited
11:10   Coffee break
11:50   Ihsen Yengui - Algorithms for computing syzygies over V[X1,…,Xn], V a valuation ring
12:40   Takako Nemoto - Finite sets and infinite sets in weak intuitionistic arithmetic
13:30   Lunch break
15:30   Fabio Pasquali - Choice principles and the tripos-to-topos construction
16:40   Chuangjie Xu - Unifying (Herbrand) functional interpretations of (nonstandard) arithmetic

Abstracts:

Hajime Ishihara The Hahn-Banach theorem, constructively revisited

We review known constructive versions, such as the separation theorem and continuous extension theorem, of the Hahn-Banach theorem and their proofs, and consider new versions including the dominated extension theorem and their proofs.

Takako Nemoto Finite sets and infinite sets in weak intuitionistic arithmetic

We consider, for a set A of natural numbers, the following notions of finiteness

FIN1: There are k and m0,…,mk-1 such that A={m0,…,mk-1} ;
FIN2: There is an upper bound for A;
FIN3: There is m such that for all B ⊆ A (|B|<m);
FIN4: It is not the case that, for all x, there is y such that y∈ A;
FIN5: It is not the case that, for all m, there is B ⊆ A such that |B|=m,

and infiniteness

INF1: There are no k and m0,…,mk-1 such that A={m0,…,mk-1};
INF2: There is no upper bound for A;
INF3: There is no m such that for all B ⊆ A (|B|<m);
INF4: For all y, there is x>y such that x∈ A;
INF5: For all m, there is B ⊆ A such that |B|=m.

We systematically compare them in the method of constructive reverse mathematics. We show that the equivalence among them can be characterized by various combinations of induction axioms and non-constructive principles, including the axiom called bounded comprehension.

Fabio Pasquali Choice principles and the tripos-to-topos construction

In this talk we study the connections between choice principles expressed in categorical logic and the Tripos-to-Topos construction [HJP80]. This is a joint work with M. E. Maietti and G. Rosolini based on [MPR, MR16, Pas17].

[HJP80] J.M.E. Hyland, P.T. Johnstone and A.M. Pitts. Tripos Theory. Math. Proc. Camb. Phil. Soc., 88:205-232, 1980.
[MR16] M.E. Maietti and G. Rosolini. Relating quotient completions via categorical logic. In Dieter Probst and Peter Schuster (eds), editors, Concepts of Proof in Mathematics, Philosophy and Computer Science, pages 229 - 250. De Gruyter, 2016.
[Pas17] F. Pasquali. Hilbert’s epsilon-operator in Doctrines. IfCoLog Journal of Logics and their Applications. Vol 4, Num 2: 381-400, 2017
[MPR] M.E. Maietti, F. Pasquali and G. Rosolini. Triposes, exact completions and Hilbert’s epsilon operator. In preparation.

Chuangjie Xu Unifying (Herbrand) functional interpretations of (nonstandard) arithmetic

We extend Oliva’s method [3] to obtain a parametrised functional interpretation for nonstandard arithmetic. By instantiating the parametrised relations, we obtain the Herbrand functional interpretations introduced in [2,4] for nonstandard arithmetic as well as the usual, well-known ones for Berger’s uniform Heyting arithmetic [1].

[1] U. Berger, Uniform Heyting arithmetic, Annals of Pure and Applied Logic 133 (2005), no. 1, 125-148.
[2] F. Ferreira and J. Gaspar, Nonstandardness and the bounded functional interpretation, Annals of
Pure and Applied Logic 166 (2015), no. 6, 701-712.
[3] P. Oliva, Unifying functional interpretations, Notre Dame J. Formal Logic 47 (2006), no. 2, 263-290.
[4] B. van den Berg, E. Briseid, and P. Safarik, A functional interpretation for nonstandard arithmetic, Annals of Pure and Applied Logic 163 (2012), no. 12, 1962-1994.

Organised by Peter Schuster and Daniel Wessel.

Please note further that on Thursday, October 5th, 4pm, there will be a departmental seminar with Olivia Caramello: The proof-theoretic relevance of Grothendieck topologies