Pedagogical natural deduction systems: the propositional case
This paper introduces the notion of pedagogical natural deduction systems, which are natural deduction systems with the following additional constraint: all hypotheses made in a proof must be motivated by some example. It is established that such systems are negationless. The expressive power of the pedagogical version of some propositional calculi are studied.
natural deduction mathematical logic negationless mathematics constructive mathematics typed lambda-calculus