categories: Szabo's Algebra of Proofs

[Todd Wilson <twilson@csufresno.edu>]

In the book

    M. E. Szabo, Algebra of Proofs, Studies in Logic and the
    Foundations of Mathematics, Vol. 88, North-Holland, 1978.

the author, according to a 1980 review by Carlo Cellucci published in
Mathematical Reviews (80b:03097),

    [...] studies the algebraic properties of the proof theory of
    intuitionistic first-order logic in a categorical setting. [...]
    Following the Introduction (Chapter I), there are twelve
    additional chapters, in which the author studies twelve theories
    of varied linguistic and deductive strength. The theories are
    divided into two main types: the monoidal type, in which theories
    based on the common algebraic properties of conjunction and
    disjunction are investigated, and the Cartesian type, in which
    conjunction and disjunction have their proper meanings. In every
    chapter the author follows the same scheme. He first constructs a
    category of a certain type as an algebraic model for the class of
    formal proofs being considered. Then he proves a completeness
    theorem to the effect that the arrows of the constructed category
    can be represented by formal proofs in a Gentzen-style sequent
    calculus with cut elimination. In the propositional cases the
    algorithmic character of the cut-elimination process is used to
    provide an effective description of the arrows of the category
    constructed and to develop decision procedures, in the form of
    Church-Rosser theorems, for the commutativity of the finite
    diagrams of these categories. In the last chapter, the author also
    shows how to accommodate quantifiers in the calculus of adjoints
    and describes the topos-theoretic setting required in order to
    develop the proof theory of intuitionistic first-order logic.

The book itself contains a wealth of technical detail that includes
many dozens of claims whose proofs are not worked out in detail.  I'm
writing to ask whether anyone has any knowledge about the degree to
which this work was refereed and/or whether the results have been
verified independently.  I'm appealing especially to those who work in
categorical logic or those interested in automatic proof verification
in category theory, both of which groups, it would seem, should be
interested in Szabo's work.

-- 
Todd Wilson                               A smile is not an individual
Computer Science Department               product; it is a co-product.
California State University, Fresno                 -- Thich Nhat Hanh