From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1773 Path: news.gmane.org!not-for-mail From: Tom Leinster Newsgroups: gmane.science.mathematics.categories Subject: Re: Szabo's Algebra of Proofs Date: Wed, 3 Jan 2001 23:49:05 +0000 (GMT) Message-ID: References: <14931.40881.870584.819395@goedel.engr.csufresno.edu> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018090 380 80.91.229.2 (29 Apr 2009 15:14:50 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:14:50 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Wed Jan 3 20:17:34 2001 -0400 Return-Path: Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f03NqKv30672 for categories-list; Wed, 3 Jan 2001 19:52:20 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f In-Reply-To: <14931.40881.870584.819395@goedel.engr.csufresno.edu> from "Todd Wilson" at Jan 03, 2001 01:54:57 PM X-Mailer: ELM [version 2.5 PL3] X-Scanner: exiscan *14DxeT-0000PR-00*U1gWsyiz2/U* http://duncanthrax.net/exiscan/ Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 3 Original-Lines: 28 Xref: news.gmane.org gmane.science.mathematics.categories:1773 Archived-At: 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.