2.6 Because Blocks


Among the 4 blocks (quantitization block, implication block, because block, and replacement block) used in the demonstrations of theorems, only the because block is not logically needed (although it is useful to have one). In traditional mathematics, <Formula 1> exists and a word like "because..." frequently appears. Logically, reasons can be explained first; however, it is this way because people's reasoning is not always deductive but sometimes inductive. In THEAX, this is indicated by the because blocks. Because blocks start with a line like (<because.head.line >) as

<Label 1>:<Formula 1>because;

At this time, <Formula 1> does not have to be demonstrated. Therefore, this line does not need an inference value. The because block ends with a line (<end.Because.line>) saying

because by <Inference Value 1>;

Do not cite a formula of <Label 1> in blocks. However, after pulling out of blocks, it is permitted to cite <Label 1>. In that case, it will be the same with writing

<Label 1>:<Formula 1> by <Inference Value 1>;

on the line saying <end. because. line> ( provided that <because. head. line> does not exist). Therefore, the inference value that follows because by explains the reason why the corresponding <because. head. line> deduct.

The because blocks can be multiplexed, be inserted into other blocks, or hold other kinds of blocks within itself. These are the same cases as quantitization blocks and implication blocks, as explained previously.

Figure A is an example that used because block for the theory of semi order set

00010'Text Poset;

00020'Definition /*Partially Ordered Set */;

00030' PosDe1:Put Poset(X,p)=/*1*(All x)(X(x)imp p(x,x))

00040' and /* 2*/(All x)(All y)(p(x,y)and

00050' p(y,x) imp [x=y])

00060' and /* 3*/ (All x)(All y)(All z)(

00070' p(x,y)and p(y,z)imp p(x,z));

00080' PosDe2:Put Upper-Bound(p)(S)(c)=(All y)(S(y) imp

00090' p(y,c));

00100' PosDe3:Put 1.u.b.(p)(S)(a)=Upper-Bound(p)(S)(a)and

00120' imp p(a,x));

00130'End Def;

00140'

00150'Proposition; /* The least upper bound is unique */

00160' PosPro1: (All X)(All p)(All S)

00165' (All a)(All b)(Poset(X,p)and 1.u.b.(p)(S)(a)

00170' and 1.u.b.(p)(S)(b) imp [a=b]);

00180'Proof;a1: (All X)(All p)(All S)

00190' (All a)(All b)(;

00200' a2: Poset(X,p)and 1.u.b.(p)(S)(a)

00210' and 1.u.b.(p)(S)(b) imp;

00220' a3: 1.u.b.(p)(S)(a) by LOGIC(a2);

00230' a4: Upper-Bound (p)(S)(a)and (All x)(Upper-Bound(p)

00240' (S)(x)imp p(a,x)) by FUNF(PosDe3,a3);

00250' a5: Upper-Bound(p)(S)(b)because;

00260' a6: 1.u.b.(p)(S)(b) by LOGIC(a2);

00270' a7: Upper-Bound(p)(S)(b)and (All x)(Upper-Bound

00280' (p)(S)(x)imp p(b,x)) by FUNF(PosDe3,a6);

00290' because by LOGIC(a7);

00300' a8: p(a,b) because;

00310' a9: (All x)(Upper-Bound(p)(S)(x)imp p(a,x))

00320' by LOGIC(a4);

00330' because by ALS(a9,a5);

00340' a10: Upper-Bound(p)(S)(a) by LOGIC(a4);

00350' all: (All x)(Upper-Bound(p)(S)(x)imp p(b,x))

00360' by LOGIC(a7);

00370' a12: p(b,a) by ALS(a11,a10);

00380' a13: p(a,b)and p(b,a) by LOGIC(a8,a12);

00390' a14: Poset(X,p) by LOGIC(a2);

00400' a15: (All x)(X(x)imp p(x,x) and (All x)(All y)(

00410' p(x,y)and p(y,x)imp [x=y]) and

00420' (All x)(All y)(All z)(p(x,y)and p(y,z)imp

00430' p(x,z)) by FUNF(PosDe1,a14);

00440' a16: (All x)(All y)(p(x,y)and p(y,x)imp [x=y])

00450' by LOGIC(a15);

00460' imp [a=b] by ALS(a16,a13);

00470' );

00480'Q.E.D.(a1);

Figure A An example using a because block (theory of semi order set). Line 250 originally comes to line 290. Also line 300 comes to line 330.