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