The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Feb 19, 2018 at 6: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.

I have a development of both under
https://github.com/dschepler/coq-sequent-calculus .  It's not
extremely well commented, though, so I'm not sure how useful it would
be for beginners.

> 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

Well, my development actually made an inductive proposition of
provability - but it would hopefully be simple enough to change that
to a type of proof objects if needed.

> 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).

I think that might be mixing up the formal structure of an implication
proof on the one hand, and the interpretation of such a proof as a
function on the other.  In particular, my ND_proves proposition is a
function "list (prop atom) -> prop atom -> Prop" of both a context and
a goal, with the context being a crucial ingredient because in natural
deduction proofs, the context to the left of the turnstyle varies
through the different parts of the proof tree.  In particular, the
form of an implication proof is:

| ND_cond_proof {Γ P Q} :
  P :: Γ ⊢ Q ->
  Γ ⊢ P ⊃ Q

And then I didn't develop this explicitly, though I did develop an
interpretation in terms of Heyting algebras which could be adapted.
But the interpretation of a proof object in Γ ⊢ P as a function in the
sense of Curry-Howard would look something like an element of
(fold_left (fun (Q : prop) (X : Type) => prop_interp Q -> X) Γ
(prop_interp P)) where
Variable type_assign : atom -> Type.
Fixpoint prop_interp (P : prop atom) : Type :=
match P with
| atom_prop x => type_assign x
| bot_prop => Empty_set
| top_prop => unit
| and_prop Q R => prop_interp Q * prop_interp R
| or_prop Q R => prop_interp Q + prop_interp R
| impl_prop Q R => prop_interp Q -> prop_interp R  (* <- this term is
probably what you were thinking of *)
end.

In this formulation, the interpretation types of both sides of
ND_cond_proof end up being pretty much the same, so the corresponding
map of interpretation types would just be essentially the identity
map.

> 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.

I think the definition of ND_proves (or classic_ND_proves in
ClassicalND.v) should be straightforward enough to read.  And it would
be easy to play around with constructing proofs using the proof rules
- I don't remember having too many examples of intuitionistic natural
deduction, except as steps in equivalence proofs with my formulations
of sequent calculus and with a Hilbert-style proof system.  But in
ClassicalND.v, I do have example proofs of excluded middle and
Peirce's law based on the classical proof rule of "proof by
contradiction".  For this part, what I wrote above about Curry-Howard
style interpretations of proof objects as functions wouldn't be needed
at all.

Though be warned I did make a few choices which are apparently
nonstandard.  For example, my formulation includes an explicit cut
rule even though it could easily be deduced from a combination of the
"conditional proof" and "modus ponens" rules.  (This was because my
intended interpretation of this proof rule was more like "let x :=
interp phi in interp psi" rather than "(fun x => interp psi) (interp
phi)".)  On the other hand, the version of sequent calculus I
presented is a cut-free version since my goal there was to formalize a
proof of the cut elimination theorem.

(Also, I developed that in Coq 8.5, I think, so I can't promise all
the proofs would still work in the latest Coq version.)
-- 
Daniel Schepler