"new foundations must give new math"

from "The Basic Picture. Structures for constructive topology"

by Giovanni Sambin, Oxford University Press, forthcoming

Registration

To register send an e-mail to maietti @ math.unipd.it

Registration fee: 40 euros
(to be paid at arrival).

Under the patronage of

Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova, Italy

University of Padova, Italy

AILA (Italian Association of Logic and Applications), whose first president was Giovanni Sambin (from 1987 to 1994).

Abstracts » Taylor

Peter Aczel
Manchester

Core Extensional Mathematics and Local Constructive Set Theory

Core Extensional Mathematics (CEM) is that part of mathematical practise that can be viewed as common to extensional constructive mathematics and topos mathematics. One possible setting for CEM is constructive set theory (CST) with generalised predicative axiom systems such as CZF and CZF+ (= CZF+REA).

In my talk I will suggest that a good alternative setting for CEM is local constructive set theory (LCST), which differs from CST in not having a global iterative universe of sets. Most of the axioms and schemes of CZF have local formulations. But the Set Induction Scheme of CZF and the axiom REA of CZF+ seem to be essentially global. As these are central to the development of the theory of inductive and coinductive definitions in CST we reconsider how to treat such definitions when working in LCST.