How difficult is contraposition for DC Proof and Dan Christensen?

330 views

Mostowski Collapse

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

Mostowski Collapse

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!
Message has been deleted
Message has been deleted

Dan Christensen

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:

1. A => B
Premise

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

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

I hope this helps.

Dan

Visit my Math Blog at http://www.dcproof.wordpress.com

Mostowski Collapse

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)

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

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
Message has been deleted

Dan Christensen

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

Fritz Feldhase

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)
> >
> >
> > (~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

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)
> > >
> > >
> > > (~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

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.

Fritz Feldhase

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

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

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.

> 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

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

Mostowski Collapse

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

Dan Christensen

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.

> {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.
Message has been deleted

Dan Christensen

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

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

Sep 8, 2022, 1:01:50 AMSep 8
to
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

Sep 8, 2022, 1:07:02 AMSep 8
to
Peter Aczel is 80 years old. Hope this helps.

Fritz Feldhase

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.

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

Can write this in DC Spoof?

Dan Christensen

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

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

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:

Mostowski Collapse

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:

Mostowski Collapse

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:

Jeff Barnett

Sep 8, 2022, 1:29:07 PMSep 8
to
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

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

Mostowski Collapse

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!

Mostowski Collapse

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.

Dan Christensen

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.

> 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

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

Mostowski Collapse

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

Dan Christensen

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.

Dan Christensen

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.

Mostowski Collapse

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?

Dan Christensen

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.

Fritz Feldhase

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:

"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

Sep 10, 2022, 1:59:15 AMSep 10
to
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

Sep 10, 2022, 9:49:14 AMSep 10
to
In this case, the usual definition of function equality is not applicable. The truth value of f=g remains indeterminate.

Dan Christensen

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.

Fritz Feldhase

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.

Fritz Feldhase

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.

Fritz Feldhase

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

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

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

Fritz Feldhase

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.

Fritz Feldhase

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.

Mostowski Collapse

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

Dan Christensen

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

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