Re: Semantic tableaux and intuitionistic logic

Re: Semantic tableaux and intuitionistic logic

[Thomas Streicher]

>     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

RE: Semantic tableaux and intuitionistic logic

[Jean-Pierre Marquis]

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

Re: Semantic tableaux and intuitionistic logic

[Galchin Vasili]

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

Semantic tableaux and intuitionistic logic

[Galchin Vasili]

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

Re: Semantic tableaux and intuitionistic logic

[jlipton]

Nerode, Shore: logic for Applications, Springer, has detailed tableau
development for intuitionistic, and modal logics: i.e. there is
nothing intrinsically classical about the method. The ideas go back to
Hintikka and Beth (at least) in the 1950s and 60s.



On Fri, 30 May 2003, Galchin Vasili wrote:

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

--------------------------------------------------------------------
Jim Lipton   Math Dept.Wesleyan University, Middletown,CT 06459-0128
             www.wesleyan.edu/~jlipton  jlipton@wesleyan.edu,
             (860) 685-2188 fax:685-2571
====================================================================