Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.

Topic: update to arithmetical axioms based on parts
Replies: 24   Last Post: Feb 23, 2014 2:32 AM

 Messages: [ Previous | Next ]
 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 ) ) ) )

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) ) ) ) )

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 ( { x|z /\ y|z }
xor { [ x=z /\ y=1 ] xor [ x=1 /\ y=z ] } ) ] AND [ { x|z /\ y|z } ->
every divisor of x, say k, has a y-1 length general successor chain such
that (y-1)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) ) ) ) ) ) ) ) )

Date Subject Author
2/18/14 fom
2/18/14 fom
2/18/14 fom
2/18/14 thenewcalculus@gmail.com
2/18/14 Wizard-Of-Oz
2/19/14 fom
2/19/14 fom
2/19/14 Wizard-Of-Oz
2/19/14 fom
2/20/14 Wizard-Of-Oz
2/20/14 fom
2/20/14 Wizard-Of-Oz
2/20/14 fom
2/20/14 fom
2/20/14 fom
2/20/14 Wizard-Of-Oz
2/20/14 fom
2/20/14 ross.finlayson@gmail.com
2/20/14 fom
2/20/14 ross.finlayson@gmail.com
2/21/14 fom
2/21/14 fom
2/22/14 ross.finlayson@gmail.com
2/23/14 fom
2/23/14 fom