How difficult is contraposition for DC Proof and Dan Christensen?

[Mostowski Collapse]

Contraposition is a quite handy rule, in classical
logic the following are interchangeable:

A => B
----------------
~B => ~A

Does DC Proof not manage to provide contraposition.
Dan Christensen seems to have severe mental issues

to see that this "iff", also known as bi-conditional:

A <=> B

Can be separated into:

(A => B) &
(B => A)

Or alternatively separated into:

(A => B) &
(~A => ~B)

LoL

[Mostowski Collapse]

Maybe his truth table approach is too limited.
Like if I list this truth table:

A B A => B
0 0 1
0 1 1
1 0 0
1 1 1

Did I then also list the truth table for B => A
respectively ~A => ~B?

What about a truth table for ~A => C, is it
the same as the truth table for A => B.

LMAO!

[Dan Christensen]

On Tuesday, September 6, 2022 at 11:41:02 PM UTC-4, Mostowski Collapse wrote:
> Contraposition is a quite handy rule, in classical
> logic the following are interchangeable:
>
> A => B
> ----------------
> ~B => ~A
>

From DC Proof:

1. A => B
Premise

2. ~B => ~A
Contra, 1 <---------- On Logic menu

3. A => B => [~B => ~A]
Conclusion, 1

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

[Mostowski Collapse]

And why cant you answer this question:

Taos Formal definition only covers (one direction of "if"):

(SameDomCod => Postive_Def)

What about this direction (the other direction of "if"):

(~SameDomCod => Negative_Def)

If you make axioms that claim to cover text book mathematics,
you need to cover all text book mathematics. Also this

mathematics. Where is your axiom for this direction.
How would it read this axiom so that it covers the below?

Example 8.1.5 Recall that R+ denotes the subset
of R, the set of real numbers, given by {x e R > 0 }.
Consider the following four functions:
(i) f1: R -> R given by f1(x) = x2;
(ii) f2: R+ -> R given by f2(x) = x2;
(iii) f3: R -> R+ given by f3(x) = x2;
(iv) f4: R+ -> R+ given by f4(x) = x2.
Notice that, although the formula fi(x) = x2
is the same for each of these four functions,
they are considered to be four **distinct**
functions since the domain and codomain are
part of the definition of the function. We
will see later that these four functions have
different properties even though they are
given by the same formula.

Source:
An Introduction to Mathematical Reasoning:
Numbers, Sets and Functions von Peter J. Eccles

[Mostowski Collapse]

Interestingly Fritz has found more text book
sites, that amount to the same what Peter J. Eccles,
writes, even sometimes less based on examples,

but more explicit:

a) Fritz Feldhase schrieb am Mittwoch, 7. September 2022 um 08:00:47 UTC+2:

"if f : R → R is the function f(x) := x^2, and g := f|[1, 2] is the
restriction of f to the interval [1, 2],
then f and g both perform the operation of squaring, i.e., f(x) = x^2
and g(x) = x^2, but the two functions f and g are not considered the
same function, f =/= g, because they have different domains."
--Terence Tao, Analysis I

b) Fritz Feldhase schrieb am Mittwoch, 7. September 2022 um 08:25:48 UTC+2:

"2.2.1 Definition. Zwei Funktionen f: A --> B, g: C --> D heißen genau
dann gleich, wenn A = C und B = D ist und für jedes a e A f(a) = g(a) gilt."
--H. B. Griffiths, P. J. Hilton: Klassische Mathematik in zeitgemäßer
Darstellung [orig.: H. B. Griffiths, P. J. Hilton: A Comprehensive Textbook of Classical Mathematics]

c) Fritz Feldhase schrieb am Mittwoch, 7. September 2022 um 08:52:45 UTC+2:

Sebastian Pauli - 7.2 Equality of Functions
"Two functions that do not have the same domain and codomain are not equal.
[If f and g are not equal, we write f =/= g.]"
https://mathstats.uncg.edu/sites/pauli/112/HTML/secfuneq.html

[Dan Christensen]

On Wednesday, September 7, 2022 at 12:02:57 PM UTC-4, Mostowski Collapse wrote:
> And why cant you answer this question:
>
> Taos Formal definition only covers (one direction of "if"):
>
> (SameDomCod => Postive_Def)
>
> What about this direction (the other direction of "if"):
>
> (~SameDomCod => Negative_Def)
>

By design, the built-in axiom leaves indeterminate the equality of a pair of functions with different domains or codomains, but you don't have to use it. You can introduce your own definition no matter how outdated, wonky or unconventional it may be as long as it syntactically correct.

[snip text already addressed here]

[Fritz Feldhase]

On Wednesday, September 7, 2022 at 6:53:13 PM UTC+2, Dan Christensen wrote:
> On Wednesday, September 7, 2022 at 12:02:57 PM UTC-4, Mostowski Collapse wrote:
> > And why cant you answer this question:
> >
> > Taos Formal definition only covers (one direction of "if"):
> >
> > (SameDomCod => Postive_Def)
> >
> > What about this direction (the other direction of "if"):
> >
> > (~SameDomCod => Negative_Def)
> >

> By design [...]

It seems to me that for everyone -except you- it's clear that two functions that do not have the same domain and/or codomain _are not equal_.

I'd like to see a quote which contradicts my claim. (John Gabriel maybe?)

Actually, we find statements like:

"Two functions that do not have the same domain and codomain are not equal.
[If f and g are not equal, we write f =/= g.]"
https://mathstats.uncg.edu/sites/pauli/112/HTML/secfuneq.html

or:

"if f : R → R is the function f(x) := x^2, and g := f|[1, 2] is the
restriction of f to the interval [1, 2],
then f and g both perform the operation of squaring, i.e., f(x) = x^2
and g(x) = x^2, but the two functions f and g are not considered the
same function, f =/= g, because they have different domains."
--Terence Tao, Analysis I

etc.

[Dan Christensen]

On Wednesday, September 7, 2022 at 1:44:09 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, September 7, 2022 at 6:53:13 PM UTC+2, Dan Christensen wrote:
> > On Wednesday, September 7, 2022 at 12:02:57 PM UTC-4, Mostowski Collapse wrote:
> > > And why cant you answer this question:
> > >
> > > Taos Formal definition only covers (one direction of "if"):
> > >
> > > (SameDomCod => Postive_Def)
> > >
> > > What about this direction (the other direction of "if"):
> > >
> > > (~SameDomCod => Negative_Def)
> > >
> > By design [...]
>
> It seems to me that for everyone -except you- it's clear that two functions that do not have the same domain and/or codomain _are not equal_.
>

[snip]

If you want to use a different definition, you are free to do so, even within DC Proof. With its Axiom Rule, you can establish your own axioms/definitions at the beginning of any proof, as long as they are syntactically correct.

The user will be in good company, however, if they decide to use the built-in formal axiom of equality in DC Proof based on that in the best-selling analysis textbook by none other than Terence Tao, "widely regarded as one of the greatest living mathematicians and has been referred to as the 'Mozart' of mathematics." https://en.wikipedia.org/wiki/Terence_Tao (Notwithstanding his informal commentary.)

[Mostowski Collapse]

Well the built-in axiom only covers the direction =>:

(SameDomCod => Postive_Def)

What about the other direction <=, as contraposition:

(~SameDomCod => Negative_Def)

There seems to be a sever gap in DC Proof, which has
consequences for function spaces. If you have two
function spaces F and G, then by extensionality they

should be equal if we have:

ALL(x):[x e F <=> x e G]

Or written as:

ALL(x):[x e F <=> EXIST(y):[y e G & x = y]]

How do you define equality of function spaces,
if the equality = on the member of function spaces
is missing? Has gaps, where it is undefined?

Are these function spaces the same or different,
or does DC Proof not have enough axioms to
decide either A=B or A=\=B :

A = {f1, f2, f3}

B = {f1, f2, f3, f4} ?

Where f1, f2, f3 and f4 are from below:

Example 8.1.5 Recall that R+ denotes the subset
of R, the set of real numbers, given by {x e R > 0 }.
Consider the following four functions:
(i) f1: R -> R given by f1(x) = x2;
(ii) f2: R+ -> R given by f2(x) = x2;
(iii) f3: R -> R+ given by f3(x) = x2;
(iv) f4: R+ -> R+ given by f4(x) = x2.
Notice that, although the formula fi(x) = x2
is the same for each of these four functions,
they are considered to be four **distinct**
functions since the domain and codomain are
part of the definition of the function. We
will see later that these four functions have
different properties even though they are
given by the same formula.

[Fritz Feldhase]

On Wednesday, September 7, 2022 at 9:37:10 PM UTC+2, Mostowski Collapse wrote:
>
> There seems to be a sever gap in DC Proof, which has consequences for function spaces.

Agree. Actually, it seems to me that it's clear for everyone -except Dan- that two functions that do not have the same domain and/or codomain _are not equal_.

I'd like to see a quote which contradicts my claim. (John Gabriel maybe?)

Usually we find statements like:

"Two functions that do not have the same domain and codomain are not equal.
[If f and g are not equal, we write f =/= g.]"
https://mathstats.uncg.edu/sites/pauli/112/HTML/secfuneq.html

or:

"if f : R → R is the function f(x) := x^2, and g := f|[1, 2] is the
restriction of f to the interval [1, 2],
then f and g both perform the operation of squaring, i.e., f(x) = x^2
and g(x) = x^2, but the two functions f and g are not considered the
same function, f =/= g, because they have different domains."
--Terence Tao, Analysis I

etc.

- or a formal definition for the "equality of functions" which does not need such an "extra clause".

Say, "2.2.1 Definition. Zwei Funktionen f: A --> B, g: C --> D heißen genau

dann gleich, wenn A = C und B = D ist und für jedes a e A f(a) = g(a) gilt."
--H. B. Griffiths, P. J. Hilton: Klassische Mathematik in zeitgemäßer
Darstellung [orig.: H. B. Griffiths, P. J. Hilton: A Comprehensive Textbook of Classical Mathematics]

Finally, in any set theoretic treatment of functions a la Bourbaki it just follows from the axiom of extensionality, no "definition" needed. There, say, "2.2.1 Definition" is a theorem!

It seems to me that DC does not unterstand these states of affairs concerning "functions".

[Dan Christensen]

On Wednesday, September 7, 2022 at 3:37:10 PM UTC-4, Mostowski Collapse wrote:
> Well the built-in axiom only covers the direction =>:
>
> (SameDomCod => Postive_Def)
>

As it should be.

> What about the other direction <=, as contraposition:
>
> (~SameDomCod => Negative_Def)
>

Not required.

> There seems to be a sever gap in DC Proof, which has
> consequences for function spaces. If you have two
> function spaces F and G, then by extensionality they
>
> should be equal if we have:
>
> ALL(x):[x e F <=> x e G]
>
> Or written as:
>
> ALL(x):[x e F <=> EXIST(y):[y e G & x = y]]
>
> How do you define equality of function spaces,
> if the equality = on the member of function spaces
> is missing?
> Has gaps, where it is undefined?
>
> Are these function spaces the same or different,
> or does DC Proof not have enough axioms to
> decide either A=B or A=\=B :
>
> A = {f1, f2, f3}
>
> B = {f1, f2, f3, f4} ?
>
> Where f1, f2, f3 and f4 are from below:
> Example 8.1.5 Recall that R+ denotes the subset
> of R, the set of real numbers, given by {x e R > 0 }.
> Consider the following four functions:

> (i) f1: R -> R given by f1(x) = x^2; <----- assuming exponentiation
> (ii) f2: R+ -> R given by f2(x) = x^2;
> (iii) f3: R -> R+ given by f3(x) = x^2;
> (iv) f4: R+ -> R+ given by f4(x) = x^ 2.

[snip]

What has this got to do with function spaces? Every element of a given function space has the SAME domain and codomain. You need another example.

[Mostowski Collapse]

They are sets of functions. They are subset of this
union of function spaces:

F = (R -> R) u (R+ -> R) u (R -> R+) u (R+ -> R+)

{f1, f2, f3} ⊆ F

{f1, f2, f3, f4} ⊆ F

Do you think function spaces are something to
put into a vitrine and only look at? They can be

used like any other set. Whats wrong with you?
So what is the answer to this question:

{f1, f2, f3} =?= {f1, f2, f3, f4}

LoL

Ha Ha, Dan Christensen thinks function spaces
are not sets only knick-knacks like this dog:

RAKSO Der Original Wackeldackel
https://www.amazon.de/dp/B003KM95C4

[Mostowski Collapse]

Pitty DC Proof cannot prove:

Proposition: 4.2.5 If A is a set and F : A -> B then F is a set.
http://www1.maths.leeds.ac.uk/~rathjen/book.pdf

LoL

[Dan Christensen]

> They are sets of functions. They are subset of this
> union of function spaces:
>
> F = (R -> R) u (R+ -> R) u (R -> R+) u (R+ -> R+)
>

Not a function space since different functions within F have different domains and codomains.

> {f1, f2, f3} ⊆ F
>
> {f1, f2, f3, f4} ⊆ F
>
> Do you think function spaces are something to
> put into a vitrine and only look at? They can be
>
> used like any other set.

[snip childish abuse]

> So what is the answer to this question:
>
> {f1, f2, f3} =?= {f1, f2, f3, f4}
>

These are not function spaces either. Try again, Jan Burse.

[Dan Christensen]

On Wednesday, September 7, 2022 at 8:00:09 PM UTC-4, Mostowski Collapse wrote:
> Pitty DC Proof cannot prove:
>
> Proposition: 4.2.5 If A is a set and F : A -> B then F is a set.

No need to. It is easy, however, to reconstruct graph g of function f in DC Proof (only 60 lines):

ALL(a):ALL(b):ALL(f):[Set(a) & Set(b) & ALL(c):[c in a => f(c) in b]
=> EXIST(g):[Set'(g)
& ALL(c):ALL(d):[(c,d) in g => c in a & d in b]
& ALL(c):ALL(d):[c in a & d in b => [(c,d) in g <=> f(c)=d]]]]

[Jeff Barnett]

A log time ago (1970s?) I dug thru a book on solving "functional
equations" by a man named Aczel. Your url above seems to lead to a
fairly current manuscript with authors Peter Aczel and Michael Rathjen.
Is the first of these the son of the one I was reading 50 years ago?
--
Jeff Barnett

[Fritz Feldhase]

Peter Aczel is 80 years old. Hope this helps.

[Fritz Feldhase]

On Thursday, September 8, 2022 at 4:22:19 AM UTC+2, Dan Christensen wrote:
>
> No need to. It is easy, however, to reconstruct graph g of function f in DC Proof (only 60 lines):

A set which consists of elements you cannot work with, idiot.

AX(X e f -> Ex(X = (x, x)))

Can write this in DC Spoof?

[Dan Christensen]

On Wednesday, September 7, 2022 at 10:22:19 PM UTC-4, Dan Christensen wrote:
> On Wednesday, September 7, 2022 at 8:00:09 PM UTC-4, Mostowski Collapse wrote:
> > Pitty DC Proof cannot prove:
> >
> > Proposition: 4.2.5 If A is a set and F : A -> B then F is a set.
> No need to. It is easy, however, to reconstruct graph g of function f in DC Proof (only 60 lines):
>
> ALL(a):ALL(b):ALL(f):[Set(a) & Set(b) & ALL(c):[c in a => f(c) in b]
> => EXIST(g):[Set'(g)
> & ALL(c):ALL(d):[(c,d) in g => c in a & d in b]
> & ALL(c):ALL(d):[c in a & d in b => [(c,d) in g <=> f(c)=d]]]]

PROOF

Suppose...

1 Set(x) & Set(y) & ALL(c):[c in x => f(c) in y]
Premise

2 Set(x)
Split, 1

3 Set(y)
Split, 1

4 ALL(c):[c in x => f(c) in y]
Split, 1

Apply Cartesian Product Axiom

5 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in a1 & c2 in a2]]]
Cart Prod

6 ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in a2]]]
U Spec, 5

7 Set(x) & Set(y) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in y]]
U Spec, 6

8 Set(x) & Set(y)
Join, 2, 3

9 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) in b <=> c1 in x & c2 in y]]
Detach, 7, 8

10 Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) in xy <=> c1 in x & c2 in y]
E Spec, 9


Define: xy (Cartesian product x*y)

11 Set'(xy)
Split, 10

12 ALL(c1):ALL(c2):[(c1,c2) in xy <=> c1 in x & c2 in y]
Split, 10

Apply Subset Axiom

13 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) in sub <=> (a,b) in xy & f(a)=b]]
Subset, 11

14 Set'(g) & ALL(a):ALL(b):[(a,b) in g <=> (a,b) in xy & f(a)=b]
E Spec, 13


Define: g (graph set for function f)

15 Set'(g)
Split, 14

16 ALL(a):ALL(b):[(a,b) in g <=> (a,b) in xy & f(a)=b]
Split, 14

Prove: ALL(c):ALL(d):[c in x & d in y => [(c,d) in g <=> f(c)=d]]

Suppose...

17 t in x & u in y
Premise

18 t in x
Split, 17

19 u in y
Split, 17


Suppose...

20 (t,u) in g
Premise

21 ALL(b):[(t,b) in g <=> (t,b) in xy & f(t)=b]
U Spec, 16

22 (t,u) in g <=> (t,u) in xy & f(t)=u
U Spec, 21

23 [(t,u) in g => (t,u) in xy & f(t)=u]
& [(t,u) in xy & f(t)=u => (t,u) in g]
Iff-And, 22

24 (t,u) in g => (t,u) in xy & f(t)=u
Split, 23

25 (t,u) in xy & f(t)=u
Detach, 24, 20

26 (t,u) in xy
Split, 25

27 f(t)=u
Split, 25

As Required:

28 (t,u) in g => f(t)=u
Conclusion, 20

Prove: f(t)=u => (t,u) in g

Suppose...

29 f(t)=u
Premise

30 ALL(b):[(t,b) in g <=> (t,b) in xy & f(t)=b]
U Spec, 16

31 (t,u) in g <=> (t,u) in xy & f(t)=u
U Spec, 30

32 [(t,u) in g => (t,u) in xy & f(t)=u]
& [(t,u) in xy & f(t)=u => (t,u) in g]
Iff-And, 31

33 (t,u) in xy & f(t)=u => (t,u) in g
Split, 32

34 ALL(c2):[(t,c2) in xy <=> t in x & c2 in y]
U Spec, 12

35 (t,u) in xy <=> t in x & u in y
U Spec, 34

36 [(t,u) in xy => t in x & u in y]
& [t in x & u in y => (t,u) in xy]
Iff-And, 35

37 t in x & u in y => (t,u) in xy
Split, 36

38 (t,u) in xy
Detach, 37, 17

39 (t,u) in xy & f(t)=u
Join, 38, 29

40 (t,u) in g
Detach, 33, 39

As Required:

41 f(t)=u => (t,u) in g
Conclusion, 29

42 [(t,u) in g => f(t)=u] & [f(t)=u => (t,u) in g]
Join, 28, 41

43 (t,u) in g <=> f(t)=u
Iff-And, 42

As Required:

44 ALL(c):ALL(d):[c in x & d in y => [(c,d) in g <=> f(c)=d]]
Conclusion, 17

Prove: ALL(c):ALL(d):[(c,d) in g => c in x & d in y]

Suppose...

45 (t,u) in g
Premise

46 ALL(b):[(t,b) in g <=> (t,b) in xy & f(t)=b]
U Spec, 16

47 (t,u) in g <=> (t,u) in xy & f(t)=u
U Spec, 46

48 [(t,u) in g => (t,u) in xy & f(t)=u]
& [(t,u) in xy & f(t)=u => (t,u) in g]
Iff-And, 47

49 (t,u) in g => (t,u) in xy & f(t)=u
Split, 48

50 (t,u) in xy & f(t)=u
Detach, 49, 45

51 (t,u) in xy
Split, 50

52 ALL(c2):[(t,c2) in xy <=> t in x & c2 in y]
U Spec, 12

53 (t,u) in xy <=> t in x & u in y
U Spec, 52

54 [(t,u) in xy => t in x & u in y]
& [t in x & u in y => (t,u) in xy]
Iff-And, 53

55 (t,u) in xy => t in x & u in y
Split, 54

56 t in x & u in y
Detach, 55, 51

As Required:

57 ALL(c):ALL(d):[(c,d) in g => c in x & d in y]
Conclusion, 45

58 Set'(g)
& ALL(c):ALL(d):[(c,d) in g => c in x & d in y]
Join, 15, 57

59 Set'(g)
& ALL(c):ALL(d):[(c,d) in g => c in x & d in y]
& ALL(c):ALL(d):[c in x & d in y => [(c,d) in g <=> f(c)=d]]
Join, 58, 44

As Required:

60 ALL(a):ALL(b):ALL(f):[Set(a) & Set(b) & ALL(c):[c in a => f(c) in b]

=> EXIST(g):[Set'(g)
& ALL(c):ALL(d):[(c,d) in g => c in a & d in b]
& ALL(c):ALL(d):[c in a & d in b => [(c,d) in g <=> f(c)=d]]]]

Conclusion, 1

[Mostowski Collapse]

Hi,

Its basically a book about constructive set theory,
it has also sections about Relations and functions
and Function Spaces.

Can DC Spoof prove?

Proposition: 4.2.3 If R (a class symbol) is a set of
pairs then dom(R) and ran(R) are sets.

CST Book draft
http://www1.maths.leeds.ac.uk/~rathjen/book.pdf

LMAO!

Fritz Feldhase schrieb:

[Mostowski Collapse]

Hi,


John Bell wanted to name his book about
intuitionistic set theory first constructive
set theory, but then he decided against it.

These authors consequently call their book
constructive set theory, there seems to be
now a distinction between intuitionistic

and constructive, can be seen in section
3 axioms. It says:

"Constructive Set Theory is a variant of Classical
Set Theory which uses intuitionistic logic. It
di ers from another such variant called Intuitionistic
Set Theory because of its avoidance of the full
impredicativity that Intuitionistic Set Theory has."

CST Book draft
http://www1.maths.leeds.ac.uk/~rathjen/book.pdf

Bye

Mostowski Collapse schrieb:

[Mostowski Collapse]

Wromg again. You are confusing the

**product** function space

A -> B = pi_A B

with function space generis, which is
just a set of functions. Its the same
with Euclidean space. Here the word

"space" is also subset, a subset
A ⊆ R^3. Like the space inside an
ellipsoid, like the space of the Earth,

is also a space. Need not be full R^3.
You forget or are ignorant of the ethymology
of the word space, it means:

https://en.wikipedia.org/wiki/Volume

Whats wrong with you? Don't you live
in a spacy appartment, somewhere in
a dark hole under a rock, that youre that dumb?

Dan Christensen schrieb:

[Jeff Barnett]

I assume the Aczel who wrote the text on functional analysis was not
Peter. I was guessing they were related and asking what the relation was.
--
Jeff Barnett

[Fritz Feldhase]

Maybe not related.

https://en.m.wikipedia.org/wiki/J%C3%A1nos_Acz%C3%A9l_(mathematician)

https://en.m.wikipedia.org/wiki/Peter_Aczel

[Mostowski Collapse]

Since Logicians usually get as old as the Queen, you
can say Peter Aczel, with his 81 years, is still quite young.
People that walked the earth in 80's might know him from AFA:

AFA ("Anti-Foundation Axiom") – due to M. Forti and F. Honsell
(this is also known as Aczel's anti-foundation axiom);
https://en.wikipedia.org/wiki/Non-well-founded_set_theory

What stroke me that the CST Book draft
has a chapter about Co-Induction. Thats pretty cool!

[Mostowski Collapse]

This is also a nice marketing pitch:

Aczel’s hypersets were extensively used by
Jon Barwise and John Etchemendy in thei
1987 book The Liar, on the liar's paradox; The
book is also a good introduction to the topic
of non-well-founded sets.

[Dan Christensen]

On Thursday, September 8, 2022 at 12:05:40 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb:
> >> {f1, f2, f3} =?= {f1, f2, f3, f4}
> > These are not function spaces either. Try again, Jan Burse.

> Wromg again. You are confusing the
>
> **product** function space
>
> A -> B = pi_A B
>
> with function space generis, which is
> just a set of functions.

[snip]

Again, if you want to use alternative definitions to those built-into DC Proof, that, too, is possible within DC Proof by using the Axiom Rule. In DC Proof, the built-in definition of function equality, for example, is applicable only for functions with the same domain and codomain. If you want to make it more widely applicable, e.g .to any arbitrary pair of functions, it may be possible to do so--it might even work, who knows? Likewise, if you want to define a function space as just an arbitrary collection of sets, you are free to do so. But why not just it call a set of functions?

[Mostowski Collapse]

The problem with your higher order substitution, the
higher order substitution of Dan Christensen in DC Spoof,
and the problem with the function equality axioms also in

DC Spoof, is probably that I can provoke an inconsistency.
I can use the same substition trick to derive an inequality,
by using the contrapositive of "The indiscernibility of identicals":

f1 =\= f2
https://en.wikipedia.org/wiki/Identity_of_indiscernibles#Identity_and_indiscernibility

Where the function equality axiom of Dan Christensen gives me:

f1 = f2

Simple example:

Take f1 : {0} -> {0}, f1(0)=0, f1(1)=1,
f2 : {0} -> {0}, f2(0)=0, f2(1)=0

I only need a formula A(_) that discriminates f1 and f2. My point
for long is already that the main problem of Dan Christensens approach
is that he cannot prove:

Mostowski Collapse schrieb am Donnerstag, 8. September 2022 um 02:00:09 UTC+2:
> Pitty DC Proof cannot prove:
>
> Proposition: 4.2.5 If A is a set and F : A -> B then F is a set.
> http://www1.maths.leeds.ac.uk/~rathjen/book.pdf
>

> LoL
https://groups.google.com/g/sci.logic/c/UGlOyyBYVLU/m/Lv4mduDABAAJ

[Mostowski Collapse]

A formula A(_) that does the discrimination is relatively
easy. Dan Christensen was begging for it to use Surjective(_,_,_).
Ok lets use Surjective, of course we have:

Surjective(f1,{0,1},{0,1})
~Surjective(f2,{0,1},{0,1})

Therefore:

f1 =\= f2.

LoL

[Dan Christensen]

On Friday, September 9, 2022 at 10:25:23 AM UTC-4, Mostowski Collapse wrote:

[snip childish abuse]

> f1 =\= f2
> https://en.wikipedia.org/wiki/Identity_of_indiscernibles#Identity_and_indiscernibility
>
> Where the function equality axiom of Dan Christensen gives me:
>
> f1 = f2
>
> Simple example:
>
> Take f1 : {0} -> {0}, f1(0)=0, f1(1)=1,
> f2 : {0} -> {0}, f2(0)=0, f2(1)=0
>

Both f1(1) and f2(1) are undefined since 1 is not in their domains. What is your point here, Jan Burse? If you can prove f1=f2 from certain assumptions, then adding these other assumptions will not change this fact. Try again, Jan Burse.

[Dan Christensen]

On Friday, September 9, 2022 at 2:38:51 PM UTC-4, Mostowski Collapse wrote:
> A formula A(_) that does the discrimination is relatively
> easy. Dan Christensen was begging for it to use Surjective(_,_,_).
> Ok lets use Surjective, of course we have:
>
> Surjective(f1,{0,1},{0,1})
> ~Surjective(f2,{0,1},{0,1})
>
> Therefore:
>
> f1 =\= f2.
>

Requires formal proof. Hint: Try proof by cases. Only 4 cases to consider.

[Mostowski Collapse]

f1 and f2 are surely defined at 1, since I wrote:

> > Take f1 : {0} -> {0}, f1(0)=0, f1(1)=1,
> > f2 : {0} -> {0}, f2(0)=0, f2(1)=0

Whats wrong with you?

[Dan Christensen]

On Friday, September 9, 2022 at 7:54:02 PM UTC-4, Mostowski Collapse wrote:
> f1 and f2 are surely defined at 1, since I wrote:
>
> > > Take f1 : {0} -> {0}, f1(0)=0, f1(1)=1,
> > > f2 : {0} -> {0}, f2(0)=0, f2(1)=0
> Whats wrong with you?
> Dan Christensen schrieb am Freitag, 9. September 2022 um 23:57:05 UTC+2:
> > On Friday, September 9, 2022 at 10:25:23 AM UTC-4, Mostowski Collapse wrote:
> >
> > [snip childish abuse]
> > > f1 =\= f2
> > > https://en.wikipedia.org/wiki/Identity_of_indiscernibles#Identity_and_indiscernibility
> > >
> > > Where the function equality axiom of Dan Christensen gives me:
> > >
> > > f1 = f2
> > >
> > > Simple example:
> > >
> > > Take f1 : {0} -> {0}, f1(0)=0, f1(1)=1,
> > > f2 : {0} -> {0}, f2(0)=0, f2(1)=0
> > >
> > Both f1(1) and f2(1) are undefined since 1 is not in their domains. What is your point here, Jan Burse? If you can prove f1=f2 from certain assumptions, then adding these other assumptions will not change this fact. Try again, Jan Burse.

> f1 and f2 are surely defined at 1, since I wrote:
>
> > > Take f1 : {0} -> {0}, f1(0)=0, f1(1)=1,
> > > f2 : {0} -> {0}, f2(0)=0, f2(1)=0

Perhaps you didn't know, but f1 : {0} -> {0} means something different from f1: {0,1} --> {0}. Yes, really! Can you guess what the difference is, Jan Burse? No???? Didn't think so.

[Fritz Feldhase]

On Friday, September 9, 2022 at 4:25:23 PM UTC+2, Mostowski Collapse wrote:
>
> I can use the same substition trick to derive an inequality,
> by using the contrapositive of "The indiscernibility of identicals":
>
> f1 =\= f2

Yeah, some days ago I tried to teach DC some basic math:

"Hint: If a and b are two mathematical objects, then a = b or a =/= b. If a = b then any property that holds for a also holds for b [and vice versa], and hence especially dom(a) = dom(b) [assuming a and b were functions]. Now in our case we have dom(f) =/= dom(g). Hence ~(f = g) or f =/= g."

- but DC is too dumb to get it.

[Fritz Feldhase]

On Wednesday, September 7, 2022 at 11:21:33 PM UTC+2, Fritz Feldhase wrote:

> On Wednesday, September 7, 2022 at 9:37:10 PM UTC+2, Mostowski Collapse wrote:
> >
> > There seems to be a sever gap in DC Proof, which has consequences for function spaces.
> >

> Agree. Actually, it seems to me that it's clear for everyone -except Dan- that two functions that do not have the same domain and/or codomain _are not equal_.
>
> I'd like to see a quote which contradicts my claim. (John Gabriel maybe? Mückenheim?)
>
> Usually we find statements like:
>
> "Two functions that do not have the same domain and codomain are not equal.
> [If f and g are not equal, we write f =/= g.]"
> Source: https://mathstats.uncg.edu/sites/pauli/112/HTML/secfuneq.html
>
> or:
>
> "the two functions f and g are not considered the same function, f =/= g,
> because they have different domains." --Terence Tao, Analysis I
>
> etc.
>
> and/or a formal definition for the "equality of functions" which does not need such an "extra clause".
>
> Say, "2.2.1 Definition. Zwei Funktionen f: A --> B, g: C --> D heißen genau
> dann gleich, wenn A = C und B = D ist und für jedes a e A f(a) = g(a) gilt."
> --H. B. Griffiths, P. J. Hilton: Klassische Mathematik in zeitgemäßer
> Darstellung [orig.: H. B. Griffiths, P. J. Hilton: A Comprehensive Textbook of Classical Mathematics]

or:

"We say two functions f and g are equal if they have the same domain and the same codomain, and if for every a in the domain, f(a) = g(a)."
Source: https://www.whitman.edu/mathematics/higher_math_online/section04.01.html

So, what's the problem with this idiot (Dan)?

> It seems to me that DC does not unterstand these states of affairs concerning "functions".

Is he demented? Or just a genuine crank (like JG, WM, AP, ...)?

[Dan Christensen]

In this case, the usual definition of function equality is not applicable. The truth value of f=g remains indeterminate.

[Dan Christensen]

On Saturday, September 10, 2022 at 1:59:15 AM UTC-4, Fritz Feldhase wrote:
[snip]

> > Say, "2.2.1 Definition. Zwei Funktionen f: A --> B, g: C --> D heißen genau
> > dann gleich, wenn A = C und B = D ist und für jedes a e A f(a) = g(a) gilt."
> > --H. B. Griffiths, P. J. Hilton: Klassische Mathematik in zeitgemäßer
> > Darstellung [orig.: H. B. Griffiths, P. J. Hilton: A Comprehensive Textbook of Classical Mathematics]
>
> or:
>
> "We say two functions f and g are equal if they have the same domain and the same codomain, and if for every a in the domain, f(a) = g(a)."
> Source: https://www.whitman.edu/mathematics/higher_math_online/section04.01.html
>

[snip abuse]

The problem with that apparently outdated definition of function equality is that it is applicable even for functions with different domains and codomains.

The following definition would seem to reflect a new consensus:

"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 [with respect to the domain X], 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.)"
--Terence Tao, "Analysis I," p. 51

This definition is built-into DC Proof on the Sets menu, but you can play around with out-dated definitions or concoct something entirely new by using the Axiom Rule on the Logic menu.

[Fritz Feldhase]

On Saturday, September 10, 2022 at 4:03:07 PM UTC+2, Dan Christensen wrote:

> The <bla>

Shut up, crank.

[Fritz Feldhase]

On Saturday, September 10, 2022 at 3:49:14 PM UTC+2, Dan Christensen wrote:
>
> In this case

Shut up, crank.

[Fritz Feldhase]

On Saturday, September 10, 2022 at 4:03:07 PM UTC+2, Dan Christensen wrote:

> This definition is built-into DC Proof on the Sets menu

A rather bad choice.

Hint: https://proofwiki.org/wiki/Equality_of_Mappings

It's not clear to me, what's your problem, Dan.

Are you suffering from some sort of brain damage? (I'm serious.)

Or are you a lying fraud? Having never attended a math class at university?

[Mostowski Collapse]

If this would be the case, that there is some
obligation, why do you propose Surjective(_,_,_)
and not Surjective(_).

I think the point of have Surjective(_,_,_),
that you can use it like that:

Surjective(f,dom1,cod1)

Or like that:

Surjective(f,dom2,cod2)

Isn't this the point of Surjective(_,_,_)?

Dan Christensen halucinated:> Perhaps you didn't know, but f1 : {0} ->

[Fritz Feldhase]

On Saturday, September 10, 2022 at 8:45:04 PM UTC+2, Mostowski Collapse wrote:

> Dan Christensen halucinated ...

It seems to me that he does that all the time.

[Fritz Feldhase]

On Saturday, September 10, 2022 at 8:45:04 PM UTC+2, Mostowski Collapse wrote:

> Surjective(_,_,_)

I'd prefere to call that "surjection(f, X, Y)" and read it as

"f is a surjection from X to Y"

sometimes written as

"f: X -->> Y".

Hence the following should hold:

surjection(f, X, Y) <-> function(f) & dom(f) = X & codom(f) = Y & forall y e Y there exists an x e X such that f(x) = y.

We might even DEFINE /surjection(., ., .)/ that way.

This way we might be able to use 2 different predicates:

- surjection(., ., .)

AND

- surjective(.).

Both might be helful in certain contexts.

[Mostowski Collapse]

Here is a challenge that involves "iff" beyond a simple
reading of Terrence Tao. Take these two function spaces:

A = { f : X -> X }
B = { f : Y -> Y }

Can you prove in DC Spoiled this standard theorem:

X =\= Y -> A ∩ B = {}

Mostowski Collapse schrieb am Mittwoch, 7. September 2022 um 05:41:02 UTC+2:
> Contraposition is a quite handy rule, in classical
> logic the following are interchangeable:
>
> A => B
> ----------------
> ~B => ~A
>
> Does DC Proof not manage to provide contraposition.
> Dan Christensen seems to have severe mental issues
>
> to see that this "iff", also known as bi-conditional:
>
> A <=> B
>
> Can be separated into:
>
> (A => B) &
> (B => A)
>
> Or alternatively separated into:
>
> (A => B) &
> (~A => ~B)
>
> LoL

[Dan Christensen]

On Thursday, September 22, 2022 at 12:53:30 PM UTC-4, Mostowski Collapse wrote:
> Here is a challenge that involves "iff" beyond a simple
> reading of Terrence Tao. Take these two function spaces:
>
> A = { f : X -> X }
> B = { f : Y -> Y }
>

> Can you prove in DC Proof this standard theorem:

>
> X =\= Y -> A ∩ B = {}
>

It may be a "standard theorem" if you assume all functions are comparable (wrt functional equality). I doubt it is provable otherwise, i.e. if, as in Tao, only functions with the same domains and codomains are comparable. No great loss IMHO.

[Fritz Feldhase]

On Thursday, September 22, 2022 at 8:22:10 PM UTC+2, Dan Christensen wrote:

> if, as in Tao, only functions with the same domains and codomains are comparable.

No, you silly asshole full of shit. That's NOT what Tao claims.

"if f : R → R is the function f(x) := x^2, and g := f | [1, 2] is the restriction of f to the interval [1, 2], then f and g both perform
the operation of squaring, i.e., f(x) = x^2 and g(x) = x^2, but the two functions f and g are not considered the same function,
f =/= g, because they have different domains." -Terence Tao, Analysis I

What's the matter with you, asshole? Are you demented?

[Dan Christensen]

On Thursday, September 22, 2022 at 6:20:33 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, September 22, 2022 at 8:22:10 PM UTC+2, Dan Christensen wrote:
>
> > if, as in Tao, only functions with the same domains and codomains are comparable.

[snip childish abuse]

> That's NOT what Tao claims.
>

Still grasping at straws trying to save face, Fritz? It isn't working. It's really kind of pathetic.

"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 [with respect to the domain X], 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.)"
--Terence Tao, "Analysis I," p. 51

[Fritz Feldhase]

On Friday, September 23, 2022 at 12:54:35 AM UTC+2, Dan Christensen wrote:
> On Thursday, September 22, 2022 at 6:20:33 PM UTC-4, Fritz Feldhase wrote:
> > On Thursday, September 22, 2022 at 8:22:10 PM UTC+2, Dan Christensen wrote:
> > >
> > > if, as in Tao, only functions with the same domains and codomains are comparable.

No, you silly asshole full of shit. That's NOT what Tao claims

"if f : R → R is the function f(x) := x^2, and g := f | [1, 2] is the restriction of f to the interval [1, 2], then f and g both perform
the operation of squaring, i.e., f(x) = x^2 and g(x) = x^2, but the two functions f and g are not considered the same function,
f =/= g, because they have different domains." -Terence Tao, Analysis I

What's the matter with you? Are you on drugs?

[Mostowski Collapse]

Dan Christensen doesn't understand what Terrence Tao writes.
He cannot form f | [1,2] in DC Spoiled. After his application of the
function axiom, his idea is that he has then "named" a graph,

given it a "name". But these name lives not in some domain
where for example function restriction cannot be easily
defined, as is done here:

In mathematics, the restriction of a function f is a new function, denoted f | A
https://en.wikipedia.org/wiki/Restriction_%28mathematics%29

But he would prefers to rather become the king of cranks,
instead of letting go of all the DC Spoiled nonsense.

[Mostowski Collapse]

Corr.: Typo

given it a "name". But these name do not live in some domain
where for example function restriction could be easily defined

[Fritz Feldhase]

On Friday, September 23, 2022 at 2:21:04 AM UTC+2, Mostowski Collapse wrote:

> > In mathematics, the restriction of a function f is a new function, denoted f | A
> > https://en.wikipedia.org/wiki/Restriction_%28mathematics%29
> >
> > But he would prefers to rather become the king of cranks,
> > instead of letting go of all the DC Spoiled nonsense.

Agree. Strange that he is not able to comprehend that his beloved statement:

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y [...] are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X." --Terence Tao, "Analysis I," p. 51

DOES NOT EXCLUDE the following "additional clause":

"For any two functions f : X → Y, g : Z → T: if X =/= Z or Y =/= T, then f =/= g."

Tao MUST have such a (or a semiilar) statement/theorem/axiom/law/definition (whatever) in mind, when declairing:

"f and g are not considered the same function, f =/= g, because they have different domains." -Terence Tao, Analysis I

Actually, it's a trivial implication from the "substitution property of equality" (by an application of contraposition).

[Dan Christensen]

On Thursday, September 22, 2022 at 7:27:19 PM UTC-4, Fritz Feldhase wrote:
> On Friday, September 23, 2022 at 12:54:35 AM UTC+2, Dan Christensen wrote:
> > On Thursday, September 22, 2022 at 6:20:33 PM UTC-4, Fritz Feldhase wrote:
> > > On Thursday, September 22, 2022 at 8:22:10 PM UTC+2, Dan Christensen wrote:
> > > >
> > > > if, as in Tao, only functions with the same domains and codomains are comparable.

[snip the same childish abuse]

> That's NOT what Tao claims

[snip repetitious grasping at straws]

See my previous reply to your identical claim here. What is wrong with you, Fritz? I think I know. Likewise your little buddy here, Jan Burse.

Dan

[Fritz Feldhase]

On Friday, September 23, 2022 at 3:49:26 AM UTC+2, Dan Christensen wrote:

| "if, as in Tao, only functions with the same domains and codomains are comparable."

Nope, you silly crank, that's NOT what Tao claims. Actually, he writes:

"if f : R → R is the function f(x) := x^2, and g := f | [1, 2] is the restriction of f to the interval [1, 2], then f and g both perform
the operation of squaring, i.e., f(x) = x^2 and g(x) = x^2, but the two functions f and g are not considered the same function,

f =/= g, because they have different domains." --Terence Tao, Analysis I

[Dan Christensen]

On Thursday, September 22, 2022 at 11:20:11 PM UTC-4, Fritz Feldhase wrote:
> On Friday, September 23, 2022 at 3:49:26 AM UTC+2, Dan Christensen wrote:
>
> | "if, as in Tao, only functions with the same domains and codomains are comparable."
> Nope, you silly crank, that's NOT what Tao claims. Actually, he writes:
>

Proof by constant repetition a la Donald Trump? How many times now? Scroll up and see my reply the first time you made this claim, Fritz.

Dan

[Fritz Feldhase]

On Friday, September 23, 2022 at 5:43:20 AM UTC+2, Dan Christensen wrote:
> On Thursday, September 22, 2022 at 11:20:11 PM UTC-4, Fritz Feldhase wrote:
> > On Friday, September 23, 2022 at 3:49:26 AM UTC+2, Dan Christensen wrote:
> >
> > | "if, as in Tao, only functions with the same domains and codomains are comparable."
> >
> > Nope, you silly crank, that's NOT what Tao claims. Actually, he writes:

[Fritz Feldhase]

On Friday, September 23, 2022 at 2:56:37 AM UTC+2, Fritz Feldhase wrote:
> On Friday, September 23, 2022 at 2:21:04 AM UTC+2, Mostowski Collapse wrote:
> > >
> > > In mathematics, the restriction of a function f is a new function, denoted f | A
> > > https://en.wikipedia.org/wiki/Restriction_%28mathematics%29
> > >
> > > But he would prefers to rather become the king of cranks,
> > > instead of letting go of all the DC Spoiled nonsense.
> > >
> Agree. Strange that he is not able to comprehend that his beloved statement:
>
> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y [...] are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X." --Terence Tao, "Analysis I," p. 51
>
> DOES NOT EXCLUDE the following "additional clause":
>
> "For any two functions f : X → Y, g : Z → T: if X =/= Z or Y =/= T, then f =/= g."
>

> Tao MUST have such a (or a similar) statement/theorem/axiom/law/definition (whatever) in mind, when declaring:
>
> "f and g are not considered the same function, f =/= g, because they have different domains." --Terence Tao, Analysis I

>
> Actually, it's a trivial implication from the "substitution property of equality" (by an application of contraposition).

Tao [Analysis I, A.7 Equality]:

| "for the purpose of logic we require that equality obeys the following four /axioms of equality/:
|
| (Reflexive axiom). Given any object x, we have x = x. [...]
|
| (Substitution axiom). [...] for any property P(x) depending on x, if x = y, then P(x) and P(y) are equivalent statements."

This substitution axiom implies: f = g -> (dom(f) = dom(f) <-> dom(f) = dom(g)). And hence with dom(f) = dom(f):

f = g -> dom(f) = dom(g).

With contraposition we get:

dom(f) =/= dom(g) -> f =/= g.

THIS theorem allows Tao to state:

[Dan Christensen]

On Friday, September 23, 2022 at 12:31:26 AM UTC-4, Fritz Feldhase wrote:
> On Friday, September 23, 2022 at 2:56:37 AM UTC+2, Fritz Feldhase wrote:
> > On Friday, September 23, 2022 at 2:21:04 AM UTC+2, Mostowski Collapse wrote:
> > > >
> > > > In mathematics, the restriction of a function f is a new function, denoted f | A
> > > > https://en.wikipedia.org/wiki/Restriction_%28mathematics%29
> > > >
> > > > But he would prefers to rather become the king of cranks,
> > > > instead of letting go of all the DC Spoiled nonsense.
> > > >
> > Agree. Strange that he is not able to comprehend that his beloved statement:
> >
> > "Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y [...] are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X." --Terence Tao, "Analysis I," p. 51
> >

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range [codomain] 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.)"

--Terence Tao, "Analysis I," p. 51

This defines the equality of pairs of functions that have the same domain and codomain ("range" here). It defines when they are equal and when they are not. It tells us nothing about pairs of functions with differing domains or codomains. Frtz and Jan here imagine otherwise.

In the notation of DC Proof:

ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod) & Function(f1,dom,cod) & Function(f2,dom,cod)
=> [f1=f2 <=> ALL(a):[a @ dom => f1(a)=f2(a)]]]

Where Function(f,x,y) is equivalent to f: x --> y.

> > DOES NOT EXCLUDE the following "additional clause":
> >
> > "For any two functions f : X → Y, g : Z → T: if X =/= Z or Y =/= T, then f =/= g."

The context:

"One could also restrict the range from R to some smaller subset Y of R, provided of course that all the values of f(x) lie inside Y. For instance, the function f : R → R defined by f(x) := x^2 could also be thought of as a function from R to [0,∞), instead of a function from R to R. Formally, these two functions are different functions, but the distinction between them is so minor that we shall often be CARELESS about the range of a function in our discussion.

"Strictly speaking, there is a distinction between a function f, an its value f(x) at a point x. f is a function; but f(x) is a number (which depends on some free variable x). This distinction is rather subtle and we will not stress it too much, but there are times when one has to distinguish between the two. For instance, if f : R → R is the function f(x) := x2, and g := f | [1,2] is the restriction of f to the interval [1, 2], then f and g both perform the operation of squaring, i.e., f(x) = x^2 and g(x) = x^2, but the two functions f and g are not considered the same function, f =/= g, because they have different domains."
p.218

You are grasping at straws to suggest that this forgivably "careless" and informal discussion somehow overrules the above formal definition equality (p.51). But I guess, it's all you've got, eh, Fritz?

> >
> > Tao MUST have such a (or a similar) statement/theorem/axiom/law/definition (whatever) in mind, when declaring:
> >
> > "f and g are not considered the same function, f =/= g, because they have different domains." --Terence Tao, Analysis I
> >
> > Actually, it's a trivial implication from the "substitution property of equality" (by an application of contraposition).
> Tao [Analysis I, A.7 Equality]:
>
> | "for the purpose of logic we require that equality obeys the following four /axioms of equality/:
> |
> | (Reflexive axiom). Given any object x, we have x = x. [...]
> |
> | (Substitution axiom). [...] for any property P(x) depending on x, if x = y, then P(x) and P(y) are equivalent statements."
>
> This substitution axiom implies: f = g -> (dom(f) = dom(f) <-> dom(f) = dom(g)). And hence with dom(f) = dom(f):
>
> f = g -> dom(f) = dom(g).
>

[snip]

More like: dom(f) = dom(g) & cod(f) = cod(g) => [f=g <=> ALL(a):[a in dom(f) => f(a)=g(a)]]

In any case, nowhere does Tao refer to such domain and codomain operators.

Interestingly, he writes:

"Remark 3.3.6. Strictly speaking, functions are not sets, and sets are not functions; it does not make sense to ask whether an object x is an element of a function f, and it does not make sense to apply a set A to an input x to create an output A(x).[...]"
p.51

Also as implemented in DC Proof. Must be frustrating as hell for you, Fritz!

[Mostowski Collapse]

And why can you not prove:

Here is a challenge that involves "iff" beyond a simple
reading of Terrence Tao. Take these two function spaces:

A = { f : X -> X }
B = { f : Y -> Y }

Can you prove in DC Spoiled this standard theorem:

X =\= Y -> A ∩ B = {}

It works also in the more general case:

A = { f : X -> Z }
B = { f : Y -> T }

We can then also prove:

X =\= Y -> A ∩ B = {}

[Dan Christensen]

On Friday, September 23, 2022 at 7:31:25 PM UTC-4, Mostowski Collapse wrote:
> And why can you not prove:
> Here is a challenge that involves "iff" beyond a simple
> reading of Terrence Tao.

[snip]

You mean involving defining the equality of pairs of functions with different domains or codomains (unlike Tao)? Seems like a waste of time to me, but you can introduce your own definitions/axiom at the beginning of proofs if you like in DC Proof.

[Mostowski Collapse]

You can introduce this axiom:

5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Present(h,x) <=> x ε dom]]
Axiom

It doesn't formalize Terrence Tao, but it formalizes a much more important
mathematician since Galileo and Einstein together, i.e. Dan Christensen.
Namely this definition of Dan Christensen. I even used a Type 1 definition,

the favorite form of definition for the genius Dan Christensen:

Dan Christensen schrieb am Samstag, 1. Oktober 2022 um 20:33:11 UTC+2:
> If we are given only a function f mapping elements of set A to elements
> of set B, nothing can be inferred about f(x) from x not in A. In this case,
> we say that f(x) is UNDEFINED.
https://groups.google.com/g/sci.logic/c/InGcDaFcuKE/m/ZesxKIrSAAAJ

I didn't make UNDEFINED the primitive notion, I made PRESENT the
primitive notion. You could now define, like in your famous
odd even example, where odd was the opposite of even:

ALL(h):ALL(x):[Undefined(h,x) <=> ~Present(h,x)]

So I was using two times idioms of the logic and mathematics
master classes of Dan Christensen, first type 1 definition and then
definition of an opposite. We can use the definition of PRESENT

to prove function inequality, like this:

f =/= g

For f : {0} -> {0} , f(x) = x and g : {0,1} -> {0,1}, g(x) = x.

but I guess using UNDEFINED works also.

[Dan Christensen]

On Saturday, October 1, 2022 at 9:06:46 PM UTC-4, Mostowski Collapse wrote:

>
> Dan Christensen schrieb am Samstag, 1. Oktober 2022 um 20:33:11 UTC+2:
> > If we are given only a function f mapping elements of set A to elements
> > of set B, nothing can be inferred about f(x) from x not in A. In this case,
> > we say that f(x) is UNDEFINED.
> https://groups.google.com/g/sci.logic/c/InGcDaFcuKE/m/ZesxKIrSAAAJ
>
> I didn't make UNDEFINED the primitive notion,

Neither did I. You can think of it as a "meta" term, but it isn't strictly necessary.

> I made PRESENT the
> primitive notion. You could now define, like in your famous
> odd even example, where odd was the opposite of even:
>
> ALL(h):ALL(x):[Undefined(h,x) <=> ~Present(h,x)]
>

Offhand, it doesn't look very useful, but see what you can do with it, Jan Burse.

> So I was using two times idioms of the logic and mathematics
> master classes of Dan Christensen, first type 1 definition and then
> definition of an opposite. We can use the definition of PRESENT
>
> to prove function inequality, like this:
>
> f =/= g
>
> For f : {0} -> {0} , f(x) = x and g : {0,1} -> {0,1}, g(x) = x.
>
> but I guess using UNDEFINED works also.

> Dan Christensen schrieb am Samstag, 24. September 2022 um 17:26:46 UTC+2:
> > On Friday, September 23, 2022 at 7:31:25 PM UTC-4, Mostowski Collapse wrote:
> > > And why can you not prove:
> > > Here is a challenge that involves "iff" beyond a simple
> > > reading of Terrence Tao.
> > [snip]
> >
> > You mean involving defining the equality of pairs of functions with different domains or codomains (unlike Tao)? Seems like a waste of time to me, but you can introduce your own definitions/axiom at the beginning of proofs if you like in DC Proof.

> You can introduce this axiom:
>
> 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Present(h,x) <=> x ε dom]]
> Axiom
>

Here is the full text of the Function Axiom (for one variable) built-into DC Proof:

ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)

=> [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]

& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]

& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod => [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]

=> EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 in dom & b in cod => [fun(a1)=b <=> (a1,b) in gra]]]]]

[Mostowski Collapse]

Yes your function axiom could be helpful, it would deliver
Function(fun,dom,cod). But DC Spoild is obviously incomplete.
We make a further axiom, to define the most important observation

since Galileo and Einstein, namely a definition of UNDEFINED,
rendered by Dan Christensen verbally and informally as follows,
to fill a gap in the axioms that DC Spoild has as menu items:

Dan Christensen schrieb am Samstag, 1. Oktober 2022 um 20:33:11 UTC+2:
> If we are given only a function f mapping elements of set A to elements
> of set B, nothing can be inferred about f(x) from x not in A. In this case,
> we say that f(x) is UNDEFINED.
https://groups.google.com/g/sci.logic/c/InGcDaFcuKE/m/ZesxKIrSAAAJ

So we formally define UNDEFINED as follows, thus leaving no
stone unturned, rendering everything that mathematics used to
say formally, using Type 1 definition (these forms of definition

are in the special liking scope of Dan Christiansen):

5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]]
Axiom

We can then prove as expected:

29 ~f=g
Conclusion, 26

[Dan Christensen]

On Sunday, October 2, 2022 at 5:10:57 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Sonntag, 2. Oktober 2022 um 03:42:44 UTC+2:
> > Here is the full text of the Function Axiom (for one variable) built-into DC Proof:
> > ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
> > => [ALL(a1):ALL(b):[(a1,b) in gra => a1 in dom & b in cod]
> > & ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in gra]]
> > & ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod => [(a1,b1) in gra & (a1,b2) in gra => b1=b2]]
> > => EXIST(fun):[Function(fun,dom,cod) & ALL(a1):ALL(b):[a1 in dom & b in cod => [fun(a1)=b <=> (a1,b) in gra]]]]]

> Yes your function axiom could be helpful, it would deliver

> Function(fun,dom,cod). But DC Proof is obviously incomplete.

> We make a further axiom, to define the most important observation
> since Galileo and Einstein, namely a definition of UNDEFINED,
> rendered by Dan Christensen verbally and informally as follows,

> to fill a gap in the axioms that DC Proof has as menu items:

> Dan Christensen schrieb am Samstag, 1. Oktober 2022 um 20:33:11 UTC+2:
> > If we are given only a function f mapping elements of set A to elements
> > of set B, nothing can be inferred about f(x) from x not in A. In this case,
> > we say that f(x) is UNDEFINED.

That is not a formal definition. Again, if you want to concoct an abbreviation for "Function(f,x,y) & ~z in x" (see Create Axiom Rule), it is easy enough to do in DC Proof, but I have never found a need for such a construct.

> https://groups.google.com/g/sci.logic/c/InGcDaFcuKE/m/ZesxKIrSAAAJ
> So we formally define UNDEFINED as follows, thus leaving no
> stone unturned, rendering everything that mathematics used to
> say formally, using Type 1 definition (these forms of definition
>
> are in the special liking scope of Dan Christiansen):
>
> 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]]
> Axiom
>
> We can then prove as expected:
>
> 29 ~f=g
> Conclusion, 26

Not sure how (or why) you would obtain such nonsensical results, but, if you insist, a more flexible definition of an Undefined predicate/abbreviation might be:

ALL(f):ALL(dom):ALL(cod):ALL(x):[Undefined(f,dom,cod,x) <=> ALL(a):[a in dom => f(a) in cod] & ~x in dom]

I hope this helps.

[Fritz Feldhase]

On Sunday, October 2, 2022 at 6:03:46 PM UTC+2, Dan Christensen wrote:

> > Dan Christensen schrieb am Samstag, 1. Oktober 2022 um 20:33:11 UTC+2:
> > >
> > > If we are given only a function f mapping elements of set A to elements
> > > of set B, nothing can be inferred about f(x) from x not in A. In this case,
> > > we say that f(x) is UNDEFINED.
> > >
> That is not a formal definition.

No one claimed that it is. But it CERTAINLY *is* a definition(sort of), namely of the notion /UNDEFINED/, crank.

The FOLLOWING Is a formalized version of this definition:

> > ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]]
> > Axiom

MC:

> > So we formally define UNDEFINED as [above], thus leaving no

> > stone unturned, rendering everything that mathematics used to
> > say formally, using Type 1 definition (these forms of definition
> > are in the special liking scope of Dan Christiansen):

Indeed!

In any case:

> > We can then prove as expected:
> >
> > 29 ~f=g
> > Conclusion, 26
> >

> Not sure [.] why you would [like to] obtain such [a] results

Because it may serve as a strict justification for Tao's "informal" statement

| "f and g are not considered the same function, f =/= g, because they have different domains."

you silly idiot.

You know, "f =/= g" is just short for "~(f = g)".

[Dan Christensen]

Wrong again, Fritz. As it turns out, the problem with Jan Burse's definition of the "Undefined" predicate would seem to be a couple of missing arguments for the domain and codomain in question.

[Fritz Feldhase]

On Sunday, October 2, 2022 at 8:52:37 PM UTC+2, Dan Christensen wrote:
> >
> > You know, "f =/= g" is just short for "~(f = g)".
> >
> Wrong again, Fritz.

Well...

DC in full crank mode now. :-)

[Mostowski Collapse]

Defining Undefined(f,x) as we did is perfectly fine.
Its the same situation with your definition of f1=f2 here:

1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& Function(f1,dom,cod) & Function(f2,dom,cod)
=> [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
Fn Equality
(From DC Spoiled in dcpsetup17.exe)

You also don't define Eq(f1,f2,dom,cod).
Whats wrong with you? Stop whining.

Nothing has turned out, only the fact that
you are a complete nuthead.

[Dan Christensen]

On Monday, October 3, 2022 at 2:47:42 AM UTC-4, Mostowski Collapse wrote:
> Defining Undefined(f,x) as we did is perfectly fine.

Should be "Undefined(f,dom,cod,x).

If you really think it is necessary, I recommend defining the following abbreviation:

ALL(f):ALL(dom):ALL(cod):ALL(x):[Undefined(f,dom,cod,x) <=> ALL(a):[a in f => f(a) in dom] & ~x in dom]

Where
f = function name
dom = name of domain set
cod = name of codomain set
x = name arbitrary object

For obvious reasons, Jan Burse (aka Mr. Collapse) hopes to make his "Undefined" predicate independent of the domain and range under consideration. His wonky little theorem is unprovable otherwise. Really kind of pathetic.

> Its the same situation with your definition of f1=f2 here:
>
> 1 ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & Function(f1,dom,cod) & Function(f2,dom,cod)
> => [f1=f2 <=> ALL(a):[a ε dom => f1(a)=f2(a)]]]
> Fn Equality

> (From DC Proof in dcpsetup17.exe)
>

As in Terence Tao's definition of function:

"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 [with respect to the domain X], 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.)"

--Terence Tao, "Analysis I," p. 51

(BTW that is not the latest version of DC Proof. See link.)

> You also don't define Eq(f1,f2,dom,cod).

Both of the above definitions can be used to determine whether or not functions are equal ONLY when they have the same domain and codomain. Deal with it, Jan Burse.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com <--- Latest version here

[Fritz Feldhase]

On Monday, October 3, 2022 at 7:03:03 PM UTC+2, Dan Christensen wrote:

> I recommend defining the following abbreviation:
>
> ALL(f):ALL(dom):ALL(cod):ALL(x):[Undefined(f,dom,cod,x) <=> ALL(a):[a in f => f(a) in dom] & ~x in dom]

Did you mean

ALL(f):ALL(dom):ALL(cod):ALL(x):[Undefined(f,dom,cod,x) <=> ALL(a):[a in dom => f(a) in codom] & ~x in dom]

?

[Dan Christensen]

On Monday, October 3, 2022 at 1:03:03 PM UTC-4, Dan Christensen wrote:
> On Monday, October 3, 2022 at 2:47:42 AM UTC-4, Mostowski Collapse wrote:
> > Defining Undefined(f,x) as we did is perfectly fine.
> Should be "Undefined(f,dom,cod,x).
>
> If you really think it is necessary, I recommend defining the following abbreviation:
>
> ALL(f):ALL(dom):ALL(cod):ALL(x):[Undefined(f,dom,cod,x) <=> ALL(a):[a in f => f(a) in dom] & ~x in dom]
>

Should be: ALL(f):ALL(dom):ALL(cod):ALL(x):[Undefined(f,dom,cod,x) <=> ALL(a):[a in dom => f(a) in cod] & ~x in dom]

Thanks, Fritz.

[Mostowski Collapse]

Well I prefer this definition:

ALL(f):ALL(dom):ALL(cod):[Function(f,dom,cod) => [Undefined(f,x) <=> ~x in dom]]

Why would you not use Function(_,_,_). Whats your function axiom
made for? Why replace it with nonsense like ALL(a):[a in dom => f(a) in cod]?
The longer you try to tweak a perfectly fine definition, the longer

it gets more worse. Until it is foobar, fucked up beyond recognition.

[Mostowski Collapse]

Corr.: I think it was this one:

ALL(h):ALL(dom):ALL(cod):[Function(f,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x in dom]]

[Dan Christensen]

On Monday, October 3, 2022 at 6:59:53 PM UTC-4, Mostowski Collapse wrote:
> Corr.: I think it was this one:
>
> ALL(h):ALL(dom):ALL(cod):[Function(f,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x in dom]]
> Mostowski Collapse schrieb am Dienstag, 4. Oktober 2022 um 00:57:37 UTC+2:
> > Well I prefer this definition:
> >
> > ALL(f):ALL(dom):ALL(cod):[Function(f,dom,cod) => [Undefined(f,x) <=> ~x in dom]]
> >

Apart from not giving you the result you so desperately crave, Jan, why do you not accept this simpler abbreviation of Undefined(f,dom,cod,x):

ALL(f):ALL(dom):ALL(cod):ALL(x):[Undefined(f,dom,cod,x) <=> ALL(a):[a in dom => f(a) in cod] & ~x in dom]

Under what circumstances do you imagine it would give you the "wrong" answer to the question as to whether a given function is undefined for some element of its domain?

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com

[Fritz Feldhase]

On Tuesday, October 4, 2022 at 4:42:08 AM UTC+2, Dan Christensen wrote:

> > Mostowski Collapse schrieb am Dienstag, 4. Oktober 2022 um 00:57:37 UTC+2:
> > > Well I prefer this definition:
> > >
> > > ALL(f):ALL(dom):ALL(cod):[Function(f,dom,cod) => [Undefined(f,x) <=> ~x in dom]]

Well, in the context of DC Spoof this might amount to the "axiom":

| ALL(f):ALL(dom):ALL(x):ALL(cod):[Function(f, dom, cod) => [Undefined(f, x) <=> ~x in dom]]

> Jan, why do you not <bla bla bla>

Look, crank: THIS DEFINITION just formalizes the common notion "f is undefined at x".

See: https://www.quora.com/If-a-function-is-in-a-form-undefined-at-x-0-and-can-be-re-written-so-that-this-is-not-true-what-changes-about-the-function
for example.

Actually, it ***could*** be SIMPLIFIED by adopting the usual dom() operation for functions:

| ALL(f):ALL(x):[Function(f) => [Undefined(f, x) <=> ~x in dom(f)]]

Now, PLEASE FUCK OFF FOR GOOD, YOU SILLY CRANK!

[Fritz Feldhase]

On Tuesday, October 4, 2022 at 8:24:11 AM UTC+2, Fritz Feldhase wrote:

> [...]

>
> Actually, it ***could*** be SIMPLIFIED by adopting the usual dom() operation for functions:
>

> | ALL(f):[Function(f) => ALL(x):[Undefined(f, x) <=> ~x in dom(f)]]

You see: A function f is /undefined/ at (some point) x iff x is not in f's domain.

[Fritz Feldhase]

Tao: " we [...] define a decrement function h : N\{0} → N [...].
[Now] h(0) is undefined since 0 is not in the domain N\{0}."

Of course, this is "slightly" unprecise. A better formulation would be: "h is undefined at 0, since 0 is not in h's domain N\{0}." But Tao just use common math lingo to express the very same state of affairs. [Hint: You may try to formalize Tao's claim "h(0) is undefined since 0 is not in the domain N\{0}".]

Tao: "We can take any one of the previous functions f : R → R defined on
all of R, and restrict the domain to a smaller set X ⊆ R, creating a new [!]
function, sometimes called f|X, from X to R. This is the same function
as the original function f, but is only defined on a smaller domain. (Thus
f|X(x) := f(x) when x ∈ X, and f|X(x) is undefined when x !∈ X.)

For instance, we can restrict the function f(x) := x^2, which is initially
defined from R to R, to the interval [1, 2], thus creating a new [!] function
f|[1,2] : [1, 2] → R, which is defined as f|[1,2](x) = x^2 when x ∈ [1, 2] but
is undefined elsewhere."

Hint: Again, this is a rather imprecise formulation...: ".... creating a new [!] function ... This is the same function
as the original function f" --- Huh?! f|[1,2] is a new/different function but the same function [as f]! Well... :-)

Of course, the FUNCTIONs are not the same, but "on X" the course of values of f|[1,2] is the same as the course of values of f.

Hope this helps.

[Ross A. Finlayson]

According to some definitions of well-foundedness, any set with an empty set element
is well-founded, kind of like Frege's "after Russell sank my universe I found it is one".

But, that's for conscientious formalists, who are for that matter
humble fundamentalists.

[Dan Christensen]

On Tuesday, October 4, 2022 at 2:24:11 AM UTC-4, Fritz Feldhase wrote:
> On Tuesday, October 4, 2022 at 4:42:08 AM UTC+2, Dan Christensen wrote:
>
> > > Mostowski Collapse schrieb am Dienstag, 4. Oktober 2022 um 00:57:37 UTC+2:
> > > > Well I prefer this definition:
> > > >
> > > > ALL(f):ALL(dom):ALL(cod):[Function(f,dom,cod) => [Undefined(f,x) <=> ~x in dom]]

> Well, in the context of DC Proof this might amount to the "axiom":

>
> | ALL(f):ALL(dom):ALL(x):ALL(cod):[Function(f, dom, cod) => [Undefined(f, x) <=> ~x in dom]]
>
> >

[snip childish abuse]

> THIS DEFINITION just formalizes the common notion "f is undefined at x".

[snip more childish abuse]

It is often hard to get formal definitions right. In this case, poor Jan Burse seems to have gotten it wrong. He seems to have problems formally defining predicates in general. In this case, you don't really even need one. To indicate a given a function f: X --> Y is undefined for x0, we usually simply write that x0 is not an element of X. I suggest he give this approach a try. He could begin his "proof" as follows:

1. ALL(a):[a in s0 => f(a) in s0]
Axiom

2. ALL(a):[a in s01 => g(a) in s01]
Axiom

3. 1 in s01
Axiom

4. ~1 in s0
Axiom

Line 3 tells us that g is defined at 1. Line 4 tells us that f is UNDEFINED at 1. See how simple? Now, let him try to prove that f=/=g. (Don't hold your breath, folks!)

[Fritz Feldhase]

On Tuesday, October 4, 2022 at 5:48:08 PM UTC+2, Dan Christensen wrote:

> a function f: X --> Y is undefined [at] x0 [iff] x0 is not an element of X

Exactly. Using symbols:

function(f, X, Y) -> undefined(f, x) <-> x !e X.

Though I'd prefer the simpler definition:

function(f) -> undefined(f, x) <-> x !e dom(f).

> 1. ALL(a):[a in s0 => f(a) in s0]
> Axiom
>
> 2. ALL(a):[a in s01 => g(a) in s01]
> Axiom
>
> 3. 1 in s01
> Axiom
>
> 4. ~1 in s0
> Axiom
>

> [...] Line 4 tells us that f is UNDEFINED at 1.

Nope.

Let's consider the functions f: s01 --> s01, f(x) = x, with s01= {0, 1}.

If s0 = {0} (and hence s0 c s01), then for all x e s0: f(x) e s0 (since f(x) = x),
BUT f *is* defined at 1 (since 1 is in the domain of f). Actually, f(1) = 1, by
definition (of f).

You are quite bad at math, dumbo.

Hint: Line 4 tells us that 1 is not in s0. That's all. None of the axioms 1-4 ensures (claims or implies) that 1 is not in f's domain.

[Dan Christensen]

On Tuesday, October 4, 2022 at 12:53:05 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, October 4, 2022 at 5:48:08 PM UTC+2, Dan Christensen wrote:
>
> > a function f: X --> Y is undefined [at] x0 [iff] x0 is not an element of X
>
> Exactly. Using symbols:
>
> function(f, X, Y) -> undefined(f, x) <-> x !e X.
>
> Though I'd prefer the simpler definition:
>
> function(f) -> undefined(f, x) <-> x !e dom(f).
> > 1. ALL(a):[a in s0 => f(a) in s0]
> > Axiom
> >
> > 2. ALL(a):[a in s01 => g(a) in s01]
> > Axiom
> >
> > 3. 1 in s01
> > Axiom
> >
> > 4. ~1 in s0
> > Axiom
> >
> > [...] Line 4 tells us that f is UNDEFINED at 1.
>
> Nope.
>
> Let's consider the functions f: s01 --> s01, f(x) = x, with s01= {0, 1}.
>

[snip]

Now you want add more axioms that will define f(1)? Ummm... OK. But Jan Burse will still have to prove f=/=g.

[Fritz Feldhase]

On Tuesday, October 4, 2022 at 8:06:40 PM UTC+2, Dan Christensen wrote:
> On Tuesday, October 4, 2022 at 12:53:05 PM UTC-4, Fritz Feldhase wrote:
> > On Tuesday, October 4, 2022 at 5:48:08 PM UTC+2, Dan Christensen wrote:
> > >
> > > a function f: X --> Y is undefined [at] x0 [iff] x0 is not an element of X
> > >
> > Exactly. Using symbols:
> >
> > function(f, X, Y) -> undefined(f, x) <-> x !e X.
> >
> > Though I'd prefer the simpler definition:
> >
> > function(f) -> undefined(f, x) <-> x !e dom(f).

Now let's consider your "alternative approach":

> > > 1. ALL(a):[a in s0 => f(a) in s0]
> > > Axiom
> > >
> > > 2. ALL(a):[a in s01 => g(a) in s01]
> > > Axiom
> > >
> > > 3. 1 in s01
> > > Axiom
> > >
> > > 4. ~1 in s0
> > > Axiom
> > >
> > > [...] Line 4 tells us that f is UNDEFINED at 1.
> > >
> > Nope.

Meaning: NO, it DOES NOT.

Hint: [ A short consideration that shows that your claim is wrong: ]

> > Let's consider the functions f: s01 --> s01, f(x) = x, with s01= {0, 1}.
> >

> > If s0 = {0} (and hence s0 c s01), then for all x e s0: f(x) e s0 (since f(x) = x),
> > BUT f *is* defined at 1 (since 1 is in the domain of f). Actually, f(1) = 1, by
> > definition (of f).

==> Line 4 tells us that 1 is not in s0. That's all. None of the axioms 1-4 ensures (claims or implies) that 1 is not in f's domain.

> Now you want add more axioms that <bla>

Huh?! Man, we are talking about YOUR FALSE CLAIM (above), not about things I might or might not want to do.

STAY FOCUSED, dumbo!

[Dan Christensen]

On Tuesday, October 4, 2022 at 3:37:05 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, October 4, 2022 at 8:06:40 PM UTC+2, Dan Christensen wrote:
> > On Tuesday, October 4, 2022 at 12:53:05 PM UTC-4, Fritz Feldhase wrote:
> > > On Tuesday, October 4, 2022 at 5:48:08 PM UTC+2, Dan Christensen wrote:
> > > >
> > > > a function f: X --> Y is undefined [at] x0 [iff] x0 is not an element of X
> > > >
> > > Exactly. Using symbols:
> > >
> > > function(f, X, Y) -> undefined(f, x) <-> x !e X.
> > >
> > > Though I'd prefer the simpler definition:
> > >
> > > function(f) -> undefined(f, x) <-> x !e dom(f).
> Now let's consider your "alternative approach":
> > > > 1. ALL(a):[a in s0 => f(a) in s0]
> > > > Axiom
> > > >
> > > > 2. ALL(a):[a in s01 => g(a) in s01]
> > > > Axiom
> > > >
> > > > 3. 1 in s01
> > > > Axiom
> > > >
> > > > 4. ~1 in s0
> > > > Axiom
> > > >
> > > > [...] Line 4 tells us that f is UNDEFINED at 1.
> > > >
> > > Nope.

> Meaning: NO, it DOES NOT.
>

Base on what was originally given, we could not determine even if there exists a value for f(1), i.e. f(1) was undefined. You effectively added other axioms that would given f(1)=1. So what?

> > > Let's consider the functions f: s01 --> s01, f(x) = x, with s01= {0, 1}.
> > >
> > > If s0 = {0} (and hence s0 c s01), then for all x e s0: f(x) e s0 (since f(x) = x),
> > > BUT f *is* defined at 1 (since 1 is in the domain of f). Actually, f(1) = 1, by
> > > definition (of f).

> ==> Line 4 tells us that 1 is not in s0. That's all.

And s0 was effectively given as the domain of f on line 1. All we were told about s0 is that 1 is not an element of it. We could not even prove the existence, never mind the value of f(1) without your additional axioms.

> None of the axioms 1-4 ensures (claims or implies) that 1 is not in f's domain.
>

> > Now you want add more axioms that will define f(1)? Ummm... OK. But Jan Burse will still have to prove f=/=g.
>

> Huh?! Man, we are talking about YOUR FALSE CLAIM (above), not about things I might or might not want to do.
>

If Jan Burse won't step up to the plate as we say, maybe you can prove f=/=g with or without your additional axioms. How about it, Fritz?

[Fritz Feldhase]

On Tuesday, October 4, 2022 at 10:10:03 PM UTC+2, Dan Christensen wrote:

"1 ALL(a):[a in s0 => f(a) in s0]
Axiom" (DC)

> s0 was [...] given as the domain of f on line 1.

Nonsense.

You really don't know what you are talking about.

EOD

[Dan Christensen]

On Tuesday, October 4, 2022 at 4:26:17 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, October 4, 2022 at 10:10:03 PM UTC+2, Dan Christensen wrote:
>
> "1 ALL(a):[a in s0 => f(a) in s0]
> Axiom" (DC)
>
> > s0 was [...] given as the domain of f on line 1.
>
> Nonsense.
>

Oh, well... I guess I will have to wait for Jan Burse.

Dan

[Fritz Feldhase]

On Tuesday, October 4, 2022 at 11:25:59 PM UTC+2, Dan Christensen wrote:
> On Tuesday, October 4, 2022 at 4:26:17 PM UTC-4, Fritz Feldhase wrote:
> > On Tuesday, October 4, 2022 at 10:10:03 PM UTC+2, Dan Christensen wrote:
> > >
> > > 1 ALL(a):[a in s0 => f(a) in s0]
> > > Axiom" (DC)

> > > ...

> > >
> > > s0 was [...] given as the domain of f on line 1.
> > >
> > Nonsense.
> >
> Oh, well... I guess I will have to wait for Jan Burse.

No, we don't have to wait for anyone, idiot.

Hint:

Consider the function f with a nonempty domain X and codomain X, defined with f(x) = x for all x e X. Then for each and every X' c X: ALL(a):[a in X' => f(a) in X']. Hence we cannot conlude that X' is "the domain of f". (After all, __X__ is the domain of f, and X' may be =/= X).

An example. Consider the function f with domain {0, 1} and codomain {0, 1}, defined with f(x) = 1/x for all x e {0, 1}.
Now let X' = {0}. Then ALL(a):[a in X' => f(a) in X']. But clearly X' = {0} is NOT "the domain of f", since we DEFINED f such that its domain is X = {0, 1} =/= X'.
[Btw. X' = {} will do too! But f's domain is non-empty by definition.]

Hence "ALL(a):[a in s0 => f(a) in s0]" does NOT mean (state, imply, ...) that s0 is "the domain of f".

Get a grip, man!

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 12:17:30 AM UTC+2, Fritz Feldhase wrote:

> An example. Consider the function f with domain {0, 1} and codomain {0, 1}, defined with f(x) = 1/x for all x e {0, 1}.
> Now let X' = {0}. Then ALL(a):[a in X' => f(a) in X']. But clearly X' = {0} is NOT "the domain of f", since we DEFINED f such that its domain is X = {0, 1} =/= X'.

Hint: X' = {0} is the domain of f|{0}, the restriction of f to {0}.

Tao: "We can take any one of the previous functions f : R → R defined on
all of R, and restrict the domain to a smaller set X ⊆ R, creating a new [!]

function, sometimes called f|X, from X to R. This [function] is [ similar to the ]
original function f, but is [...] defined on a smaller domain. (Thus
f|X(x) := f(x) when x ∈ X, [but] f|X [.] is undefined [at x] when x !∈ X.)

[Dan Christensen]

On Tuesday, October 4, 2022 at 6:30:02 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, October 5, 2022 at 12:17:30 AM UTC+2, Fritz Feldhase wrote:
>
> > An example. Consider the function f with domain {0, 1} and codomain {0, 1}, defined with f(x) = 1/x for all x e {0, 1}.
> > Now let X' = {0}. Then ALL(a):[a in X' => f(a) in X']. But clearly X' = {0} is NOT "the domain of f", since we DEFINED f such that its domain is X = {0, 1} =/= X'.

[snip]

You are introducing additional axioms. Try to avoid that and just complete Jan Burse's "proof" that f=/=g.

Given:

1. ALL(a):[a in s0 => f(a) in s0]
Axiom

2. ALL(a):[a in s01 => g(a) in s01]
Axiom

3. 1 in s01
Axiom

4. ~1 in s0
Axiom

Prove (without additional axioms):

~[f=g]

If you can't do that, just say so, Fritz.

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 2:17:50 AM UTC+2, Dan Christensen wrote:
> On Tuesday, October 4, 2022 at 6:30:02 PM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, October 5, 2022 at 12:17:30 AM UTC+2, Fritz Feldhase wrote:
> > >
> > > An example. Consider the function f with domain {0, 1} and codomain {0, 1}, defined with f(x) = 1/x for all x e {0, 1}.
> > > Now let X' = {0}. Then ALL(a):[a in X' => f(a) in X']. But clearly X' = {0} is NOT "the domain of f", since we DEFINED f such that its domain is X = {0, 1} =/= X'.
> > >

> You are introducing additional axioms.

No, I am considering a countermodel, dumbo.

Please try to learn the basics befor talking with grown-ups.

See: https://math.stackexchange.com/questions/4528176/understanding-a-countermodel-to-%e2%88%80x%e2%88%83yaxy%e2%86%92%e2%88%83y%e2%88%80xaxy

So here's a specific countermodel:

> > An example. Consider the function f with domain {0, 1} and codomain {0, 1}, defined with f(x) = 1/x for all x e {0, 1}.
> > Now let X' = {0}. Then ALL(a):[a in X' => f(a) in X']. But clearly X' = {0} is NOT "the domain of f", since we DEFINED f such that its domain is X = {0, 1} =/= X'.

> > [Btw. X' = {} will do too! But f's domain is non-empty by definition.]
> >

> > Hence "ALL(a):[a in s0 => f(a) in s0]" does NOT mean (state, imply, ...) that s0 is "the domain of f".

Now you are changing the topic. A common crank maneuvre. Ok, noted.

> ...complete Jan Burse's "proof" that <bla>

Why should I "complete" a proof which is just fine, dumbo?

Hint: I've postet a related proof (and a general proof idea) myself. So eat shit, asshole.

EOD

[Dan Christensen]

On Tuesday, October 4, 2022 at 8:57:52 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, October 5, 2022 at 2:17:50 AM UTC+2, Dan Christensen wrote:
> > On Tuesday, October 4, 2022 at 6:30:02 PM UTC-4, Fritz Feldhase wrote:
> > > On Wednesday, October 5, 2022 at 12:17:30 AM UTC+2, Fritz Feldhase wrote:
> > > >
> > > > An example. Consider the function f with domain {0, 1} and codomain {0, 1}, defined with f(x) = 1/x for all x e {0, 1}.
> > > > Now let X' = {0}. Then ALL(a):[a in X' => f(a) in X']. But clearly X' = {0} is NOT "the domain of f", since we DEFINED f such that its domain is X = {0, 1} =/= X'.
> > > >
> > You are introducing additional axioms.

> No, I am considering a countermodel...

You should be considering a way to patch up Jan Burse's proof. Something along the lines of:

1. ALL(a):[a in s0 => f(a) in s0]
Axiom

2. ALL(a):[a in s01 => g(a) in s01]
Axiom

3. 1 in s01
Axiom

4. ~1 in s0
Axiom

5. ALL(a):[a in s0 => f(a) in s0] & ~1 in s0 <--- f is undefined at 1
Join, 1, 4

6. ALL(a):[a in s01 => g(a) in s01] & 1 in s01 <--- g is defined at 1
Join, 2, 3

7. f=g
Premise

8. ALL(a):[a in s01 => f(a) in s01] & 1 in s01
Substitute, 7, 6

9. ALL(a):[a in s0 => f(a) in s0] & ~1 in s0
& [ALL(a):[a in s01 => f(a) in s01] & 1 in s01]
Join, 5, 8

10. f=g
=> ALL(a):[a in s0 => f(a) in s0] & ~1 in s0
& [ALL(a):[a in s01 => f(a) in s01] & 1 in s01] <--- Oooooops! Domain and codomain don't match. No contradiction.
Conclusion, 7

Of course, this proof didn't work either, but maybe it will give you or Jan Burse some ideas as to how to proceed. (Hee, hee!)

[Mostowski Collapse]

Ever wondered why Russel appears on a picture for
the Drinker Paradox? Me too.
http://www.dcproof.com/DrinkersParadox.html

It was popularised by the mathematical logician Raymond
Smullyan, who called it the "drinking principle" in his 1978
book What Is the Name of this Book?
https://en.wikipedia.org/wiki/Drinker_paradox

But I guess we cannot use DC Spookies function axiom
to prove, because its only for same domain and codomain:

Raymond Smullyan =\= Bertrand Russell

[Mostowski Collapse]

According to Wikipedia the Barber paradox is a loaded question:

"The question is a loaded question that assumes
the existence of the barber, which is false.
A loaded question is a form of complex question
that contains a controversial assumption"
https://en.wikipedia.org/wiki/Barber_paradox
https://en.wikipedia.org/wiki/Loaded_question

What premise are you talking about? The Barber paradox
is completely solved by not using any premise:

/* With non-empty domain assumption, FOL proof */
¬∃x∀y(Sxy ↔ ¬Syy) is valid.
https://www.umsu.de/trees/#~3~7x~6y(Sxy~4~3Syy)

/* Without non-empty domain assumption, FOL proof */
¬∃x(Dx ∧ ∀y(Dx → (Sxy ↔ ¬Syy))) is valid.
https://www.umsu.de/trees/#~3~7x(Dx~1~6y(Dx~5(Sxy~4~3Syy)))

No barber! Sorry.