Dan Christensen wrote:

> On Friday, February 4, 2022 at 2:54:34 PM UTC-5, Mostowski Collapse
> wrote:
>> Well the domain of a function is easy: dom(f) := { x | ∃y (x,y) e f }
>> You then have: f = g => dom(f) = dom(g) Don't you have dom()
>
> I haven't found it necessary. As is standard practice in textbook math
> proofs, whenever I introduce a function in a proof, I also introduce its
> domain and codomain sets.

yes, sure, but in capitalism

YOU CANNOT TRUST THESE HOSPITALS - THEY ARE KILLING PEOPLE
https://www.brighteon.com/c827bb83-95e5-4f9d-a86e-0c7e3a396d54

On Friday, February 4, 2022 at 3:15:38 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> And what is your standard practice SAME-ness, that you
> are using.

Again, for any sets X and Y, and for functions f and g such that, for all x in X, we have both f(x) in Y and g(x) in Y, then f and g are said to be the same functions iff for all x in X, we have f(x)=g(x).

Deal with it, Jan Burse. Maybe read a math textbook and see for yourself.

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, February 4, 2022 at 3:26:29 PM UTC-5, Vendle Dower wrote:
> Dan Christensen wrote:
>
> > On Friday, February 4, 2022 at 2:54:34 PM UTC-5, Mostowski Collapse
> > wrote:
> >> Well the domain of a function is easy: dom(f) := { x | ∃y (x,y) e f }
> >> You then have: f = g => dom(f) = dom(g) Don't you have dom()
> >
> > I haven't found it necessary. As is standard practice in textbook math
> > proofs, whenever I introduce a function in a proof, I also introduce its
> > domain and codomain sets.
> yes, sure, but in capitalism
>
> YOU CANNOT TRUST THESE HOSPITALS - THEY ARE KILLING PEOPLE
> https://www.brighteon.com/c827bb83-95e5-4f9d-a86e-0c7e3a396d54

You need to find a forum for dumber people, "Vendle." Didn't Donald Trump start up some social media thing? You are wasting your time here.

Dan

Dan-O-Matik halucinated:
> for all x in X, we have f(x)=g(x)
Your sameness ≈ doesn't work:

∀x(ExX → f(x)=g(x)) → ∀y(∃xy=f(x) ↔ ∃xy=g(x)) is invalid.

Hence you cannot prove:

f ≈ g => dom(f) = dom(g)

With your shitty sameness.

Dan Christensen schrieb:
> On Friday, February 4, 2022 at 3:26:29 PM UTC-5, Vendle Dower wrote:
>> Dan Christensen wrote:
>>
>>> On Friday, February 4, 2022 at 2:54:34 PM UTC-5, Mostowski Collapse
>>> wrote:
>>>> Well the domain of a function is easy: dom(f) := { x | ∃y (x,y) e f }
>>>> You then have: f = g => dom(f) = dom(g) Don't you have dom()
>>>
>>> I haven't found it necessary. As is standard practice in textbook math
>>> proofs, whenever I introduce a function in a proof, I also introduce its
>>> domain and codomain sets.
>> yes, sure, but in capitalism
>>
>> YOU CANNOT TRUST THESE HOSPITALS - THEY ARE KILLING PEOPLE
>> https://www.brighteon.com/c827bb83-95e5-4f9d-a86e-0c7e3a396d54
>
> You need to find a forum for dumber people, "Vendle." Didn't Donald Trump start up some social media thing? You are wasting your time here.
>
> Dan
>

Corr.:

Dan-O-Matik halucinated:
> for all x in X, we have f(x)=g(x)
Your sameness ≈ doesn't work:

∀x(ExX → (Exf ↔ Exg)) → ∀x(∃y(Eyf ∧ x=p(y))
↔ ∃y(Eyg ∧ x=p(y))) is invalid.
https://www.umsu.de/trees/#~6x%28ExX~5%28Exf~4Exg%29%29~5~6x%28~7y%28Eyf~1x=p%28y%29%29~4~7y%28Eyg~1x=p%28y%29%29%29

Hence you cannot prove:

f ≈ g => dom(f) = dom(g)

With your shitty sameness.

Dan Christensen schrieb:
> On Friday, February 4, 2022 at 3:26:29 PM UTC-5, Vendle Dower wrote:
>> Dan Christensen wrote:
>>
>>> On Friday, February 4, 2022 at 2:54:34 PM UTC-5, Mostowski Collapse
>>> wrote:
>>>> Well the domain of a function is easy: dom(f) := { x | ∃y (x,y) e f }
>>>> You then have: f = g => dom(f) = dom(g) Don't you have dom()
>>>
>>> I haven't found it necessary. As is standard practice in textbook math
>>> proofs, whenever I introduce a function in a proof, I also introduce its
>>> domain and codomain sets.
>> yes, sure, but in capitalism
>>
>> YOU CANNOT TRUST THESE HOSPITALS - THEY ARE KILLING PEOPLE
>> https://www.brighteon.com/c827bb83-95e5-4f9d-a86e-0c7e3a396d54
>
> You need to find a forum for dumber people, "Vendle." Didn't Donald Trump start up some social media thing? You are wasting your time here.
>
> Dan
>

Corr. Corr.:

Dan-O-Matik halucinated:
> for all x in X, we have f(x)=g(x)
Your sameness ≈ doesn't work:

/* Variable z ranges over pairs, p(z) is
the first projection, Exy is used to encode x in y */
∀z(Ep(z)X → (Ezf ↔ Ezg)) → ∀x(∃z(Ezf ∧ x=p(z)) ↔ ∃z(Ezg ∧ x=p(z))) is
invalid.
https://www.umsu.de/trees/#~6z%28Ep%28z%29X~5%28Ezf~4Ezg%29%29~5~6x%28~7z%28Ezf~1x=p%28z%29%29~4~7z%28Ezg~1x=p%28z%29%29%29

Hence you cannot prove:

f ≈ g => dom(f) = dom(g)

With your shitty sameness.

Dan Christensen schrieb:
> On Friday, February 4, 2022 at 3:26:29 PM UTC-5, Vendle Dower wrote:
>> Dan Christensen wrote:
>>
>>> On Friday, February 4, 2022 at 2:54:34 PM UTC-5, Mostowski Collapse
>>> wrote:
>>>> Well the domain of a function is easy: dom(f) := { x | ∃y (x,y) e f }
>>>> You then have: f = g => dom(f) = dom(g) Don't you have dom()
>>>
>>> I haven't found it necessary. As is standard practice in textbook math
>>> proofs, whenever I introduce a function in a proof, I also introduce its
>>> domain and codomain sets.
>> yes, sure, but in capitalism
>>
>> YOU CANNOT TRUST THESE HOSPITALS - THEY ARE KILLING PEOPLE
>> https://www.brighteon.com/c827bb83-95e5-4f9d-a86e-0c7e3a396d54
>
> You need to find a forum for dumber people, "Vendle." Didn't Donald Trump start up some social media thing? You are wasting your time here.
>
> Dan
>

On Friday, February 4, 2022 at 3:58:18 PM UTC-5, Mostowski Collapse wrote:

> Your sameness ≈ doesn't work:

Wrong again, Jan Burse.

> /* Variable z ranges over pairs, p(z) is
> the first projection, Exy is used to encode x in y */
> ∀z(Ep(z)X → (Ezf ↔ Ezg)) → ∀x(∃z(Ezf ∧ x=p(z)) ↔ ∃z(Ezg ∧ x=p(z))) is
> invalid.
>

Still makes no sense. Please translate into some reasonable approximation of the notation of set theory.

https://www.umsu.de/trees/#~6z%28Ep%28z%29X~5%28Ezf~4Ezg%29%29~5~6x%28~7z%28Ezf~1x=p%28z%29%29~4~7z%28Ezg~1x=p%28z%29%29%29
> Hence you cannot prove:
>
> f ≈ g => dom(f) = dom(g)
>

True, because there is no dom function/operator built into DC Proof. So what???

Dan

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

Dan-O-Matik halucinated:
> for all x in X, we have f(x)=g(x)
You cannot prove:

f ≈ g => dom(f) = dom(g)

With your nonsense sameness.
Thats pretty evident, isn't it?

What if X' is a superset of X, and
f : X' -> Y, and X'' is a another superset of X,
g : X'' -> Y, and the following is provable,

since f and g agree on X:

for all x in X, we have f(x)=g(x)

Nevertheless dom(f) =\= dom(g).
How would you formulate your same-ness
so that this doesn't happen?

Can you give a formula of your sameness
without this defect?

Dan Christensen schrieb am Freitag, 4. Februar 2022 um 22:17:50 UTC+1:
> On Friday, February 4, 2022 at 3:58:18 PM UTC-5, Mostowski Collapse wrote:
>
> > Your sameness ≈ doesn't work:
> Wrong again, Jan Burse.
> > /* Variable z ranges over pairs, p(z) is
> > the first projection, Exy is used to encode x in y */
> > ∀z(Ep(z)X → (Ezf ↔ Ezg)) → ∀x(∃z(Ezf ∧ x=p(z)) ↔ ∃z(Ezg ∧ x=p(z))) is
> > invalid.
> >
> Still makes no sense. Please translate into some reasonable approximation of the notation of set theory.
> https://www.umsu.de/trees/#~6z%28Ep%28z%29X~5%28Ezf~4Ezg%29%29~5~6x%28~7z%28Ezf~1x=p%28z%29%29~4~7z%28Ezg~1x=p%28z%29%29%29
> > Hence you cannot prove:
> >
> > f ≈ g => dom(f) = dom(g)
> >
> True, because there is no dom function/operator built into DC Proof. So what???
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Dan Christensen wrote:

>> > I haven't found it necessary. As is standard practice in textbook
>> > math proofs, whenever I introduce a function in a proof, I also
>> > introduce its domain and codomain sets.
>> yes, sure, but in capitalism
>>
>> YOU CANNOT TRUST THESE HOSPITALS - THEY ARE KILLING PEOPLE
>> https://www.brighteon.com/c827bb83-95e5-4f9d-a86e-0c7e3a396d54
>
> You need to find a forum for dumber people, "Vendle." Didn't Donald
> Trump start up some social media thing? You are wasting your time here.

let me translate, you are stupid like a door. Doors are made by wood. You
disgusting *big_pharma_capitalist*. You are a *mass_murderer*. The
*trucker_convoy* is about to shit the crap out of you.

On Friday, February 4, 2022 at 5:21:40 PM UTC-5, Mostowski Collapse (aka Collapsing Jan Burse) wrote:
> Dan-O-Matik halucinated:
> > for all x in X, we have f(x)=g(x)
> You cannot prove:
> f ≈ g => dom(f) = dom(g)

Geez, yer dumb, Jan Burse! If the domains and codomains of a pair of functions are not identical, the functions in question are simply not comparable. Quit making a fool of yourself.

Dan

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

What do you mean by not comparable?
You got a third truth value for SAME-ness:

{true,false,meaningless}

Did you develop DC poop in the 80's (*) under
heavy drug use and are still searching somebody who

buys it? Dan-O-Matik during development of DC poop:

80's Acid Clubland Part 1 (Dream Police)
https://www.youtube.com/watch?v=r4JzaOkliwg

Dan Christensen schrieb am Samstag, 5. Februar 2022 um 02:46:10 UTC+1:
> On Friday, February 4, 2022 at 5:21:40 PM UTC-5, Mostowski Collapse (aka Collapsing Jan Burse) wrote:
> > Dan-O-Matik halucinated:
> > > for all x in X, we have f(x)=g(x)
> > You cannot prove:
> > f ≈ g => dom(f) = dom(g)
> Geez, yer dumb, Jan Burse! If the domains and codomains of a pair of functions are not identical, the functions in question are simply not comparable. Quit making a fool of yourself.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

So f ≈ g is not always definite, i.e. has a truth value
true or false. Sometimes if f and g are incomparable
and then f ≈ g flounders right? It then has the third

truth value "meaningless". So f ≈ g is not definable,
how convenient! Because a definition would give it
a truth value true or false, depending on f,g.

So my initial question what SAME-ness is used in the
uniqueness here remains for ever unanswered?

Dan Christensen schrieb am Dienstag, 1. Februar 2022 um 21:16:23 UTC+1:
> & ALL(idx'):[ALL(a):[a in x => idx'(a)=a] <-- Uniqueness
=> ALL(a):[a in x => idx'(a)=idx(a)]]]]

Woa! Because you only prove uniqueness for comparable
f and g. If f and g are not comparable we dont know whether
idx is unique. So there can be indeed idx', not comparable

with idx, but nevertheless ALL(a):[a in x => idx'(a)=a].

Right? So idx is in fact not unique, because it can have non-
comparable idx' which can be substituted for idx. So your
proof is nonsense, you nowhere proved uniqueness.

LMAO!

Mostowski Collapse schrieb am Samstag, 5. Februar 2022 um 16:13:30 UTC+1:
> What do you mean by not comparable?
> You got a third truth value for SAME-ness:
>
> {true,false,meaningless}
>
> Did you develop DC poop in the 80's (*) under
> heavy drug use and are still searching somebody who
>
> buys it? Dan-O-Matik during development of DC poop:
>
> 80's Acid Clubland Part 1 (Dream Police)
> https://www.youtube.com/watch?v=r4JzaOkliwg
> Dan Christensen schrieb am Samstag, 5. Februar 2022 um 02:46:10 UTC+1:
> > On Friday, February 4, 2022 at 5:21:40 PM UTC-5, Mostowski Collapse (aka Collapsing Jan Burse) wrote:
> > > Dan-O-Matik halucinated:
> > > > for all x in X, we have f(x)=g(x)
> > > You cannot prove:
> > > f ≈ g => dom(f) = dom(g)
> > Geez, yer dumb, Jan Burse! If the domains and codomains of a pair of functions are not identical, the functions in question are simply not comparable. Quit making a fool of yourself.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

Your nonsense would make some sense if you would replace:
"uniqueness"

By the following:
"uniqueness among comparable elements"

And if you would define f and g comparable, i.e. f ↓ g.
But the ordinary uniqueness has no comparable provision,
namely you dont find comparable:

1) ∃ x ( P ( x ) ∧ ∀ y ( P ( y ) → y = x ) ) .
2) ∃ x P ( x ) ∧ ∀ y ∀ z [ ( P ( y ) ∧ P ( z ) ) → y = z ] .
3) ∃ x ∀ y ( P ( y ) ↔ y = x ) .
https://en.wikipedia.org/wiki/Uniqueness_quantification

But it is then still questionable what sameness you
are using, and whether we could possibly get:

∀ x ∀ y [ x ↓ y & x ≈ y → ∀ F ( F x ↔ F y ) ]
https://en.wikipedia.org/wiki/Identity_of_indiscernibles

I doubt so. By the kind of nonsense that you were
proving, I guess this will never happen.

Mostowski Collapse schrieb am Samstag, 5. Februar 2022 um 16:26:00 UTC+1:
> So f ≈ g is not always definite, i.e. has a truth value
> true or false. Sometimes if f and g are incomparable
> and then f ≈ g flounders right? It then has the third
>
> truth value "meaningless". So f ≈ g is not definable,
> how convenient! Because a definition would give it
> a truth value true or false, depending on f,g.
>
> So my initial question what SAME-ness is used in the
> uniqueness here remains for ever unanswered?
>
> Dan Christensen schrieb am Dienstag, 1. Februar 2022 um 21:16:23 UTC+1:
> > & ALL(idx'):[ALL(a):[a in x => idx'(a)=a] <-- Uniqueness
> => ALL(a):[a in x => idx'(a)=idx(a)]]]]
>
> Woa! Because you only prove uniqueness for comparable
> f and g. If f and g are not comparable we dont know whether
> idx is unique. So there can be indeed idx', not comparable
>
> with idx, but nevertheless ALL(a):[a in x => idx'(a)=a].
>
> Right? So idx is in fact not unique, because it can have non-
> comparable idx' which can be substituted for idx. So your
> proof is nonsense, you nowhere proved uniqueness.
>
> LMAO!
> Mostowski Collapse schrieb am Samstag, 5. Februar 2022 um 16:13:30 UTC+1:
> > What do you mean by not comparable?
> > You got a third truth value for SAME-ness:
> >
> > {true,false,meaningless}
> >
> > Did you develop DC poop in the 80's (*) under
> > heavy drug use and are still searching somebody who
> >
> > buys it? Dan-O-Matik during development of DC poop:
> >
> > 80's Acid Clubland Part 1 (Dream Police)
> > https://www.youtube.com/watch?v=r4JzaOkliwg
> > Dan Christensen schrieb am Samstag, 5. Februar 2022 um 02:46:10 UTC+1:
> > > On Friday, February 4, 2022 at 5:21:40 PM UTC-5, Mostowski Collapse (aka Collapsing Jan Burse) wrote:
> > > > Dan-O-Matik halucinated:
> > > > > for all x in X, we have f(x)=g(x)
> > > > You cannot prove:
> > > > f ≈ g => dom(f) = dom(g)
> > > Geez, yer dumb, Jan Burse! If the domains and codomains of a pair of functions are not identical, the functions in question are simply not comparable. Quit making a fool of yourself.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, February 5, 2022 at 10:26:00 AM UTC-5, Mostowski Collapse wrote:
> So f ≈ g is not always definite, i.e. has a truth value
> true or false. Sometimes if f and g are incomparable
> and then f ≈ g flounders right?

Once again...

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
g : X → Y with the same domain and range are said to be equal, f = g,
if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for
some values of x, but not others, then we do not consider f and g to be
equal.)"
--Terance Tao, "Analysis I", p. 51

If you want to concoct some wonky, unconventional alternative definition, I guess you are free to do so. I will stick to this one.

Dan

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

I thought DC Proof is for textbook mathematics. But you
can only repeat verbally like a monke. You cannot bring
it on the computer so that it can be used out of the box:

> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> g : X → Y with the same domain and range are said to be equal, f = g,
> if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for
> some values of x, but not others, then we do not consider f and g to be equal.)"
> --Terance Tao, "Analysis I", p. 51

But you cannot bring your ideas to DC Poop. This is unlike
ZFC which has much more extensive possibilties. Want to define
comparability in ZFC? No problem just define for example:

f ↓ g :<=> dom(f) = dom(g)

Dan Christensen schrieb am Samstag, 5. Februar 2022 um 17:28:11 UTC+1:
> On Saturday, February 5, 2022 at 10:26:00 AM UTC-5, Mostowski Collapse wrote:
> > So f ≈ g is not always definite, i.e. has a truth value
> > true or false. Sometimes if f and g are incomparable
> > and then f ≈ g flounders right?
> Once again...
>
> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> g : X → Y with the same domain and range are said to be equal, f = g,
> if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for
> some values of x, but not others, then we do not consider f and g to be
> equal.)"
> --Terance Tao, "Analysis I", p. 51
>
> If you want to concoct some wonky, unconventional alternative definition, I guess you are free to do so. I will stick to this one.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, February 5, 2022 at 11:52:17 AM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:

> > > Once again...
> >
> > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y ,
> > g : X → Y with the same domain and range are said to be equal, f = g,
> > if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for
> > some values of x, but not others, then we do not consider f and g to be
> > equal.)"
> > --Terance Tao, "Analysis I", p. 51
> >
> > If you want to concoct some wonky, unconventional alternative definition, I guess you are free to do so. I will stick to this one.

> I thought DC Proof is for textbook mathematics. But you
> can only repeat verbally like a monke. You cannot bring
> it on the computer so that it can be used out of the box:

HA, HA!! They must be calling you the Swiss John Gabriel.

Maybe you missed the example I posted here: https://www.dcproof.com/ExistenceUniqueIdentityFunction.htm (see lines 114-123). There, I prove that functions idx and idx', both with the same domain and codomain x, are the same functions as defined by Tao (above).

Deal with it, Jan Burse (aka The Swiss John Gabriel). Just admit you were wrong.

Dan

Ok, here is a high school exercise:

f : R \ {0} -> R, identity function except for x=0 where undefined
g : R \ {1} -> R, identity function except for x=1 where undefined

h(x) = g(f(x))

Prove with DC Poop the domain of h. Can you do it?

With ZFC its pretty trivial.

On Monday, February 7, 2022 at 5:58:14 AM UTC-5, Mostowski Collapse wrote:
> Ok, here is a high school exercise:
>
> f : R \ {0} -> R, identity function except for x=0 where undefined
> g : R \ {1} -> R, identity function except for x=1 where undefined
>
> h(x) = g(f(x))
>
> Prove with DC Poof the domain of h.

Easy It's domain is the set of non-zero reals.

1. 0 in r
Axiom

2. 1 in r
Axiom

3. ~0=1
Axiom

Define: non0

4. ALL(a):[a in non0 <=> a in r & ~a=0]
Axiom

Define: non1

5. ALL(a):[a in non1 <=> a in r & ~a=1]
Axiom

Define: f

6. ALL(a):[a in non0 => f(a)=0]
Axiom

Define: g

7. ALL(a):[a in non1 => g(a)=1]
Axiom

Suppose...

8. x in non0
Premise

9. x in non0 => f(x)=0
U Spec, 6

10. f(x)=0
Detach, 9, 8

11. f(x) in r
Substitute, 10, 1

12. f(x) in non1 <=> f(x) in r & ~f(x)=1
U Spec, 5, 11

13. [f(x) in non1 => f(x) in r & ~f(x)=1]
& [f(x) in r & ~f(x)=1 => f(x) in non1]
Iff-And, 12

14. f(x) in r & ~f(x)=1 => f(x) in non1
Split, 13

15. ~f(x)=1
Substitute, 10, 3

16. f(x) in r & ~f(x)=1
Join, 11, 15

17. f(x) in non1
Detach, 14, 16

18. f(x) in non1 => g(f(x))=1
U Spec, 7, 17

19. g(f(x))=1
Detach, 18, 17

20. ALL(a):[a in non0 => g(f(a))=1]
Conclusion, 8

Dan

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

You see, your result is nonsense:
ALL(a):[a in non0 => g(f(a))=1]

Thats a strange identity function h, to the best of
of my knowledge the composition of two identity functions
is again an identity function.

Now your h is a constant function?

Ther error is here:
> 6. ALL(a):[a in non0 => f(a)=0]
> Axiom
> 7. ALL(a):[a in non1 => g(a)=1]
> Axiom

The spec was:
> f : R \ {0} -> R, identity function except for x=0 where undefined
> g : R \ {1} -> R, identity function except for x=1 where undefined

so you need to have f(a)=a where the function is defined
and similarly g(a)=a where the function is defined.

Dan Christensen schrieb am Montag, 7. Februar 2022 um 14:54:46 UTC+1:
> On Monday, February 7, 2022 at 5:58:14 AM UTC-5, Mostowski Collapse wrote:
> > Ok, here is a high school exercise:
> >
> > f : R \ {0} -> R, identity function except for x=0 where undefined
> > g : R \ {1} -> R, identity function except for x=1 where undefined
> >
> > h(x) = g(f(x))
> >
> > Prove with DC Poof the domain of h.
>
> Easy It's domain is the set of non-zero reals.
>
> 1. 0 in r
> Axiom
>
> 2. 1 in r
> Axiom
>
> 3. ~0=1
> Axiom
>
> Define: non0
>
> 4. ALL(a):[a in non0 <=> a in r & ~a=0]
> Axiom
>
> Define: non1
>
> 5. ALL(a):[a in non1 <=> a in r & ~a=1]
> Axiom
>
> Define: f
>
> 6. ALL(a):[a in non0 => f(a)=0]
> Axiom
>
> Define: g
>
> 7. ALL(a):[a in non1 => g(a)=1]
> Axiom
>
> Suppose...
>
> 8. x in non0
> Premise
>
> 9. x in non0 => f(x)=0
> U Spec, 6
>
> 10. f(x)=0
> Detach, 9, 8
>
> 11. f(x) in r
> Substitute, 10, 1
>
> 12. f(x) in non1 <=> f(x) in r & ~f(x)=1
> U Spec, 5, 11
>
> 13. [f(x) in non1 => f(x) in r & ~f(x)=1]
> & [f(x) in r & ~f(x)=1 => f(x) in non1]
> Iff-And, 12
>
> 14. f(x) in r & ~f(x)=1 => f(x) in non1
> Split, 13
>
> 15. ~f(x)=1
> Substitute, 10, 3
>
> 16. f(x) in r & ~f(x)=1
> Join, 11, 15
>
> 17. f(x) in non1
> Detach, 14, 16
>
> 18. f(x) in non1 => g(f(x))=1
> U Spec, 7, 17
>
> 19. g(f(x))=1
> Detach, 18, 17
>
> 20. ALL(a):[a in non0 => g(f(a))=1]
> Conclusion, 8
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

This theorem is not provable in DC poop:

dom(g o h) = h^(-1)[dom(g)]

Because DC poop refuses to define dom(_).
So its not provable because it is not expressible.
Possibly DC poop will also refuse to define h^(-1)[_].

On the other hand this kind of Highschool math only...

Mostowski Collapse schrieb am Montag, 7. Februar 2022 um 21:47:00 UTC+1:
> You see, your result is nonsense:
> ALL(a):[a in non0 => g(f(a))=1]
> Thats a strange identity function h, to the best of
> of my knowledge the composition of two identity functions
> is again an identity function.
>
> Now your h is a constant function?
>
> Ther error is here:
> > 6. ALL(a):[a in non0 => f(a)=0]
> > Axiom
> > 7. ALL(a):[a in non1 => g(a)=1]
> > Axiom
> The spec was:
> > f : R \ {0} -> R, identity function except for x=0 where undefined
> > g : R \ {1} -> R, identity function except for x=1 where undefined
> so you need to have f(a)=a where the function is defined
> and similarly g(a)=a where the function is defined.
> Dan Christensen schrieb am Montag, 7. Februar 2022 um 14:54:46 UTC+1:
> > On Monday, February 7, 2022 at 5:58:14 AM UTC-5, Mostowski Collapse wrote:
> > > Ok, here is a high school exercise:
> > >
> > > f : R \ {0} -> R, identity function except for x=0 where undefined
> > > g : R \ {1} -> R, identity function except for x=1 where undefined
> > >
> > > h(x) = g(f(x))
> > >
> > > Prove with DC Poof the domain of h.

(Correction)

On Monday, February 7, 2022 at 5:58:14 AM UTC-5, Mostowski Collapse wrote:
> Ok, here is a high school exercise:
>
> f : R \ {0} -> R, identity function except for x=0 where undefined
> g : R \ {1} -> R, identity function except for x=1 where undefined
>
> h(x) = g(f(x))
>

> Prove with DC Proff the domain of h.

The domain is R \ {0, 1}

Proof:

1. 0 in r
Axiom

2. 1 in r
Axiom

3. ~0=1
Axiom

Define: non0

4. ALL(a):[a in non0 <=> a in r & ~a=0]
Axiom

Define: non1

5. ALL(a):[a in non1 <=> a in r & ~a=1]
Axiom

Define: non01

6. ALL(a):[a in non01 <=> a in r & ~a=0 & ~a=1]
Axiom

Define: f

7. ALL(a):[a in non0 => f(a)=a]
Axiom

Define: g

8. ALL(a):[a in non1 => g(a)=a]
Axiom

Suppose...

9. x in non01
Premise

10. x in non01 <=> x in r & ~x=0 & ~x=1
U Spec, 6

11. [x in non01 => x in r & ~x=0 & ~x=1] & [x in r & ~x=0 & ~x=1 => x in non01]
Iff-And, 10

12. x in non01 => x in r & ~x=0 & ~x=1
Split, 11

13. x in r & ~x=0 & ~x=1
Detach, 12, 9

14. x in r
Split, 13

15. ~x=0
Split, 13

16. ~x=1
Split, 13

17. x in non0 => f(x)=x
U Spec, 7

18. x in non0 <=> x in r & ~x=0
U Spec, 4

19. [x in non0 => x in r & ~x=0] & [x in r & ~x=0 => x in non0]
Iff-And, 18

20. x in r & ~x=0 => x in non0
Split, 19

21. x in r & ~x=0
Join, 14, 15

22. x in non0
Detach, 20, 21

23. f(x)=x
Detach, 17, 22

24. x in non1 => g(x)=x
U Spec, 8

25. x in non1 <=> x in r & ~x=1
U Spec, 5

26. [x in non1 => x in r & ~x=1] & [x in r & ~x=1 => x in non1]
Iff-And, 25

27. x in r & ~x=1 => x in non1
Split, 26

28. x in r & ~x=1
Join, 14, 16

29. x in non1
Detach, 27, 28

30. g(x)=x
Detach, 24, 29

31. g(f(x))=x
Substitute, 23, 30

As Required:

32. ALL(a):[a in non01 => g(f(a))=a]
Conclusion, 9

Dan

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

One more nonsense:
> 32. ALL(a):[a in non01 => g(f(a))=a]
Conclusion, 9

Try this here:

6. ALL(a):[a in non012 <=> a in r & ~a=0 & ~a=1 & ~a=2]
Axiom

You can also prove:
ALL(a):[a in non012 => g(f(a))=a]

So what tells you that non01 is THE domain? You just made
an educated guess, plugged it into your Dan-O-Matik nonsense,

but DC poop didn't infer dom(_). You would need to prove:

finds the **largest domain** of definition of the real function f of the variable x.
https://reference.wolfram.com/language/ref/FunctionDomain.html

Dan Christensen schrieb am Dienstag, 8. Februar 2022 um 01:21:41 UTC+1:
> (Correction)
> On Monday, February 7, 2022 at 5:58:14 AM UTC-5, Mostowski Collapse wrote:
> > Ok, here is a high school exercise:
> >
> > f : R \ {0} -> R, identity function except for x=0 where undefined
> > g : R \ {1} -> R, identity function except for x=1 where undefined
> >
> > h(x) = g(f(x))
> >
> > Prove with DC Proff the domain of h.

See my reply just now to your similar posting at sci.math

Dan

On Tuesday, February 8, 2022 at 6:39:21 AM UTC-5, Mostowski Collapse wrote:
> One more nonsense:
> > 32. ALL(a):[a in non01 => g(f(a))=a]
> Conclusion, 9
> Try this here:
>
> 6. ALL(a):[a in non012 <=> a in r & ~a=0 & ~a=1 & ~a=2]
> Axiom
>
> You can also prove:
> ALL(a):[a in non012 => g(f(a))=a]
>
> So what tells you that non01 is THE domain? You just made
> an educated guess, plugged it into your Dan-O-Matik nonsense,
>
> but DC poop didn't infer dom(_). You would need to prove:
>
> finds the **largest domain** of definition of the real function f of the variable x.
> https://reference.wolfram.com/language/ref/FunctionDomain.html
> Dan Christensen schrieb am Dienstag, 8. Februar 2022 um 01:21:41 UTC+1:
> > (Correction)
> > On Monday, February 7, 2022 at 5:58:14 AM UTC-5, Mostowski Collapse wrote:
> > > Ok, here is a high school exercise:
> > >
> > > f : R \ {0} -> R, identity function except for x=0 where undefined
> > > g : R \ {1} -> R, identity function except for x=1 where undefined
> > >
> > > h(x) = g(f(x))
> > >
> > > Prove with DC Proff the domain of h.

WHATS WRONG WITH YOU?????

Where do you see the domain of f' given
for example for the problem f : R -> R, f(x) = |x|.

The domain of f' has to be infered from the
domain and codomain of f. But the domain and
codomain of f' are not given. It can be {}

for a function that is nowhere differentiable, and
it can be R for a function that is everywhere
differentiable.

Dan Christensen schrieb am Dienstag, 8. Februar 2022 um 17:38:58 UTC+1:
> See my reply just now to your similar posting at sci.math

On Wednesday, February 9, 2022 at 1:50:13 PM UTC-5, Mostowski Collapse (aka Jan Burse) wrote:
> WHATS WRONG WITH YOU, JAN BURSE?????
>
> Where do you see the domain of f' given
> for example for the problem f : R -> R, f(x) = |x|.
>

In a formal proof anyway, you first need to construct, i.e. prove the existence of the subset D of R where f is differentiable. In this case D = R \ {0}. Only then can you construct a function f' on D such that f'(x) = -1 for x<0, and +1 for x>0.

Remember: First comes domains and codomains, THEN comes functions. I hope this helps.

Dan

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