
Re: Two Finite Arithmetics
Posted:
Apr 8, 2014 1:09 AM


On Monday, April 7, 2014 11:51:08 PM UTC4, William Elliot wrote: > On Mon, 7 Apr 2014, Dan Christensen wrote: > > > > > On Sunday, April 6, 2014 4:54:57 AM UTC4, William Elliot wrote: > > > > Naive Finite Arithmetic > > > > > > > > Let N be a set, 0,m two elements and SN > N a function. > > > > Axioms for naive finite arithmetic: > > > > > > > > 0, m in N; Sm = m > > > > > > m should have no successor. Perhaps a partial function S on N? > > Naive finite arithmetic is not your finite arithmetic. > > S is a full function to banish the pests of your system. >
Inventing a successor for the maximum number seems a bit weird to me.
An elementary result of ordinary number theory is that no number can be it's own successor. You can probably obtain the same result with your axioms, so you may need another axiom to get around this potential contradiction.
> > > > > for all x, Sx in N > > > > for all x, x /= S0 > > > > for all x, Sx /= 0. > > > > > > for all x,y /= m. (Sx = Sy implies x = y) > > > > For all A subset N, if > > > > 0 in A, (for all x in A implies Sx in A) > > > > then N subset A > > > > Definition of addition by induction. > > > > 0 + y = y > > Sx + y = x + Sy > > > > > Is this where the "naive" comes in? The use of the infix '+' really needs to > > > be justified, i.e. the sum of a pair of a numbers should be formally proven > > > to be unique, however you may define sums. > > > > That definition is a binary function over N^2. > > That it works for double induction is common knowledge. >
So, you are defining your way out of the problem. Why prove sums are unique when you can just assert that it is true? It's, ahem... "common knowledge" after all, right?
> > > > As with your function S, perhaps '+' should be a partially function. > > > > No. That's a mess for the partiallity is difficult to describe. > > This way, once you get to m, then adding more is not more. > > > > > Also, shouldn't you have something have something like Sx + y = S(x+y)? > > > > Hey, that's a better idea, avoiding double induction > > as now the inductive definition is the add y function. > > > > > > Definition of mulplication by induction. > > > > 0 * y = 0 > > > > Sx * y = x*y + y > > > > Sx + y = x + Sy > > > > Is this a consistent set of axioms with the model of a finite > > > > set of integerss { 0,1,.. m } and addition defined by > > > > a + b = max{ m, a+b }? > > > > For the model work, I should have carified that + is usual addition > > ++ the naive finite arithmetic and write, by definition > > a ++ b = max( m, a+b } > > > Again, you probably want a partial function. The way I see it, m + 1 should > > > be undefined. > > > > No way!. You have been able to finish your system. > > Mine is done and complete, corrected and imporved. >
It may need a bit more work.
> > > > There may be a good reason that finite arithmetic has never been > > > successfully formalized. It may be impossible. > > > > The max ceiling prevents cancelation >
Can you prove this, or this yet another new axiom?
> a + b = a + c implies b = c > > At best, if a + b = a + c /= m, then b = c. > > > > Also it not very useful. For very large m, it can > > suffice for most mathematics, but the needed m seems to > > keep increasing with time. Would m = googleplex suffice?
m could be 0, and no number would have a successor. Not very interesting, but a possibility.
Dan Download my DC Proof 2.0 software at http://www.dcproof.com Visit my new math blog at http://www.dcproof.wordpress.com

