[Prev][Next][Index][Thread]
papers available
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
Title: Making proofs without Modus Ponens: An introduction to the
combinatorics and complexity of cut elimination
Authors: A.Carbone and S.Semmes
Email: ale@logic.tuwien.ac.at, semmes@math.rice.edu
Available: IHES preprint M/96/35, or
ftp://ftp.math.ufl.edu/pub/logic/carbone-semmes, or
by anonymous ftp (128.42.62.24)
cd pub/semmes
get cut.dvi or cut.ps
This paper is intended to provide an introduction to cut
elimination which is accessible to a broad mathematical audience.
Gentzen's cut elimination theorem is not as well known as it deserves
to be, and it is tied to a lot of interesting mathematical structure.
In particular we try to indicate some dynamical and combinatorial
aspects of cut elimination, as well as its connections to complexity theory.
We discuss two concrete examples where one can see the structure
of short proofs with cuts, one concerning feasible numbers and the
other concerning "bounded mean oscillation" from real analysis.
Title: Looking from the inside and from the outside
Authors: A.Carbone and S.Semmes
Email: ale@logic.tuwien.ac.at, semmes@math.rice.edu
Available: IHES preprint M/96/44, or
ftp://ftp.math.ufl.edu/pub/logic/carbone-semmes, or
by anonymous ftp (128.42.62.24)
cd pub/semmes
get io.dvi or io.ps
One often sees a sharp distinction in mathematics between
descriptions from the outside and from the inside. Think of defining
a set in the plane through an algebraic equation, or dynamically as
the closure of the orbit of some point under iterations of a given
mapping. In logic one sees this dichotomy in the descriptions of sets
of tautologies through semantics and proofs. Logic provides several
tools for making outer descriptions of mathematical objects.
This paper concerns a slightly complicated mixture of themes
related to inner descriptions and formal proofs. We use the notion of
feasibility to embed mathematical structures into spaces of logical
formulas, from which we can obtain new structures through proofs. We
present new geometries on finitely generated groups through proofs,
and new structure on the rational numbers (or other fields) which is
susceptible to dynamical processes, such as the action of $SL(2,Z)$ by
projective transformations. We consider the topological notion of
{\em Serre fibrations}. This entails more difficulties of
formalization, but basic points arise already for {\em torus bundles},
which present exponential distortion through cycling in a nicely
geometric way.
One of our goals is to bring out mathematical structure
related to cuts and cut elimination. Our geometry on groups through
proofs is far from the word metric precisely because of the cut rule.
We want to explore the idea that in general the existence of short
proofs with cuts should be related to internal symmetry or dynamical
processes in the underlying mathematical objects.
We also want to bring ordinary mathematical proofs closer to
proof theory. In this regard the topological example is attractive
for presenting realistic difficulties.