[Logiweb] Removing object quantifiers

[Klaus Ebbe Grue]

Hi Frederik,

> I've tried to prove the following lemma, using system S from Klaus's "check" 
> page:
>
> Lemma Tester: Pi V : (FORALL V. V=V) => V=V
>
> 'V' is a meta variable ('meta v') and  'FORALL'  is the object quantifier 
> from the "check" page ('for all * indeed *'). I'm using  Repetition and the 
> Ded-rule in the proof, but it's not working. Any suggestions? (For more 
> details about my proof, see the very bottom of the "eriksen/frozen" page).

One problem is that V in "(FORALL V. V=V) => V=V" can denote *any* term. 
One would expect the lemma to hold only when V denotes an object variable 
(which would require a side condition on V).

But one thing that works is:

Lemma Test: Pi V : (FORALL v. v=v) => V=V

Proof:
L01: Arbitrary >> V;
L02: Block >> Begin;
L03: Premise >> v=v;
L04: Repetition |> L03 >> v=v;
L05: Block >> End;
L06: Ded |> L05 >> (FORALL v. v=v) => V=V

Above, v is the object variable 'object v' whereas V is the meta variable 
'meta v'. I hope you can do with that lemma. The benefit of the lemma is 
that it is easy to prove. A drawback is that it fixes the object variable 
in the premise. For a page with the lemma and proof above see
http://www.diku.dk/~grue/logiweb/20060417/home/grue/eriksen

The deduction rule puts a FORALL on all object variables in premisses and 
allows arbitrary instantiation of object variables in the conclusion (as 
long as intantiation does not lead to variable clashes).

Cheers,
Klaus