Jason (jcreed) wrote,

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.
Tags: math, soundness, work
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded