Pedagogical Second-order Propositional Calculi
Loïc Colson, David Michel · Journal of Logic and Computation · 2007
The present work 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 an example. Technically speaking, we replace the rule (Hyp): with the rule (PHyp): with σ denoting a substitution replacing all variables of Γ with an example. This substitution is called the motivation of Γ. These systems are in essence negationless. In the present article, we study the second-order propositional calculus, since it is the simplest non-trivial natural deduction system in which the negation is definable. Some pedagogical versions of the second-order propositional calculus are proposed. We argue that these pedagogical calculi are negationless and we study their expressive power.