Logiweb(TM)

8.5.6 Lemmas

Prev Up Next Page 331 of 800 Search internet


One of the things an argumentation can contain is a reference to a lemma. The proof of Mendelson Exercise 1.47(a) uses Lemma M1.8f in Line L03:

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 : M1.8f >> not #x imply not #x ; line L04 : MP ponens L02 ponens L03 >> ( not #x imply #x ) imply #x qed

To use Mendelson Lemma 1.8 we need a version M1.8f which allows instantiation of the metavariable:

Prop lemma M1.8f : All #x : #x imply #x end lemma

prepare proof indentation,proof of M1.8f : line L01 : Premise >> Prop ; line L99 : 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 ( #x imply #y imply #x ) Init >> #x imply #x qed

Prev Up Next Page 331 of 800 Search logiweb.eu

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