The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Another way to ask the question: Are there some good pedagogical explications out there of formalizations of natural deduction proof systems, including "-> introduction" as an inference rule, appropriate for early undergraduates, not advanced undergrads or graduate students? And thank you, Stefan, for pointing to the cool "game". I'll give it a go. --Kevin

On Mon, Feb 19, 2018 at 9:16 AM, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

​ I'm looking for a simplest way to teach my early undergraduate students about natural deduction and/or sequent calculus proof objects without having to get into lambda terms and type systems.

The following "POPL tutorial" suggests a standard solution:  formalize proofs  as values of an inductive type, where the constructors mirror the rules of inference.

http://twelf.org/wiki/POPL_Tutorial/Sequent_vs_Natural_Deduction#Syntax_for_Propositions​

The rule for implication introduction says (naturally enough) that if you have a function from proofs of A to proofs of B, you can construct a proof of (Impl A B).

A straightforward translation of this into Coq, as copied right below this sentence, results in a non-positivity error for the encoding of this inference rule.

/* variables */

Inductive var := mk_var: nat -> var.

/* propositions in my minimal propositional logic */

Inductive prop :=

   | atom: var -> prop

   | and: prop -> prop -> prop

   | impl: prop -> prop -> prop.

/* proof rules */

Inductive proof: prop -> Type  :=

  | axiom: forall A: prop, proof A

  | andIntro: forall A B: prop, proof A -> proof B -> proof (and A B)

  | andElimL: forall A B: prop, proof (and A B) -> proof A

  | andElimR: forall A B: prop, proof (and A B) -> proof B

  | implElim: forall A B: prop, proof A -> proof (impl A B) -> proof B

  | implIntro: forall A B: prop, (proof A -> proof B) -> proof (impl A B). (* oops!!! *)

What would be the canonical way to represent the same ideas in Coq in a way that works?

Again, the aim is a super-straightforward pedagogical explication of rules of natural deduction (or sequent calculus), for a propositional logic only, with the ability to "play around" by building proof terms by explicit application of introduction and elimination inference rules. 

Kevin