Human ecology

Two proofs of "eight plus three equals eleven"

Proof I

Notation:
a(x,y)=x+y
s(x)="the successor of x"

D1 s(zero)=one DEFINITION s0=1
D2 s(one)=two DEFINITION s1=2
D3 s(two)=three DEFINITION s2=3
s(three)=four DEFINITION s3=4
s(four)=five DEFINITION s4=5
s(five)=six DEFINITION s5=6
s(six)=seven DEFINITION s6=7
s(seven)=eight DEFINITION s7=8
D4 s(eight)=nine DEFINITION s8=9
D5 s(nine)=ten DEFINITION s9=10
D6 s(ten)=eleven DEFINITION s10=11
A7 a(x,s(y))=s(a(x,y)) AXIOM x+sy=s(x+y)
T8 a(eight,s(y))=s(a(eight,y)) FROM A7 8+sy=s(8+y)
A9 a(x,zero)=x AXIOM x+0=x
T10 a(eight,zero)=eight FROM A9 8+0=8
T11 a(eight,s(zero))=s(a(eight,zero)) FROM T8 8+s0=s(8+0)
T12 a(eight,s(zero))=s(eight) FROM T11 AND T10 8+s0=s8
T13 a(eight,s(zero))=nine FROM T12 AND D4 8+s0=9
T14 a(eight,one)=nine FROM T13 AND D1 8+1=9
T15 a(eight,s(one)=s(a(eight,one)) FROM T8 8+s1=s(8+1)
T16 a(eight,s(one))=s(nine) FROM T15 AND T14 8+s1=s9
T17 a(eight,s(one))=ten FROM T16 AND D5 8+s1=10
T18 a(eight,two)=ten FROM T17 AND D2 8+2=10
T19 a(eight,s(two))=s(a(eight,two)) FROM T8 8+s2=s(8+2)
T20 a(eight,s(two))=s(ten) FROM T19 AND T18 8+s2=s10
T21 a(eight,s(two))=eleven FROM T20 AND D6 8+s2=11
T22 a(eight,three)=eleven FROM T21 AND D3 8+3=11


Alternative Proof II

Notation:
a(x,y)=x+y
i(x)="the increment of x"
d(x)="the decrement of x"

D1 i(zero)=one DEFINITION
D2 i(one)=two DEFINITION
D3 i(two)=three DEFINITION
i(three)=four DEFINITION
i(four)=five DEFINITION
i(five)=six DEFINITION
i(six)=seven DEFINITION
i(seven)=eight DEFINITION
D4 i(eight)=nine DEFINITION
D5 i(nine)=ten DEFINITION
D6 i(ten)=eleven DEFINITION
A7 d(i(x))=x AXIOM
T8 d(i(two))=two FROM A7
T9 d(three)=two FROM T8 AND D3
T10 d(i(one))=one FROM A7
T11 d(two)=one FROM T10 AND D2
T12 d(i(zero))=zero FROM A7
T13 d(one)=zero FROM T10 AND D1
A14 a(x,y)=a(i(x),d(y)) AXIOM
T15 a(eight,y)=a(i(eight),d(y)) FROM A14
T16 a(eight,three)=a(i(eight),d(three)) FROM T15
T17 a(eight,three)=a(nine,d(three)) FROM T16 AND D4
T18 a(eight,three)=a(nine,two) FROM T17 AND T9
T19 a(nine,y)=a(i(nine),d(y)) FROM A14
T20 a(nine,two)=a(i(nine),d(two)) FROM T19
T21 a(nine,two)=a(ten,d(two)) FROM T20 AND D5
T22 a(nine,two)=a(ten,one) FROM T21 AND T11
T23 a(eight,three)=a(ten,one) FROM T18 AND T22
T24 a(ten,y)=a(i(ten),d(y)) FROM A14
T25 a(ten,one)=a(i(ten),d(one)) FROM T24
T26 a(ten,one)=a(eleven,d(one)) FROM T25 AND D6
T27 a(ten,one)=a(eleven,zero) FROM T26 AND D13
T28 a(eight,three)=a(eleven,zero) FROM T23 AND T27
A29 a(x,zero)=x AXIOM
T30 a(eleven,zero)=eleven FROM A29
T31 a(eight,three)=eleven FROM T25 AND T27



Links to other sites...
Created 16/8/99