Discussion:
[isabelle] "natural deduction" vs. Gentzen-style
(too old to reply)
Andreas Röhler
2016-07-11 08:23:55 UTC
Permalink
Raw Message
Hi,
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.
Cheers,
Andreas
Andreas Röhler
2016-07-11 09:30:36 UTC
Permalink
Raw Message
Dear Andreas,
Post by 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 athttp://incredible.pm/ which is an incredibly
natural way of doing proofs!
It is also more fun than worrying about names.
Cheers,
Joachim
Hallo Joachim,

was introduced to your work thanks to our meetup in Berlin:
http://www.meetup.com/Logic-Types-and-Programs/events/231039680/

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.



A

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

Cheers,

Andreas,
who still tries to reconcile his stomach with logic

Loading...