Pedagogical Second-order Propositional Calculi

摘要

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): (F∈Γ)/(Γ⊥F)(Hyp) with the rule (P-Hyp): (F∈Γ⊥δ·Γ)/(Γ⊥F)(p-Hyp) 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.