MHB Axiomatic Proving: A) a0=0, B) 0<1

[solakis1]

Given the following axioms:

For all a,b,c we have:

1) a+b = b+c
2) a+(b+c)=(a+b)+c
3) ab = ba
4) a(bc) = (ab)c
5) a(b+c) =ab+ac
NOTE,here the multiplication sign (.) between the variables have been ommited
6) There ia a number called 0 such that for all a,
a+0 =a
7)For each a, there is a number -a such that for any a,
a+(-a) = 0
8)There is a number called 1(diofferent from 0) such that for any a,
a1 = a
9)For each a which is different than 0there exists a number called 1/a such that;
a.(1/a)= 1.

For any numbers a,b

10) either a<b or a>b or a=b
11) if a<b and b<c then a<c
12) if a<b then a+c<b+c for any c
13) if a<b and c>0 then ac<bc for any c.

Then by using only the axioms stated above prove:

A) a0 = 0 ,B) 0<1

In trying to prove A i followed the proof shown below:

1) 0+0=0 ......by using axiom 6

2) (0+0)x =0x....by multiplying both sides by x

3)0x+ox =0x.....by using axiom 5

4) (0x+0x) +(-0x) =0x+(-0x) .....by adding (-0x) to both sides

5) 0x +[0x+(-0x)]= 0x+(-0x)......by using axiom 2

6) 0x +0 = 0 .....by using axiom 7

7) 0x = 0 ......by using axiom 6

For B ,I could not show a proof based only on the axioms stated above

Is my proof for A, correct 100%?

 

[Evgeny.Makarov]

3)0x+ox =0x.....by using axiom 5

You need to use commutativity first. Also note that adding the same term to both sides or multiplying both sides by the same number is, in fact, an application of an equality axiom. It is sometimes considered a part of first-order logic and is thus not listed. Finally, note that -0x in the proof is -(0x), not (-0)x.

Yes, with the correction about commutativity before distributivity, the proof of A) is correct. I'll think about a proof of B).

 

[solakis1]

You need to use commutativity first. Also note that adding the same term to both sides or multiplying both sides by the same number is, in fact, an application of an equality axiom. It is sometimes considered a part of first-order logic and is thus not listed. Finally, note that -0x in the proof is -(0x), not (-0)x.

Yes, with the correction about commutativity before distributivity, the proof of A) is correct. I'll think about a proof of B).

Itried the following proof for B:

1) 1<0 or 1>0......by axioms 8 ND 10

2) For 1>0 there is nothing to prove

3) For 1<0 we have :

4) 1+(-1)< 0+(-1).....by axiom 12

5) 1+(-1)< (-1) +0.....by axiom 1

6) 0< -1.......by axioms 6 and 7

7) Now here we need a definition which is missing .
The definition is : for a,b a<b <=> b>a

8) So according to the above definition we have:

-1>0

9) -1>0

10) 1(-1)< 0(-1) ......by axiom 13

11) 1(-1)< 0........by part A (0A=0)

12) 1(-1)+1<0+1......BY axiom 12

13) 1.1+ 1(-1)<1+0......by axioms 1,3 and 8

14) 1(1+(-1))< 1.....by axioms 5 and 6

15) 1.0 <1.......by axiom 7

16) 0<1........by part A

 

[Evgeny.Makarov]

I believe your proof of B is correct. Well done.

 

[solakis1]

I believe your proof of B is correct. Well done.

That means that the department of Mathematics o f the University of the Witwatersrand In Johannesburg in the year 1965 gave a wrong question in the final exams of Mathematics I.

They repeated the same mistake the year 1966 ,although they slightly changed the order axioms as shown below:

1) exactly one of a>b,a<b or a=b holds
2) if a>b ,b>c then a>c
3) if c>0 ,a>b then ac>bc
4) if a>b then a+c>b+c for any c

Here they also asked for a proof of :

A) ao =0 and B) 1>0

again based only on the axioms stated above

I think the set of order axioms that will produce a proof of 1>0 without the definition, a>b <=> b<a is the fololowing:

1) exactly one of a>b,b>a or a=b holds

2) if a>b ,b>c then a>c

3) if c>0 ,a>b then ac>bc

4) if a>b then a+c>b+c for any c

 

[Evgeny.Makarov]

Yes, you need a connection between $a<b$ and $b>a$. Maybe the authors of the problem believed that the equivalence is assumed. Similarly to how in the context of a field one often writes $x/y$ meaning $x\cdot y^{-1}$, maybe they assumed that $b>a$ is defined to mean $a<b$. This approach is used, for example, in the Coq theorem prover in regard to real numbers.