[Logiweb] Side conditions

[Klaus Ebbe Grue]

Hi Frederik

> Suppose you've proven a lemma called "Lemma A" which has the form
>
> SIDECOND-1 |= SIDECOND-2 |= (whatever Lemma A states)
>
> where SIDECOND-1 and -2 are two side conditions. Suppose further that you 
> want to use Lemma A to prove a lemma called "Lemma B". The side condition 
> SIDECOND-1 happens to be necessarily true in the context of Lemma B; however, 
> SIDECOND-2 is not necessarily true. Is there any way to prove
>
> SIDECOND-2 |= (whatever Lemma B states)   ,
>
> or will you have to make do with the weaker claim
>
> SIDECOND-1 |= SIDECOND-2 |= (whatever Lemma B states) ?

It is indeed possible in the underlying 'Logiweb sequent calculus'.

The problem is to figure out how to write the proof using 'medium level 
proofs' (base page, Section 6.8.2). Maybe the following works:

---

X lemma Lemma A': SIDECOND-2 |= SIDECOND-1 |= (whatever Lemma A states)

X proof of Lemma A':
L01: Side-condition >> SIDECOND-2 ;
L02: Side-condition >> SIDECOND-1 ;
L03: Lemma A modus probans L02 modus probans L01 >> (what Lemma A states)

X proof of Lemma B:
L01: Side-condition >> SIDECOND-2
...
L17: Lemma A' modus probans L01 >> (whatever Lemma A states)
...

---

The trick is to swap the side conditions so that the modus probans in line 
L17 in the proof of Lemma B connects the side condition from line L01 with 
the right side condition in Lemma A, c.f. line 5 of the definition of 
conclude_3 in Section 6.8.6 of the base page which says that
   (x |= y) modus probans z
gives rise to unification of x and z whereas
   (x |= y) applied to anything but modus probans
gives rise to evaluation of x.

If my suggestion does not work, try putting the page on Logiweb and post 
its reference.

-Klaus