fom
Posts:
1,969
Registered:
12/4/12


update to arithmetical axioms based on parts
Posted:
Feb 18, 2014 11:12 AM


Yesterday I went through the arithmetical axioms that I had posted in the past. With time, more refined thoughts have yielded better axioms.
Yes, I know these are not for practical application. No, I do not know if I have faithfully captured all of the relations needed.
And, I am still working on a notion of ordered pair that I will need for implementing a representation of modular arithmetic. Axiom 17 is a first step in that direction.
============================================
Axiom 1: (proper division, general incidence, "x is a proper divisor of y")
AxAy( x pdiv y <> ( Az( y pdiv z > x pdiv z ) /\ Ez( x pdiv z /\ ~( y pdiv z ) ) ) )
Axiom 2: (monadic division, urelement incidence, "x is a monadic divisor of y")
AxAy( x mdiv y <> ( Az( y pdiv z > x mdiv z ) /\ Az( z mdiv x > z mdiv z ) ) )
Axiom 3: (monadic succession, "z is an x successor of y", [ y = ax /\ z = bx + ax ], nothing is an x successor of itself, x successors are between each other)
AxAyAz( MS(x,y,z) <> ( ( ( ( x mdiv x /\ ( x mdiv y /\ ( x mdiv z /\ x pdiv z ) ) ) /\ Aw( ~MS(x,w,w) /\ ( ( MS(x,y,w) /\ ~MS(x,z,w) ) > MS(x,w,z) ) ) ) /\ ( ( ~Aw( y mdiv w ) /\ y mdiv x ) > ( MS(y,x,z) <> MS(x,y,z) ) ) ) )
Axiom 4: (additive relation, successor pairing relation , x + y = z, wa + wb = w( a + b ) )
AwAxAyAz( +(w,x,y,z) <> ( ( ( w mdiv w /\ ( w mdiv x /\ ( w mdiv y /\ w mdiv z ) ) ) /\ +(w,y,x,z) ) /\ EsEtEuEv( ( MS(w,x,s) /\ ( MS(w,y,t) /\ ( MS(w,z,u) /\ MS(w,MS(w,y,t),v) ) ) ) /\ ( +(w,s,z,t) <> +(w,x,u,t) ) /\ +(w,s,u,v) ) ) )
Axiom 5: (difference relations, successor partition relation, z  y = x, [ [ z = w( a + b ) /\ y = wa ] > [ w( a + b )  wa = wb ] ] )
AwAxAyAz( (w,x,y,z) <> ( ( +(w,x,y,z) /\ (w,y,x,z) ) /\ ( ~( (w,y,z,x) ) /\ ( ~( (w,x,z,y) ) /\ ( ~( (w,z,x,y) ) /\ ~( (w,z,y,x) ) ) ) ) ) )
Axiom 6: (grammatical equality, Leibniz' identity of indiscernibles)
AxAy( xEQy <> ( Az( x pdiv z <> y pdiv z ) /\ Az( z pdiv x <> z pdiv y ) /\ Az( x mdiv z <> y mdiv z ) /\ Az( z mdiv x <> z mdiv y ) /\ AuAv( MS(x,u,v) <> MS(y,u,v) ) /\ AuAv( MS(u,x,v) <> MS(u,y,v) ) /\ AuAv( MS(u,v,x) <> MS(u,v,y) ) /\ AtAuAV( +(x,t,u,v) <> +(y,t,u,v) ) /\ AtAuAV( +(t,x,u,v) <> +(t,y,u,v) ) /\ AtAuAV( +(t,u,x,v) <> +(t,u,y,v) ) /\ AtAuAV( +(t,u,v,x) <> +(t,u,v,y) ) ) )
Axiom 7: (pointed set domain assertion, there exists a unit monad and a unit successor to the unit monad)
ExEy( Az( x mdiv z ) /\ MS(x,x,y) /\ ~Ez( MS(x,x,z) /\ MS(x,z,y) ) )
Axiom 8: (asserted identity, x is identical to y if, for every monadic divisor, x and y have the same monadic successors)
AxAy( x = y <> Au( u mdiv u > Av( MS(u,x,v) <> MS(u,y,v) ) ) ) )
Axiom 9: (if there exists a unit monad, then the unit monad uniquely has no proper divisors)
Ax( Ay( x mdiv y ) > ( Ay( x mdiv y ) <> ~EuEv( MS(u,v,x) ) ) )
Axiom 10: (if there exists a unit monad, then every object has a unit successor)
AxEyAz( Aw( z mdiv w ) > ( MS(z,x,y) /\ ~Ew( MS(z,x,w) /\ MS(z,w,y) ) ) )
Axiom 11: (if there exists a unit monad, then every object different from the unit monad is a unit successor )
AxEyAz( Aw( z mdiv w ) > ( EuEv( MS(u,v,x) ) > ( MS(z,y,x) /\ ~Ew( MS(z,w,x) /\ MS(z,y,w) ) ) ) )
Axiom 12: (prime monad segregation, every object with a nonunit monadic divisor is either semiprime composite or a prime power)
Ax( ( x mdiv x /\ ~Ay( x mdiv y ) ) > Ay( x mdiv y > Az( ( x mdiv z /\ ~( y pdiv z ) ) > ( ~( Ew( ( w mdiv w /\ Ev( v pdiv w ) ) /\ ( w mdiv y /\ ~( x mdiv w ) ) ) <> Aw( y pdiv w <> x mdiv w ) ) ) ) ) )
Axiom 13: (general successon)
AxAyAz( GS(x,y,z) <> ( ( ( ( x = y \/ x pdiv y ) /\ x pdiv z ) ) /\ Aw( ~GS(x,w,w) /\ ( ~( w = z ) > ( ( GS(x,y,w) /\ ~GS(x,z,w) ) > GS(x,w,z) ) ) ) ) /\ ( x = y > ( GS(y,x,z) <> GS(x,y,z) ) ) ) )
Axiom 14: (multiplicative relation, [ ( x=y=z=1 ) xor ( { xz /\ yz } xor { [ x=z /\ y=1 ] xor [ x=1 /\ y=z ] } ) ] AND [ { xz /\ yz } > every divisor of x, say k, has a y1 length general successor chain such that (y1)k + k = z and similarly for y ] )
AxAyAz( *(x,y,z) <> ( ~( ( Aw( x mdiv w ) /\ Aw( y mdiv w ) /\ Aw( z mdiv w ) ) <> ~( ( x pdiv z /\ y pdiv z ) <> ~( ( x = z /\ Aw( y mdiv w ) ) <> ( Aw( x mdiv w ) /\ y = z ) ) ) ) /\ ( ( x pdiv z /\ y pdiv z ) > ( Aw( ( ( ~At( w mdiv t ) /\ w mdiv x ) \/ w pdiv x ) > ( ArAs( ( Aq( r mdiv q ) /\ MS(r,s,y) ) > EuEv( ( GS(w,u,z) /\ (r,v,s,y) ) /\ v pdiv u ) ) ) ) /\ AW( ( ( ~At( w mdiv t ) /\ w mdiv y ) \/ w pdiv y ) > (ArAs( ( Aq( r mdiv q ) /\ S(r,s,x) ) > EuEv( ( S(w,u,z) /\ (r,v,s,x) ) /\ v pdiv u ) ) ) ) ) )
Axiom 15: (Archimedean principle, every object is a proper divisor for some successor of every monadic divisor)
Ax( Ew( w mdiv w ) > EuEv( MS(w,v,u) /\ x pdiv u ) )
Axiom 16: (Euclid's principle, every unit successor is either a prime or a monadic successor for some prime)
Ax( ~Ay( x mdiv y ) > Au( Az( u mdiv z ) > Av( ( ( MS(u,x,v) /\ ~Ez( MS(u,x,z) /\ MS(u,z,v) ) ) > ~( Ey( ( y mdiv y /\ ~Az( y mdiv z ) ) /\ y=v ) <> EwEy( ( y mdiv y /\ ~Az( y mdiv z ) ) /\ MS(y,w,v) ) ) ) ) )
Axiom 17: (binary partition asymmetry relations, w + x => w^2 + x^2 + 2wx + v(w + x) + (x + x), x + w => x^2 + w^2 + 2xw + v(x + w) + (w + w) )
AvAwAxAyAz( P(v,w,x,y,z) <> ( Ar( At( r mdiv t ) > As( ( ( S(r,r,s) /\ ~Et( MS(r,r,t) /\ MS(r,t,s) ) ) /\ ~( s midv v ) ) > ( v mdiv v > ( EoEpEq( ( ( +(r,w,x,p) /\ +(r,v,p,q) ) /\ *(q,p,o) ) /\ EjEkEmEn( ( +(r,w,w,j) /\ +(r,x,x,k) ) /\ ( ( +(r,o,j,m) /\ +(r,o,k,n) ) /\ ( *(s,y,m) /\ *(s,z,n) ) ) ) ) ) ) ) )

