330 views

Skip to first unread message

Sep 6, 2022, 11:41:02 PMSep 6

to

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

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

Sep 6, 2022, 11:45:22 PMSep 6

to

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!

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!

Message has been deleted

Message has been deleted

Sep 7, 2022, 12:32:30 AMSep 7

to

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:
> Contraposition is a quite handy rule, in classical

> logic the following are interchangeable:

>

> A => B

> ----------------

> ~B => ~A

>

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

Sep 7, 2022, 12:02:57 PMSep 7

to

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

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

Sep 7, 2022, 12:10:28 PMSep 7

to

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

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

Message has been deleted

Sep 7, 2022, 12:53:13 PMSep 7

to

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.
> 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)

>

[snip text already addressed here]

Sep 7, 2022, 1:44:09 PMSep 7

to

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 [...]
> 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)

> >

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

"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

Sep 7, 2022, 2:12:12 PMSep 7

to

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]
> 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_.

>

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.)

Sep 7, 2022, 3:37:10 PMSep 7

to

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.

(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.

Sep 7, 2022, 5:21:33 PMSep 7

to

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_.
>

> There seems to be a sever gap in DC Proof, which has consequences for function spaces.

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

"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.

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!
--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]

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

Sep 7, 2022, 5:54:09 PMSep 7

to

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.
> 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:

> (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.

Sep 7, 2022, 7:12:36 PMSep 7

to

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

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

Sep 7, 2022, 8:00:09 PMSep 7

to

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

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

Sep 7, 2022, 9:38:46 PMSep 7

to

> 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.
> 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.

> So what is the answer to this question:

>

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

>

Message has been deleted

Sep 7, 2022, 10:22:19 PMSep 7

to

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):
> Pitty DC Proof cannot prove:

>

> Proposition: 4.2.5 If A is a set and F : A -> B then F is a set.

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]]]]

Sep 8, 2022, 1:01:50 AMSep 8

to

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

Sep 8, 2022, 1:07:02 AMSep 8

to

Sep 8, 2022, 1:14:17 AMSep 8

to

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.
>

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

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

Can write this in DC Spoof?

Sep 8, 2022, 1:18:54 AMSep 8

to

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
> 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]]]]

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
& 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]]]]

Sep 8, 2022, 11:52:14 AMSep 8

to

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:

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:

Sep 8, 2022, 11:56:45 AMSep 8

to

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."

Bye

Mostowski Collapse schrieb:

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."

Bye

Mostowski Collapse schrieb:

Sep 8, 2022, 12:05:40 PMSep 8

to

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:

**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:

Sep 8, 2022, 1:29:07 PMSep 8

to

Peter. I was guessing they were related and asking what the relation was.

--

Jeff Barnett

Sep 8, 2022, 2:31:30 PMSep 8

to

Sep 8, 2022, 4:47:43 PMSep 8

to

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!

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!

Sep 8, 2022, 4:57:43 PMSep 8

to

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.

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.

Sep 8, 2022, 10:23:34 PMSep 8

to

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.

> 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]
>

> **product** function space

>

> A -> B = pi_A B

>

> with function space generis, which is

> just a set of functions.

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?

Sep 9, 2022, 10:25:23 AMSep 9

to

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

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

>

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

Sep 9, 2022, 2:38:51 PMSep 9

to

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

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

Sep 9, 2022, 5:57:05 PMSep 9

to

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.

[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

>

Sep 9, 2022, 6:07:52 PMSep 9

to

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.
> 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.

>

Sep 9, 2022, 7:54:02 PMSep 9

to

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?
> > Take f1 : {0} -> {0}, f1(0)=0, f1(1)=1,

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

Sep 9, 2022, 10:52:57 PMSep 9

to

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.
> 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

Sep 10, 2022, 1:37:34 AMSep 10

to

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:
>

> I can use the same substition trick to derive an inequality,

> by using the contrapositive of "The indiscernibility of identicals":

>

> f1 =\= f2

"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.

Sep 10, 2022, 1:59:15 AMSep 10

to

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

>

> 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, ...)?

> 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_.
> >

> > There seems to be a sever gap in DC Proof, which has consequences for function spaces.

> >

>

> 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, ...)?

Sep 10, 2022, 9:49:14 AMSep 10

to

Sep 10, 2022, 10:03:07 AMSep 10

to

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.

[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

>

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.

Sep 10, 2022, 11:38:26 AMSep 10

to

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

> The <bla>

Shut up, crank.

> The <bla>

Shut up, crank.

Sep 10, 2022, 11:38:52 AMSep 10

to

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

>

> In this case

Shut up, crank.

>

> In this case

Shut up, crank.

Sep 10, 2022, 1:39:37 PMSep 10

to

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.
> This definition is built-into DC Proof on the Sets menu

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?

Sep 10, 2022, 2:45:04 PMSep 10

to

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} ->

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} ->

Sep 10, 2022, 2:53:48 PMSep 10

to

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.

> Dan Christensen halucinated ...

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

Sep 10, 2022, 3:00:47 PMSep 10

to

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.

Sep 22, 2022, 12:53:30 PMSep 22

to

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

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

Sep 22, 2022, 2:22:10 PMSep 22

to

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:
> 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 }

>

>

> 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.
> X =\= Y -> A ∩ B = {}

>

Sep 22, 2022, 6:20:33 PMSep 22

to

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, as in Tao, only functions with the same domains and codomains are comparable.

"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?

Sep 22, 2022, 6:54:35 PMSep 22