From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2336 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Semantic tableaux and intuitionistic logic Date: Fri, 6 Jun 2003 10:13:44 +0200 (CEST) Message-ID: <200306060813.KAA04256@fb04209.mathematik.tu-darmstadt.de> 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 1241018588 3654 80.91.229.2 (29 Apr 2009 15:23:08 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:23:08 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Fri Jun 6 17:21:04 2003 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 06 Jun 2003 17:21:04 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 19ONbk-0004IG-00 for categories-list@mta.ca; Fri, 06 Jun 2003 17:14:40 -0300 X-Mailer: ELM [version 2.4ME+ PL66 (25)] X-MailScanner: Found to be clean Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 27 Original-Lines: 25 Xref: news.gmane.org gmane.science.mathematics.categories:2336 Archived-At: > I am only familiar with semantic tableaux for > classical propositional logic (and classical 1st order > logic). It seems that as an inference system it is > based squarely around the law of the excluded middle > because it is essentially reductio ad absurdum. Hence, > as an inference system it can't be simply modified for > intuitionistic propositional calculus?? (Of course, I > am bringing this because the role that Heyting > algebras play in Topos theory). the point is that tableau calculus may be best understood as a search for cut-free proofs in either classical or intuitionistic logic; this fact is systematically overlooked in the literature on tableaux methods like in the logic programming community one hardly ever finds exposed the view that executing a logic program is nothing but unravelling an inductive definition for information on tableau methods from a proof-theoretic point of view see Troelstra & van Dalen's book "Constructivism in Mathematics" vol.2, the chapter on proof theory of intuitionistic logic Best, Thomas