Workshop

PaC

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

Advertisements