Sun Aug 30 15:44:55 CEST 2009

Proof Calculus

A proof calculus[2] corresponds to a family of formal systems that use
a common style of formal inference for its inference rules.  A rule of
inference[3] (also called a transformation rule) is a syntactic rule
used in a formal system which is used to produce valid statements
within that system.  Examples of proof systems:

  * Hilbert-style deduction system[4], where a formal deduction is a
    finite sequence of formulas in which each formula is either an
    axiom or is obtained from previous formulas by a rule of

  * Natural deduction[5] is an approach to proof theory that attempts
    to provide a deductive system which is a formal model of logical
    reasoning as it "naturally" occurs.  This approach is in contrast
    to axiomatic systems which use axioms.

The sequent calculus[1] is a widely known proof calculus for
first-order logic.  The term "sequent calculus" applies both to a
family of formal systems sharing a certain style of formal inference,
and to its individual members, of which the first, and best known, is
known under the name LK, distinguishing it from other systems in the
family.  The sequent calculus LK was introduced by Gerhard Gentzen as
a tool for studying natural deduction.

In the sequent calculus all inference rules have a purely bottom-up
reading.  In natural deduction the flow of information is
bi-directional: elimination rules flow information downwards by
deconstruction, and introduction rules flow information upwards by
assembly. Thus, a natural deduction proof does not have a purely
bottom-up or top-down reading, making it unsuitable for automation in
proof search, or even for proof checking (or type-checking in type
theory). [5]

In Kleene's Metamathematics, Chapter V, p.86[6] ``The labour required
to establish the formal provability of formulas can be greatly
lessened by using metamathematical theorems concerning the existence
of formal proofs.''

-- remarks

The way I understand this is that natural deduction has no axioms (no
primitive assumptions) but contains all its structure in the inference
rules: the way propsitions can be combined to create new propositions.
In contrast, a Hilbert-style deduction system has both axioms and
inference rules (i.e. Modues Ponens).

Reading more in [6].  It seems that meta-mathematics is quite similar
to lisp macros: the meta math serves the purpose to abstract over the
_construction_ of formal proofs = meaningless pure syntax.  Because
formal logic's composition mechanisms at the foundations of
mathematics are so barbaric, a macro system makes sense to lift the

What I find surprising however is that this meta system itself is
_not_ formal: proofs in the meta system are not formal proofs, but are
intuitive justifications of correctness.  I'd say this is because of
the chicken-and-egg problem: you can't use a formal system to do this,
because you don't _have_ one yet (remember, your using this meta-math
to _build_ a formal system).  This sounds like compiler bootstrapping
to me.

[1] http://en.wikipedia.org/wiki/Sequent_calculus
[2] http://en.wikipedia.org/wiki/Proof_calculus
[3] http://en.wikipedia.org/wiki/Inference_rules
[4] http://en.wikipedia.org/wiki/Hilbert_system
[5] http://en.wikipedia.org/wiki/Natural_deduction
[6] isbn://0720421039