Pedagogical Natural Deduction Systems: the Propositional Case
Loïc Colson (L.I.T.A. University of Metz, France)
David Michel (L.I.T.A. University of Metz, France)
Abstract: 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.
Keywords: constructive mathematics, mathematical logic, natural deduction, negationless mathematics, typed λ-calculus
Categories: F.1.1, F.4.1