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



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




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