Intuitionistic Logic in the Calculus of Structures

In this note I present a system for (minimal) intuitionistic logic and some ideas about it.


S ::=  t | a | (S,S) | <S,S>

The constant true is "t", conjunction is "(-,-)" and implication is "<-,->". Sorry for not sticking to standard notation, but outfix connectives are much more readable even in relatively small derivations.

(S1,...,Sn) abbreviates some formula which is composed by using only conjunction and exactly one occurence of each Si.
<S1,...,Sn> abbreviates <(S1,...,Sn-1),Sn>.

Positive contexts, S+{ }, and negative contexts, S-{ }, are defined as usual.


The constant t is unit for conjunction and left unit for implication.
Conjunction is associative and commutative, implication is neither.

currying   <(R,T),U> = <R,<T,U>>

System IS






or simpler


The dual of a rule is obtained from by exchanging premise and conclusion and reversing the polarity restriction on the context. The rule i^ is the dual of i_ and is called cut. System SIS is obtained from system IS by adding the dual for each rule. There is perfect duality in the system, so where does the asymmetry of intuitionistic logic hide? It hides in the fact that the empty context is positive. Thus we can't dualise derivations as we can in classical logic, and the law of contraposition is not derivable in that way.

Soundness, Completeness, Cut admissibility

It's all true. We can translate back and forth between derivations in LJ+cut and derivations in IS+cut, without introducing any new cuts when going from sequent calculus to calculus of structures.

Derivations in LJ+cut are easily translated by induction on the proof tree, there are only three non-obvious cases: the and-right rule, the cut rule, and the implication-left rule. The first is derived by using currying and s-and_.

Cut, i.e.

Gamma |- A         A, Delta |- C
    Gamma, Delta |- C

is derived as follows:


    = --------------------------
s-and_-------------------------- (twice)

    = ------------------------------
    = ------------------------------
   i^ --------------------------
    = ----------------------

and the rule implication-left, i.e.

Gamma |- A         B, Delta |- C
   A implies B, Gamma, Delta |- C

is derived as follows:

    = --------------------------

    = --------------------------


Identity and Cut are derivable for their atomic versions and {s-and,s-imp}. Finding local rules to replace contraction is still an open problem.

Computational Interpretation of Cut Elimination

I don't know yet. Here's some speculation.

Functional composition is not composing two proofs via cut-rule, but should be composing two derivations in the obvious way:

|                A
B                |
       ->        B
B                |
|                C

Computation should then be the pushing up of up-rules inside the lower derivation. This is very much in the spirit of natural deduction, where computation is not the elimination of an admissible rule, but transforming successions of elimination and introduction rule. A derivation is normal if it contains no up-rules below down-rules. So, the composition of two normal ("cut"-free) derivations is not necessarily normal. Moving up w^ corresponds to normalising successions of and-intro and and-elim rules in natural deduction. So we can (trivially) represent booleans as in system F.  The interesting case is of course to represent natural numbers somehow using i^, and that's the problem. The rule c^ looks like a sharing operator.