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.
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