Logiweb(TM)

8.5.4 Line numbers

Prev Up Next Page 329 of 800 Search internet


One of the things an argumentation can contain is a reference to a line number. The proof of M1.8c above contains lots of line numbers, but the proof of M1.8d below makes the point even more explicit:

Prop lemma M1.8d : #x imply #x end lemma

prepare proof indentation,proof of M1.8d : line L01 : Premise >> Prop ; line L99 : A1 >> All #x ,, #y : #x imply #y imply #x ; line L02 : A2 >> ( #x imply ( #y imply #x ) imply #x ) imply newline ( #x imply #y imply #x ) imply #x imply #x ; line L03 : L99 >> #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 : L99 >> #x imply #y imply #x ; line L06 : MP ponens L04 ponens L05 >> #x imply #x qed

In Line L99 we use Axiom A1 to prove Axiom A1, then we use Line L99 in place of Axiom A1 in the argumentations in Line L03 and L05. So in the extreme case, an argumentation may contain nothing but a line number.

Prev Up Next Page 329 of 800 Search logiweb.eu

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