categories - Category Theory list
 help / color / mirror / Atom feed
From: "Jean-Pierre Marquis" <jean-pierre.marquis@UMontreal.CA>
To: <categories@mta.ca>
Subject: RE: Semantic tableaux and intuitionistic logic
Date: Mon, 9 Jun 2003 10:05:01 -0400	[thread overview]
Message-ID: <EDEJIMOKNCPHKICKNMEPOEEGCGAA.jean-pierre.marquis@umontreal.ca> (raw)

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








             reply	other threads:[~2003-06-09 14:05 UTC|newest]

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2003-06-09 14:05 Jean-Pierre Marquis [this message]
  -- strict thread matches above, loose matches on Subject: below --
2003-06-06  8:13 Thomas Streicher
     [not found] <Law10-F92545aW1OHBt00034f9f@hotmail.com>
2003-06-02 20:08 ` Galchin Vasili
2003-05-30 20:14 Galchin Vasili
2003-06-02 13:02 ` jlipton

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=EDEJIMOKNCPHKICKNMEPOEEGCGAA.jean-pierre.marquis@umontreal.ca \
    --to=jean-pierre.marquis@umontreal.ca \
    --cc=categories@mta.ca \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).