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 m_{0},…,m_{k-1} such that A={m_{0},…,m_{k-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 m_{0},…,m_{k-1} such that A={m_{0},…,m_{k-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*