Logiweb(TM)

8.5.8 Instantiation

Prev Up Next Page 333 of 800 Search internet


The instantiation operator A at x allows to instantiate a meta-variable explicitly. After adaption the conclusion of A must have a meta-quantifier as principle operator.

Explicit instantiation is handy in situations where unification gives an Incomplete unification. Uninstantiated variable: x error message. The multzero proof provides a good example in Line L09:

prepare proof indentation,PA proof of 3.2l : line L01 : S7 >> 0 * 0 = 0 ; line L02 : Block >> Begin ; line L03 : Hypothesis >> 0 * x = 0 ; line L04 : S8 >> 0 * x suc = 0 * x + 0 ; line L05 : S5 >> 0 * x + 0 = 0 * x ; line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ; line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ; line L08 : Block >> End ; line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ; line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed

Unification is unable to guess from 0 * 0 = 0 and 0 * x = 0 imply 0 * x suc = 0 that x is the induction variable. Such guessing is possible but requires more intelligence than unification provides. Thus, the induction variable has to be given explicitly.

Prev Up Next Page 333 of 800 Search logiweb.eu

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