"** new foundations must give new math**"

from

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.