Re: Semantic tableaux and intuitionistic logic

[Galchin Vasili <vngalchin@yahoo.com>]

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
> >