LOGIKSEMINARIET STOCKHOLM-UPPSALA


Onsdagen 19 maj blir det två seminarier


1. Douglas S. Bridges (University of Canterbury, N.Z.)

     Constructive Reverse Mathematics

kl 10.30 - 12.15, onsdagen den 19 maj i sal Å64119
(Ångströmlaboratoriet, Uppsala).

Abstract. Reverse mathematics is a program in mathematical logic that 
seeks to determine which axioms are required to prove theorems of 
mathematics. Constructive reverse mathematics is reverse mathematics 
carried out in Bishop-style constructive math (BISH)---that is, using 
intuitionistic logic and, where necessary, constructive ZF set theory; see 
(Bridges and Vita 2006). There are two primary foci of constructive 
reverse mathematics:

first, investigating which constructive principles are necessary to prove a
given constructive theorem;

secondly, investigating what non-constructive principles are necessary
additions to BISH in order to prove a given non-constructive theorem.

I will present work on constructive reverse mathematics, carried out with 
Josef Berger and Hannes Diener. The main theme of the talk is the 
connection between the antithesis of Specker's theorem, various continuity 
properties, versions of the fan theorem, and Ishihara's principle BD-N.

References

J. Berger and D.S. Bridges, `A fan-theoretic equivalent of the
antithesis of Specker's theorem', Proc. Koninklijke Nederlandse Akad. Weten.
(Indag. Math., N.S.), 18(2), 195--202, 2007.

D.S. Bridges and H. Diener, `The pseudocompactness of [0,1] is equivalent 
to the uniform continuity theorem', J. Symbolic Logic 72(4), 1379--1383, 
2007.

D.S. Bridges and L.S. Vita, Techniques of Constructive Analysis, 
Universitext, Springer-New-York, September 2006.

                      -----

2. Richard Garner (Cambridge University)

     Ionads and constructive topology

kl 14.00 - 15.45, onsdagen den 19 maj i sal P2214
(MIC, Polacksbacken, Uppsala).

Abstract. Formal topology provides a way of defining topological 
structures within constructive type theory. However, the theory of formal 
topologies is more akin to that of locales than to that of topological 
spaces. The purpose of this talk is to discuss a way in which the theory 
of topological spaces could be embedded directly into constructive type 
theory; it employs a new notion---that of an ionad---which may be seen as 
a proof-relevant generalisation of the notion of topological space.