JUCS - Journal of Universal Computer Science 13(10): 1396-1410, doi: 10.3217/jucs-013-10-1396
Pedagogical Natural Deduction Systems: the Propositional Case
expand article infoLoïc Colson‡, David Michel‡
‡ L.I.T.A. University of Metz, Metz, France

Corresponding author: Loïc Colson ( colson@univ-metz.fr )

© Loïc Colson, David Michel.
This article is freely available under the J.UCS Open Content License.
Citation: Colson L, Michel D (2007) Pedagogical Natural Deduction Systems: the Propositional Case. JUCS - Journal of Universal Computer Science 13(10): 1396-1410. https://doi.org/10.3217/jucs-013-10-1396
Open Access
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
mathematical logic, negationless mathematics, constructive mathematics, natural deduction, typed λ-calculus