Re: Semantic tableaux and intuitionistic logic
The reason why I suggested that the Law of Excluded Middle is required is that reductio ad absurbdum is the core concept in Tableaux or to put it another way Tableaux is built around bivalent logic. Regards, Bill --- Christopher Townsend <cft71@hotmail.com> wrote:
I can only remember Tableux from many years ago, but I don't think that their structure forced you to use the excluded middle? Can't you just drop the excluded middle as a deduction rule and then use whatever is left over as a constructive propositional theory?
Regards, Christopher Townsend
From: Galchin Vasili <vngalchin@yahoo.com> To: categories@mta.ca Subject: categories: Semantic tableaux and intuitionistic logic Date: Fri, 30 May 2003 13:14:01 -0700 (PDT)
Hello,
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).
Regards, Bill Halchin
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
The following references might be of some interest: Bell, J.L. & DeVidi, D., Solomon, G., 2001, Logical Options, Broadview Press. Marcello D'Agostino, Dov M. Gabbay, Reiner Hahnle, Joachim Posegga, 1999, Handbook of Tableau Methods, Kluwer Academic Pub. Jean-Pierre Marquis -----Message d'origine----- De : cat-dist@mta.ca [mailto:cat-dist@mta.ca]De la part de Thomas Streicher Envoye : 6 juin, 2003 04:14 A : categories@mta.ca Objet : categories: Re: Semantic tableaux and intuitionistic logic
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
participants (3)
-
Galchin Vasili -
Jean-Pierre Marquis -
Thomas Streicher