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

On 11.07.2016 10:36, Joachim Breitner wrote:
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  which is an incredibly
natural way of doing proofs!

It is also more fun than worrying about names.


Hallo Joachim,

was introduced to your work thanks to our meetup in Berlin:

Really should learn from your tuning of the haskell-compiler still. ;)

Well, have some questions which would apply to many of logical systems nowadays: The most crucial probably is deriving from bottom --which equals to false IIUC-- Start of Session 4.



If this is permitted, everything is derivable. Where would it make sense?


who still tries to reconcile his stomach with logic

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