Subject: medial
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-02-12 16:01:20 GMT (1 year, 12 weeks, 5 days, 4 hours and 46 minutes ago)
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