Logiweb(TM)

8.4.2 Argumentation lines

Prev Up Next Page 317 of 800 Search internet


The most common lines in proofs are ones which argue in favor of a conclusion. The construct for lines reads:

   line L : A >> C ; N

The construct above uses the argumentation A to prove the conclusion C. It contains a line number L which allows to refer to the conclusion C later on in the proof. The construct also has a 'next' argument N which is supposed to contain all proof lines following the given line. The notion of an argumentation is explained later.

The construct above is used for expressing Line L01, L04, L05, L06, and L09 of the multzero proof:

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

The body of the proof above has form

   line L01 : S7 >> 0 * 0 = 0 ; ...

where the ellipsis ... comprises Line L02-L10.

Prev Up Next Page 317 of 800 Search logiweb.eu

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