On Wednesday, April 20, 2022 at 10:48:36 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Ben schrieb am Sonntag, 17. April 2022 um 23:00:09 UTC+2:
> > (Reminder, in case you do have time, f' and g' are both from {0,1} and
> > to {0,1} with f'(0) = g'(0) = 0 and f'(1) = 1 but g'(1) = 0. I posted a
> > proof that they were equal but you've suggested that I needed to say
> > more about them, but none of the lines you posted would have made the
> > proof impossible.)
> Dan Christensen schrieb am Mittwoch, 20. April 2022 um 16:29:29 UTC+2:
> > On Wednesday, April 20, 2022 at 1:39:02 AM UTC-4, Fritz Feldhase wrote:
> > > On Wednesday, April 20, 2022 at 6:39:35 AM UTC+2, Dan Christensen wrote:
> > > > >
> > > > > 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > > > > Conclusion, 15
> > > > >
> > > > Revisiting your proof here, the last line looks bizarre, but only because you left out some key information about functions f and g. It can be fixed up as follows:
> > > >
> > > > :
> > > >
> > > > 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
> > > > => ALL(a):[a in s => f(a) in s]
> > > > & ALL(a):[a in s => g(a) in s]
> > > > & f=g]
> > > > Conclusion, 15
> > > >
> > > > Given that s={0} (line 3), this nails down functions f and g.
> > > Huh?! This doesn't "nail down" these functions.
> > >
> > s is a singleton. There is only one function mapping s to itself. So the above result makes perfect sense.
> >

> Your ad hoc axiom is useless, because you can
> prove f=g and ~f=g.

I would be very interested to see such a proof. Not today, Jan Burse? Oh, well...

Dan

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

Ben did it. Do you Alzheimer?

Dan Christensen schrieb am Mittwoch, 20. April 2022 um 18:30:45 UTC+2:
> On Wednesday, April 20, 2022 at 10:48:36 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
>
> > Ben schrieb am Sonntag, 17. April 2022 um 23:00:09 UTC+2:
> > > (Reminder, in case you do have time, f' and g' are both from {0,1} and
> > > to {0,1} with f'(0) = g'(0) = 0 and f'(1) = 1 but g'(1) = 0. I posted a
> > > proof that they were equal but you've suggested that I needed to say
> > > more about them, but none of the lines you posted would have made the
> > > proof impossible.)
> > Dan Christensen schrieb am Mittwoch, 20. April 2022 um 16:29:29 UTC+2:
> > > On Wednesday, April 20, 2022 at 1:39:02 AM UTC-4, Fritz Feldhase wrote:
> > > > On Wednesday, April 20, 2022 at 6:39:35 AM UTC+2, Dan Christensen wrote:
> > > > > >
> > > > > > 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > > > > > Conclusion, 15
> > > > > >
> > > > > Revisiting your proof here, the last line looks bizarre, but only because you left out some key information about functions f and g. It can be fixed up as follows:
> > > > >
> > > > > :
> > > > >
> > > > > 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
> > > > > => ALL(a):[a in s => f(a) in s]
> > > > > & ALL(a):[a in s => g(a) in s]
> > > > > & f=g]
> > > > > Conclusion, 15
> > > > >
> > > > > Given that s={0} (line 3), this nails down functions f and g.
> > > > Huh?! This doesn't "nail down" these functions.
> > > >
> > > s is a singleton. There is only one function mapping s to itself. So the above result makes perfect sense.
> > >
>
> > Your ad hoc axiom is useless, because you can
> > prove f=g and ~f=g.
>
> I would be very interested to see such a proof. Not today, Jan Burse? Oh, well...
>
> 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 wrote:

> Your ad hoc axiom is useless, because you can prove f=g and ~f=g. Never
> head of Ex Falso Quodlibet?

one more proof, you fake money makers are fucked up, how we say in
physics.

Pentagon responds to Russian missile test
The Sarmat ICBM test was not a threat, Moscow gave US advance notice, the
Pentagon spokesman told reporters
https://www.rt.com/russia/554241-pentagon-reacts-to-sarmat/
“Russia properly notified the US under its New Start treaty obligations
that it planned to test this ICBM,” Pentagon spokesman John Kirby told
reporters on Wednesday afternoon, adding that the test was routine, and
the US Defense Department deemed it “not a threat.”

Dan Christensen just like the ruSSians. Getting beaten
their asses again and again, first in the north and now
in the south of Ukraine. They will have heavy losses

in the south swamps of Ukraine. There is no winning
some war until 9 may for the ruSSians. Only rattling
with nukes, that are even not yet part of their arsenal.

Boyd Papadopulos schrieb am Mittwoch, 20. April 2022 um 19:58:39 UTC+2:
> Mostowski Collapse wrote:
>
> > Your ad hoc axiom is useless, because you can prove f=g and ~f=g. Never
> > head of Ex Falso Quodlibet?
> one more proof, you fake money makers are fucked up, how we say in
> physics.
>
> Pentagon responds to Russian missile test
> The Sarmat ICBM test was not a threat, Moscow gave US advance notice, the
> Pentagon spokesman told reporters
> https://www.rt.com/russia/554241-pentagon-reacts-to-sarmat/
> “Russia properly notified the US under its New Start treaty obligations
> that it planned to test this ICBM,” Pentagon spokesman John Kirby told
> reporters on Wednesday afternoon, adding that the test was routine, and
> the US Defense Department deemed it “not a threat.”

On Wednesday, April 20, 2022 at 1:57:34 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:

> Dan Christensen schrieb am Mittwoch, 20. April 2022 um 18:30:45 UTC+2:
> > On Wednesday, April 20, 2022 at 10:48:36 AM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> >
> > > Ben schrieb am Sonntag, 17. April 2022 um 23:00:09 UTC+2:
> > > > (Reminder, in case you do have time, f' and g' are both from {0,1} and
> > > > to {0,1} with f'(0) = g'(0) = 0 and f'(1) = 1 but g'(1) = 0. I posted a
> > > > proof that they were equal but you've suggested that I needed to say
> > > > more about them, but none of the lines you posted would have made the
> > > > proof impossible.)
> > > Dan Christensen schrieb am Mittwoch, 20. April 2022 um 16:29:29 UTC+2:
> > > > On Wednesday, April 20, 2022 at 1:39:02 AM UTC-4, Fritz Feldhase wrote:
> > > > > On Wednesday, April 20, 2022 at 6:39:35 AM UTC+2, Dan Christensen wrote:
> > > > > > >
> > > > > > > 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> > > > > > > Conclusion, 15
> > > > > > >
> > > > > > Revisiting your proof here, the last line looks bizarre, but only because you left out some key information about functions f and g. It can be fixed up as follows:
> > > > > >
> > > > > > :
> > > > > >
> > > > > > 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
> > > > > > => ALL(a):[a in s => f(a) in s]
> > > > > > & ALL(a):[a in s => g(a) in s]
> > > > > > & f=g]
> > > > > > Conclusion, 15
> > > > > >
> > > > > > Given that s={0} (line 3), this nails down functions f and g.
> > > > > Huh?! This doesn't "nail down" these functions.
> > > > >
> > > > s is a singleton. There is only one function mapping s to itself. So the above result makes perfect sense.
> > > >
> >
> > > Your ad hoc axiom is useless, because you can
> > > prove f=g and ~f=g.
> >
> > I would be very interested to see such a proof. Not today, Jan Burse? Oh, well...
> >

> Ben did it.

Wrong again, Jan Burse. So, you have no such proof yourself.

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 <Dan_Christensen@sympatico.ca> writes:

> On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:
>
>> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
>> & EXIST(a):a ε dom & EXIST(a):a ε cod
>> & ALL(a):[a ε dom => f1(a) ε cod]
>> & ALL(a):[a ε dom => f2(a) ε cod]
>> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
>> Axiom
>>
>> 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
>> Axiom
>>
>> 3 Set(s) & ALL(a):[a ε s <=> a=0]
>> E Spec, 2
>>
>> 4 Set(s)
>> Split, 3
>>
>> 5 ALL(a):[a ε s <=> a=0]
>> Split, 3
>>
>> 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
>> & EXIST(a):a ε s & EXIST(a):a ε cod
>> & ALL(a):[a ε s => f1(a) ε cod]
>> & ALL(a):[a ε s => f2(a) ε cod]
>> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
>> U Spec, 1
>>
>> 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
>> & EXIST(a):a ε s & EXIST(a):a ε s
>> & ALL(a):[a ε s => f1(a) ε s]
>> & ALL(a):[a ε s => f2(a) ε s]
>> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
>> U Spec, 6
>>
>> 8 0 ε s <=> 0=0
>> U Spec, 5
>>
>> 9 [0 ε s => 0=0] & [0=0 => 0 ε s]
>> Iff-And, 8
>>
>> 10 0 ε s => 0=0
>> Split, 9
>>
>> 11 0=0 => 0 ε s
>> Split, 9
>>
>> 12 0=0
>> Reflex
>>
>> 13 0 ε s
>> Detach, 11, 12
>>
>> 14 EXIST(a):a ε s
>> E Gen, 13
>>
>> 15 f(0)=0 & g(0)=0
>> Premise
>>
>> 16 z ε s
>> Premise
>>
>> 17 z ε s <=> z=0
>> U Spec, 5
>>
>> 18 [z ε s => z=0] & [z=0 => z ε s]
>> Iff-And, 17
>>
>> 19 z ε s => z=0
>> Split, 18
>>
>> 20 z=0 => z ε s
>> Split, 18
>>
>> 21 z=0
>> Detach, 19, 16
>>
>> 22 0 ε s
>> Substitute, 21, 16
>>
>> 23 f(0)=0
>> Split, 15
>>
>> 24 g(0)=0
>> Split, 15
>>
>> 25 f(0) ε s
>> Substitute, 23, 22
>>
>> 26 f(z) ε s
>> Substitute, 21, 25
>>
>> 27 ALL(a):[a ε s => f(a) ε s]
>> Conclusion, 16
>>
>> 28 z ε s
>> Premise
>>
>> 29 z ε s <=> z=0
>> U Spec, 5
>>
>> 30 [z ε s => z=0] & [z=0 => z ε s]
>> Iff-And, 29
>>
>> 31 z ε s => z=0
>> Split, 30
>>
>> 32 z=0 => z ε s
>> Split, 30
>>
>> 33 z=0
>> Detach, 31, 28
>>
>> 34 0 ε s
>> Substitute, 33, 28
>>
>> 35 f(0)=0
>> Split, 15
>>
>> 36 g(0)=0
>> Split, 15
>>
>> 37 g(0) ε s
>> Substitute, 36, 34
>>
>> 38 g(z) ε s
>> Substitute, 33, 37
>>
>> 39 ALL(a):[a ε s => g(a) ε s]
>> Conclusion, 28
>>
>> 40 ALL(f2):[Set(s) & Set(s)
>> & EXIST(a):a ε s & EXIST(a):a ε s
>> & ALL(a):[a ε s => f(a) ε s]
>> & ALL(a):[a ε s => f2(a) ε s]
>> => [f=f2 <=> ALL(a):[a ε s => f(a)=f2(a)]]]
>> U Spec, 7
>>
>> 41 Set(s) & Set(s)
>> & EXIST(a):a ε s & EXIST(a):a ε s
>> & ALL(a):[a ε s => f(a) ε s]
>> & ALL(a):[a ε s => g(a) ε s]
>> => [f=g <=> ALL(a):[a ε s => f(a)=g(a)]]
>> U Spec, 40
>>
>> 42 Set(s) & Set(s)
>> Join, 4, 4
>>
>> 43 Set(s) & Set(s) & EXIST(a):a ε s
>> Join, 42, 14
>>
>> 44 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
>> Join, 43, 14
>>
>> 45 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
>> & ALL(a):[a ε s => f(a) ε s]
>> Join, 44, 27
>>
>> 46 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
>> & ALL(a):[a ε s => f(a) ε s]
>> & ALL(a):[a ε s => g(a) ε s]
>> Join, 45, 39
>>
>> 47 f=g <=> ALL(a):[a ε s => f(a)=g(a)]
>> Detach, 41, 46
>>
>> 48 [f=g => ALL(a):[a ε s => f(a)=g(a)]]
>> & [ALL(a):[a ε s => f(a)=g(a)] => f=g]
>> Iff-And, 47
>>
>> 49 f=g => ALL(a):[a ε s => f(a)=g(a)]
>> Split, 48
>>
>> 50 ALL(a):[a ε s => f(a)=g(a)] => f=g
>> Split, 48
>>
>> 51 z ε s
>> Premise
>>
>> 52 z ε s <=> z=0
>> U Spec, 5
>>
>> 53 [z ε s => z=0] & [z=0 => z ε s]
>> Iff-And, 52
>>
>> 54 z ε s => z=0
>> Split, 53
>>
>> 55 z=0 => z ε s
>> Split, 53
>>
>> 56 z=0
>> Detach, 54, 51
>>
>> 57 f(0)=0
>> Split, 15
>>
>> 58 g(0)=0
>> Split, 15
>>
>> 59 z=g(0)
>> Substitute, 58, 56
>>
>> 60 0=g(0)
>> Substitute, 56, 59
>>
>> 61 f(0)=g(0)
>> Substitute, 57, 60
>>
>> 62 f(z)=g(z)
>> Substitute, 56, 61
>>
>> 63 ALL(a):[a ε s => f(a)=g(a)]
>> Conclusion, 51
>>
>> 64 f=g
>> Detach, 50, 63
>>
>> 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>> Conclusion, 15
>
> Revisiting your proof here, the last line looks bizarre, but only
> because you left out some key information about functions f and g. It
> can be fixed up as follows:
>
> 65. ALL(a):[a in s => f(a) in s]
> & ALL(a):[a in s => g(a) in s]
> Join, 27, 39
>
> 66. ALL(a):[a in s => f(a) in s]
> & ALL(a):[a in s => g(a) in s]
> & f=g
> Join, 65, 64
>
> 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
> => ALL(a):[a in s => f(a) in s]
> & ALL(a):[a in s => g(a) in s]
> & f=g]
> Conclusion, 15

Pointless. It does not stop someone writing the proof that you think
needs to be "fixed up". To stop that you would need a valid axiom about
function equality.

Of course you can choose to prove other things but I thought you said
you did not intend for your axiom to entail

ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

Have you changed your mind and you are now OK with it?

(I won't go into the details of what you've chosen to prove, but I'll
comment on it if you want me to.)

> Given that s={0} (line 3), this nails down functions f and g.

The theorem is about all functions:

ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g].

How does naming the set {0} nail down all functions? It's your axiom
that does that. Yes, there has to be a set with only 0 in it, but that
is not the reason DC Proof can prove ALL(f):ALL(g):[f(0)=0 & g(0)=0 =>
f=g]. That's down to your axiom.

> What is there to be concerned about here?

The fact that ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g] is nonsense and it
follows rigorously from your axiom (and, as you point out, the innocent
existence of the set {0}).

> Perhaps I over-reacted in disabling the Function Equality Axiom.

It depends. If you are happy someone could come along and prove
something like this

ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

about all pairs of functions with nothing but your axiom and the
existence of the set {0}, then yes, keep the axiom!

--
Ben.

Finally my counter example straight line and absolute value
has been proved. How many weeks ago did I propose
this example as a counter example to the ad hoc axiom,

these two real valued functions:

f(x) = x

g(x) = abs(x)

They satisfy f(0)=0 and g(0)=0, don't they. So we have f=g?
So after 13 days, The Equality of Functions: Big Controversy
is still unresolved, only the mistery and fog increased?

Woa!

Ben schrieb am Donnerstag, 21. April 2022 um 00:33:54 UTC+2:
> It depends. If you are happy someone could come along and prove
> something like this
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> about all pairs of functions with nothing but your axiom and the
> existence of the set {0}, then yes, keep the axiom!

On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:
> >
> >> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> >> & EXIST(a):a ε dom & EXIST(a):a ε cod
> >> & ALL(a):[a ε dom => f1(a) ε cod]
> >> & ALL(a):[a ε dom => f2(a) ε cod]
> >> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> >> Axiom
> >>
> >> 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
> >> Axiom
> >>
> >> 3 Set(s) & ALL(a):[a ε s <=> a=0]
> >> E Spec, 2
> >>
> >> 4 Set(s)
> >> Split, 3
> >>
> >> 5 ALL(a):[a ε s <=> a=0]
> >> Split, 3
> >>
> >> 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
> >> & EXIST(a):a ε s & EXIST(a):a ε cod
> >> & ALL(a):[a ε s => f1(a) ε cod]
> >> & ALL(a):[a ε s => f2(a) ε cod]
> >> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> >> U Spec, 1
> >>
> >> 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
> >> & EXIST(a):a ε s & EXIST(a):a ε s
> >> & ALL(a):[a ε s => f1(a) ε s]
> >> & ALL(a):[a ε s => f2(a) ε s]
> >> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
> >> U Spec, 6
> >>
> >> 8 0 ε s <=> 0=0
> >> U Spec, 5
> >>
> >> 9 [0 ε s => 0=0] & [0=0 => 0 ε s]
> >> Iff-And, 8
> >>
> >> 10 0 ε s => 0=0
> >> Split, 9
> >>
> >> 11 0=0 => 0 ε s
> >> Split, 9
> >>
> >> 12 0=0
> >> Reflex
> >>
> >> 13 0 ε s
> >> Detach, 11, 12
> >>
> >> 14 EXIST(a):a ε s
> >> E Gen, 13
> >>
> >> 15 f(0)=0 & g(0)=0
> >> Premise
> >>
> >> 16 z ε s
> >> Premise
> >>
> >> 17 z ε s <=> z=0
> >> U Spec, 5
> >>
> >> 18 [z ε s => z=0] & [z=0 => z ε s]
> >> Iff-And, 17
> >>
> >> 19 z ε s => z=0
> >> Split, 18
> >>
> >> 20 z=0 => z ε s
> >> Split, 18
> >>
> >> 21 z=0
> >> Detach, 19, 16
> >>
> >> 22 0 ε s
> >> Substitute, 21, 16
> >>
> >> 23 f(0)=0
> >> Split, 15
> >>
> >> 24 g(0)=0
> >> Split, 15
> >>
> >> 25 f(0) ε s
> >> Substitute, 23, 22
> >>
> >> 26 f(z) ε s
> >> Substitute, 21, 25
> >>
> >> 27 ALL(a):[a ε s => f(a) ε s]
> >> Conclusion, 16
> >>
> >> 28 z ε s
> >> Premise
> >>
> >> 29 z ε s <=> z=0
> >> U Spec, 5
> >>
> >> 30 [z ε s => z=0] & [z=0 => z ε s]
> >> Iff-And, 29
> >>
> >> 31 z ε s => z=0
> >> Split, 30
> >>
> >> 32 z=0 => z ε s
> >> Split, 30
> >>
> >> 33 z=0
> >> Detach, 31, 28
> >>
> >> 34 0 ε s
> >> Substitute, 33, 28
> >>
> >> 35 f(0)=0
> >> Split, 15
> >>
> >> 36 g(0)=0
> >> Split, 15
> >>
> >> 37 g(0) ε s
> >> Substitute, 36, 34
> >>
> >> 38 g(z) ε s
> >> Substitute, 33, 37
> >>
> >> 39 ALL(a):[a ε s => g(a) ε s]
> >> Conclusion, 28
> >>
> >> 40 ALL(f2):[Set(s) & Set(s)
> >> & EXIST(a):a ε s & EXIST(a):a ε s
> >> & ALL(a):[a ε s => f(a) ε s]
> >> & ALL(a):[a ε s => f2(a) ε s]
> >> => [f=f2 <=> ALL(a):[a ε s => f(a)=f2(a)]]]
> >> U Spec, 7
> >>
> >> 41 Set(s) & Set(s)
> >> & EXIST(a):a ε s & EXIST(a):a ε s
> >> & ALL(a):[a ε s => f(a) ε s]
> >> & ALL(a):[a ε s => g(a) ε s]
> >> => [f=g <=> ALL(a):[a ε s => f(a)=g(a)]]
> >> U Spec, 40
> >>
> >> 42 Set(s) & Set(s)
> >> Join, 4, 4
> >>
> >> 43 Set(s) & Set(s) & EXIST(a):a ε s
> >> Join, 42, 14
> >>
> >> 44 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> >> Join, 43, 14
> >>
> >> 45 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> >> & ALL(a):[a ε s => f(a) ε s]
> >> Join, 44, 27
> >>
> >> 46 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
> >> & ALL(a):[a ε s => f(a) ε s]
> >> & ALL(a):[a ε s => g(a) ε s]
> >> Join, 45, 39
> >>
> >> 47 f=g <=> ALL(a):[a ε s => f(a)=g(a)]
> >> Detach, 41, 46
> >>
> >> 48 [f=g => ALL(a):[a ε s => f(a)=g(a)]]
> >> & [ALL(a):[a ε s => f(a)=g(a)] => f=g]
> >> Iff-And, 47
> >>
> >> 49 f=g => ALL(a):[a ε s => f(a)=g(a)]
> >> Split, 48
> >>
> >> 50 ALL(a):[a ε s => f(a)=g(a)] => f=g
> >> Split, 48
> >>
> >> 51 z ε s
> >> Premise
> >>
> >> 52 z ε s <=> z=0
> >> U Spec, 5
> >>
> >> 53 [z ε s => z=0] & [z=0 => z ε s]
> >> Iff-And, 52
> >>
> >> 54 z ε s => z=0
> >> Split, 53
> >>
> >> 55 z=0 => z ε s
> >> Split, 53
> >>
> >> 56 z=0
> >> Detach, 54, 51
> >>
> >> 57 f(0)=0
> >> Split, 15
> >>
> >> 58 g(0)=0
> >> Split, 15
> >>
> >> 59 z=g(0)
> >> Substitute, 58, 56
> >>
> >> 60 0=g(0)
> >> Substitute, 56, 59
> >>
> >> 61 f(0)=g(0)
> >> Substitute, 57, 60
> >>
> >> 62 f(z)=g(z)
> >> Substitute, 56, 61
> >>
> >> 63 ALL(a):[a ε s => f(a)=g(a)]
> >> Conclusion, 51
> >>
> >> 64 f=g
> >> Detach, 50, 63
> >>
> >> 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> >> Conclusion, 15
> >
> > Revisiting your proof here, the last line looks bizarre, but only
> > because you left out some key information about functions f and g. It
> > can be fixed up as follows:
> >
> > 65. ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > Join, 27, 39
> >
> > 66. ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g
> > Join, 65, 64
> >
> > 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
> > => ALL(a):[a in s => f(a) in s]
> > & ALL(a):[a in s => g(a) in s]
> > & f=g]
> > Conclusion, 15

> Pointless. It does not stop someone writing the proof that you think
> needs to be "fixed up".

There was nothing technically wrong with your proof. The new ending just makes it a little less perplexing.

> Of course you can choose to prove other things but I thought you said
> you did not intend for your axiom to entail
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

This, given the singleton {0}. That makes all the difference. Only one function f: {0} --> {0} is possible.

> Have you changed your mind and you are now OK with it?
>

Yes. It is greatly improved IMHO.

> (I won't go into the details of what you've chosen to prove, but I'll
> comment on it if you want me to.)
> > Given that s={0} (line 3), this nails down functions f and g.
> The theorem is about all functions:
>

Not really.

> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g].
>

With your singleton {0} as the domain and codomain, only one function is possible.

On Wednesday, April 20, 2022 at 7:03:07 PM UTC-4, Mostowski Collapse wrote:
> Finally my counter example straight line and absolute value
> has been proved. How many weeks ago did I propose
> this example as a counter example to the ad hoc axiom,
>
> these two real valued functions:
>
> f(x) = x
>
> g(x) = abs(x)
>
> They satisfy f(0)=0 and g(0)=0, don't they. So we have f=g?

You specified a domain of the non-negative reals. So, of course, they are the same functions there.

Dan

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

On Thursday, April 21, 2022 at 1:47:18 AM UTC+2, Dan Christensen wrote:
> On Wednesday, April 20, 2022 at 7:03:07 PM UTC-4, Mostowski Collapse wrote:
> > Finally my counter example straight line and absolute value
> > has been proved. How many weeks ago did I propose
> > this example as a counter example to the ad hoc axiom,
> >
> > these two real valued functions:
> >
> > f(x) = x
> >
> > g(x) = abs(x)
> >
> > They satisfy f(0)=0 and g(0)=0, don't they. So we have f=g?
> >
> You specified a domain of the non-negative reals. So, of course, they are the same functions there.

Look, you silly asshole we may define

f: IR --> IR with f(x) = x for all x e IR

and

g: IR --> IR with g(x) = abs(x) for all X e IR

as well

Now, these these functions satisfy f(0)=0 and g(0)=0.

Hence f = g ?

YOU FUCKING ASSHOLE FULL OF SHIT

On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
> On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> >
> With your singleton {0} as the domain and codomain,

Why are you lying all the time, you silly crank?

The common domain of f and g definded by Ben is {0, 1}.

No idea how to "specify" the domain of a function in DC Spoof though.

It seems to me that it can't be done. So all you can do in the context of DC Spoof is guessing.

DC Spoof. A guessing tool.

On Wednesday, April 20, 2022 at 8:17:00 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, April 21, 2022 at 1:47:18 AM UTC+2, Dan Christensen wrote:
> > On Wednesday, April 20, 2022 at 7:03:07 PM UTC-4, Mostowski Collapse wrote:
> > > Finally my counter example straight line and absolute value
> > > has been proved. How many weeks ago did I propose
> > > this example as a counter example to the ad hoc axiom,
> > >
> > > these two real valued functions:
> > >
> > > f(x) = x
> > >
> > > g(x) = abs(x)
> > >
> > > They satisfy f(0)=0 and g(0)=0, don't they. So we have f=g?
> > >
> > You specified a domain of the non-negative reals. So, of course, they are the same functions there.
> Look, we may define
>
> f: IR --> IR with f(x) = x for all x e IR
>
> and
>
> g: IR --> IR with g(x) = abs(x) for all X e IR
>
> as well
>
> Now, these these functions satisfy f(0)=0 and g(0)=0.
>
> Hence f = g ?
>

They both give the same values on the non-negative reals. Therefore, in that domain, f(x)=g(x). Therefore IN THAT DOMAIN, we can say that f=g.

Dan

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

On Wednesday, April 20, 2022 at 8:25:44 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
> > On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> > >
> > With your singleton {0} as the domain and codomain,
>
> The common domain of f and g definded by Ben is {0, 1}.

Nope. See his lines 2-3.

2. EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
Axiom

3. Set(s) & ALL(a):[a ε s <=> a=0]
E Spec, 2

The domain s = {0}.
Dan

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

On Thursday, April 21, 2022 at 2:36:16 AM UTC+2, Dan Christensen wrote:
> On Wednesday, April 20, 2022 at 8:25:44 PM UTC-4, Fritz Feldhase wrote:
> > On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
> > > On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> > > >
> > > With your singleton {0} as the domain and codomain,
> >
> > The common domain of f and g definded by Ben is {0, 1}.
> >
> Nope.

Yes. At least this was the intended domain.

Anyway. Bens proof shows that any two functions f, g which *just* agree for ONE value, say 0, can be proved to be equal.

In other words, in your DC Proof the following holds:

Ex(f(x) = g(x) -> f = g).

Or at least

f(c) = g(c) -> f = g,

for any constant c.

Seems that just like WM, JG and AP you can't understand mathematical arguments.

Hint: "I can prove too many things equal [in your DC Proof]. The problem is how to define my two function so they /can't/ be proved equal." (Ben)

On Wednesday, April 20, 2022 at 8:56:35 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, April 21, 2022 at 2:36:16 AM UTC+2, Dan Christensen wrote:
> > On Wednesday, April 20, 2022 at 8:25:44 PM UTC-4, Fritz Feldhase wrote:
> > > On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
> > > > On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> > > > >
> > > > With your singleton {0} as the domain and codomain,
> > >
> > > The common domain of f and g definded by Ben is {0, 1}.
> > >
> > Nope.
> Yes. At least this was the intended domain.
>
> Anyway. Bens proof shows that any two functions f, g which *just* agree for ONE value, say 0, can be proved to be equal.
>

That would suffice if there is only a single element in the domain, as is the case here.

> In other words, in your DC Proof the following holds:
>
> Ex(f(x) = g(x) -> f = g).
>

You are getting desperate, Fritz. Not a good look for you.

Dan

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

On Thursday, April 21, 2022 at 2:36:16 AM UTC+2, Dan Christensen wrote:
> On Wednesday, April 20, 2022 at 8:25:44 PM UTC-4, Fritz Feldhase wrote:
> > On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
> > > On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> > >
> > > With your singleton {0} as the domain and codomain,
> > >
> > The common domain of f and g definded by Ben is {0, 1}.
> >
> Nope.

Yes. At least this was the intended domain. (Though it seems there's no way to specify this in DC Spoof.)

Anyway. Bens proof shows that any two functions f, g which *just* agree for ONE value, say 0, can be proved to be equal.

In other words, in your DC Proof the following holds:

Ex(f(x) = g(x)) -> f = g.

Or at least

f(c) = g(c) -> f = g,

for any constant c.

Seems that you -just like WM, JG and AP- can't understand mathematical arguments.

Hint: "I can prove too many things equal [in your DC Proof]. The problem is how to define my two function so they /can't/ be proved equal." (Ben)

On Thursday, April 21, 2022 at 3:03:38 AM UTC+2, Dan Christensen wrote:

> > In other words, in your DC Proof the following holds:
> >
> > Ex(f(x) = g(x)) -> f = g.

That's what Ben's proof shows.

Hint: "I can prove too many things equal [in your DC Proof]. The problem is how to define my two functions so they /can't/ be proved equal." (Ben)

Indeed. Ben's proof allows to derive f = g if there is a constant c such that f(c) = g(c). (Hint: In Ben's proof c is 0.)

Can't you get that simple facts?

Dan Christensen <Dan_Christensen@sympatico.ca> writes:

> On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>>
>> > On Monday, April 18, 2022 at 7:02:36 PM UTC-4, Ben wrote:
>> >
>> >> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
>> >> & EXIST(a):a ε dom & EXIST(a):a ε cod
>> >> & ALL(a):[a ε dom => f1(a) ε cod]
>> >> & ALL(a):[a ε dom => f2(a) ε cod]
>> >> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
>> >> Axiom
>> >>
>> >> 2 EXIST(x):[Set(x) & ALL(a):[a ε x <=> a=0]]
>> >> Axiom
>> >>
>> >> 3 Set(s) & ALL(a):[a ε s <=> a=0]
>> >> E Spec, 2
>> >>
>> >> 4 Set(s)
>> >> Split, 3
>> >>
>> >> 5 ALL(a):[a ε s <=> a=0]
>> >> Split, 3
>> >>
>> >> 6 ALL(cod):ALL(f1):ALL(f2):[Set(s) & Set(cod)
>> >> & EXIST(a):a ε s & EXIST(a):a ε cod
>> >> & ALL(a):[a ε s => f1(a) ε cod]
>> >> & ALL(a):[a ε s => f2(a) ε cod]
>> >> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
>> >> U Spec, 1
>> >>
>> >> 7 ALL(f1):ALL(f2):[Set(s) & Set(s)
>> >> & EXIST(a):a ε s & EXIST(a):a ε s
>> >> & ALL(a):[a ε s => f1(a) ε s]
>> >> & ALL(a):[a ε s => f2(a) ε s]
>> >> => [f1=f2 <=> ALL(a):[a ε s => f1(a)=f2(a)]]]
>> >> U Spec, 6
>> >>
>> >> 8 0 ε s <=> 0=0
>> >> U Spec, 5
>> >>
>> >> 9 [0 ε s => 0=0] & [0=0 => 0 ε s]
>> >> Iff-And, 8
>> >>
>> >> 10 0 ε s => 0=0
>> >> Split, 9
>> >>
>> >> 11 0=0 => 0 ε s
>> >> Split, 9
>> >>
>> >> 12 0=0
>> >> Reflex
>> >>
>> >> 13 0 ε s
>> >> Detach, 11, 12
>> >>
>> >> 14 EXIST(a):a ε s
>> >> E Gen, 13
>> >>
>> >> 15 f(0)=0 & g(0)=0
>> >> Premise
>> >>
>> >> 16 z ε s
>> >> Premise
>> >>
>> >> 17 z ε s <=> z=0
>> >> U Spec, 5
>> >>
>> >> 18 [z ε s => z=0] & [z=0 => z ε s]
>> >> Iff-And, 17
>> >>
>> >> 19 z ε s => z=0
>> >> Split, 18
>> >>
>> >> 20 z=0 => z ε s
>> >> Split, 18
>> >>
>> >> 21 z=0
>> >> Detach, 19, 16
>> >>
>> >> 22 0 ε s
>> >> Substitute, 21, 16
>> >>
>> >> 23 f(0)=0
>> >> Split, 15
>> >>
>> >> 24 g(0)=0
>> >> Split, 15
>> >>
>> >> 25 f(0) ε s
>> >> Substitute, 23, 22
>> >>
>> >> 26 f(z) ε s
>> >> Substitute, 21, 25
>> >>
>> >> 27 ALL(a):[a ε s => f(a) ε s]
>> >> Conclusion, 16
>> >>
>> >> 28 z ε s
>> >> Premise
>> >>
>> >> 29 z ε s <=> z=0
>> >> U Spec, 5
>> >>
>> >> 30 [z ε s => z=0] & [z=0 => z ε s]
>> >> Iff-And, 29
>> >>
>> >> 31 z ε s => z=0
>> >> Split, 30
>> >>
>> >> 32 z=0 => z ε s
>> >> Split, 30
>> >>
>> >> 33 z=0
>> >> Detach, 31, 28
>> >>
>> >> 34 0 ε s
>> >> Substitute, 33, 28
>> >>
>> >> 35 f(0)=0
>> >> Split, 15
>> >>
>> >> 36 g(0)=0
>> >> Split, 15
>> >>
>> >> 37 g(0) ε s
>> >> Substitute, 36, 34
>> >>
>> >> 38 g(z) ε s
>> >> Substitute, 33, 37
>> >>
>> >> 39 ALL(a):[a ε s => g(a) ε s]
>> >> Conclusion, 28
>> >>
>> >> 40 ALL(f2):[Set(s) & Set(s)
>> >> & EXIST(a):a ε s & EXIST(a):a ε s
>> >> & ALL(a):[a ε s => f(a) ε s]
>> >> & ALL(a):[a ε s => f2(a) ε s]
>> >> => [f=f2 <=> ALL(a):[a ε s => f(a)=f2(a)]]]
>> >> U Spec, 7
>> >>
>> >> 41 Set(s) & Set(s)
>> >> & EXIST(a):a ε s & EXIST(a):a ε s
>> >> & ALL(a):[a ε s => f(a) ε s]
>> >> & ALL(a):[a ε s => g(a) ε s]
>> >> => [f=g <=> ALL(a):[a ε s => f(a)=g(a)]]
>> >> U Spec, 40
>> >>
>> >> 42 Set(s) & Set(s)
>> >> Join, 4, 4
>> >>
>> >> 43 Set(s) & Set(s) & EXIST(a):a ε s
>> >> Join, 42, 14
>> >>
>> >> 44 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
>> >> Join, 43, 14
>> >>
>> >> 45 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
>> >> & ALL(a):[a ε s => f(a) ε s]
>> >> Join, 44, 27
>> >>
>> >> 46 Set(s) & Set(s) & EXIST(a):a ε s & EXIST(a):a ε s
>> >> & ALL(a):[a ε s => f(a) ε s]
>> >> & ALL(a):[a ε s => g(a) ε s]
>> >> Join, 45, 39
>> >>
>> >> 47 f=g <=> ALL(a):[a ε s => f(a)=g(a)]
>> >> Detach, 41, 46
>> >>
>> >> 48 [f=g => ALL(a):[a ε s => f(a)=g(a)]]
>> >> & [ALL(a):[a ε s => f(a)=g(a)] => f=g]
>> >> Iff-And, 47
>> >>
>> >> 49 f=g => ALL(a):[a ε s => f(a)=g(a)]
>> >> Split, 48
>> >>
>> >> 50 ALL(a):[a ε s => f(a)=g(a)] => f=g
>> >> Split, 48
>> >>
>> >> 51 z ε s
>> >> Premise
>> >>
>> >> 52 z ε s <=> z=0
>> >> U Spec, 5
>> >>
>> >> 53 [z ε s => z=0] & [z=0 => z ε s]
>> >> Iff-And, 52
>> >>
>> >> 54 z ε s => z=0
>> >> Split, 53
>> >>
>> >> 55 z=0 => z ε s
>> >> Split, 53
>> >>
>> >> 56 z=0
>> >> Detach, 54, 51
>> >>
>> >> 57 f(0)=0
>> >> Split, 15
>> >>
>> >> 58 g(0)=0
>> >> Split, 15
>> >>
>> >> 59 z=g(0)
>> >> Substitute, 58, 56
>> >>
>> >> 60 0=g(0)
>> >> Substitute, 56, 59
>> >>
>> >> 61 f(0)=g(0)
>> >> Substitute, 57, 60
>> >>
>> >> 62 f(z)=g(z)
>> >> Substitute, 56, 61
>> >>
>> >> 63 ALL(a):[a ε s => f(a)=g(a)]
>> >> Conclusion, 51
>> >>
>> >> 64 f=g
>> >> Detach, 50, 63
>> >>
>> >> 65 ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>> >> Conclusion, 15
>> >
>> > Revisiting your proof here, the last line looks bizarre, but only
>> > because you left out some key information about functions f and g. It
>> > can be fixed up as follows:
>> >
>> > 65. ALL(a):[a in s => f(a) in s]
>> > & ALL(a):[a in s => g(a) in s]
>> > Join, 27, 39
>> >
>> > 66. ALL(a):[a in s => f(a) in s]
>> > & ALL(a):[a in s => g(a) in s]
>> > & f=g
>> > Join, 65, 64
>> >
>> > 67. ALL(f):ALL(g):[f(0)=0 & g(0)=0
>> > => ALL(a):[a in s => f(a) in s]
>> > & ALL(a):[a in s => g(a) in s]
>> > & f=g]
>> > Conclusion, 15
>
>> Pointless. It does not stop someone writing the proof that you think
>> needs to be "fixed up".
>
> There was nothing technically wrong with your proof. The new ending
> just makes it a little less perplexing.

On Wednesday, April 20, 2022 at 9:05:42 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, April 21, 2022 at 2:36:16 AM UTC+2, Dan Christensen wrote:
> > On Wednesday, April 20, 2022 at 8:25:44 PM UTC-4, Fritz Feldhase wrote:
> > > On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
> > > > On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> > > >
> > > > With your singleton {0} as the domain and codomain,
> > > >
> > > The common domain of f and g definded by Ben is {0, 1}.
> > >
> > Nope.
> Yes. At least this was the intended domain. (Though it seems there's no way to specify this in DC Proof.)

Wrong. Try:

Set(x) & ALL(a):[a in x <=> a=0 | a=1]

where '|' is the OR-operator.

> Anyway. Bens proof shows that any two functions f, g which *just* agree for ONE value, say 0, can be proved to be equal.
> In other words, in your DC Proof the following holds:
> Ex(f(x) = g(x)) -> f = g.
>

Wrong. See line 50:

ALL(a):[a ε s => f(a)=g(a)] => f=g

Dan

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

On Thursday, April 21, 2022 at 3:23:45 AM UTC+2, Dan Christensen wrote:
> On Wednesday, April 20, 2022 at 9:05:42 PM UTC-4, Fritz Feldhase wrote:
> > On Thursday, April 21, 2022 at 2:36:16 AM UTC+2, Dan Christensen wrote:
> > > On Wednesday, April 20, 2022 at 8:25:44 PM UTC-4, Fritz Feldhase wrote:
> > > > On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
> > > > > On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> > > > >
> > > > > With your singleton {0} as the domain and codomain,
> > > > >
> > > > The common domain of f and g definded by Ben is {0, 1}.
> > > >
> > > Nope.
> > Yes. At least this was the intended domain. (Though it seems there's no way to specify this in DC Proof.)
>
> Wrong. Try:
>
> Set(x) & ALL(a):[a in x <=> a=0 | a=1]
>
> where '|' is the OR-operator.

This only states that x = {0, 1}.

> > Anyway. Bens proof shows that any two functions f, g which *just* agree for ONE value, say 0, can be proved to be equal.
> >
> > In other words, in your DC Proof the following holds:
> > Ex(f(x) = g(x)) -> f = g.
> >
> Wrong.

True.

Again, Ben's proof allows to derive f = g if there is a constant c such that f(c) = g(c).

Hint: In Ben's proof c is 0.

> See line 50:
>
> ALL(a):[a ε s => f(a)=g(a)] => f=g]

Remeber s = {0}. (*)

Hence from 50 and (*) we get

f(0) = g(0) => f = g.

Fritz Feldhase <franz.fritschee.ff@gmail.com> writes:

> On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
>> On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
>> >
>> With your singleton {0} as the domain and codomain,
>
> Why are you lying all the time, you silly crank?
>
> The common domain of f and g definded by Ben is {0, 1}.

In fact no. Initially, in the first proof, I had two different
functions defined on those values that DC's axiom proved to be equal.
He objected that I had not somehow given the domain, but he was unable
to say how I should have done that.

In the second proof, that ~f=g => f=g no function was defined at all on
any domain. DC claims that the proof somehow only applied to functions
from {} since I used the empty set in the proof. The conclusion

ALL(f):ALL(g):[~f=g => f=g]

is about all f and g despite DC's claims to the contrary.

He then "fixed" this axiom to exclude empty sets, but that simply
permits other conclusions like

ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

Again, DC claims that this result is only about functions from {0} to
{0} because that's the set I used to get the result. It's a very odd
view of how proofs work.

> No idea how to "specify" the domain of a function in DC Spoof though.

That's the key problem. It's made worse by the fact that we can't
define new predicates. If we could, surely something like

Function(f,s1,s2)

that means f is a function from s1 to s2 would be both useful and easy
to define. I'd define Function(f,s1,s2) in the set-theoretic way so
that that, for a given f, it would be true for many different s1 and
s2.

> It seems to me that it can't be done. So all you can do in the context
> of DC Spoof is guessing.

DC himself can't do it, an I can't see a way to do it, but then I've not
looked at his set axioms. Maybe they can be used. It would mean
avoiding the notation f(x)=y, but (x,y) in f would do.

--
Ben.

On Thursday, April 21, 2022 at 3:35:39 AM UTC+2, Fritz Feldhase wrote:
>
> Again, Ben's proof allows to derive f = g if there is a constant c such that f(c) = g(c).
> Hint: In Ben's proof c is 0.
>>
> > See line 50:
> >
> > ALL(a):[a ε s => f(a)=g(a)] => f=g]
>
> Remeber s = {0}. (*)
>
> Hence from 50 and (*) we get
>
> f(0) = g(0) => f = g.

How to get that result?

Imho

Ax(x e {c} -> P(x)) <-> P(c)

is a theorem.

Hint:

Ax(x e {c} <-> x = c)

should be a theorem too.

Now isn't

Ax(x = c -> P(x)) <-> P(c)

a theorem in DC Proof?

On Wednesday, April 20, 2022 at 9:35:39 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, April 21, 2022 at 3:23:45 AM UTC+2, Dan Christensen wrote:
> > On Wednesday, April 20, 2022 at 9:05:42 PM UTC-4, Fritz Feldhase wrote:
> > > On Thursday, April 21, 2022 at 2:36:16 AM UTC+2, Dan Christensen wrote:
> > > > On Wednesday, April 20, 2022 at 8:25:44 PM UTC-4, Fritz Feldhase wrote:
> > > > > On Thursday, April 21, 2022 at 1:42:26 AM UTC+2, Dan Christensen wrote:
> > > > > > On Wednesday, April 20, 2022 at 6:33:54 PM UTC-4, Ben wrote:
> > > > > >
> > > > > > With your singleton {0} as the domain and codomain,
> > > > > >
> > > > > The common domain of f and g definded by Ben is {0, 1}.
> > > > >
> > > > Nope.
> > > Yes. At least this was the intended domain. (Though it seems there's no way to specify this in DC Proof.)
> >
> > Wrong. Try:
> >
> > Set(x) & ALL(a):[a in x <=> a=0 | a=1]
> >
> > where '|' is the OR-operator.

> This only states that x = {0, 1}.

As requested.

> > > Anyway. Bens proof shows that any two functions f, g which *just* agree for ONE value, say 0, can be proved to be equal.
> > >
> > > In other words, in your DC Proof the following holds:
> > > Ex(f(x) = g(x)) -> f = g.
> > >
> > Wrong.
> True.
>
> Again, Ben's proof allows to derive f = g if there is a constant c such that f(c) = g(c).

That works, as in this case, when the domain is a singleton.

> Hint: In Ben's proof c is 0.
> > See line 50:
> >
> > ALL(a):[a ε s => f(a)=g(a)] => f=g]
>
> Remeber s = {0}. (*)
>
> Hence from 50 and (*) we get
>
> f(0) = g(0) => f = g.

Since 0 is the only element of s, we can then conclude that:

ALL(a):[a ε s => f(a)=g(a)] => f=g]

Dan

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

On Wednesday, April 20, 2022 at 9:17:13 PM UTC-4, Ben wrote:
> Dan Christensen writes:
>

See Ben's Singleton Theorem at https://dcproof.com/Ben2.htm

Dan

Dan Christensen <Dan_Christensen@sympatico.ca> writes:

> On Wednesday, April 20, 2022 at 9:17:13 PM UTC-4, Ben wrote:
>> Dan Christensen writes:
>>
>
> See Ben's Singleton Theorem at https://dcproof.com/Ben2.htm

Please remove my name from your website -- both in file names and in any
pages where you might have used it.

Also what you prove is not my theorem. Why would you dishonestly
pretend that it is? What you show is your attempt to make

ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

look less silly.

If you asked a student (your target audience I think) to write, in DC
Proof, that the equality of all pairs of two things was a consequence of
some predicate, they would write (I hope)

ALL(x):ALL(y):[P(x,y) => x=y]

And I hope they would question (indeed reject) an axiom that allowed
that predicate to be x(0)=0 & y(0)=0.

--
Ben.