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