From: Todd Wilson <twilson@csufresno.edu>
To: categories@mta.ca
Subject: Szabo's Algebra of Proofs
Date: Wed, 3 Jan 2001 13:54:57 -0800 (PST) [thread overview]
Message-ID: <14931.40881.870584.819395@goedel.engr.csufresno.edu> (raw)
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
next reply other threads:[~2001-01-03 21:54 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2001-01-03 21:54 Todd Wilson [this message]
2001-01-03 23:49 ` Tom Leinster
2001-01-04 0:47 ` Robert A.G. Seely
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=14931.40881.870584.819395@goedel.engr.csufresno.edu \
--to=twilson@csufresno.edu \
--cc=categories@mta.ca \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).