Re: [isabelle] "natural deduction" vs. Gentzen-style



Dear Andreas,

Am Montag, den 11.07.2016, 10:24 +0200 schrieb Andreas RÃhler:
> IIUC what's called "natural deduction" dates back to Gentzen.
> Hence suggest to call it Gentzen-style. These proceedings are by no wayÂ
> natural, but artificial.
> When rules are declared natural, people tend to believe it in aÂ
> religion-like way - no longer disposed to throw away and replace theÂ
> model if not suitable.

I wholeheartedly agree that ânatural style deductionâ is a misnomer,
and it is far from natural to draw these trees, or alternatively these
strangle indented text lines with numbers and possibly vertical bars.

I recommend you look atÂhttp://incredible.pm/Âwhich is an incredibly
natural way of doing proofs!

It is also more fun than worrying about names.

Cheers,
Joachim



--Â
Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.