Re: Minimal logic valid?

Jan Burse <janburse@xxxxxxxxxxx> writes:

Alan Smaill schrieb:

The derive it from contradiction and
proof by cases.
This rather suggests that single succedent sequent calculus
does not correspond to natural deduction ...

Yes, and 2+2=4 indicates that 4 belongs not
to peano arithmetic, as it is derived and not
builtin.

I agree that wasn't a convincing suggestion --
but there is a serious point to be made here, however ...

You did suggest that single succedent sequent calculus corresponds to
natural deduction, yet the most natural system obtained from classical
sequent calculus under that restriction is still a sequent calculus
system (for intuitionist logic). Pointing out the existence of a
single succedent sequent calculi for classical logic was
not convincing on your part either.

I welcome arguments to the contrary.

Bye

--
Alan Smaill
.

Relevant Pages

  • Re: Help with proof in Gentzens system NK
    ... corresponding notions in natural deduction. ... I was hoping that normal form for classical natural deduction would be ... analogous enough to cut-free for classical sequent calculus that we ... is a contradiction in terms, ...
    (sci.logic)
  • Re: Minimal logic valid?
    ... implication, if possible. ... But it surely looks more like sequent calculus than natural deduction. ...
    (sci.logic)
  • Re: Minimal logic valid?
    ... So my system is natural deduction. ... sukzedent sequent calculus. ...
    (sci.logic)
  • Re: Minimal logic valid?
    ... is that natural deduction is single ... sukzedent sequent calculus. ... The usual view, going back to Gentzen, is that intuitionistic sequent ...
    (sci.logic)
  • Re: Minimal logic valid?
    ... The usual view, going back to Gentzen, is that intuitionistic sequent ... Ebbinghaus and Flum have a single succedent ... sequent calculus by a simple restriction on the shape of the ... does not correspond to natural deduction ... ...
    (sci.logic)
Quantcast