Re-2: [Logiweb] Side conditions

[Frederik Eriksen]

Klaus Ebbe Grue wrote:

>> 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.
>
Hi Klaus,

It worked! Thanks for the tip.

Best Regards
Frederik.