8.5.17 Quantify

Prev Up Next Page 342 of 800 Search internet

The quantify operator All x : C is similar to the infer and endorse operators. The quantify operator can be used for replacing lines containing the keyword 'Arbitrary'.

In the section on using lemmas in argumentations, we proved ME1.47a using a variant M1.8f of M1.8a. M1.8f says All #x : #x imply #x whereas M1.8a just says #x imply #x.

The problem with M1.8a is that it states that the concrete meta-variable #x implies itself. One cannot instantiate that. To instantiate, the lemma has to have a meta-quantifier in the root as M1.8f has.

Instead of proving a variant M1.8f of M1.8a we may also use the quantify operator:

Prop lemma ME1.47a' : ( not #x imply #x ) imply #x end lemma

prepare proof indentation,proof of ME1.47a' : line L01 : Premise >> Prop ; line L02 : A3 >> ( not #x imply not #x ) imply ( not #x imply #x ) imply #x ; line L03 : All #x : M1.8a >> not #x imply not #x ; line L04 : MP ponens L02 ponens L03 >> ( not #x imply #x ) imply #x qed

In line L03 above, the quantify operator adds All #x : *** to #x imply #x. Then the unification tactic notes that the conclusion has a meta-quantifier in the root whereas the intended conclusion has not, and thus the unification tactic changes the argumentation to ( All #x : M1.8a ) at ***. Finally, the unification tactic uses unification to replace the ellipsis with not #x as in

( All #x : M1.8a ) at not #x

Actually, the unification tactic does double instantiation as in ( All #y : ( All #x : M1.8a ) at #y ) at not #x where #y is a fresh meta-variable. It does so to avoid problems when instantiating several meta-variables in parallel.

Prev Up Next Page 342 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05