Intuitionistic Logic in the Calculus of Structures
In this note I present a system for
(minimal) intuitionistic
logic and some ideas about it.
Formulas
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.
Equations
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
S+{t}
i_----------
S+<R,R>
S-{t}
w_----------
S-{R}
S-(R,R)
c_-----------
S-{R}
S+(<R,T>,<U,V>)
s-imp_--------------------
S+<<T,U>,<R,V>>
or simpler
S+(T,<U,V>)
s-imp'_--------------------
S+<<T,U>,V>
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:
(<Gamma,A>,<(A,Delta),C>)
=
--------------------------
(<Gamma,A>,<Delta,<A,C>>)
s-and_-------------------------- (twice)
<(Gamma,Delta),(A,<A,C>)>
= ------------------------------
<(Gamma,Delta),(<t,A>,<A,C>)>
s-imp_------------------------------
<(Gamma,Delta),<<A,A>,<t,C>>>
=
------------------------------
<(Gamma,Delta),<<A,A>,C>>
i^
--------------------------
<(Gamma,Delta),<t,C>>
=
----------------------
<(Gamma,Delta),C>
and the rule implication-left, i.e.
Gamma |-
A B, Delta |- C
-----------------------------------
A implies B, Gamma, Delta |- C
is derived as follows:
(<Gamma,A>,<(B,Delta),C>)
=
--------------------------
(<Gamma,A>,<B,<Delta,C>>)
s-imp_--------------------------
<<A,B>,<Gamma,<Delta,C>>>
= --------------------------
<(<A,B>,Gamma,Delta),C>
Locality
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
|
A
B
|
->
B
B
|
|
C
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.