"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 » Schröder-Heister

Peter Schröder-Heister
Tübingen

Definitional reflection

Definitional reflection was proposed by Lars Hallnäs in the 1980s and has since been further developed by Hallnäs and S.-H., both as a tool of logic programming and as a foundational principle.

It is an inversion principle, incorporating the idea that everything that can be obtained from all definientia of a defined object can be obtained from the definiendum itself.

In its general form, it is not confined to logical constants but applies to any inductively defined object, quite in accordance with Lorenzen (1950), who coined the term "inversion principle".

Unlike standard applications of inversion in proof-theoretic semantics, definitional reflection does not require well-foundedness of definitions.

After a presentation of its basic ingredients, this talk compares (extensions of) definitional reflection with ideas developed by Giovanni Sambin together with G. Battilotti, C. Faggian in their "Basic Logic" (2000) and later with M.E. Maietti (2005), where they speak of "reflection" in connection with their deductive justification of logical inferences from "definitional equations".