The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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