ABSTRACT
C o n s id e r as b e fo re th e L -s e n te n c e u : V £ 3 y v ( £ , y ) . I m a y assum e th a t no v a r ia b le fro m £ occurs b o u n d in v ( £ ,y ) because o th e rw is e an a p p lic a t io n o f a s u ita b le m ap t o t ( Y 1 | - ) w i l l t ra n s fo rm u in to a sentence in te rd e d u c ib le w i th u w h ic h does h a v e t h a t p r o p e r ty ; th u s £ (y , f ( £ ) ) is fre e fo r v ( £ , y ) . C o n s i d e r th e e x te n d e d la n g u a g e L f a n d th e d e f in it io n u b V £ v ( £ , f ( £ ) ) . A s s u m e f ro m n o w on t h a t G is se t o f L -s e n te n c e s w h ic h G p ro v e s b o th u a n d
u n : v ( £ , x ) A v ( £ ,y ) -> x = y .
