"new foundations must give new math"
from "The Basic Picture. Structures for constructive
topology"
by Giovanni Sambin, Oxford University Press, forthcoming
To register send an e-mail to maietti @ math.unipd.it
Registration fee: 40 euros
(to be paid at arrival).
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).
Damiano Macedonio
Venezia
Sambin's Principle of Reflection and Relational Semantics
Basic Logic has been introduced with the aim of finding a structure
in the space of the logics. Classical, intuitionistic and non-modal
linear logics, are all obtained as extensions in a uniform way.
The logical constants and the connectives are introduced by following
the foundational principle of reflection: every logical entity is
bound to a meta-linguistic link by a definitional equation, whose
solution provides the syntactic inference rules.
This principle, along with the definitional equations, is essential
to provide a notion of model for the logic itself: the relational
monoids. We prove soundness and refined completeness results for this
class of models. In particular the completeness result allows a semantical
proof of cut-elimination.
Basic Logic can be extended in two directions: one direction is the
addition of structural rules, the other is the move to intuitionistic
logic, thus obtaining Intuitionistic Linear Logic and Intuitionistic
Logic. The notion of model, in turn, can be extended to these logics,
and in each case the soundness and refined completeness results are
retained. These newly found models can be related to more traditional
models of the logics so discovered: Kripke models for Intuitionistic
Logic and Phase Spaces for Linear Logic. Finally, combining the two
extensions leads us to the Logic of Bunched Implications.