"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).

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

Paul Taylor

Equideductive logic

In any category with products, equalisers and powers of a base object, the regular monos (those than can be expressed as equalisers) admit intersections and a universal quantifier of the form

q(x) === All y. \p(y) ==> f x y = g x y

Although this is a very feeble logic, it is interesting because

  • it is enough to state judgements and proof rules in algebra,
  • some forms of induction can be written in it,
  • it fits together very neatly with the lattice structure and especially the Euclidean principle in ASD, and
  • it is enough to reproduce a construction similar to that of Scott's equilogical spaces.

The modified equilogical space construction does not have all of the properties that one would like from either ASD or functional analysis.

However, since equideductive logic is so simple, it should be easy to show that axioms can be added to it conservativity, although this is a point on which I would find advice from proof theorists very useful.

Please see the final section of my paper "Foundations for Computable Topology" for more details: www.PaulTaylor.EU/ASD/foufct/