medial

Hi Frogs,

I'd like to announce a new result about medial, namely, a precise 
characterization in terms of relation webs, when there is a derivation 
from a formula P to a formula Q using only medial, i.e.,

        P
        |
    {m} |
        |
        Q

where m is the inference rule

    S[(A,B),(C,D)]
  m --------------
    S([A,C],[B,D])

The details of the characterization, which uses relation webs, can be 
found here:
http://www.lix.polytechnique.fr/~lutz/papers/CharMedial.pdf

An interesting application is a purely combinatorial proof of a 
decomposition theorem for KS, namely, that every proof

     _
     |
  KS |
     |
     A

can be decomposed into a proof

     _
     |
ai_ |
     |
     F
     |
   s |
     |
     E
     |
   m |
     |
     C
     |
ac_ |
     |
     B
     |
  w_ |
     |
     A

for some formulas B,C,D,F.

So, we finally can prove decomposition for classical logic without using 
the permutation of inference rules.

Cheers,
Lutz