info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Functions: Not just sets of ordered pairs
183 views
Skip to first unread message
Dan Christensen
Jan 17, 2022, 5:24:54โฏPM1/17/22
to
RECALL:
A function is often represented as a set of ordered pairs.
Example: Function f = {(0, 0), (1,2), (2, 4)}
The domain of f in this case would be {0, 1, 2}.
The range would be {0, 2, 4}.
The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.
Using the standard function notation, we can write:
f(0) = 0, f(1) = 2 and f(2) = 4
Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:
f = {(a, b) : a in X & b in Y & F(a,b)}
where F is a suitable binary predicate.
Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).
Alternatively, we could write as follows use predicate logic:
(1) ALL(a): ALL(b): [f(a) = b <=> a in x & b in y & F(a,b)]
BURSE'S PARADOX
If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.
We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:
(2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]
Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.
(To be continued)
Comments so far?
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
A function is often represented as a set of ordered pairs.
Example: Function f = {(0, 0), (1,2), (2, 4)}
The domain of f in this case would be {0, 1, 2}.
The range would be {0, 2, 4}.
The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.
Using the standard function notation, we can write:
f(0) = 0, f(1) = 2 and f(2) = 4
Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:
f = {(a, b) : a in X & b in Y & F(a,b)}
where F is a suitable binary predicate.
Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).
Alternatively, we could write as follows use predicate logic:
(1) ALL(a): ALL(b): [f(a) = b <=> a in x & b in y & F(a,b)]
BURSE'S PARADOX
If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.
We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:
(2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]
Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.
(To be continued)
Comments so far?
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
Mostowski Collapse
Jan 17, 2022, 5:35:12โฏPM1/17/22
to
You can make the "paradox" stronger. Not only outside the
domain, also outside the codomain. Here is the proof
sketch for the butterfly color paradox.
The rest is relatively easy, take some h e F,
you can construct this set:
H = { (x,y) | x e butterfly & y e color & g(x)=y }
Now by Russell construction there is an a,
with ~(a e butterfly) and by the same construction
there is some a b, with ~(b e color).
Now construct this set:
G = H u { (a,b) }
By your Function Axiom there is a function g.
Its easy to show:
i) g e F
ii) ~g(a) e color
Therefore EXIST(y):EXIST(g):[g e F & ~g(y) e color] .
Q.E.D.
domain, also outside the codomain. Here is the proof
sketch for the butterfly color paradox.
The rest is relatively easy, take some h e F,
you can construct this set:
H = { (x,y) | x e butterfly & y e color & g(x)=y }
Now by Russell construction there is an a,
with ~(a e butterfly) and by the same construction
there is some a b, with ~(b e color).
Now construct this set:
G = H u { (a,b) }
By your Function Axiom there is a function g.
Its easy to show:
i) g e F
ii) ~g(a) e color
Therefore EXIST(y):EXIST(g):[g e F & ~g(y) e color] .
Q.E.D.
Dan Christensen
Jan 17, 2022, 5:57:19โฏPM1/17/22
to
On Monday, January 17, 2022 at 5:35:12 PM UTC-5, Mostowski Collapse wrote:
> Dan Christensen schrieb am Montag, 17. Januar 2022 um 23:24:54 UTC+1:
> > RECALL:
> >
> > A function is often represented as a set of ordered pairs.
> >
> > Example: Function f = {(0, 0), (1,2), (2, 4)}
> >
> > The domain of f in this case would be {0, 1, 2}.
> >
> > The range would be {0, 2, 4}.
> >
> > The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.
> >
> > Using the standard function notation, we can write:
> >
> > f(0) = 0, f(1) = 2 and f(2) = 4
> >
> > Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:
> >
> > f = {(a, b) : a in X & b in Y & F(a,b)}
> >
> > where F is a suitable binary predicate.
> >
> > Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).
> >
> > Alternatively, we could write as follows use predicate logic:
> >
> > (1) ALL(a): ALL(b): [f(a) = b <=> a in x & b in y & F(a,b)]
> >
> > BURSE'S PARADOX
> >
> > If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.
> >
> > We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:
> >
> > (2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]
> >
> > Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.
> >
> > (To be continued)
> >
> > Comments so far?
> >
> >
> Dan Christensen schrieb am Montag, 17. Januar 2022 um 23:24:54 UTC+1:
> > RECALL:
> >
> > A function is often represented as a set of ordered pairs.
> >
> > Example: Function f = {(0, 0), (1,2), (2, 4)}
> >
> > The domain of f in this case would be {0, 1, 2}.
> >
> > The range would be {0, 2, 4}.
> >
> > The codomain is ambiguous in this case. It could be any superset of {0, 2, 4}, e.g. the range set itself, the set of all even numbers or the set of all natural numbers.
> >
> > Using the standard function notation, we can write:
> >
> > f(0) = 0, f(1) = 2 and f(2) = 4
> >
> > Generalizing, for a domain of X and codomain of Y might define a function f as follows using set-builder notation:
> >
> > f = {(a, b) : a in X & b in Y & F(a,b)}
> >
> > where F is a suitable binary predicate.
> >
> > Here, f is a set of ordered pairs, a subset of the X*Y (the Cartesian product).
> >
> > Alternatively, we could write as follows use predicate logic:
> >
> > (1) ALL(a): ALL(b): [f(a) = b <=> a in x & b in y & F(a,b)]
> >
> > BURSE'S PARADOX
> >
> > If we have t not in X and u in Y, then from (1), we can obtain f(t) =/= u even though t is OUTSIDE of the domain of f. Shouldn't f(t) be UNDEFINED in this case? Yes.
> >
> > We can resolve this paradoxical situation for tweaking (1) just a bit to obtain:
> >
> > (2) ALL(a): ALL(b): [a in X & b in Y => [f(a) = b <=> F(a,b)]
> >
> > Then f(t) would be UNDEFINED for t outside of its domain X. Then, of course, f would no longer be just a set of ordered pairs.
> >
> > (To be continued)
> >
> > Comments so far?
> >
> >
> You can make the "paradox" stronger. Not only outside the
> domain, also outside the codomain.
Not necessary here.
> domain, also outside the codomain.
> Here is the proof
> sketch for the butterfly color paradox.
>
> The rest is relatively easy, take some h e F,
> you can construct this set:
>
> H = { (x,y) | x e butterfly & y e color & g(x)=y }
>
> Now by Russell construction there is an a,
> with ~(a e butterfly) and by the same construction
> there is some a b, with ~(b e color).
>
> Now construct this set:
>
> G = H u { (a,b) }
>
> By your Function Axiom there is a function g.
> Its easy to show:
>
> i) g e F
> ii) ~g(a) e color
>
> Therefore EXIST(y):EXIST(g):[g e F & ~g(y) e color] .
>
Chung Haas
Jan 17, 2022, 6:22:44โฏPM1/17/22
to
Dan Christensen wrote:
> RECALL: A function is often represented as a set of ordered pairs.
> Example: Function f = {(0, 0), (1,2), (2, 4)}
> The domain of f in this case would be {0, 1, 2}.
> The range would be {0, 2, 4}.
SHOCK VIDEO: NHS Doctor Says โAll The Vaccines Will Be Recalled Soonโ
> RECALL: A function is often represented as a set of ordered pairs.
> Example: Function f = {(0, 0), (1,2), (2, 4)}
> The domain of f in this case would be {0, 1, 2}.
> The range would be {0, 2, 4}.
https://banned.video/watch?id=61e5c97eaf1fcf7b54e28a0a
REINER FUELLMICH- "THESE BA$TARDS ARE TRYING TO KILL US AND THATS THE
BOTTOM LINE.. WE MUST ACT NOW
https://153news.net/watch_video.php?v=Y9A461YX8HHO
Is This Evidence That All The Jabs In The UK Are Being Pulled?
https://www.bitchute.com/video/Mk8yEdDkk4ua/
Timothy Golden
Jan 18, 2022, 9:07:05โฏAM1/18/22
to
Still, it is true that calculus can be performed albeit errantly at discrete intervals.
Still, what makes it calculus is its ability to refine arbitrarily.
I just bumped into this in the Boolean sense, thinking maybe I had created a Boolean differential.
I think possibly this discrete form could be taken as an open problem with a bifurcated interpretation:
1. Differential discrete form allowed.
2. No such thing as a differential in discrete form exists.
I suppose then we have to ask whether 1+1=2 in your system?
By claiming such a limited space to work in are you caught further defining that space's qualities?
Or are they inherited from some old assumptions that are going unstated?
The invalid assumption is generally the one of interest.
The bug lays there.
Dan Christensen
Jan 18, 2022, 12:33:53โฏPM1/18/22
to
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.
>
> I suppose then we have to ask whether 1+1=2 in your system?
>
Mostowski Collapse
Jan 18, 2022, 12:44:00โฏPM1/18/22
to
With Peano unit its much more easier.
Define Zermelo natural numbers as:
b = a <=> b e {a}
Now 0={}, 1={{}}, 2={{{}}}.
Define Zermelo natural numbers as:
b = a <=> b e {a}
Now 0={}, 1={{}}, 2={{{}}}.
Then it is trivial to derive 1+1=2.
Dan Christensen schrieb:
Mostowski Collapse
Jan 18, 2022, 12:48:46โฏPM1/18/22
to
Here is a proof, write i(a) for {a}:
(โxAxnx โง โxโyโz(Axyz โ Axi(y)i(z))) โ Ai(n)i(n)i(i(n)) is valid.
https://www.umsu.de/trees/#~6x%28Axnx%29~1~6x~6y~6z%28Axyz~5Axi%28y%29i%28z%29%29~5Ai%28n%29i%28n%29i%28i%28n%29%29
Only 11 proof lines.
Mostowski Collapse schrieb:
(โxAxnx โง โxโyโz(Axyz โ Axi(y)i(z))) โ Ai(n)i(n)i(i(n)) is valid.
https://www.umsu.de/trees/#~6x%28Axnx%29~1~6x~6y~6z%28Axyz~5Axi%28y%29i%28z%29%29~5Ai%28n%29i%28n%29i%28i%28n%29%29
Only 11 proof lines.
Mostowski Collapse schrieb:
Timothy Golden
Jan 18, 2022, 12:57:37โฏPM1/18/22
to
where is f(3)?
I understand I can't break you here, but it does seem troubling doesn't it?
You want to claim some pure function that works on one and works on two, but refuses to work on 3?
What sort of f'ing f() is this?
Mostowski Collapse
Jan 18, 2022, 1:01:44โฏPM1/18/22
to
Here is a proof, 2+1=3, this time p(_,_) function and not A(_,_,_) relation:
?- prove0('(โx p(x,n)=x โง โxโyโz(p(x,y)=z โ p(x,i(y))=i(z))) โ p(i(i(n)),i(n))=i(i(i(n)))', 4, unicode), !.
http://www.xlog.ch/izytab/moblet/en/docs/18_live/34_bil2022/paste22/package.html
1. โx p(x, n) = x โง โx โy โz (p(x, y) = z โ p(x, i(y)) = i(z)) โ p(i(i(n)), i(n)) = i(i(i(n)))
2. p(i(i(n)), i(n)) = i(i(i(n))) (Tโ2 1)
3. ยฌ(โx p(x, n) = x โง โx โy โz (p(x, y) = z โ p(x, i(y)) = i(z))) (Tโ1 1)
4. ยฌโx โy โz (p(x, y) = z โ p(x, i(y)) = i(z)) (Fโง2 3)
5. ยฌโx p(x, n) = x (Fโง1 3)
6. ยฌp(i(i(n)), n) = i(i(n)) (Fโ 5)
7. ยฌโy โz (p(i(i(n)), y) = z โ p(i(i(n)), i(y)) = i(z)) (Fโ 4)
8. ยฌโz (p(i(i(n)), n) = z โ p(i(i(n)), i(n)) = i(z)) (Fโ 7)
9. ยฌ(p(i(i(n)), n) = i(i(n)) โ p(i(i(n)), i(n)) = i(i(i(n)))) (Fโ 8)
10. p(i(i(n)), n) = i(i(n)) (Fโ1 9)
โ (ax 6, 10)
10. ยฌp(i(i(n)), i(n)) = i(i(i(n))) (Fโ2 9)
โ (ax 10, 2)
?- prove0('(โx p(x,n)=x โง โxโyโz(p(x,y)=z โ p(x,i(y))=i(z))) โ p(i(i(n)),i(n))=i(i(i(n)))', 4, unicode), !.
http://www.xlog.ch/izytab/moblet/en/docs/18_live/34_bil2022/paste22/package.html
1. โx p(x, n) = x โง โx โy โz (p(x, y) = z โ p(x, i(y)) = i(z)) โ p(i(i(n)), i(n)) = i(i(i(n)))
2. p(i(i(n)), i(n)) = i(i(i(n))) (Tโ2 1)
3. ยฌ(โx p(x, n) = x โง โx โy โz (p(x, y) = z โ p(x, i(y)) = i(z))) (Tโ1 1)
4. ยฌโx โy โz (p(x, y) = z โ p(x, i(y)) = i(z)) (Fโง2 3)
5. ยฌโx p(x, n) = x (Fโง1 3)
6. ยฌp(i(i(n)), n) = i(i(n)) (Fโ 5)
7. ยฌโy โz (p(i(i(n)), y) = z โ p(i(i(n)), i(y)) = i(z)) (Fโ 4)
8. ยฌโz (p(i(i(n)), n) = z โ p(i(i(n)), i(n)) = i(z)) (Fโ 7)
9. ยฌ(p(i(i(n)), n) = i(i(n)) โ p(i(i(n)), i(n)) = i(i(i(n)))) (Fโ 8)
10. p(i(i(n)), n) = i(i(n)) (Fโ1 9)
โ (ax 6, 10)
10. ยฌp(i(i(n)), i(n)) = i(i(i(n))) (Fโ2 9)
โ (ax 10, 2)
Dan Christensen
Jan 18, 2022, 1:12:18โฏPM1/18/22
to
On Tuesday, January 18, 2022 at 12:44:00 PM UTC-5, Mostowski Collapse wrote:
> With Peano unit its much more easier.
> Define Zermelo natural numbers as:
>
> b = a <=> b e {a}
>
> Now 0={}, 1={{}}, 2={{{}}}.
> Then it is trivial to derive 1+1=2.
Since the addition function is not defined in the ZFC axioms, you would first have to prove its existence using only the ZFC axioms.
> With Peano unit its much more easier.
> Define Zermelo natural numbers as:
>
> b = a <=> b e {a}
>
> Now 0={}, 1={{}}, 2={{{}}}.
> Then it is trivial to derive 1+1=2.
Dan Christensen
Jan 18, 2022, 1:19:31โฏPM1/18/22
to
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).
> 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?
> where is f(3)?
> I understand I can't break you here, but it does seem troubling doesn't it?
> You want to claim some pure function that works on one and works on two, but refuses to work on 3?
sergio
Jan 18, 2022, 1:24:15โฏPM1/18/22
to
https://tutorial.math.lamar.edu/Classes/Alg/FunctionDefn.aspx
Definition of Relation: A relation is a set of ordered pairs.
Definition of a Function: A function is a relation for which each value from the set the first components of the ordered pairs is associated with
exactly one value from the set of second components of the ordered pair.
โWorking Definitionโ of Function: A function is an equation for which any x that can be plugged into the equation will yield exactly one y out of the
equation.
SO you are rightamundo!
Mostowski Collapse
Jan 18, 2022, 1:45:52โฏPM1/18/22
to
Ha Ha, the Thread Says "Not just sets of ordered pairs",
But Dan-O-Matic nevertheless rants:
of existence of addition? But why is then your addition
not just set, since you proved it like that?
The answer is the "Working Practice" uses different cosmetics.
This is what causes Dan-O-Matik a sisyphus. He invented the
Function Axiom, because he does not want to write (x,y) e f,
he prefers that from the outside one sees f(x,y).
The problem is that his Function Axiom transfers a set-like
function into a FOL function symbol. But FOL function symbols
are classes and not sets. But the Function Axiom is
totally unnecessary, I can directly prove:
1. โx (x, n, x) โ a โง โx โy โz ((x, y, z) โ a โ (x, i(y), i(z)) โ a) โ (i(i(n)), i(n), i(i(i(n)))) โ a
2. (i(i(n)), i(n), i(i(i(n)))) โ a (Tโ2 1)
3. ยฌ(โx (x, n, x) โ a โง โx โy โz ((x, y, z) โ a โ (x, i(y), i(z)) โ a)) (Tโ1 1)
4. ยฌโx โy โz ((x, y, z) โ a โ (x, i(y), i(z)) โ a) (Fโง2 3)
5. ยฌโx (x, n, x) โ a (Fโง1 3)
6. ยฌ(i(i(n)), n, i(i(n))) โ a (Fโ 5)
7. ยฌโy โz ((i(i(n)), y, z) โ a โ (i(i(n)), i(y), i(z)) โ a) (Fโ 4)
8. ยฌโz ((i(i(n)), n, z) โ a โ (i(i(n)), i(n), i(z)) โ a) (Fโ 7)
9. ยฌ((i(i(n)), n, i(i(n))) โ a โ (i(i(n)), i(n), i(i(i(n)))) โ a) (Fโ 8)
10. (i(i(n)), n, i(i(n))) โ a (Fโ1 9)
โ (ax 6, 10)
10. ยฌ(i(i(n)), i(n), i(i(i(n)))) โ a (Fโ2 9)
โ (ax 10, 2)
You can further restrict a and show that it exists. But
its NOWHERE NEEDED TO PROVE 2+1=3. You only
more about a when you for example want to prove:
2+1 =\= 4
But it would be more easier to abandon the Function Axiom
and provide some notation based on Peano Apostroph, or
some such. And not run into class problems and
function spaces that are as big as the universal class.
But Dan-O-Matic nevertheless rants:
> Since the addition function is not defined in the ZFC
axioms, you would first have to prove its existence
using only the ZFC axioms
If I remember well you use pairs resp. triples for your proof
axioms, you would first have to prove its existence
using only the ZFC axioms
of existence of addition? But why is then your addition
not just set, since you proved it like that?
The answer is the "Working Practice" uses different cosmetics.
This is what causes Dan-O-Matik a sisyphus. He invented the
Function Axiom, because he does not want to write (x,y) e f,
he prefers that from the outside one sees f(x,y).
The problem is that his Function Axiom transfers a set-like
function into a FOL function symbol. But FOL function symbols
are classes and not sets. But the Function Axiom is
totally unnecessary, I can directly prove:
1. โx (x, n, x) โ a โง โx โy โz ((x, y, z) โ a โ (x, i(y), i(z)) โ a) โ (i(i(n)), i(n), i(i(i(n)))) โ a
2. (i(i(n)), i(n), i(i(i(n)))) โ a (Tโ2 1)
3. ยฌ(โx (x, n, x) โ a โง โx โy โz ((x, y, z) โ a โ (x, i(y), i(z)) โ a)) (Tโ1 1)
4. ยฌโx โy โz ((x, y, z) โ a โ (x, i(y), i(z)) โ a) (Fโง2 3)
5. ยฌโx (x, n, x) โ a (Fโง1 3)
6. ยฌ(i(i(n)), n, i(i(n))) โ a (Fโ 5)
7. ยฌโy โz ((i(i(n)), y, z) โ a โ (i(i(n)), i(y), i(z)) โ a) (Fโ 4)
8. ยฌโz ((i(i(n)), n, z) โ a โ (i(i(n)), i(n), i(z)) โ a) (Fโ 7)
9. ยฌ((i(i(n)), n, i(i(n))) โ a โ (i(i(n)), i(n), i(i(i(n)))) โ a) (Fโ 8)
10. (i(i(n)), n, i(i(n))) โ a (Fโ1 9)
โ (ax 6, 10)
10. ยฌ(i(i(n)), i(n), i(i(i(n)))) โ a (Fโ2 9)
โ (ax 10, 2)
You can further restrict a and show that it exists. But
its NOWHERE NEEDED TO PROVE 2+1=3. You only
more about a when you for example want to prove:
2+1 =\= 4
But it would be more easier to abandon the Function Axiom
and provide some notation based on Peano Apostroph, or
some such. And not run into class problems and
function spaces that are as big as the universal class.
Dan Christensen
Jan 18, 2022, 2:38:11โฏPM1/18/22
to
On Tuesday, January 18, 2022 at 1:45:52 PM UTC-5, Mostowski Collapse wrote:
> Ha Ha, the Thread Says "Not just sets of ordered pairs",
>
> But Dan-O-Matic nevertheless rants:
> > Since the addition function is not defined in the ZFC
> > axioms, you would first have to prove its existence
> > using only the ZFC axioms
> If I remember well you use pairs resp. triples for your proof
> of existence of addition? But why is then your addition
> not just set, since you proved it like that?
>
I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in n].
> Ha Ha, the Thread Says "Not just sets of ordered pairs",
>
> But Dan-O-Matic nevertheless rants:
> > Since the addition function is not defined in the ZFC
> > axioms, you would first have to prove its existence
> > using only the ZFC axioms
> If I remember well you use pairs resp. triples for your proof
> of existence of addition? But why is then your addition
> not just set, since you proved it like that?
>
Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in n (see Burse's Paradox). Deal with, Jan Burse.
> The answer is the "Working Practice" uses different cosmetics.
>
> This is what causes Dan-O-Matik a sisyphus. He invented the
> Function Axiom, because he does not want to write (x,y) e f,
> he prefers that from the outside one sees f(x,y).
>
> The problem is that his Function Axiom transfers a set-like
> function into a FOL function symbol. But FOL function symbols
> are classes and not sets.
There they say that, " In common usage, the function is generally distinguished from its graph [G]. In this approach, a function is defined as an ordered triple (X, Y, G)."
G is a set of ordered n-tuples. For addition, G would include (0, 0, 0), (1, 0, 1), (0, 1, 1), (1, 1, 2), etc. You want to equate f and G. That may work quite well in informal settings, but not in formal proofs (see Burse's Paradox).
> But the Function Axiom is totally unnecessary...
On the contrary, it gives the sufficient conditions for the existence of a function. It formally enables us use the functional notation, e.g. y = f(x).
Mostowski Collapse
Jan 18, 2022, 2:42:58โฏPM1/18/22
to
WHATS WRONG WITH YOU????
DONT YOU REMEMBER WHAT YOU PROVED YOURSELF???
"common usage" is something informal. If you want to dig deeper
things become much more complicated. And your function axiom
does not guarantee existence of add(_,_,_). It depends on existence
of (_,_,_) e add. Namely the subset axiom or however you created
add. Your function axiom only transfers one existence into another
existence. Its not the primary cause of existence of add in your proof.
You can check your own proof by yourself. Or did you forget what you proved?
You don't have a function axiom that shows existence directly
inside some "common usage" only. You nevertheless fall back to set
theory. You wouldn't be able to show existence of add without set theory.
DONT YOU REMEMBER WHAT YOU PROVED YOURSELF???
"common usage" is something informal. If you want to dig deeper
things become much more complicated. And your function axiom
does not guarantee existence of add(_,_,_). It depends on existence
of (_,_,_) e add. Namely the subset axiom or however you created
add. Your function axiom only transfers one existence into another
existence. Its not the primary cause of existence of add in your proof.
You can check your own proof by yourself. Or did you forget what you proved?
You don't have a function axiom that shows existence directly
inside some "common usage" only. You nevertheless fall back to set
theory. You wouldn't be able to show existence of add without set theory.
Crypto Rich
Jan 18, 2022, 2:55:15โฏPM1/18/22
to
Dan Christensen wrote:
>> If I remember well you use pairs resp. triples for your proof of
>> existence of addition? But why is then your addition not just set,
>> since you proved it like that?
>>
> I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in
> n]. Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in
> n (see Burse's Paradox). Deal with, Jan Burse.
this theory sucks big time. Rand Paul Wonders If YouTube Will "Kiss My
>> If I remember well you use pairs resp. triples for your proof of
>> existence of addition? But why is then your addition not just set,
>> since you proved it like that?
>>
> I was able to show that: ALL(a): ALL(b): [a in n & b in n => add(a,b) in
> n]. Much to your chagrin, add(x, y) is then UNDEFINED for x or y not in
> n (see Burse's Paradox). Deal with, Jan Burse.
Ass And Apologize" After CDC Admits Cloth Masks Aren't Effective
Mostowski Collapse
Jan 18, 2022, 3:01:07โฏPM1/18/22
to
Here is what you do, instead of only using this here:
โx (x, n, x) โ a โง โx โy โz ((x, y, z) โ a โ (x, i(y), i(z)) โ a) โ (i(i(n)), i(n), i(i(i(n)))) โ a
Call a set a, that satisfies the above, an adder-inductive-set,
abbrevatied ais. You make a minimal, in that you define it:
(x,y,z) e a <=> (x,y,z) e N x N x N & (โa' ais(a) => (x,y,z) e a')
https://math.stackexchange.com/a/784504/1002973
The above construction primarily uses the Subset Axiom.
The Function Axiom only transfers into your cosmetic,
that you wrongly think is "common usage". The fallacy
is not how you construct add or some such, how you use
set theory. The fallacy in your doing is the function axiom,
since it transfers into FOL function symbols.
You cannot prove:
EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
You even dont have equality f=g for function symbols f,g.
On the otherhand, what is constructed with the Subset Axiom
is unique. It is easy to prove EXISTUNIQUE(a). Everything that
is constructed with the Subset Axiom is unique.
โx (x, n, x) โ a โง โx โy โz ((x, y, z) โ a โ (x, i(y), i(z)) โ a) โ (i(i(n)), i(n), i(i(i(n)))) โ a
abbrevatied ais. You make a minimal, in that you define it:
(x,y,z) e a <=> (x,y,z) e N x N x N & (โa' ais(a) => (x,y,z) e a')
https://math.stackexchange.com/a/784504/1002973
The above construction primarily uses the Subset Axiom.
The Function Axiom only transfers into your cosmetic,
that you wrongly think is "common usage". The fallacy
is not how you construct add or some such, how you use
set theory. The fallacy in your doing is the function axiom,
since it transfers into FOL function symbols.
You cannot prove:
EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
You even dont have equality f=g for function symbols f,g.
On the otherhand, what is constructed with the Subset Axiom
is unique. It is easy to prove EXISTUNIQUE(a). Everything that
is constructed with the Subset Axiom is unique.
Mostowski Collapse
Jan 18, 2022, 3:06:17โฏPM1/18/22
to
Corr.: Typo
(x,y,z) e a <=> (x,y,z) e N x N x N & (โa' ais(a') => (x,y,z) e a')
https://math.stackexchange.com/a/784504/1002973
(x,y,z) e a <=> (x,y,z) e N x N x N & (โa' ais(a') => (x,y,z) e a')
https://math.stackexchange.com/a/784504/1002973
Dan Christensen
Jan 18, 2022, 3:07:59โฏPM1/18/22
to
> "common usage" is something informal. If you want to dig deeper
> things become much more complicated. And your function axiom
> does not guarantee existence of add(_,_,_). It depends on existence
>
> of (_,_,_) e add.
This overloading is an issue I addressed in my latest update to DC Proof. The name assigned to a function must now differ from the name of graph set. I can see that it has caused you some confusion. I hope the change will clear things up for you. No, I won't hold my breath!
> things become much more complicated. And your function axiom
> does not guarantee existence of add(_,_,_). It depends on existence
>
> of (_,_,_) e add.
Mostowski Collapse
Jan 18, 2022, 3:15:33โฏPM1/18/22
to
Its useless nonsense what you are doing. Its not anymore
"common usage". You cannot prove:
EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
You only read Landau. You didn't read Dedekind:
"Richard Dedekind's theorem 126 of his "Was sind und was sollen
die Zahlen? (1888)". This work was the first to give a proof that
a certain recursive construction defines a unique function.
https://en.wikipedia.org/wiki/Primitive_recursive_function#History
You cannot replicate the above in your "common usage".
There is much missing.
"common usage". You cannot prove:
EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
You only read Landau. You didn't read Dedekind:
"Richard Dedekind's theorem 126 of his "Was sind und was sollen
die Zahlen? (1888)". This work was the first to give a proof that
a certain recursive construction defines a unique function.
https://en.wikipedia.org/wiki/Primitive_recursive_function#History
You cannot replicate the above in your "common usage".
There is much missing.
Mostowski Collapse
Jan 18, 2022, 4:01:57โฏPM1/18/22
to
Also there is very poor motivation for these exercises,
since Landau doesn't show anything with an implication
in it, when he talks about some equations.
Just use the equations directly. Here is a proof 1+1 =/= 1:
โxโy(s(x)=s(y) โ x=y),
โxยฌn=s(x),
โxp(x,n)=x, /* Landau x+1=x', but with zero */
โxโyโzp(x,s(y))=s(p(x,y)) /* Landau x+y' = (x+y)' */
entails ยฌp(s(n),s(n))=s(n).
So why bother and answer on MSE, when the OP showed
equations without an implication. Where does this
implication come from?
[(e,f,g)โdโน(e,S(f),S(g))โd]
https://math.stackexchange.com/a/784504/1002973
Its not a translation of /* Landau x+y' = (x+y)' */.
How do you correctly translate Landau?
since Landau doesn't show anything with an implication
in it, when he talks about some equations.
Just use the equations directly. Here is a proof 1+1 =/= 1:
โxโy(s(x)=s(y) โ x=y),
โxยฌn=s(x),
โxp(x,n)=x, /* Landau x+1=x', but with zero */
โxโyโzp(x,s(y))=s(p(x,y)) /* Landau x+y' = (x+y)' */
entails ยฌp(s(n),s(n))=s(n).
So why bother and answer on MSE, when the OP showed
equations without an implication. Where does this
implication come from?
[(e,f,g)โdโน(e,S(f),S(g))โd]
https://math.stackexchange.com/a/784504/1002973
Its not a translation of /* Landau x+y' = (x+y)' */.
How do you correctly translate Landau?
Dan Christensen
Jan 18, 2022, 4:11:29โฏPM1/18/22
to
On Tuesday, January 18, 2022 at 3:15:33 PM UTC-5, Mostowski Collapse wrote:
> Its useless nonsense what you are doing. Its not anymore
> "common usage". You cannot prove:
>
> EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
>
Recently posted here...
> Its useless nonsense what you are doing. Its not anymore
> "common usage". You cannot prove:
>
> EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
>
Existence of Add Function on N:
EXIST(add):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
& ALL(a):[a in n => add(a,0)=a]
& ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]
https://www.dcproof.com/ConstructAdditionNew.htm (712 lines)
Uniqueness of Add Function on N:
ALL(add):ALL(add'):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
& ALL(a):[a in n => add(a,0)=a]
& ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]
& ALL(a):ALL(b):[a in n & b in n => add'(a,b) in n]
& ALL(a):[a in n => add'(a,0)=a]
& ALL(a):ALL(b):[a in n & b in n => add'(a,s(b))=s(add'(a,b))]
=> ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
https://dcproof.com/AdditionOnNUnique.htm (84 lines)
Mostowski Collapse
Jan 18, 2022, 4:22:42โฏPM1/18/22
to
Its not the same as what you can prove for sets.
You only prove relative equality:
ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
For the set itself, you can prove absolute equality.
If you have two sets:
ALL(x):[x e s1 <=> x e d & A(x)]
ALL(x):[x e s2 <=> x e d & A(x)]
Then you can prove s1 = s2 absolutely. Try
it, you don't need the a in n & b in n for sets.
You only prove relative equality:
ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
If you have two sets:
ALL(x):[x e s1 <=> x e d & A(x)]
ALL(x):[x e s2 <=> x e d & A(x)]
Then you can prove s1 = s2 absolutely. Try
it, you don't need the a in n & b in n for sets.
Mostowski Collapse
Jan 18, 2022, 4:27:59โฏPM1/18/22
to
This absolute uniqueness of the addition function,
how you create it as a set and not as a Dan-O-Matik
function, is a consequence of:
- Extensionality Axiom for Sets
(- And the Subset Axiom itself of course)
You can try yourself:
โsโt(โx(Exs โ Ext) โ s=t), /* Extensionality */
โx(Exa โ (Exd โง px)), /* a is from Subset */
โx(Exb โ (Exd โง px)) /* b is from Subset */
entails a=b. /* They are absolutely the same */
https://www.umsu.de/trees/#~6s~6t%28~6x%28Exs~4Ext%29~5s=t%29,~6x%28Exa~4Exd~1p%28x%29%29,~6x%28Exb~4Exd~1p%28x%29%29|=a=b
Unfortunately you cannot prove it, when you would add:
- Extenionality Axiom for Dan-O-Matik function
Because your Function Axiom is nonsense.
how you create it as a set and not as a Dan-O-Matik
function, is a consequence of:
- Extensionality Axiom for Sets
(- And the Subset Axiom itself of course)
You can try yourself:
โsโt(โx(Exs โ Ext) โ s=t), /* Extensionality */
โx(Exa โ (Exd โง px)), /* a is from Subset */
โx(Exb โ (Exd โง px)) /* b is from Subset */
entails a=b. /* They are absolutely the same */
https://www.umsu.de/trees/#~6s~6t%28~6x%28Exs~4Ext%29~5s=t%29,~6x%28Exa~4Exd~1p%28x%29%29,~6x%28Exb~4Exd~1p%28x%29%29|=a=b
Unfortunately you cannot prove it, when you would add:
- Extenionality Axiom for Dan-O-Matik function
Because your Function Axiom is nonsense.
Dan Christensen
Jan 18, 2022, 5:25:36โฏPM1/18/22
to
On Tuesday, January 18, 2022 at 4:22:42 PM UTC-5, Mostowski Collapse wrote:
> Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 22:11:29 UTC+1:
> > On Tuesday, January 18, 2022 at 3:15:33 PM UTC-5, Mostowski Collapse wrote:
> > > Its useless nonsense what you are doing. Its not anymore
> > > "common usage". You cannot prove:
> > >
> > > EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
> > >
> > Recently posted here...
> >
> > Existence of Add Function on N:
> >
> > EXIST(add):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
> > & ALL(a):[a in n => add(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]
> >
> > https://www.dcproof.com/ConstructAdditionNew.htm (712 lines)
> >
> > Uniqueness of Add Function on N:
> >
> > ALL(add):ALL(add'):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
> > & ALL(a):[a in n => add(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]
> >
> > & ALL(a):ALL(b):[a in n & b in n => add'(a,b) in n]
> > & ALL(a):[a in n => add'(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add'(a,s(b))=s(add'(a,b))]
> >
> > => ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
> >
> > https://dcproof.com/AdditionOnNUnique.htm (84 lines)
> Dan Christensen schrieb am Dienstag, 18. Januar 2022 um 22:11:29 UTC+1:
> > On Tuesday, January 18, 2022 at 3:15:33 PM UTC-5, Mostowski Collapse wrote:
> > > Its useless nonsense what you are doing. Its not anymore
> > > "common usage". You cannot prove:
> > >
> > > EXISTUNIQUE(add):ALL(a):ALL(b): [a in n & b in n => add(a,b) in n]
> > >
> > Recently posted here...
> >
> > Existence of Add Function on N:
> >
> > EXIST(add):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
> > & ALL(a):[a in n => add(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]]
> >
> > https://www.dcproof.com/ConstructAdditionNew.htm (712 lines)
> >
> > Uniqueness of Add Function on N:
> >
> > ALL(add):ALL(add'):[ALL(a):ALL(b):[a in n & b in n => add(a,b) in n]
> > & ALL(a):[a in n => add(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add(a,s(b))=s(add(a,b))]
> >
> > & ALL(a):ALL(b):[a in n & b in n => add'(a,b) in n]
> > & ALL(a):[a in n => add'(a,0)=a]
> > & ALL(a):ALL(b):[a in n & b in n => add'(a,s(b))=s(add'(a,b))]
> >
> > => ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
> >
> > https://dcproof.com/AdditionOnNUnique.htm (84 lines)
> Its not the same as what you can prove for sets.
> You only prove relative equality:
> ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
Thus avoiding Burse's Paradox.
> You only prove relative equality:
> ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
> For the set itself, you can prove absolute equality.
> If you have two sets:
>
> ALL(x):[x e s1 <=> x e d & A(x)]
>
> ALL(x):[x e s2 <=> x e d & A(x)]
>
Mostowski Collapse
Jan 18, 2022, 5:58:36โฏPM1/18/22
to
Then you are talking about another case.
Not the EXISTUNIQUE case.
Not the EXISTUNIQUE case.
Mostowski Collapse
Jan 18, 2022, 6:04:56โฏPM1/18/22
to
You can check yourself, there is no domain involved,
and there are no arguments involved, for the existence
of an object uniquely:
https://en.wikipedia.org/wiki/Uniqueness_quantification#Reduction_to_ordinary_existential_and_universal_quantification
So this here is nonsense, what you proved. Its all
useless nonsense:
ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
What you need to be able to prove is this here:
add = add'
This is the conclusion in the uniqueness part,
of the uniqueness quantification, namely this variant
of the quantifier:
EXIST(x):P(x) & ALL(y):ALL)(z);[(P(y) & P(z)) => y=z].
This means your Function Axiom has the following
pros and cons:
- Pro: The Dan-O-Matik Function Axiom gives indeed
existence, i.e. EXIST(x):P(x)
- Cons: The Dan-O-Matik Function Axiom doesn't give
unqiueness, i.e. ALL(y):ALL)(z);[(P(y) & P(z)) => y=z]
The later is a multifacted problem, there is not only
no definition of equality of function symbols in
DC Proof, if such an equality would be there,
an absolute equality would not yield unique functions,
only a relative equality does, where the y and z are
further restrained.
So your Function Axiom doesn't work. It does not
yield EXISTUNIQUE.
and there are no arguments involved, for the existence
of an object uniquely:
https://en.wikipedia.org/wiki/Uniqueness_quantification#Reduction_to_ordinary_existential_and_universal_quantification
So this here is nonsense, what you proved. Its all
useless nonsense:
ALL(a):ALL(b):[a in n & b in n => add(a,b)=add'(a,b)]]
add = add'
This is the conclusion in the uniqueness part,
of the uniqueness quantification, namely this variant
of the quantifier:
EXIST(x):P(x) & ALL(y):ALL)(z);[(P(y) & P(z)) => y=z].
This means your Function Axiom has the following
pros and cons:
- Pro: The Dan-O-Matik Function Axiom gives indeed
existence, i.e. EXIST(x):P(x)
- Cons: The Dan-O-Matik Function Axiom doesn't give
unqiueness, i.e. ALL(y):ALL)(z);[(P(y) & P(z)) => y=z]
The later is a multifacted problem, there is not only
no definition of equality of function symbols in
DC Proof, if such an equality would be there,
an absolute equality would not yield unique functions,
only a relative equality does, where the y and z are
further restrained.
So your Function Axiom doesn't work. It does not
yield EXISTUNIQUE.
Dan Christensen
Jan 18, 2022, 6:26:52โฏPM1/18/22
to
Get a life.
Dan
Timothy Golden
Jan 18, 2022, 7:12:41โฏPM1/18/22
to
Since you seem keen to allow in the successor within this context then X is Y. No Cartesian product is possible; at least this could be a route to identify the problem: Copies of sets do not actually exist. A set is in an abstract land whereby X is X is X. Y is X is X is X. All is X and all is X and X in X need no Cartesian product. So the pair as points do alight and the graph is of three distinct points; like spikes but there is no zero return. We are in purely graphical space and possibly not even the origin shows itself. Colors at zero are blue and red, say. blue at one and two. red at two and four.
Now we have a cryptic representation of your land. Should segments exist it is clear how they go. They tie the correct red to the correct blue. They will grow in thickness in a way that can get you some 2D action, but the usual way is too lame.
Thinking of a triple spike is more the signal processors' route, but we do not have a physical undefined within the possibility space. Indeed we probably blow fuses past ten volts for the sake of the instrument. It is sad to think that both of these constructions come flatly under the term 'function' and it poses some sort of maybeland of a conjunction and I suppose this ranks back toward the brc.
What other classes are there? Are these here discretes?
If 2 in X is 2 in Y and zero likewise how then how, now, brown cow?
The first set mentioned I suppose takes precedence, but is that set defined?
Should it be defined first? Before it is put into hard use and confused by two names?
Dan Christensen
Jan 18, 2022, 7:36:30โฏPM1/18/22
to
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.
> 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.
>
[snip]
Timothy Golden
Jan 19, 2022, 8:54:54โฏAM1/19/22
to
X is Y is X is X is the natural numbers.
Defining things as undefined is not a legitimate business.
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.
I'll stand by me earlier tripe that you ignore here.
X is Y and so there is only X.
Just as in the sum the resultant is in the space of the source.
Possibly there lays an option, but I'm not going to state it here yet.
And by the way, what I haven't said is undefined.
And as well what I say I believe to be true.
Ought that be stated clearly?
Well certainly mistakes do deserve to be corrected.
Anyone's, really.
I do think there is room for criticism, though what you've got does seem to be by the book, other than a few peculiatities.
Of course to most this bookish mode is all they care to pursue.
Yet the way you've posed it it seems you are prepared to engage in a progression.
Even the triple spike is dubious, you know.
Dan Christensen
Jan 19, 2022, 10:52:07โฏAM1/19/22
to
> Defining things as undefined is not a legitimate business.
> 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.
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.
Makes no sense. I cannot comment. Sorry.
Mostowski Collapse
Jan 19, 2022, 11:47:28โฏAM1/19/22
to
ts rather students beware of DC Proof. Why would one
construct add with material implication, when equations
offer everything that is needed?
[(e,f,g)โdโน(e,S(f),S(g))โd]
Dan-O-Matiks Add Construction
https://math.stackexchange.com/a/784504/1002973
Just use the equations directly. Here is a proof 1+1 =/= 1:
โxโy(s(x)=s(y) โ x=y),
โxยฌn=s(x),
โxp(x,n)=x, /* Landau x+1=x', but with zero */
โxโyโzp(x,s(y))=s(p(x,y)) /* Landau x+y' = (x+y)' */
entails ยฌp(s(n),s(n))=s(n).
https://www.umsu.de/trees/#~6x~6y%28s%28x%29=s%28y%29~5x=y%29,~6x~3n=s%28x%29,~6xp%28x,n%29=x,~6x~6y~6zp%28x,s%28y%29%29=s%28p%28x,y%29%29|=~3p%28s%28n%29,s%28n%29%29=s%28n%29
What theorem of number theory requires the add
construction, i.e. is not yet covered by equations
and induction over successor?
construct add with material implication, when equations
offer everything that is needed?
[(e,f,g)โdโน(e,S(f),S(g))โd]
Dan-O-Matiks Add Construction
https://math.stackexchange.com/a/784504/1002973
Just use the equations directly. Here is a proof 1+1 =/= 1:
โxโy(s(x)=s(y) โ x=y),
โxยฌn=s(x),
โxp(x,n)=x, /* Landau x+1=x', but with zero */
โxโyโzp(x,s(y))=s(p(x,y)) /* Landau x+y' = (x+y)' */
entails ยฌp(s(n),s(n))=s(n).
What theorem of number theory requires the add
construction, i.e. is not yet covered by equations
and induction over successor?
Mostowski Collapse
Jan 19, 2022, 11:54:28โฏAM1/19/22
to
Who believes even that Number Theory needs x e N, i.e.
DC Poop set theory. Cannot a large part of Number Theory
been done without the extra x e N, and with only equations?
What did Landau post on MSE where Dan-O-Matik
responded. It was a) only equations and b) there was
no x e N. So why an off topic response? What theorems
in Number Theory cannot be proved with:
- Landau Equations
- This induction schema without set theory, no x e N:
A(0) forall x (A(x) => A(x+1))
-----------------------------------------------------
forall y A(y)
A(x) is generically a formula which talks about x.
DC Poop set theory. Cannot a large part of Number Theory
been done without the extra x e N, and with only equations?
What did Landau post on MSE where Dan-O-Matik
responded. It was a) only equations and b) there was
no x e N. So why an off topic response? What theorems
in Number Theory cannot be proved with:
- Landau Equations
- This induction schema without set theory, no x e N:
A(0) forall x (A(x) => A(x+1))
-----------------------------------------------------
forall y A(y)
A(x) is generically a formula which talks about x.
Mostowski Collapse
Jan 19, 2022, 12:04:10โฏPM1/19/22
to
If you have nowhere x e N , and do Number Theory like that,
most of Dan-O-Matiks proof are anyway not needed. Since
for FOL function symbol we can anway prove that they
are "functions", this here is provable:
โxโy(y=f(x) โง โz(z=f(x) โ y=z)) is valid.
Its not anymore provable in DC Proof. LoL
So FOL functions carry a kind of passport, and the passport
is recognized by a prover, and the prover can then show
"function"-ness for FOL functions.
Unfortunately the passport of Dan-O-Matik FOL function
symbols has been ripped apart by changes in (forall)
Rule. The FOL function symbols in DC Proof
don't carry this passport anymore.
most of Dan-O-Matiks proof are anyway not needed. Since
for FOL function symbol we can anway prove that they
are "functions", this here is provable:
โxโy(y=f(x) โง โz(z=f(x) โ y=z)) is valid.
Its not anymore provable in DC Proof. LoL
So FOL functions carry a kind of passport, and the passport
is recognized by a prover, and the prover can then show
"function"-ness for FOL functions.
Unfortunately the passport of Dan-O-Matik FOL function
symbols has been ripped apart by changes in (forall)
Rule. The FOL function symbols in DC Proof
don't carry this passport anymore.
Dan Christensen
Jan 19, 2022, 1:21:12โฏPM1/19/22
to
On Wednesday, January 19, 2022 at 11:47:28 AM UTC-5, Mostowski Collapse wrote:
> Why would one
> construct add with material implication, when equations
> offer everything that is needed?
>
Material implication???
> Why would one
> construct add with material implication, when equations
> offer everything that is needed?
>
The purpose of the proof was to not simply define addition on N in a line or two, but to actually prove the existence of the required function, starting from first principles--from Peano's axioms for (N, S, 0) in this case.
https://www.dcproof.com/ConstructAdditionNew.htm (712 lines)
Dan Christensen
Jan 19, 2022, 2:25:02โฏPM1/19/22
to
On Wednesday, January 19, 2022 at 12:04:10 PM UTC-5, Mostowski Collapse wrote:
> Since for FOL function symbol we can anway prove that they
>
> are "functions", this here is provable:
>
> โxโy(y=f(x) โง โz(z=f(x) โ y=z)) is valid.
>
As in most textbook math proofs, as in DC Proof, here you really need to specify a domain (dom) and codomain (cod) for function f, ie. ALL(x):[x in dom => f(x) in cod].
> Since for FOL function symbol we can anway prove that they
>
> are "functions", this here is provable:
>
> โxโy(y=f(x) โง โz(z=f(x) โ y=z)) is valid.
>
Then it is easy to prove:
ALL(x):[x in dom => EXIST(y):[y in cod & [y=f(x) & ALL(z):[z in cod => [z=f(x) => y=z]]]]] (16 lines in DC Proof)
[snip]
> Unfortunately the passport of Dan-O-Matik FOL function
> symbols has been ripped apart by changes in (forall)
> Rule. The FOL function symbols in DC Proof
>
Mostowski Collapse
Jan 20, 2022, 12:52:26โฏAM1/20/22
to
Take Landaus textbook here, scroll to the screenshot in the question.
(e,f,g)โdโน(e,S(f),S(g))โd]
Dan-O-Matiks Add Construction
https://math.stackexchange.com/a/784504/1002973
There is no x e N, no y e N, etc...
What is going on, how can he do so much textbook
mathematics without any Dan-O-Matik-ism.
When is Dan-O-Matik-ism necessary?
(e,f,g)โdโน(e,S(f),S(g))โd]
Dan-O-Matiks Add Construction
https://math.stackexchange.com/a/784504/1002973
What is going on, how can he do so much textbook
mathematics without any Dan-O-Matik-ism.
When is Dan-O-Matik-ism necessary?
Mostowski Collapse
Jan 20, 2022, 12:58:47โฏAM1/20/22
to
Can you make a number theory example where your
"add" is needed, that cannot be proved with:
โxโy(s(x)=s(y) โ x=y),
โxยฌn=s(x),
โxp(x,n)=x, /* Landau x+1=x', but with zero */
โxโyโzp(x,s(y))=s(p(x,y)) /* Landau x+y' = (x+y)' */
And with:
A(0) forall x (A(x) => A(x+1))
-----------------------------------------------------
forall y A(y)
A(x) is generically a formula which talks about x.
The only problem is that without x e N, y e N etc you
cannot formulate induction in your tool. You
have no schema variables, whereby other tools and
we humans can use the schema.
"add" is needed, that cannot be proved with:
โxโy(s(x)=s(y) โ x=y),
โxยฌn=s(x),
โxp(x,n)=x, /* Landau x+1=x', but with zero */
โxโyโzp(x,s(y))=s(p(x,y)) /* Landau x+y' = (x+y)' */
A(0) forall x (A(x) => A(x+1))
-----------------------------------------------------
forall y A(y)
A(x) is generically a formula which talks about x.
cannot formulate induction in your tool. You
have no schema variables, whereby other tools and
we humans can use the schema.
Mostowski Collapse
Jan 20, 2022, 1:13:46โฏAM1/20/22
to
Also generally I have doubt that Dan-O-Matiks material
implication construction says something. Material
implication is bugged with paradoxes:
"In most systems of formal logic, a broader relationship
called material implication is employed, which is read
โIf A, then B,โ and is denoted by A โ B or A โ B. The
truth or falsity of the compound proposition A โ B
depends not on any relationship between the meanings
of the propositions but only on the truth-values of A and
B; A โ B is false when A is true and B is false,
and it is true in all other cases."
"Equivalently, A โ B is often defined as โผ(AยทโผB) or as
โผAโจB (in which โผ means โnot,โ ยท means โand,โ and โจ
means โorโ). This way of interpreting โ leads to the
so-called paradoxes of material implication: โgrass is
red โ ice is coldโ is a true proposition according to
this definition of โ."
For example Dan-O-Matik uses, when he constructs add:
[(๐,๐,๐)โ๐โน(๐,๐(๐),๐(๐))โ๐]
And arrives at the definition of add via equations:
โ๐โ๐:๐๐๐(๐,0)=๐
โ๐,๐โ๐:๐๐๐(๐,๐(๐))=๐(๐๐๐(๐,๐))
But I was rather expecting something stronger for add:
[(๐,๐,๐)โadd <=> (๐,๐(๐),๐(๐))โadd]
Can he prove the above bi-conditional? And follows
the bi-conditional from the equations?
implication construction says something. Material
implication is bugged with paradoxes:
"In most systems of formal logic, a broader relationship
called material implication is employed, which is read
โIf A, then B,โ and is denoted by A โ B or A โ B. The
truth or falsity of the compound proposition A โ B
depends not on any relationship between the meanings
of the propositions but only on the truth-values of A and
B; A โ B is false when A is true and B is false,
and it is true in all other cases."
"Equivalently, A โ B is often defined as โผ(AยทโผB) or as
โผAโจB (in which โผ means โnot,โ ยท means โand,โ and โจ
means โorโ). This way of interpreting โ leads to the
so-called paradoxes of material implication: โgrass is
red โ ice is coldโ is a true proposition according to
this definition of โ."
For example Dan-O-Matik uses, when he constructs add:
[(๐,๐,๐)โ๐โน(๐,๐(๐),๐(๐))โ๐]
And arrives at the definition of add via equations:
โ๐โ๐:๐๐๐(๐,0)=๐
โ๐,๐โ๐:๐๐๐(๐,๐(๐))=๐(๐๐๐(๐,๐))
But I was rather expecting something stronger for add:
[(๐,๐,๐)โadd <=> (๐,๐(๐),๐(๐))โadd]
Can he prove the above bi-conditional? And follows
the bi-conditional from the equations?
Dan Christensen
Jan 20, 2022, 9:58:39โฏAM1/20/22
to
On Thursday, January 20, 2022 at 12:58:47 AM UTC-5, Mostowski Collapse wrote:
>
> A(x) is generically a formula which talks about x.
> The only problem is that without x e N, y e N etc you
> cannot formulate induction in your tool.
Wrong again, Jan Burse. Once again, here is the DC Proof version of Peano's Axioms
>
> A(x) is generically a formula which talks about x.
> The only problem is that without x e N, y e N etc you
> cannot formulate induction in your tool.
1. Set(n)
Axiom
2 0 in n
Axiom
3. ALL(a):[a in n => s(a) in n]
Axiom
4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
Axiom
5. ALL(a):[a in n => ~s(a)=0]
Axiom
Here is the induction axiom. Note that the set a is subset of N.
6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in a => s(b) in a]
=> ALL(b):[b in n => b in a]]]
Axiom
> You
>
> have no schema variables, whereby other tools and
> we humans can use the schema.
Mostowski Collapse
Jan 20, 2022, 10:04:29โฏAM1/20/22
to
Why do you need x e N. Doesn't make any sense.
Its not shown by Landau. People have become
schizophrenic, and are ambivalent to ZFC, up to
for example the love and hate of Dan-O-Matik.
So he has set, like x e N, in his DC Proof but he rants
about ZFC all the time. I guess a real logic teacher
would not do that. For example take this ZFC theorem:
/* Problem from Set Theory */
?- time(prove0('โpโq(โx(xโpโxโq)โp=q) โง \
โx(xโuโr(x)) โง \
โx(xโvโr(x)) โ \
u=v', 6, unicode)), !.
% Wall 4902 ms, gc 7 ms, 1830308 lips
http://www.xlog.ch/izytab/moblet/en/docs/18_live/34_bil2022/paste23/package.html
Shows uniqueness of the naive set builder. Thats quite
interesting that the above theorem is agnostic to any
further backround set theory and is purely logical:
/* Encoding Mxy for xโy */
โpโq(โx(MxpโMxq)โp=q)โงโx(Mxuโr(x))โงโx(Mxvโr(x))โu=v
https://www.umsu.de/trees/#~6p~6q(~6x(Mxp~4Mxq)~5p=q)~1~6x(Mxu~4r(x))~1~6x(Mxv~4r(x))~5u=v
We can even go one step further, its purely logical
that it even does not depend on first order equality:
/* Encoding Mxy for xโy, Exy for x=y */
(โpโq(โx(Mxp โ Mxq) โ Epq) โง (โx(Mxu โ rx) โง โx(Mxv โ rx))) โ Euv is valid.
https://www.umsu.de/trees/#~6p~6q(~6x(Mxp~4Mxq)~5Epq)~1~6x(Mxu~4r(x))~1~6x(Mxv~4r(x))~5Euv
So the real logic teaching is all about relations or
complexes as the name that Russell used, borrowed
from Moore it seems:
Russellโs Logical Atomism
https://plato.stanford.edu/entries/logical-atomism/
Its not shown by Landau. People have become
schizophrenic, and are ambivalent to ZFC, up to
for example the love and hate of Dan-O-Matik.
So he has set, like x e N, in his DC Proof but he rants
about ZFC all the time. I guess a real logic teacher
would not do that. For example take this ZFC theorem:
/* Problem from Set Theory */
?- time(prove0('โpโq(โx(xโpโxโq)โp=q) โง \
โx(xโuโr(x)) โง \
โx(xโvโr(x)) โ \
u=v', 6, unicode)), !.
% Wall 4902 ms, gc 7 ms, 1830308 lips
http://www.xlog.ch/izytab/moblet/en/docs/18_live/34_bil2022/paste23/package.html
Shows uniqueness of the naive set builder. Thats quite
interesting that the above theorem is agnostic to any
further backround set theory and is purely logical:
/* Encoding Mxy for xโy */
โpโq(โx(MxpโMxq)โp=q)โงโx(Mxuโr(x))โงโx(Mxvโr(x))โu=v
https://www.umsu.de/trees/#~6p~6q(~6x(Mxp~4Mxq)~5p=q)~1~6x(Mxu~4r(x))~1~6x(Mxv~4r(x))~5u=v
We can even go one step further, its purely logical
that it even does not depend on first order equality:
/* Encoding Mxy for xโy, Exy for x=y */
(โpโq(โx(Mxp โ Mxq) โ Epq) โง (โx(Mxu โ rx) โง โx(Mxv โ rx))) โ Euv is valid.
https://www.umsu.de/trees/#~6p~6q(~6x(Mxp~4Mxq)~5Epq)~1~6x(Mxu~4r(x))~1~6x(Mxv~4r(x))~5Euv
So the real logic teaching is all about relations or
complexes as the name that Russell used, borrowed
from Moore it seems:
Russellโs Logical Atomism
https://plato.stanford.edu/entries/logical-atomism/
Dan Christensen
Jan 20, 2022, 10:11:36โฏAM1/20/22
to
On Thursday, January 20, 2022 at 1:13:46 AM UTC-5, Mostowski Collapse wrote:
> Also generally I have doubt that Dan-O-Matiks material
> implication construction says something. Material
> implication is bugged with paradoxes:
>
Do not confuse the counterintuitive with the paradoxical. I have seen lists of so-called paradoxes of material implication, but they were all easily resolved.
> Also generally I have doubt that Dan-O-Matiks material
> implication construction says something. Material
> implication is bugged with paradoxes:
>
Dan Christensen
Jan 20, 2022, 10:20:32โฏAM1/20/22
to
On Thursday, January 20, 2022 at 10:04:29 AM UTC-5, Mostowski Collapse wrote:
> > > The only problem is that without x e N, y e N etc you
> > > cannot formulate induction in your tool.
> > Wrong again, Jan Burse. Once again, here is the DC Proof version of Peano's Axioms
> >
> > 1. Set(n)
> > Axiom
> >
> > 2 0 in n
> > Axiom
> >
> > 3. ALL(a):[a in n => s(a) in n]
> > Axiom
> >
> > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > Axiom
> >
> > 5. ALL(a):[a in n => ~s(a)=0]
> > Axiom
> >
> > Here is the induction axiom. Note that the set a is subset of N.
> >
> > 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in a => s(b) in a]
> > => ALL(b):[b in n => b in a]]]
> > Axiom
> > > You
> > >
> > > have no schema variables, whereby other tools and
> > > we humans can use the schema.
> > Note that we are talking about subsets of N in the induction axiom (line 6). The "schema variables" in the Subset Axiom are sufficient for inductive proofs.
> > > The only problem is that without x e N, y e N etc you
> > > cannot formulate induction in your tool.
> > Wrong again, Jan Burse. Once again, here is the DC Proof version of Peano's Axioms
> >
> > 1. Set(n)
> > Axiom
> >
> > 2 0 in n
> > Axiom
> >
> > 3. ALL(a):[a in n => s(a) in n]
> > Axiom
> >
> > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > Axiom
> >
> > 5. ALL(a):[a in n => ~s(a)=0]
> > Axiom
> >
> > Here is the induction axiom. Note that the set a is subset of N.
> >
> > 6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in a => s(b) in a]
> > => ALL(b):[b in n => b in a]]]
> > Axiom
> > > You
> > >
> > > have no schema variables, whereby other tools and
> > > we humans can use the schema.
> > Note that we are talking about subsets of N in the induction axiom (line 6). The "schema variables" in the Subset Axiom are sufficient for inductive proofs.
> Why do you need x e N. Doesn't make any sense.
I have no "x e N" here. What are you talking about, Jan Burse?
Mostowski Collapse
Jan 20, 2022, 10:30:57โฏAM1/20/22
to
Logic itself is not based on x e N. This comes only
later. You use x e N in 6 places here:
ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in a => s(b) in a]
> > => ALL(b):[b in n => b in a]]]
and derived from it other methods and tools. Its not
clear what the world model of DC Proof is.
We hear things about non-empty domain of discourse.
We have now tweaked (refl) and (forall) rules. It
is clearly not anymore FOL logic.
What is the model theory of DC Proof?
https://en.wikipedia.org/wiki/Model_theory#Varied_emphasis
later. You use x e N in 6 places here:
ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in a => s(b) in a]
> > => ALL(b):[b in n => b in a]]]
> So the real logic teaching is all about relations or
> complexes as the name that Russell used, borrowed
> from Moore it seems:
>
> Russellโs Logical Atomism
> https://plato.stanford.edu/entries/logical-atomism/
Unless you present an other world model architecture,
> complexes as the name that Russell used, borrowed
> from Moore it seems:
>
> Russellโs Logical Atomism
> https://plato.stanford.edu/entries/logical-atomism/
and derived from it other methods and tools. Its not
clear what the world model of DC Proof is.
We hear things about non-empty domain of discourse.
We have now tweaked (refl) and (forall) rules. It
is clearly not anymore FOL logic.
What is the model theory of DC Proof?
https://en.wikipedia.org/wiki/Model_theory#Varied_emphasis
Mostowski Collapse
Jan 20, 2022, 10:36:59โฏAM1/20/22
to
Corr.: Didn't count correctly, its not six (6) its seven (7):
Logic itself is not based on x e N. This comes only
later. You use x e N in 7 places here:
ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in a => s(b) in a]
=> ALL(b):[b in n => b in a]]]
Compare what Landau would use:
A(1), forall x (A(x) => A(x+1))
-----------------------------------------------------
forall y A(y)
It only uses an unary Russell complex A(_) 4 times.
Thats what is used in education:
Initial Step. We must verify that P(1) is True.
Inductive Step. Here we must prove the following assertion:
"If there is a k such that P(k) is true, then (for this same k) P(k+1) is true.
http://zimmer.csufresno.edu/~larryc/proofs/proofs.mathinduction.html
Logic itself is not based on x e N. This comes only
ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in a => s(b) in a]
=> ALL(b):[b in n => b in a]]]
A(1), forall x (A(x) => A(x+1))
-----------------------------------------------------
forall y A(y)
It only uses an unary Russell complex A(_) 4 times.
Thats what is used in education:
Initial Step. We must verify that P(1) is True.
Inductive Step. Here we must prove the following assertion:
"If there is a k such that P(k) is true, then (for this same k) P(k+1) is true.
http://zimmer.csufresno.edu/~larryc/proofs/proofs.mathinduction.html
Mostowski Collapse
Jan 20, 2022, 10:38:11โฏAM1/20/22
to
If Landau works in Number Theory, why would he need x e N?
Can you make an example, of a Number Theory theorem,
that needs x e N, and cannot be proved with Landau?
Dan Christensen
Jan 20, 2022, 10:41:50โฏAM1/20/22
to
On Thursday, January 20, 2022 at 1:13:46 AM UTC-5, Mostowski Collapse wrote:
> ...when he constructs add:
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.
> ...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]
>
Wesi Ebbs
Jan 20, 2022, 1:24:03โฏPM1/20/22
to
Mostowski Collapse wrote:
> Can you make a number theory example where your "add" is needed, that
> cannot be proved with: โxโy(s(x)=s(y) โ x=y), โxยฌn=s(x),
> โxp(x,n)=x, /* Landau x+1=x', but with zero */ โxโyโzp(x,s(y))=s(p(x,y))
> /* Landau x+y' = (x+y)' */
you fake money capitalists have to forget the fake "covid_19" plandemic,
> Can you make a number theory example where your "add" is needed, that
> cannot be proved with: โxโy(s(x)=s(y) โ x=y), โxยฌn=s(x),
> โxp(x,n)=x, /* Landau x+1=x', but with zero */ โxโyโzp(x,s(y))=s(p(x,y))
> /* Landau x+y' = (x+y)' */
same way you forgot the fake manned moon landing, 9/11, the weapons of
mass destruction, the bombing of Serbia and the fake chemical attacks in
Syria, for instance. That's fake money capitalism.
Mostowski Collapse
Jan 20, 2022, 1:31:02โฏPM1/20/22
to
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
โxโy(x + y = y + x)
A: Not at all, it doesn't use x e N. LoL
Dan Christensen
Jan 20, 2022, 1:51:53โฏPM1/20/22
to
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:
Dan
> 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.
> โxโy(x + y = y + x)
>
Dan
Dan Christensen
Jan 21, 2022, 12:24:14โฏAM1/21/22
to
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:
> Q: How do you use DC Proof to prove Landau's:
>
> โxโy(x + y = y + x)
>
https://dcproof.com/AddComm.htm
> โxโy(x + y = y + x)
>
Mostowski Collapse
Jan 21, 2022, 12:48:26โฏPM1/21/22
to
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
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-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
Dan-O-Matiks Add Construction
https://math.stackexchange.com/a/784504/1002973
|
|
|
|
|
|
|
|
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)
Mostowski Collapse
Jan 21, 2022, 12:50:18โฏPM1/21/22
to
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.
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
Jan 21, 2022, 12:51:32โฏPM1/21/22
to
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.
โ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.
Dan Christensen
Jan 21, 2022, 4:16:51โฏPM1/21/22
to
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.
> 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,
Timothy Golden
Jan 23, 2022, 8:03:30โฏAM1/23/22
to
> > 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).
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.
Dan Christensen
Jan 23, 2022, 8:55:03โฏAM1/23/22
to
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]
> > > 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.
Not interested in drawing representations of graph sets here.
0 new messages