Sat Sep 10 20:49:38 EDT 2011


I know very little of mathematical logic.  When I think of logic, I
mostly think of boolean algebra and logic gates.

The thing is that, being educated as an engineer and not a
mathematician, I'm very much biased towards semantics (sets and
functions), or maybe even more the relationship between some
mathematical structure and the measurable reality it models.

Semantically, Boolean algebra talks about operations (functions)
B^n->B, defined on the set of truth values B = {0,1} and its powers.
It is the model for logic gates.  Such a system is easy to work with
in a muddy intuitive way because it is feasible to exhaustively verify
correctness of expression manipulations.

However, the approach used in formal logic is axiomatic.  The point of
an axiomatic system is to provide a means to derive new expressions
(theorems) from a collection of initial expressions and rules of
inference/construction.  Such a system is called a "calculus".  A
derivation that leads from axioms to theorems is called a proof.

In [1] Wadler mentions that:

    In a single landmark paper Genzen (1935) introduced the two
    formulations of logic most widely used today, natural deduction[3]
    and the sequent calculus[2], in both classical and intuitionistic

Reading further, it seems that the importantance of the sequent
calculus is mostly because of the cut-elimination theorem[4] which is
about "composition of proofs": if there exists a chain of proofs that
can be combined using the cut rule, there also exists a direct proof.

[1] http://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf
[2] http://en.wikipedia.org/wiki/Sequent_calculus
[3] http://en.wikipedia.org/wiki/Natural_deduction
[4] http://en.wikipedia.org/wiki/Cut-elimination_theorem
[5] http://en.wikipedia.org/wiki/Boolean_algebra_(logic)