* Szabo's Algebra of Proofs
@ 2001-01-03 21:54 Todd Wilson
2001-01-03 23:49 ` Tom Leinster
0 siblings, 1 reply; 3+ messages in thread
From: Todd Wilson @ 2001-01-03 21:54 UTC (permalink / raw)
To: categories
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
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Szabo's Algebra of Proofs
2001-01-03 21:54 Szabo's Algebra of Proofs Todd Wilson
@ 2001-01-03 23:49 ` Tom Leinster
2001-01-04 0:47 ` Robert A.G. Seely
0 siblings, 1 reply; 3+ messages in thread
From: Tom Leinster @ 2001-01-03 23:49 UTC (permalink / raw)
To: categories
I don't know anything about the subject itself, but according to math. review
93a:03062 there's a paper by Barry Jay refuting one of Szabo's claims. The
paper is `Coherence in category theory and the Church-Rosser property',
Notre Dame J Formal Logic 33 (1992), no 1, 140-143.
Tom
Todd Wilson wrote:
>
> In the book
>
> M. E. Szabo, Algebra of Proofs, Studies in Logic and the
> Foundations of Mathematics, Vol. 88, North-Holland, 1978.
[...]
> 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.
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Szabo's Algebra of Proofs
2001-01-03 23:49 ` Tom Leinster
@ 2001-01-04 0:47 ` Robert A.G. Seely
0 siblings, 0 replies; 3+ messages in thread
From: Robert A.G. Seely @ 2001-01-04 0:47 UTC (permalink / raw)
To: categories
On Wed, 3 Jan 2001, Tom Leinster wrote:
>
> I don't know anything about the subject itself, but according to math. review
> 93a:03062 there's a paper by Barry Jay refuting one of Szabo's claims. The
> paper is `Coherence in category theory and the Church-Rosser property',
> Notre Dame J Formal Logic 33 (1992), no 1, 140-143.
The interested reader might also want to look at the recent paper by
Borisavljevic, Dosen and Petric ("On permuting cut with contraction")
in Math Struc in Comp Sci, Vol 10 (2000) (the Lambekfestschrift) which
corrects and amplifies another matter in the Szabo book.
-= rags =-
==================
R.A.G. Seely
<rags@math.mcgill.ca>
<http://www.math.mcgill.ca/rags>
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2001-01-04 0:47 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2001-01-03 21:54 Szabo's Algebra of Proofs Todd Wilson
2001-01-03 23:49 ` Tom Leinster
2001-01-04 0:47 ` Robert A.G. Seely
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).