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. Key Words: mathematical logic, negationless mathematics, constructive mathematics, natural deduction, typed λ-calculus

• Type: Journal
• Year: 2007
• Where: JUCS
• Authors: Loïc Colson, David Michel
• Keywords: JUCS 2007, Natural Deduction, Natural Deduction Systems, Pedagogical Natural Deduction