New Version of DC Proof with expanded tutorial

387 views
Skip to first unread message

Dan Christensen

unread,
Sep 23, 2022, 6:18:10 PMSep 23
to
Expanded tutorial includes exercises to develop the truth table for the IMPLIES-operator, now a hot topic on various math forums. Each of these 4 definitive proofs (IMHO) is very simple, being no more than 9 lines each (see exercises 1.3, 1.4, 3.4 and 3.5). Ideal for the beginner.

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

unread,
Sep 23, 2022, 7:25:09 PMSep 23
to
As hot as a frozen mamut in the nord pole. LoL

Why is DC Spoiled not able to work with cardinality?

It has an easy definition:

|A| = |B| <=> EXIST(f): f : A -> B, f bijective

Dan Christensen

unread,
Sep 23, 2022, 8:37:57 PMSep 23
to


> Dan Christensen schrieb am Samstag, 24. September 2022 um 00:18:10 UTC+2:
> > Expanded tutorial includes exercises to develop the truth table for the IMPLIES-operator, now a hot topic on various math forums. Each of these 4 definitive proofs (IMHO) is very simple, being no more than 9 lines each (see exercises 1.3, 1.4, 3.4 and 3.5). Ideal for the beginner.
> >

On Friday, September 23, 2022 at 7:25:09 PM UTC-4, Mostowski Collapse wrote:
> As hot as a frozen mamut in the nord pole. LoL
>
> Why is DC Proof not able to work with cardinality?
>

That has not been established.

> It has an easy definition:
>
> |A| = |B| <=> EXIST(f): f : A -> B, f bijective

You also have to establish the trichotomy rule for |A| < |B|. Give it a try, Jan Burse. Can you even do it in ZFC?

Jeff Barnett

unread,
Sep 24, 2022, 12:18:39 AMSep 24
to
On 9/23/2022 6:37 PM, Dan Christensen wrote:
>
>
>> Dan Christensen schrieb am Samstag, 24. September 2022 um 00:18:10 UTC+2:
>>> Expanded tutorial includes exercises to develop the truth table for the IMPLIES-operator, now a hot topic on various math forums. Each of these 4 definitive proofs (IMHO) is very simple, being no more than 9 lines each (see exercises 1.3, 1.4, 3.4 and 3.5). Ideal for the beginner.
>>>
>
> On Friday, September 23, 2022 at 7:25:09 PM UTC-4, Mostowski Collapse wrote:
>> As hot as a frozen mamut in the nord pole. LoL
>>
>> Why is DC Proof not able to work with cardinality?
>>
>
> That has not been established.
>
>> It has an easy definition:
>>
>> |A| = |B| <=> EXIST(f): f : A -> B, f bijective
>
> You also have to establish the trichotomy rule for |A| < |B|. Give it a try, Jan Burse. Can you even do it in ZFC?
As long as you are passing out assignments, why don't you try to show
that ZF with trichotomy (as an axiom) is just ZFC? It would be very
impressive if your toy could do that!
--
Jeff Barnett


Fritz Feldhase

unread,
Sep 24, 2022, 12:23:58 AMSep 24
to
On Saturday, September 24, 2022 at 2:37:57 AM UTC+2, Dan Christensen wrote:

> Can you even do it in ZFC?

Yes, we can, dumbo.

Dan Christensen

unread,
Sep 24, 2022, 1:24:22 AMSep 24
to
A related result is apparently the Cantor Bernstein Schroeder Theorem: http://dcproof.com/CBS.htm (Several thousand lines of formal proof.) No "toy" could pull that off.

Dan Christensen

unread,
Sep 24, 2022, 1:31:01 AMSep 24
to
[snip childish abuse]

Let's see your formal proof, Fritz. Sets only. No proper classes.

Mostowski Collapse

unread,
Sep 24, 2022, 4:54:59 AMSep 24
to
Hi,

Why would you need classes for cardinality?
The typical text book approach bootstraps
cardinality from ordinals. You then don't

need to make a class equivalence class.
Please read this:

Basic Set Theory
Azriel Levy - 13. August 2002
https://www.amazon.com/dp/0486420795

It says "Basic", LoL.
Its very easy you define:

|A| := k <=> smallest of your ordinals k,
such that there is bijection A -> k.

your ordinal k <=> for example von Neuman ordinals
x is a transitive set totally
ordered by set inclusion,

Trichotomy of cardinals follows from
trichotomy of ordinals.

Bye

Dan Christensen schrieb:

Mostowski Collapse

unread,
Sep 24, 2022, 5:04:30 AMSep 24
to
Here are some exercises:

1. Show that ⋃S⊆S is an equivalent definition of transitivity.
2. Show that x∈S⟹x⊆S is an equivalent definition of transitivity.
3. Prove that if S is a transitive set, then ⋃(S+)=S.
4. Prove that if a+=b+, then a=b.
5. Prove that every natural number is a transitive set.
6. Prove that N is a transitive set.

Can you do them with DC Spoild? I doubt, it
even doesn't have the pairing axiom. So how
would one define S+ ?

LMAO!

Remark: Nr. 4 Resembles some of the Peano Axiom
for successor. You can find more of such
analogy. Nr. 5 and Nr. 6 needs to read natural

number and set of natural numbers as corresponding
ordinals and set of ordinals.

Mostowski Collapse schrieb:

Dan Christensen

unread,
Sep 24, 2022, 11:06:58 AMSep 24
to
On Saturday, September 24, 2022 at 4:54:59 AM UTC-4, Mostowski Collapse wrote:
> Hi,
>
> Why would you need classes for cardinality?
> The typical text book approach bootstraps
> cardinality from ordinals. You then don't
>
> need to make a class equivalence class.
> Please read this:
>
> Basic Set Theory
> Azriel Levy - 13. August 2002
> https://www.amazon.com/dp/0486420795
>
> It says "Basic", LoL.
> Its very easy you define:
>
> |A| := k <=> smallest of your ordinals k,
> such that there is bijection A -> k.
>
> your ordinal k <=> for example von Neuman ordinals
> x is a transitive set totally
> ordered by set inclusion,
>
> Trichotomy of cardinals follows from
> trichotomy of ordinals.
>

Still waiting for formal proofs and definitions of the above starting from the axioms of set theory.

Fritz Feldhase

unread,
Sep 25, 2022, 12:01:35 AMSep 25
to
On Saturday, September 24, 2022 at 5:06:58 PM UTC+2, Dan Christensen wrote:

> Still waiting for [...] proofs and definitions of the above starting from the axioms of set theory.

Read a (any) set theory textbook, you silly idiot.

Dan Christensen

unread,
Sep 25, 2022, 12:35:45 AMSep 25
to
[snip childish abuse]

Sorry, but plowing through a book on ZFC set theory that sounds like a real waste of time. If I want to formalize the cardinalities of arbitrary sets, I guess I will have to do it myself -- not a priority for me. Thanks anyway.

Fritz Feldhase

unread,
Sep 25, 2022, 11:37:54 AMSep 25
to
On Sunday, September 25, 2022 at 6:35:45 AM UTC+2, Dan Christensen wrote:

> Sorry, but plowing through a book on ZFC set theory that sounds like a real waste of time.

Yeah, in your case that's for sure.

Jim Burns

unread,
Sep 25, 2022, 12:09:01 PMSep 25
to
On 9/25/2022 12:35 AM, Dan Christensen wrote:

> Sorry, but plowing through a book on ZFC set theory
> that sounds like a real waste of time.
> If I want to formalize the cardinalities of
> arbitrary sets, I guess I will have to do it myself

Bizarre.

| Driven by hunger, a fox tried to reach some grapes
| hanging high on the vine but was unable to, although
| he leaped with all his strength. As he went away,
| the fox remarked 'Oh, you aren't even ripe yet!
| I don't need any sour grapes.' People who speak
| disparagingly of things that they cannot attain
| would do well to apply this story to themselves.[4]
|
https://en.wikipedia.org/wiki/The_Fox_and_the_Grapes




Mostowski Collapse

unread,
Sep 25, 2022, 4:40:12 PMSep 25
to
If you have problems reading books, feel free to ask
us. The cardinals as ordinals approach needs a lot
of work. If I am not totally mistaken, the rank of

a set helps. So you can use your subset axiom:

|A| = ∩ { k =< rank(A) }

but using the internet, and not the book, I found
two different definitions of rank. So I am not
sure whether its ok.

Maybe should comsult the book agains. Books
have the advantage that they are more coherent
than bits and pieces from the internet.

Mostowski Collapse

unread,
Sep 25, 2022, 4:42:59 PMSep 25
to
Corr:

|A| = ∩ { k =< rank(A) | exists f : A -> k, f bijection }

Fritz Feldhase

unread,
Sep 25, 2022, 7:39:53 PMSep 25
to
On Sunday, September 25, 2022 at 10:40:12 PM UTC+2, Mostowski Collapse wrote:

> If you have problems reading books, feel free to ask
> us. The cardinals as ordinals approach needs a lot
> of work.

Indeed. But if we restrict our considerations to finite cardinals things ar quite simple.

Let's assume that we have defined IN, the set of natural numbers. [IN = {0, 1, 2, 3, ...}]

Then we may define (for any set A):

finite(A) :<-> En e IN: A ~ {k e IN: k < n}

Now we may define |.| ("the number of elements in .") for finite sets:

finite(A) -> (|A| = n <-> A ~ {k e IN: k < n})

Hence we get, for example:

|{a}| = n <-> A ~ {k e IN: k < n})

(since {a} is finite).

Moreover:

{a} ~ {0} = {k e IN: k < 1}).

Hence

|{a}| = 1.

"The number of elements in {a} is 1."

This allows to prove the theorem:

A = {0, 1} -> (|{f | f: A x A --> A}| = 2^4)

[with 1 = s(0), 2 = s(1), 3 = s(2) and 4 = s(3) and the usual definition of ^, etc.]

Dan Christensen

unread,
Sep 28, 2022, 2:47:31 PMSep 28
to
On Sunday, September 25, 2022 at 4:40:12 PM UTC-4, Mostowski Collapse wrote:
> If you have problems reading books, feel free to ask
> us.

[snip]

Strange as it may sound, the problem with books by set theorists is that their approach to set theory is not widely used in math textbooks. A proof checker based ZFC, though it might useful for the specialist, to my target audience it would be quite useless.

Mostowski Collapse

unread,
Sep 29, 2022, 8:43:21 AMSep 29
to
You are fake news!
Message has been deleted

Dan Christensen

unread,
Oct 1, 2022, 2:33:11 PMOct 1
to
On Thursday, September 29, 2022 at 8:43:21 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 28. September 2022 um 20:47:31 UTC+2:
> > On Sunday, September 25, 2022 at 4:40:12 PM UTC-4, Mostowski Collapse wrote:
> > > If you have problems reading books, feel free to ask
> > > us.
> > [snip]
> >
> > Strange as it may sound, the problem with books by set theorists is that their approach to set theory is not widely used in math textbooks. A proof checker based ZFC, though it might useful for the specialist, to my target audience it would be quite useless.

> You are fake news!

Still in denial, I see.

In math textbooks, for example, 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. Sorry, none of your "dark elements" are allowed, Jan Burse. Must be frustrating as hell.

Mostowski Collapse

unread,
Oct 1, 2022, 5:39:58 PMOct 1
to
Can you show us such a mathbook? And then compare with
your DC Spoiled. Why can you not show:

f =/= g

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

LoL

P.S.: Here is an easy proof to show f =/= g, using the
values f(x) and g(x) for x=1.

Proof: Assume to the contrary that f=g, then f(x) and g(x)
would be absent at the same x or present at the same x,
for all x.

But for for x=1 we have x not in {0}, i.e. not in the domain,
therefor f(x) absent and since x in {0,1}, g(x) present,
a contradiction, therefore f=\=g.

Q.E.D.

P.P.S.: Homework: Define absent/present.

Dan Christensen

unread,
Oct 1, 2022, 8:18:31 PMOct 1
to
On Saturday, October 1, 2022 at 5:39:58 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Samstag, 1. Oktober 2022 um 20:33:11 UTC+2:
> > On Thursday, September 29, 2022 at 8:43:21 AM UTC-4, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Mittwoch, 28. September 2022 um 20:47:31 UTC+2:
> > > > On Sunday, September 25, 2022 at 4:40:12 PM UTC-4, Mostowski Collapse wrote:
> > > > > If you have problems reading books, feel free to ask
> > > > > us.
> > > > [snip]
> > > >
> > > > Strange as it may sound, the problem with books by set theorists is that their approach to set theory is not widely used in math textbooks. A proof checker based ZFC, though it might useful for the specialist, to my target audience it would be quite useless.
> > > You are fake news!
> >
> > Still in denial, I see.
> >
> > In math textbooks, for example, 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. Sorry, none of your "dark elements" are allowed, Jan Burse. Must be frustrating as hell.

> Can you show us such a mathbook?

Terence Tao's best-selling "Analysis I." Read it and weep.

"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y , such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
--Terence Tao, "Analysis I," p. 49

If x not in X, then f(x) is undefined. Deal with it, Jan Burse.

> And then compare with
> your DC Proof. Why can you not show:
>
> f =/= g
>
> For f : {0} -> {0} , f(x) = x and g : {0,1} -> {0,1}, g(x) = x.
>

Since f and g have different domain, in math textbooks (if not in philosophy books) we usually then say that their equality is indeterminate.

Also from Tao:

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

> LoL

It's good that you can laugh at yourself, Jan Burse.

>
> P.S.: Here is an easy proof to show f =/= g, using the
> values f(x) and g(x) for x=1.
>
> Proof: Assume to the contrary that f=g, then f(x) and g(x)
> would be absent at the same x or present at the same x,
> for all x.
>

Now try to apply the actual definition of function equality above. Once you have established that their domains are different, there is nothing more to say about their equality. Deal with it.

You could, of course, introduce these "dark elements" of yours if you like. You could even do it in DC Proof if you are determined to do so. You would then have to be careful not use the usual definitions as well.

> But for for x=1 we have x not in {0}, i.e. not in the domain,
> therefor f(x) absent and since x in {0,1}, g(x) present,
> a contradiction, therefore f=\=g.
>

You must be using a different definition. I guess there is nothing wrong with that except that most mathematicians would be left wondering why you would bother.

Mostowski Collapse

unread,
Oct 1, 2022, 8:41:18 PMOct 1
to
undefined or absent, doesn't matter how you call it.
It just leads to the following fact:

f =/= g

For f : {0} -> {0} , f(x) = x and g : {0,1} -> {0,1}, g(x) = x.
Do you want me to show you a proof in DC Spoiled?
Message has been deleted

Mostowski Collapse

unread,
Oct 1, 2022, 8:53:10 PMOct 1
to
Ok here is a proof in DC Spoiled, of the fact:

29 ~f=g
Conclusion, 26

---------------------------------------- begin proof ----------------------------------------

1 Function(f,s0,s0)
Axiom

2 Function(g,s01,s01)
Axiom

3 1 ε s01
Axiom

4 ~1 ε s0
Axiom

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

6 ALL(dom):ALL(cod):[Function(f,dom,cod) => ALL(x):[Present(f,x) <=> x ε dom]]
U Spec, 5

7 ALL(cod):[Function(f,s0,cod) => ALL(x):[Present(f,x) <=> x ε s0]]
U Spec, 6

8 Function(f,s0,s0) => ALL(x):[Present(f,x) <=> x ε s0]
U Spec, 7

9 ALL(x):[Present(f,x) <=> x ε s0]
Detach, 8, 1

10 ALL(dom):ALL(cod):[Function(g,dom,cod) => ALL(x):[Present(g,x) <=> x ε dom]]
U Spec, 5

11 ALL(cod):[Function(g,s01,cod) => ALL(x):[Present(g,x) <=> x ε s01]]
U Spec, 10

12 Function(g,s01,s01) => ALL(x):[Present(g,x) <=> x ε s01]
U Spec, 11

13 ALL(x):[Present(g,x) <=> x ε s01]
Detach, 12, 2

14 Present(f,1) <=> 1 ε s0
U Spec, 9

15 Present(g,1) <=> 1 ε s01
U Spec, 13

16 [Present(f,1) => 1 ε s0] & [1 ε s0 => Present(f,1)]
Iff-And, 14

17 Present(f,1) => 1 ε s0
Split, 16

18 1 ε s0 => Present(f,1)
Split, 16

19 ~1 ε s0 => ~Present(f,1)
Contra, 17

20 ~Present(f,1)
Detach, 19, 4

21 Present(g,1) <=> 1 ε s01
U Spec, 13

22 [Present(g,1) => 1 ε s01] & [1 ε s01 => Present(g,1)]
Iff-And, 21

23 Present(g,1) => 1 ε s01
Split, 22

24 1 ε s01 => Present(g,1)
Split, 22

25 Present(g,1)
Detach, 24, 3

26 f=g
Premise

27 ~Present(g,1)
Substitute, 26, 20

28 Present(g,1) & ~Present(g,1)
Join, 25, 27

29 ~f=g
Conclusion, 26

---------------------------------------- end proof ----------------------------------------

Fritz Feldhase

unread,
Oct 1, 2022, 9:11:33 PMOct 1
to
On Sunday, October 2, 2022 at 2:18:31 AM UTC+2, Dan Christensen wrote:

> Since f and g have different domain, in math textbooks [...] we usually then say that their equality is indeterminate.

No, "we" don't say that, you silly asshole full of shit!

Especially, Tao doesn't say that. ACTUALLY, HE says:

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

GOT THAT, YOU LYING ASSHOLE?!

HAU AB, DU DUMME SAU!

Mostowski Collapse

unread,
Oct 1, 2022, 9:21:02 PMOct 1
to
Lets take him for granted, when he says:
> If x not in X, then f(x) is undefined.

He still thinks I oppose to that. But to the best of my
knowledge if x is not in X, and f ⊆ X x Y, then
there is no pair (x,y) e f for some y e Y.

Its already enough that the first coordinate is
outside of X, to that there is no pair. So we can in
set theory, indeed say, if x not in X, then f(x) is

undefined. And vice versa. What are the
consequences for equality based on the fact
that DC Proof has subsitution?

LoL

Fritz Feldhase

unread,
Oct 1, 2022, 9:25:07 PMOct 1
to
On Sunday, October 2, 2022 at 2:41:18 AM UTC+2, Mostowski Collapse wrote:

> undefined or absent, doesn't matter how you call it.

Actually, we may define:

undefined(f, x) :<-> x !e dom(f) [or undefined(f, x) :<-> ~Ey((x, y) e f)
"f is undefined at x".

Though in a set-theoreritic context this (usually) does not mean that "f_0(x_0)" is a non-denoting term, if x_0 !e dom(f_0).

Actually, "f_0(x_0)" may denote a certain "default" set, say, the empty set in this case.

Yes, there's a DIFFERENCE between the usual non-formal ("informal") approach in the context of a, say, analysis textbooks and a strictly formal approach.

Since DC Spoof pretends to be a formal system it should adhere to the "higher standard", I'd say.

Mostowski Collapse

unread,
Oct 1, 2022, 9:25:41 PMOct 1
to
The more general consequences are, that we can show:

f =\= g

In case f : dom1 -> cod1, g : dom2 -> cod2 and
dom1 =\= dom2. Which is already the half part of
function in-equality, namely this here from Terrence Tao:

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

The other part cod1 =\= cod2 could be also furnished
I guess by something "WE SAY IN MATHEMATICS"
cast into a definition.

Fritz Feldhase

unread,
Oct 1, 2022, 9:28:02 PMOct 1
to
On Sunday, October 2, 2022 at 3:21:02 AM UTC+2, Mostowski Collapse wrote:

> Lets take him for granted, when he says:
> > If x not in X [where X = dom(f) --ff], then f(x) is undefined.

Yes, that's the usual math lingo.

Still ... (see my other post)

It seems to me that we agree concerning this point.

Fritz Feldhase

unread,
Oct 1, 2022, 9:41:52 PMOct 1
to
On Sunday, October 2, 2022 at 3:25:41 AM UTC+2, Mostowski Collapse wrote:
> The more general consequences are, that we can show:
>
> f =\= g
>
> In case f : dom1 -> cod1, g : dom2 -> cod2 and
> dom1 =\= dom2. Which is already the half part of
> function in-equality, namely this here from Terrence Tao:
> "the two functions f and g are not considered the same
> function, f =/= g, because they have different domains."
> --Terence Tao, Analysis I
>
> The other part cod1 =\= cod2 could be also furnished
> I guess by something "WE SAY IN MATHEMATICS"
> cast into a definition.

Indeed, repost:

============================================

Tao's 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 [I'd say], 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:

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

============================================

And, of course, this substitution axiom implies f = g -> (codom(f) = codom(f) <-> codom(f) = codom(g)), too. And hence with codom(f) = codom(f):

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

With contraposition we get:

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

THIS theorem will allow *us* to state:

"f and g are not considered the same function, f =/= g, because they have different codomains" (if so), "as required".

Nuff said.

Dan Christensen

unread,
Oct 1, 2022, 9:53:34 PMOct 1
to
On Saturday, October 1, 2022 at 8:53:10 PM UTC-4, Mostowski Collapse wrote:
> Ok here is a proof in DC Prof, of the fact:
Very, ummm... "interesting." I guess.

But "present????"

Thanks anyway, but I think I will stick to more conventional and widely used definitions.

Fritz Feldhase

unread,
Oct 1, 2022, 10:42:05 PMOct 1
to
On Sunday, October 2, 2022 at 3:53:34 AM UTC+2, Dan Christensen wrote:

> But "present????"

Quite obviously:

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

you silly asshole.

You may read "Present(h,x)" as "h has a value at x" or "h is defined at x", etc.

Hence I'd propose to use "Defined(h, x)" instead of "Present(h, x)".

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

Hope this helps.
Message has been deleted

Dan Christensen

unread,
Oct 1, 2022, 11:13:22 PMOct 1
to
On Saturday, October 1, 2022 at 10:42:05 PM UTC-4, Fritz Feldhase wrote:
> On Sunday, October 2, 2022 at 3:53:34 AM UTC+2, Dan Christensen wrote:
>
> > But "present????"
>
> Quite obviously:
> > 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Present(h,x) <=> x ε dom]]
> > Axiom

[snip childish abuse]

>
> You may read "Present(h,x)" as "h has a value at x" or "h is defined at x", etc.
>

f: X --> Y and x is (or is not) an element of X says it all. But define an abbreviation for this if you like. I don't think you will find much use for it

Dan Christensen

unread,
Oct 2, 2022, 1:07:21 AMOct 2
to
On Saturday, October 1, 2022 at 9:41:52 PM UTC-4, Fritz Feldhase wrote:
> On Sunday, October 2, 2022 at 3:25:41 AM UTC+2, Mostowski Collapse wrote:
> > The more general consequences are, that we can show:
> >
> > f =\= g
> >
> > In case f : dom1 -> cod1, g : dom2 -> cod2 and
> > dom1 =\= dom2. Which is already the half part of
> > function in-equality, namely this here from Terrence Tao:
> > "the two functions f and g are not considered the same
> > function, f =/= g, because they have different domains."
> > --Terence Tao, Analysis I
> >
> > The other part cod1 =\= cod2 could be also furnished
> > I guess by something "WE SAY IN MATHEMATICS"
> > cast into a definition.
> Indeed, repost:
>
> ============================================
>
> Tao's 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":
>

Strictly speaking, it does just that.

According to the above definition, we can we determine whether f=g or f=/=g ONLY IF they have the same domain and codomain.


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

Very disingenuous, Fritz. You cannot really believe that such informal commentary somehow overrules his formal definition above. Or that the above formal definition, strictly speaking, leaves this as a possibility. In the same paragraph, Tao even talks about making such admittedly "careless" distinctions blurring the difference between a function and its value at a point.

You are simply grasping at straws here, Frtiz. Just admit you were wrong. You are looking quite foolish here.

Mostowski Collapse

unread,
Oct 2, 2022, 5:01:40 AMOct 2
to
Are we a little inflexible in the mind, he he?

Since you don't understand the proof, it only uses subst
i.e. a=b, P(a) => P(b), here is a variant with Undefined
instead Present, works as well:

29 ~f=g
Conclusion, 26

----------------------------------- begin proof ------------------------------------

1 Function(f,s0,s0)
Axiom

2 Function(g,s01,s01)
Axiom

3 1 ε s01
Axiom

4 ~1 ε s0
Axiom

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

6 ALL(dom):ALL(cod):[Function(f,dom,cod) => ALL(x):[Undefined(f,x) <=> ~x ε dom]]
U Spec, 5

7 ALL(cod):[Function(f,s0,cod) => ALL(x):[Undefined(f,x) <=> ~x ε s0]]
U Spec, 6

8 Function(f,s0,s0) => ALL(x):[Undefined(f,x) <=> ~x ε s0]
U Spec, 7

9 ALL(x):[Undefined(f,x) <=> ~x ε s0]
Detach, 8, 1

10 Undefined(f,1) <=> ~1 ε s0
U Spec, 9

11 [Undefined(f,1) => ~1 ε s0]
& [~1 ε s0 => Undefined(f,1)]
Iff-And, 10

12 Undefined(f,1) => ~1 ε s0
Split, 11

13 ~1 ε s0 => Undefined(f,1)
Split, 11

14 Undefined(f,1)
Detach, 13, 4

15 ALL(dom):ALL(cod):[Function(g,dom,cod) => ALL(x):[Undefined(g,x) <=> ~x ε dom]]
U Spec, 5

16 ALL(cod):[Function(g,s01,cod) => ALL(x):[Undefined(g,x) <=> ~x ε s01]]
U Spec, 15

17 Function(g,s01,s01) => ALL(x):[Undefined(g,x) <=> ~x ε s01]
U Spec, 16

18 ALL(x):[Undefined(g,x) <=> ~x ε s01]
Detach, 17, 2

19 Undefined(g,1) <=> ~1 ε s01
U Spec, 18

20 [Undefined(g,1) => ~1 ε s01]
& [~1 ε s01 => Undefined(g,1)]
Iff-And, 19

21 Undefined(g,1) => ~1 ε s01
Split, 20

22 ~1 ε s01 => Undefined(g,1)
Split, 20

23 ~~1 ε s01 => ~Undefined(g,1)
Contra, 21

24 1 ε s01 => ~Undefined(g,1)
Rem DNeg, 23

25 ~Undefined(g,1)
Detach, 24, 3

26 f=g
Premise

27 Undefined(g,1)
Substitute, 26, 14

28 ~Undefined(g,1) & Undefined(g,1)
Join, 25, 27

29 ~f=g
Conclusion, 26

--------------------------- end proof -------------------------------------

Dan Christensen

unread,
Oct 2, 2022, 12:38:03 PMOct 2
to
On Sunday, October 2, 2022 at 5:01:40 AM UTC-4, Mostowski Collapse wrote:
> Are we a little inflexible in the mind, he he?
>
> Since you don't understand the proof, it only uses subst
> i.e. a=b, P(a) => P(b), here is a variant with Undefined
> instead Present, works as well:
>
> 29 ~f=g
> Conclusion, 26
>
> ----------------------------------- begin proof ------------------------------------
> 1 Function(f,s0,s0)
> Axiom
>
> 2 Function(g,s01,s01)
> Axiom
>
> 3 1 ε s01
> Axiom
>
> 4 ~1 ε s0
> Axiom
> 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]]
> Axiom
>

Try instead: "Undefined(h,dom,cod,x)" with the additional arguments. I think that will solve your problem.

Fritz Feldhase

unread,
Oct 2, 2022, 2:07:50 PMOct 2
to
On Sunday, October 2, 2022 at 6:38:03 PM UTC+2, Dan Christensen wrote:
> On Sunday, October 2, 2022 at 5:01:40 AM UTC-4, Mostowski Collapse wrote:
> >
> > Are we a little inflexible in the mind, he he?
> >
> > Since you don't understand the proof, it only uses subst
> > i.e. a=b, P(a) => P(b), here is a variant with Undefined
> > instead Present, works as well:
> >
> > 29 ~f=g
> > Conclusion, 26
> >
> > ----------------------------------- begin proof ------------------------------------
> > 1 Function(f,s0,s0)
> > Axiom
> >
> > 2 Function(g,s01,s01)
> > Axiom
> >
> > 3 1 ε s01
> > Axiom
> >
> > 4 ~1 ε s0
> > Axiom
> > 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]]
> > Axiom
> >
> Try instead <bla>

Why on earth should he do that? His proof is just fine.

Quote from one of my recent posts:
===================================================

Actually, we may define:

undefined(f, x) :<-> x !e dom(f)
"f is undefined at x".

===================================================

Hint: This is a formalization of a notion which is frequently used in math textbooks.

Actually, I'd even prefer the following two definitions [where f is a function]:

| defined(f, x) :<-> x e dom(f)
"f is defined at x"

and

| undefined(f, x) :<-> ~defined(f, x).
"f is not defined at x".

Dan Christensen

unread,
Oct 2, 2022, 3:01:55 PMOct 2
to
On Sunday, October 2, 2022 at 2:07:50 PM UTC-4, Fritz Feldhase wrote:
> On Sunday, October 2, 2022 at 6:38:03 PM UTC+2, Dan Christensen wrote:
> > On Sunday, October 2, 2022 at 5:01:40 AM UTC-4, Mostowski Collapse wrote:
> > >
> > > Are we a little inflexible in the mind, he he?
> > >
> > > Since you don't understand the proof, it only uses subst
> > > i.e. a=b, P(a) => P(b), here is a variant with Undefined
> > > instead Present, works as well:
> > >
> > > 29 ~f=g
> > > Conclusion, 26
> > >
> > > ----------------------------------- begin proof ------------------------------------
> > > 1 Function(f,s0,s0)
> > > Axiom
> > >
> > > 2 Function(g,s01,s01)
> > > Axiom
> > >
> > > 3 1 ε s01
> > > Axiom
> > >
> > > 4 ~1 ε s0
> > > Axiom
> > > 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]]
> > > Axiom
> > >
> > Try instead: "Undefined(h,dom,cod,x)" with the additional arguments. I think that will solve your problem.
>
> Why on earth should he do that?

[snip]

To avoid making a fool of himself. You should try it, Fritz.

Mostowski Collapse

unread,
Oct 2, 2022, 3:45:10 PMOct 2
to
Stop shedding tears and inventing bull shit. I would try
it, if your definition would say so. But you said,
Dan Christensen, the following:

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 what we define here is the pharse „f(x) is UNDEFINED“,
which has only two parametes f and x:

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

Defining Undefined(f,x,dom,cod) is nowhere required. You phrased
your definition as type 1, so we have Function(f,dom,cod) as
precondition translating your „if we are given“. Then you

talk about „x not in“ and „in this case“. So its all fine how its
done, its just what you said. No climbing down possible, you
where leaning out of the window, now be a man, and not pussy

that cannot live the consequences of his doing. The comsequences
are that we can for example show:

f =\= g

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

Dan Christensen

unread,
Oct 2, 2022, 5:22:31 PMOct 2
to
On Sunday, October 2, 2022 at 3:45:10 PM UTC-4, Mostowski Collapse wrote:

[snip]

>
> So what we define here is the pharse „f(x) is UNDEFINED“,
> which has only two parametes f and x:
>
> 5 ALL(f):ALL(dom):ALL(cod):[Function(f,dom,cod) =>
> ALL(x):[Undefined(f,x) <=> ~x ε dom]]
> Axiom
>

Each to their own, I guess. If you actually want to obtain a wonky result, this would seem to be a very good way to do it, Jan Burse. If, on the other hand, you want to avoid your wonky result, you now know that you will have to add arguments for the domain and codomain sets.

Good luck with your wonky new theory of functions, Jan Burse. Maybe the philosophy department will be interested.

Fritz Feldhase

unread,
Oct 2, 2022, 6:17:48 PMOct 2
to
On Sunday, October 2, 2022 at 11:22:31 PM UTC+2, Dan Christensen wrote:
> On Sunday, October 2, 2022 at 3:45:10 PM UTC-4, Mostowski Collapse wrote:
>
> [snip]
> >
> > So what we define here is the pharse „f(x) is UNDEFINED“,

Well, actually it's the common phrase "f is undefined at x".

See https://socratic.org/questions/is-the-statement-if-f-is-undefined-at-x-c-then-the-limit-of-f-x-as-x-approaches-
for example.

> > which has only two parametes f and x:

Indeed. :-)

> > 5 ALL(f):ALL(dom):ALL(cod):[Function(f,dom,cod) => ALL(x):[Undefined(f,x) <=> ~x ε dom]]
> > Axiom
> >
> If you actually want to obtain [your desired] result, this would seem to be a very good way to do it, Jan Burse.

Indeed!

> If, on the other hand, you want to avoid your [...] result, you <bla>

Look, dombo, in math we are trying to REACH desired results, not to AVOID them.

> Good luck with <bla>

Are you demented, Dan?

Dan Christensen

unread,
Oct 2, 2022, 7:25:56 PMOct 2
to
Done properly...

1 Function(f,s0,s0)
Axiom

2 Function(g,s01,s01)
Axiom

3 1 @ s01
Axiom

4 ~1 @ s0
Axiom

More correctly, we have:

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

6 ALL(dom):ALL(cod):[Function(f,dom,cod) => ALL(x):[Undefined(f,dom,cod,x) <=> ~x @ dom]]
U Spec, 5

7 ALL(cod):[Function(f,s0,cod) => ALL(x):[Undefined(f,s0,cod,x) <=> ~x @ s0]]
U Spec, 6

8 Function(f,s0,s0) => ALL(x):[Undefined(f,s0,s0,x) <=> ~x @ s0]
U Spec, 7

9 ALL(x):[Undefined(f,s0,s0,x) <=> ~x @ s0]
Detach, 8, 1

10 Undefined(f,s0,s0,1) <=> ~1 @ s0
U Spec, 9

11 [Undefined(f,s0,s0,1) => ~1 @ s0]
& [~1 @ s0 => Undefined(f,s0,s0,1)]
Iff-And, 10

12 Undefined(f,s0,s0,1) => ~1 @ s0
Split, 11

13 ~1 @ s0 => Undefined(f,s0,s0,1)
Split, 11

14 Undefined(f,s0,s0,1)
Detach, 13, 4

15 ALL(dom):ALL(cod):[Function(g,dom,cod) => ALL(x):[Undefined(g,dom,cod,x) <=> ~x @ dom]]
U Spec, 5

16 ALL(cod):[Function(g,s01,cod) => ALL(x):[Undefined(g,s01,cod,x) <=> ~x @ s01]]
U Spec, 15

17 Function(g,s01,s01) => ALL(x):[Undefined(g,s01,s01,x) <=> ~x @ s01]
U Spec, 16

18 ALL(x):[Undefined(g,s01,s01,x) <=> ~x @ s01]
Detach, 17, 2

19 Undefined(g,s01,s01,1) <=> ~1 @ s01
U Spec, 18

20 [Undefined(g,s01,s01,1) => ~1 @ s01]
& [~1 @ s01 => Undefined(g,s01,s01,1)]
Iff-And, 19

21 Undefined(g,s01,s01,1) => ~1 @ s01
Split, 20

22 ~1 @ s01 => Undefined(g,s01,s01,1)
Split, 20

23 ~~1 @ s01 => ~Undefined(g,s01,s01,1)
Contra, 21

24 1 @ s01 => ~Undefined(g,s01,s01,1)
Rem DNeg, 23

25 ~Undefined(g,s01,s01,1)
Detach, 24, 3

26 f=g
Premise

27 Undefined(g,s0,s0,1)
Substitute, 26, 14

28 ~Undefined(g,s01,s01,1) & Undefined(g,s0,s0,1)
Join, 25, 27

29 f=g => ~Undefined(g,s01,s01,1) & Undefined(g,s0,s0,1)
Conclusion, 26

Oh, dear... The wheels just fell off, Jan Burse! On the last line, too. Those pesky domain and codomain arguments.

Nice try, though. If it's any consolation, you are getting pretty good at DC Proof!

Fritz Feldhase

unread,
Oct 2, 2022, 9:21:43 PMOct 2
to
On Monday, October 3, 2022 at 1:25:56 AM UTC+2, Dan Christensen wrote:

> Done properly...

...from the point of view of a crank.

FUCK OFF, YOU SILLY ASSHOLE!

Dan Christensen

unread,
Oct 2, 2022, 9:34:59 PMOct 2
to
On Sunday, October 2, 2022 at 9:21:43 PM UTC-4, Fritz Feldhase wrote:
> On Monday, October 3, 2022 at 1:25:56 AM UTC+2, Dan Christensen wrote:
>
> > Done properly...
>
[snip childish abuse]

Thank you for that, ummm... "thoughtful" analysis, Fritz. (Hee, hee!)

You lose.

Dan

Mostowski Collapse

unread,
Oct 3, 2022, 2:45:36 AMOct 3
to
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.

Dan Christensen schrieb am Montag, 3. Oktober 2022 um 01:25:56 UTC+2:
> On Sunday, October 2, 2022 at 5:01:40 AM UTC-4, Mostowski Collapse wrote:
> > Are we a little inflexible in the mind, he he?
Message has been deleted

Dan Christensen

unread,
Oct 3, 2022, 2:30:45 PMOct 3
to
On Monday, October 3, 2022 at 2:45:36 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 dom => f(a) in cod] & ~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

Mostowski Collapse

unread,
Oct 3, 2022, 6:51:40 PMOct 3