|
[Aug. 4th, 2005|06:32 pm]
Jason
|
Cautiously optimistic that I have a solution to the problem mentioned yesterday, the soundness of the labelled sequent calculus (hereafter L) relative to the multiple-conclusion sequent calculus (hereafter M), from which follows its soundness relative to plain-ol' vanilla intuitionistic logic (hereafter I).
This is, of course, like the 17th likely candidate proof I've come up with in the last few days of thinking about it, and I don't have to tell you how the previous 16 fared. Nonetheless, the character of this proof approach strongly resembles the known proof of soundness of M relative to I, in that it involves using the propositional machinery available in the destination calculus (in this case M) to express the judgemental machinery of the source language (in this case L).
So from M to I, the induction hypothesis is
If G |- B1,B2,...,Bm is provable in M, then G |- B1 v B2 v ... v Bm is provable in I
and it just takes some mundane distributivity lemmas and liberal application of the cut-elimination lemma to prove the soundness theorem.
My approach from L to M has a significantly more complicated mapping from L-sequents to M-sequents, but on the two important invertible right rules in L (implication and disjunction) it causes those rules to map to the trivial rule in M, just as or-right in M is mapped to the trivial rule in I. Signs like these make me optimistic I've got something right. |
|
