Q: How do you use DC poop to prove Landau's:

∀x∀y(x + y = y + x)

A: Not at all, it doesn't use x e N. LoL

Dan Christensen schrieb am Donnerstag, 20. Januar 2022 um 16:41:50 UTC+1:
> On Thursday, January 20, 2022 at 1:13:46 AM UTC-5, Mostowski Collapse wrote:
>
> > ...when he constructs add:
> > [(𝑒,𝑓,𝑔)∈𝑑⟹(𝑒,𝑆(𝑓),𝑆(𝑔))∈𝑑]
> >
> That's only part of it.
>
> ALL(a):ALL(b):ALL(c):[(a,b,c) in add
> <=> (a,b,c) in n3 & ALL(d):[Set''(d)
> & ALL(e):ALL(f):ALL(g):[(e,f,g) in d => in e n & f in n & g in n]
> & ALL(e):[e in n => (e,0,e) in d]
> & ALL(e):ALL(f):ALL(g):[e in n & f in n & g in n => [(e,f,g) in d => (e,s(f),s(g)) in d]]
> => (a,b,c) in d]]
>
> https://www.dcproof.com/ConstructAdditionNew.htm (line 21)
> > And arrives at the definition of add via equations:
> > ∀𝑎∈𝑁:𝑎𝑑𝑑(𝑎,0)=𝑎
> > ∀𝑎,𝑏∈𝑁:𝑎𝑑𝑑(𝑎,𝑆(𝑏))=𝑆(𝑎𝑑𝑑(𝑎,𝑏))
> >
> > But I was rather expecting something stronger for add:
> > [(𝑒,𝑓,𝑔)∈add <=> (𝑒,𝑆(𝑓),𝑆(𝑔))∈add]
> >
> Not necessary to prove the existence of the addition function on N. Once you have done that, you can prove cancelability, associativity, commutativity, etc. by induction.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 20, 2022 at 1:31:02 PM UTC-5, Mostowski Collapse wrote:
> Q: How do you use DC Proof to prove Landau's:
>
> ∀x∀y(x + y = y + x)
>

Will dig up some old proofs later. Busy implementing Function Space Axiom.

Dan

On Thursday, January 20, 2022 at 1:31:02 PM UTC-5, Mostowski Collapse wrote:
> Q: How do you use DC Proof to prove Landau's:
>
> ∀x∀y(x + y = y + x)
>

https://dcproof.com/AddComm.htm

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

WHATS WRONG WITH YOU????

Dan-O-Matik asked:
> How do you express Peano's Axioms?

Well like this:

> 1) First prove by induction that ∀x(0 + x = x).
> Base Case: 0 + 0 = 0
1. ∀x x+0 = x ⇒ 0+0 = 0
> Induction Step: 0 + x = x => 0 + s(x) = s(x)
1. ∀x ∀y x+s(y) = s(x+y) ⇒ ∀x (0+x = x ⇒ 0+s(x) = s(x))

Etc..

You can now guess what the Peano Axioms are,
or read Landau once for all. Its right before your eyes:

Screenshot in OPs Question
(e,f,g)∈d⟹(e,S(f),S(g))∈d]
Dan-O-Matiks Add Construction
https://math.stackexchange.com/a/784504/1002973

|
| |
| |
| |
| v

Solution: I said it like already a thousend times, no x e N,
thats how Peano axioms are done. Here are the addition axioms,
unlinke Landau there is a zero, but thats a minor detail:

1. ∀x x+0 = x
2. ∀x ∀y x+s(y) = s(x+y)

Dan Christensen schrieb am Freitag, 21. Januar 2022 um 06:24:14 UTC+1:
> On Thursday, January 20, 2022 at 1:31:02 PM UTC-5, Mostowski Collapse wrote:
> > Q: How do you use DC Proof to prove Landau's:
> >
> > ∀x∀y(x + y = y + x)
> >
> https://dcproof.com/AddComm.htm
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Here is a transliteration of the screenshot from Landau:

Theorem 4, and at the same time Definition 1: To every
pair of nunbers x, y, we may assign exactly one way a natural
number, call x + y (+ to be read "plus"), such that:
1) x + 1 = x' for every x
2) x + y' = (x + y)' for every x and every y
x + y is called the sum of x and y, or the number obtained
by addition of y to x
https://math.stackexchange.com/q/783931/1002973

You don't need x e N if you don't have other domains.

Mostowski Collapse schrieb am Freitag, 21. Januar 2022 um 18:48:26 UTC+1:
> WHATS WRONG WITH YOU????
>
> Dan-O-Matik asked:
> > How do you express Peano's Axioms?
>
> Well like this:
>
> > 1) First prove by induction that ∀x(0 + x = x).
> > Base Case: 0 + 0 = 0
> 1. ∀x x+0 = x ⇒ 0+0 = 0
> > Induction Step: 0 + x = x => 0 + s(x) = s(x)
> 1. ∀x ∀y x+s(y) = s(x+y) ⇒ ∀x (0+x = x ⇒ 0+s(x) = s(x))
>
> Etc..
>
> You can now guess what the Peano Axioms are,
> or read Landau once for all. Its right before your eyes:
>
> Screenshot in OPs Question
> (e,f,g)∈d⟹(e,S(f),S(g))∈d]
> Dan-O-Matiks Add Construction
> https://math.stackexchange.com/a/784504/1002973
>
> |
> |
> |
> |
> |
> |
> |
> |
> v
>
> Solution: I said it like already a thousend times, no x e N,
> thats how Peano axioms are done. Here are the addition axioms,
> unlinke Landau there is a zero, but thats a minor detail:
>
> 1. ∀x x+0 = x
> 2. ∀x ∀y x+s(y) = s(x+y)
> Dan Christensen schrieb am Freitag, 21. Januar 2022 um 06:24:14 UTC+1:
> > On Thursday, January 20, 2022 at 1:31:02 PM UTC-5, Mostowski Collapse wrote:
> > > Q: How do you use DC Proof to prove Landau's:
> > >
> > > ∀x∀y(x + y = y + x)
> > >
> > https://dcproof.com/AddComm.htm
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Theorem 4 would be:

∀x ∀y ∃z (x + y = z)
∀x ∀y ∀z ∀t (x + y = z & x + y = t => z = t)

But this trivially valid in FOL=:

∀x∀y∃za(x,y)=z is valid.
https://www.umsu.de/trees/#~6x~6y~7z%28a%28x,y%29=z%29

∀x∀y∀z∀t((a(x,y)=z ∧ a(x,y)=t) → z=t) is valid.
https://www.umsu.de/trees/#~6x~6y~6z~6t%28a%28x,y%29=z~1a%28x,y%29=t~5z=t%29

On the other hand, the recursion theoretic proof doesn't use
equality from FOL=, but an equality ≈ that would capture
some computation. We can possibly thank

the ultrafinitists that recursion theory exists, since they
asked so many questions in the past what it means that
a number exists by finite means.

Mostowski Collapse schrieb am Freitag, 21. Januar 2022 um 18:50:18 UTC+1:
> Here is a transliteration of the screenshot from Landau:
>
> Theorem 4, and at the same time Definition 1: To every
> pair of nunbers x, y, we may assign exactly one way a natural
> number, call x + y (+ to be read "plus"), such that:
> 1) x + 1 = x' for every x
> 2) x + y' = (x + y)' for every x and every y
> x + y is called the sum of x and y, or the number obtained
> by addition of y to x
> https://math.stackexchange.com/q/783931/1002973
>
> You don't need x e N if you don't have other domains.
> Mostowski Collapse schrieb am Freitag, 21. Januar 2022 um 18:48:26 UTC+1:
> > WHATS WRONG WITH YOU????
> >
> > Dan-O-Matik asked:
> > > How do you express Peano's Axioms?
> >
> > Well like this:
> >
> > > 1) First prove by induction that ∀x(0 + x = x).
> > > Base Case: 0 + 0 = 0
> > 1. ∀x x+0 = x ⇒ 0+0 = 0
> > > Induction Step: 0 + x = x => 0 + s(x) = s(x)
> > 1. ∀x ∀y x+s(y) = s(x+y) ⇒ ∀x (0+x = x ⇒ 0+s(x) = s(x))
> >
> > Etc..
> >
> > You can now guess what the Peano Axioms are,
> > or read Landau once for all. Its right before your eyes:
> >
> > Screenshot in OPs Question
> > (e,f,g)∈d⟹(e,S(f),S(g))∈d]
> > Dan-O-Matiks Add Construction
> > https://math.stackexchange.com/a/784504/1002973
> >
> > |
> > |
> > |
> > |
> > |
> > |
> > |
> > |
> > v
> >
> > Solution: I said it like already a thousend times, no x e N,
> > thats how Peano axioms are done. Here are the addition axioms,
> > unlinke Landau there is a zero, but thats a minor detail:
> >
> > 1. ∀x x+0 = x
> > 2. ∀x ∀y x+s(y) = s(x+y)
> > Dan Christensen schrieb am Freitag, 21. Januar 2022 um 06:24:14 UTC+1:
> > > On Thursday, January 20, 2022 at 1:31:02 PM UTC-5, Mostowski Collapse wrote:
> > > > Q: How do you use DC Proof to prove Landau's:
> > > >
> > > > ∀x∀y(x + y = y + x)
> > > >
> > > https://dcproof.com/AddComm.htm
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Friday, January 21, 2022 at 12:48:26 PM UTC-5, Mostowski Collapse wrote:
> WHATS WRONG WITH YOU????
>
> Dan-O-Matik asked:
> > How do you express Peano's Axioms?
>
> Well like this:
>
> > 1) First prove by induction that ∀x(0 + x = x).
> > Base Case: 0 + 0 = 0
> 1. ∀x x+0 = x ⇒ 0+0 = 0
> > Induction Step: 0 + x = x => 0 + s(x) = s(x)
> 1. ∀x ∀y x+s(y) = s(x+y) ⇒ ∀x (0+x = x ⇒ 0+s(x) = s(x))
>

OMG. I really have over-estimated you, Jan Burse.

> Etc..
>
> You can now guess what the Peano Axioms are,

No need to guess. See: http://mathworld.wolfram.com/PeanosAxioms.html

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, January 19, 2022 at 10:52:07 AM UTC-5, Dan Christensen wrote:
> On Wednesday, January 19, 2022 at 8:54:54 AM UTC-5, timba...@gmail.com wrote:
> > On Tuesday, January 18, 2022 at 7:36:30 PM UTC-5, Dan Christensen wrote:
> > > On Tuesday, January 18, 2022 at 7:12:41 PM UTC-5, timba...@gmail.com wrote:
> > > > On Tuesday, January 18, 2022 at 1:19:31 PM UTC-5, Dan Christensen wrote:
> > > > > On Tuesday, January 18, 2022 at 12:57:37 PM UTC-5, timba...@gmail..com wrote:
> > > > > > On Tuesday, January 18, 2022 at 12:33:53 PM UTC-5, Dan Christensen wrote:
> > > > > > > On Tuesday, January 18, 2022 at 9:07:05 AM UTC-5, timba...@gmail.com wrote:
> > > > > > >
> > > > > > > >
> > > > > > > > I suppose then we have to ask whether 1+1=2 in your system?
> > > > > > > >
> > > > > > > Yes. Starting from the usual Peano Axioms for (N, S, 0), you can prove the existence of an addition function in my system using basic set theory. (700+ lines of proof) Then define 1 and 2 in N such that 1=S(0) and 2=S(1). Then it is trivial to derive 1+1=2.
> > > > > > > Dan
> > > > > > >
> > > > > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > > > > Visit my Math Blog at http://www.dcproof.wordpress.com
> > > > > > Well, then is 2+1=3?
> > > > > Yes. You would first have to define 3 = S(2).
> > > > > > where is f(3)?
> > > > > > I understand I can't break you here, but it does seem troubling doesn't it?
> > > > > Not at all.
> > > > > > You want to claim some pure function that works on one and works on two, but refuses to work on 3?
> > > > > "Refuses to work on 3???" Where do you get that idea?
> > > > > Dan
> > > > >
> > > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > > Visit my Math Blog at http://www.dcproof.wordpress.com
> > > > You cannot alleviate the lack of definition of f(3) by admitting that this expression is undefined. The act of claiming that f(3) is undefined should not be within the composition.
> > > >
> > > Ummm... I defined 3 = S(2) (above). The rest of your post makes even less sense. Sorry.
> > Pretty sure you've settled onto the naturals now instead of 'it could be'.
> > X is Y is X is X is the natural numbers.
> I only refer to the natural numbers since you asked about proving 1+1=2..

Are you saying that the 2 inside of your system is not the natural value?

> > Defining things as undefined is not a legitimate business.
> A function is defined only for a certain set of objects, i.e. its "domain of definition." We say that function is "undefined" for any objects not in that domain. It is not a formal distinction.
> > If you had a graphical representation then the distinction of your definition of f(t) versus say a signal realm really exposes some trouble with mathematics.
> Not really. In set theory, when we talk about the graph of a function, we are not talking about a visual graph; we are talking about a set of ordered pairs (for functions of 1 variable).

If your input is natural and you output is natural then clearly another form of graph is available. Draw a line. Mark intervals on that line with dividers. Your candidates are on those interval positions. Your inputs versus your outputs now require representation. Color and depth can answer these needs and you'll wind up in my earlier description.

The idea that your inputs and your outputs are unique sets: yes; they can be, but in your case they obviously are not. They are the same set, sir.
Do there in fact exist unique copies of the natural values? No. The Cartesian product itself is somewhat a lie. Too many of its usages have gained a seriousness that ignores this deficit.

That the Cartesian system forms an adequate representation does not mean that if forms an adequate construction.

>
> Perhaps, if there is the possibility of confusion, we should refer to it as the "graph SET" of the function in question.
>
> Example: For the function f on the real numbers such that f(x)=2x, the graph set of f is is the set of ordered pairs (a, b) such a and b are real numbers and b=2a, e.g. (1, 2), (2, 4) and (3, 6).
> > I'll stand by me earlier tripe that you ignore here.
> > X is Y and so there is only X.
> [snip]
>
> Makes no sense. I cannot comment. Sorry.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, January 23, 2022 at 8:03:30 AM UTC-5, timba...@gmail.com wrote:

> > > If you had a graphical representation then the distinction of your definition of f(t) versus say a signal realm really exposes some trouble with mathematics.

> > Not really. In set theory, when we talk about the graph of a function, we are not talking about a visual graph; we are talking about a set of ordered pairs (for functions of 1 variable).

> If your input is natural and you output is natural then clearly another form of graph is available. Draw a line.

[snip]

Not interested in drawing representations of graph sets here.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com