Logiweb(TM)

8.4.6 Arbitrary terms

Prev Up Next Page 321 of 800 Search internet


The following constructs allow to say that some metavariable V denotes an arbitrary term:

   line L : Arbitrary >> V ; N

Example:

PA lemma ArbitraryTermExample : All #x : #x imply #x end lemma

prepare proof indentation,proof of ArbitraryTermExample : line L00 : Premise >> PA ; line L01 : Arbitrary >> #x ; line L02 : A2 >> ( #x imply ( #y imply #x ) imply #x ) imply newline ( #x imply #y imply #x ) imply #x imply #x ; line L03 : A1 >> #x imply ( #y imply #x ) imply #x ; line L04 : MP ponens L02 ponens L03 >> ( #x imply #y imply #x ) imply #x imply #x ; line L05 : A1 >> #x imply #y imply #x ; line L06 : MP ponens L04 ponens L05 >> #x imply #x qed

In Line L01 we state that #x denotes an arbitrary variable.

Using 'arbitrary' is the typical way to prove a lemma of form All x : A.

Do not use 'arbitrary' in proof of form

   T proof of L : P qed

where T is Prop, FOL, or Peano from the Peano page. The tactics of Prop, FOL, and Peano are not intended to be used together with meta-quantification.

Prev Up Next Page 321 of 800 Search logiweb.eu

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