"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 » Schwichtenberg

Helmut Schwichtenberg
München

Logic of inductive definitions with formal neighborhoods

Consider free algebras, given by their constructors.
They can be seen as information systems (in Dana Scott's sense), whose tokens are constructor trees built from constructors and formal neighborhoods.

We consider ideals (or objects) as consistent deductively closed sets of tokens.

This approach allows to deal conveniently with function spaces, and since all objects are limits of finite approximations, we immediately have a notion of computability in higher types. One inductively defines total and coinductively cototal (finite or infinite stream-like) objects.

The elimination schemes for these definitions are induction and coinduction, respectively.

There is a natural extension of Kreisel's notion of (modified) realizability to these and general inductively and coinductively defined predicates.

Therefore this theory lends itself to a study of the computational content of proofs involving for instance objects like exact real numbers viewed as streams.

Logically the theory sketched is very neutral: one only needs the minimal logic rules for implication and universal quantification.

Other connectives are defined inductively, and from an (inductive) definition of Leibniz equality one can define falsity and prove ex-falso-quodlibet.

References

Ulrich Berger, From coinductive proofs to exact real arithmetic. Draft, 2008.

Helmut Schwichtenberg, Recursion on the partial continuous functionals. In: Logic Colloquium '05, (C. Dimitracopoulos and L. Newelski and D. Normann and J. Steel, eds.), 2006.