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