Paul Taylor: An Existential Quantifier for General Topology

Seminar za osnove bo tokrat izjemoma deloval v avgustu, saj imamo na obisku kar nekaj gostov, ki so prišli na konferenco Computability and Complexity in Analysis 2009. Konferenco organiziramo v času od 18. do 22. avgusta na Fakulteti za matematiko. Oglejte si urnik predavanj na lokalni strani konference in pridite poslušat, kar vas zanima!

Povzetek seminarja:

The meaning of the existential quantifier was one of the main battlegrounds between classical and constructive mathematicians, and it has been given several other meanings in type theories such as System F, category theory and proof theory.

I shall introduce a predicate calculus called equideductive logic that has universally quantified implications between equations in a simply typed lambda calculus. It was motivated by CCCs with equalisers such as Dana Scott's equilogical spaces and its leading model is the category of sober topological spaces, although there also appear to be models based on Hilbert spaces and topological vector spaces.

In this logic an existential quantifier can be defined using an old idea from higher order logic. It agrees with the categorical idea of epis. However, one must be extremely careful in using it because, logically, it doesn't obey substitution or cut elimination, whilst categorically the epis need not be surjective. Nevertheless it seems to be a useful tool.

Equideductive logic is intended to be a framework in which to generalise Abstract Stone Duality beyond local compactness, but the integration of these two approaches is still in its early stages.