Deep inference

I've read several deep inference papers and I've been wondering whether there's a common thread here.

I collected bunch of deduction systems from different papers to compare them. Most of these papers were picked up for me by people on proglangdesign irc channel.

If you wonder what different notations mean, refer to the original papers.

This first system seemed to have started the whole thing. It is from the paper "A System of Interaction and Structure".

Symmetric basic system SBV (ai, q, s)
Basic system \/ BV (o, ai, q, s)

S<[R,T]; [U,W]>
--------------- q↓
S[<R;U>, <T;W>]

S(<R;U>, <T;W>)
--------------- q↑
S<(R,T); (U,W)>

S([R,T],G)
---------- s
S[(R,G),T]

S{o}
------- ai↓
S[a,~a]

S(a,~a)
------- ai↑
S{o}

--- o↓
 o

BV presents a system of multiplicative linear logic extended with a non-commutative self-dual logical operator. The claim is that this extension would be difficult to express with sequent calculus alone.

The next system is from the paper "An Algorithmic Interpretation of a Deep Inference System". It presents a combinator system that directly represents open-deduction proofs with small programs. Kai Bruennier, one of the authors of that paper, has written a small easy-to-read scala program dicomb that shows out how an interpreter can be written around normalising these proof-encodings.

  A
----- c
A ∧ A

A ∧ B
----- w1
  A

A ∧ B
----- w2
  B

     B
----------- i
A ⊃ (B ∧ A)

(A ⊃ B) ∧ A
----------- e
     B

Interestingly, the paper "Atomic lambda-calculus: a typed lambda-calculus with explicit sharing" also provides this kind of an intuitionistic-logic system.

     B
------------ λ
A -> (A ∧ B)

A ∧ (A -> B)
------------ @
     B

     A
----------- c
A ∧ ... ∧ A

The rules seem identical but the system is constructed slightly differently to make it resemble lambda calculus.

The next one was represented in the paper "Deep Inference and Symmetry in Classical Proofs". It's intended for propositional logic, and the paper also provides an extension to predicate logic.

Deep inference for propositional logic, system SKS

  t
------ ai↓
a ∨ ¬a

a ∧ ¬a
------ ai↑
  f

A ∧ (B ∨ C)
----------- s
(A ∧ B) ∨ C

(A ∧ B) ∨ (C ∧ D)
----------------- m
(A ∨ D) ∧ (B ∨ D)

f
- aw↓
a

a
- aw↑
t

a ∨ a
----- ac↓
  a

  a
----- ac↑
a ∧ a

The medial rule seem to have special significance that will be apparent if you look into subatomic proof systems.

Finally I look at the CL16 system from the paper "Elementary-base cirquent calculus I: Parallel and choice connectives". there's a deep inference system as well.

A ∧ B
----- commutativity (also for parallel disjunction (∨))
B ∧ A

A ∧ (B ∧ C)
----------- associativity (also for parallel disjunction (∨))
(A ∧ B) ∧ C

  A
----- identity ∧
A ∧ t

  A
----- identity ∨
A ∨ f

  f
----- domination ∧
A ∧ f

  t
----- domination ∨
A ∨ t

A    B
------ choosing
A ⊔c B

A ⊓c B     B ⊓c C
----------------- cleansing
A ⊓c B ⊓c B

(A ∨ C) ∧ (B ∨ C)
----------------- distribution ∧
(A ∧ B) ∨ C

(A ∨ C) ⊓c (B ∨ C)
----------------- distribution ⊓ 
(A ⊓c B) ∨ C

   t
------ trivialization {p is elementary letter}
¬p ∨ p

((A ∧ (C ⊓b D)) ⊓a (B ∧ (C ⊓b D))) ⊓c (((A ⊓a B) ∧ C) ⊓b ((A ⊓a B) ∧ D))
------------------------------------------------------------------------ quadrilemma
(A ⊓a B) ∧ (C ⊓b D)

A    B
------ splitting {c does not occur in A, B}
A ⊓c B

This system branches at choicepoints. I may have misunderstood the paper, but it'd seem to be the case. It makes sense though, the conjunctive/disjunctive choice operators here are resembling the additive disjunction/conjunction from linear logic. It might actually be necessary to treat them like this, even under a deep inference system.

A lot of the rules seem to be similar enough that I might not be surprised to see them appear in a same system.

Computability logic has specific semantic to conjunctive and disjunctive choice. To have a proof, certain conditions must happen. Disjunctive choice is a game where you choose one formula, one you can win. Conjunctive choice is a game where you have to prepare to win any one of the formulas in the conjunction.

How should the proof represent how the choice is done?

I'm not sure what to make out of this yet.

Similar posts