The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Your Natural Deduction has a cut rule, and I find this uncommon. The elimination rules of natural deduction already contain cuts, in a sense, so you should not need a cut rule. In particular, a cut can be macro-expressed as the composition of an implication introduction and an implication elimination, which in a term syntax corresponds to the fact that (let x := t in u) can be rewritten locally into ((fun x => u) t).

On the other hand, your Sequent Calculus presentation does not have a cut rule, and this is also uncommon. Sure, cuts can be eliminated, but this requires a global (rather than local) transformation, so you cannot really build proofs in a modular way without using cuts (or the cut-elimination meta-transformation).

On Tue, May 24, 2016 at 3:53 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

I've been developing formal proofs of equivalence of some of the major
proof systems for pure propositional logic (no quantifiers, and
probably with minor variations from their "official" versions).  But
since I'm learning some of the theorems and systems from online
reading, I'm not at all sure if I'm using standard notation for the
systems.  Right now, I have:

Γ ⊢ P  for natural deduction
Γ ⊢c P  for "classical" natural deduction (so, not equivalent to the
others, but I proved the equivalence with Γ ⊢ ¬¬P)
Γ ⊢h P  for a Hilbert-style proof system
Γ ⇒ P  for sequent calculus (the version with exactly one sequent
allowed on the right hand side)
Γ ⇒* P  for LJT* of Roy Dyckhoff (as cited in the Coq reference manual
in the description of the tauto tactic)

The development is on GitHub:
https://github.com/dschepler/coq-sequent-calculus .

Anyway, I was hoping with a lot of people on this list being more
expert in these topics than I am, I could get some input on this.
--
Daniel Schepler