[Prev][Next][Index][Thread]
paper on FTP
A paper on categorical theory of proofs
MAPS II:
CHASING PROOFS IN THE LAMBEK-LAWVERE LOGIC
by Dusko Pavlovic
is available by anonymous FTP from triples.math.mcgill.ca . It is in
the directory pub/pavlovic , in the files called mapsII : there are
-A4 and -US formats; .dvi and .ps versions of both. All are
compressed.
-- Regards, Dusko
Abstract
In the Lambek-Lawvere logic, propositions and proofs are presented as
objects and arrows in a category. It is the categorical embodiment of
the strong constructivist paradigms of propositions-as-types and
proofs-as-constructions, which lie in the foundation of computational
logic. But a third paradigm arises here, not available elsewhere: the
idea of logical-operations-as-adjunctions. It opens a possibility of
genuinely categorical proof theory.
In the present paper, we study the Lambek-Lawvere version of regular
logic: the $\{\wedge,\exists\}$-fragment of the first order logic with
equality. The corresponding categorical structure is regular
fibration. The examples include stable factorisations, sites,
triposes. Regular logic is exactly what is needed to talk about maps,
as total and single-valued relations. However, when enriched with
proofs-as-arrows, this familiar concept must be supplied with an
additional conversion rule, connecting the proof of the totality with
the proof of the single-valuedness. We explain the logical meaning of
this and describe conditions under which every map in a regular
fibration corresponds to a unique arrow in the base category. When
this is the case, a natural fragment of generalized regular logic, in
the Lambek-Lawvere style, reduces to regular logic of sites.