Email Gateway (Aug 22 2022 at 13:45): Email Gateway (Aug 22 2022 at 13:45):From: Andreas Röhler <andreas.roehler@easy-emacs.de>
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
Email Gateway (Aug 22 2022 at 13:45):From: Joachim Breitner <breitner@kit.edu>
Dear Andreas,
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
signature.asc
Email Gateway (Aug 22 2022 at 13:45):From: Andreas Röhler <andreas.roehler@easy-emacs.de>
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
Last updated: Nov 21 2024 at 12:39 UTC