A Problem of Normal Form in Natural Deduction
Jan von Plato · Mathematical logic quarterly · 2000
Recently Ekman gave a derivation in natural deduction such that it either contains a substantial redundant part or else is not normal. It is shown that this problem is caused by a non-normality inherent in the usual modus ponens rule.