Re: Semantic tableaux and intuitionistic logic

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

>     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