The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, May 24, 2016 at 1:10 PM, Gabriel Scherer
<gabriel.scherer AT gmail.com>
 wrote:
> 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).

I realize ND_cut is technically redundant given ND_cond_proof and
ND_modus_ponens; I kept it in because often it's the natural way to
formalize an argument.  In other words, for much the same reason most
functional programming languages provide a let construct, even if it's
technically redundant given λ definitions of functions and function
applications (and even if behind the scenes the particular language
implements it as syntactic sugar around the combination).

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

Huh, I thought the whole point of Sequent Calculus was that without
cuts in the system, it's much easier to do things like prove
consistency or "⊢ P ∨ Q implies ⊢ P or ⊢ Q" or do proof searches.  The
reference I read (which I can't seem to Google up anymore) motivated
Sequent Calculus with cuts via some notional construction I didn't
really understand.  (I tend to think of it in terms closer to a
restriction to proof terms in normal form – though some of the rules
aren't precisely normal-form terms when converted to type judgement
rules, and conversely some things I'd consider normal form are
disallowed.)  Then it proved the cut elimination theorem, then
essentially said "given that theorem, from now on our Sequent Calculus
system will be the cut-free version".  So, as I understood it, Sequent
Calculus was meant not to be a practical system for proof building,
but as a theoretical tool for proving consistency or proving
completeness of proof search algorithms like the "tauto" tactic.  In
much the same way a Hilbert-style proof system might be good for some
theoretical purposes (though not any I can think of off the top of my
head), but without the "abstraction elimination" theorem it's painful
to actually prove much of anything in it directly, and with free use
of that theorem you might as well just be writing down a serialization
of a natural deduction argument.

In any case, this is a bit off topic to my primary question, which is
about what the typical notation is for the different proof systems,
especially when giving statements relating two different systems.
-- 
Daniel