New Version of DC Proof with expanded tutorial

[Dan Christensen]

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]

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]

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

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]

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]

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]

[snip childish abuse]

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

[Mostowski Collapse]

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]

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]

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]

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]

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

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]

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]

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]

Corr:

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

[Fritz Feldhase]

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]

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]

You are fake news!

[Dan Christensen]

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]

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]

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]

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?

[Mostowski Collapse]

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]

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]

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]

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]

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]

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]

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]

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]

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.

[Dan Christensen]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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?

[Dan Christensen]

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]

You are quite a slow thinker, he he?

You cannot use Eq(f1,f2,dom,cod) to prove, even if you
would use the definition of Eq(f1,f2,dom,cod), since the
Terrence Tao definition only talks about x e dom:

ALL(f1):ALL(f2):ALL(dom):ALL(cod):
[Eq(f1,f2,dom,cod) => ALL(x):[Undefined(f2,x) => Undefined(f1,x)]]

On the other hand this works for f1=f2. So you cannot
say f1=f2 and Eq(f1,f2,dom,cod) are logically equivalent.
The predicate definition Undefined is the counter example.

P.S.: Here is the proof that works with f1=f2:

15 ALL(f1):ALL(f2):[f1=f2 => ALL(x):[Undefined(f2,x) => Undefined(f1,x)]]
Conclusion, 1

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

1 f1=f2
Premise

2 EXIST(x):[~Undefined(f1,x) & Undefined(f2,x)]
Premise

3 ~Undefined(f1,u) & Undefined(f2,u)
E Spec, 2

4 ~Undefined(f2,u) & Undefined(f2,u)
Substitute, 1, 3

5 ~EXIST(x):[~Undefined(f1,x) & Undefined(f2,x)]
Conclusion, 2

6 ~~ALL(x):~[~Undefined(f1,x) & Undefined(f2,x)]
Quant, 5

7 ALL(x):~[~Undefined(f1,x) & Undefined(f2,x)]
Rem DNeg, 6

8 ALL(x):~~[~~Undefined(f1,x) | ~Undefined(f2,x)]
DeMorgan, 7

9 ALL(x):[~~Undefined(f1,x) | ~Undefined(f2,x)]
Rem DNeg, 8

10 ALL(x):[Undefined(f1,x) | ~Undefined(f2,x)]
Rem DNeg, 9

11 ALL(x):[~Undefined(f1,x) => ~Undefined(f2,x)]
Imply-Or, 10

12 ALL(x):[~~Undefined(f2,x) => ~~Undefined(f1,x)]
Contra, 11

13 ALL(x):[Undefined(f2,x) => ~~Undefined(f1,x)]
Rem DNeg, 12

14 ALL(x):[Undefined(f2,x) => Undefined(f1,x)]
Rem DNeg, 13

15 ALL(f1):ALL(f2):[f1=f2 => ALL(x):[Undefined(f2,x) => Undefined(f1,x)]]
Conclusion, 1

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

[Mostowski Collapse]

BTW: Same problem with Undefined(f,dom,cod,x), you cannot prove:

ALL(f1):ALL(f2):ALL(dom):ALL(cod):
[Eq(f1,f2,dom,cod) => ALL(x):[Undefined(f2,dom,cod,x) => Undefined(f1,dom,cod,x)]]

Try proving it. You will not be able to prove it. There are easy counter
examples, especially if you use ALL(a):[a in dom => f(a) in cod] in your
definition of Eq(f1,f2,dom,cod) and Undefined(f,dom,cod,x).

On the other hand this is trivially also provable:

ALL(f1):ALL(f2):
[f1=f2 => ALL(dom):ALL(cod):ALL(x):[Undefined(f2,dom,cod,x) => Undefined(f1,dom,cod,x)]]

[Dan Christensen]

On Monday, October 3, 2022 at 6:51:40 PM UTC-4, Mostowski Collapse wrote:
> You are quite a slow thinker, he he?
>
> You cannot use Eq(f1,f2,dom,cod) to prove, even if you
> would use the definition of Eq(f1,f2,dom,cod), since the
> Terrence Tao definition only talks about x e dom:
>
> ALL(f1):ALL(f2):ALL(dom):ALL(cod):
> [Eq(f1,f2,dom,cod) => ALL(x):[Undefined(f2,x) => Undefined(f1,x)]]
>

Where are you getting this nonsense, Jan Burse? Nowhere does Tao define an "Undefined" predicate. Why would he? That is just your bizarre fixation. Most people would just write something like ALL(a):[a in x => f(a) in x] & ~z in x. Try to write your "proof" using that instead. You will soon see how wrong you have been.

> On the other hand this works for f1=f2. So you cannot
> say f1=f2 and Eq(f1,f2,dom,cod) are logically equivalent.
> The predicate definition Undefined is the counter example.
>
> P.S.: Here is the proof that works with f1=f2:
>
> 15 ALL(f1):ALL(f2):[f1=f2 => ALL(x):[Undefined(f2,x) => Undefined(f1,x)]]
> Conclusion, 1
>
> ---------------------------------- begin proof --------------------------------------------
>
> 1 f1=f2
> Premise
>

What are f1 and f2?

Is this what you really want to say for some sets x and y?

ALL(a):[a in x => f1(a) in y]
& ALL(a):[a in x => f2(a) in y]
& ALL(a):[a in x => f1(a)=f2(a)]

> 2 EXIST(x):[~Undefined(f1,x) & Undefined(f2,x)]
> Premise
>

[snip nonsense]

If x is suppose to be an element of some set, can you at least give that set a name so we can talk about it?

Again, you are ignoring the critical parameters for the domain and codomain sets. No wonder you are getting such wonky results.

Get back to us when you can address these issues, Jan Burse.

Dan

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

[Fritz Feldhase]

On Tuesday, October 4, 2022 at 5:19:51 AM UTC+2, Dan Christensen wrote:

> Nowhere does Tao define an "Undefined" predicate.

So what? Maybe you noticed that his approach is NOT a "formal" one, you silly crank.

> Why would he?

Right. Why should ***he*** (in the context of an analysis textbook)?!

On in the other hand, in the context of a a FORMAL system, ***we*** HAVE TO define our notions (if we want to USE them).

Hint: Look, crank, the definition

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

just formalizes the common notion "f is /undefined/ at x".

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

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

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

> [Some] people would just write something like ALL(a):[a in X => f(a) in X] & ~x in X.

Huh?! Look, crank, this does not define the notion we want do define, namely "f is /undefined/ at x" (where f is a function).
Moreover, X = dom(f) implies ALL(a):[a in X => f(a) in X], hence no need to include that, etc.

> [...] the critical parameters for the domain and codomain sets.

The "critical parameters" for them are

dom(f) = X & codom(f) = Y ,

if f is a function with domain X and codomain Y, dumbo.

Actually, using symbols, we have:

f: X --> Y =df function(f) & dom(f) = X & codom(f) = Y.

Try to get that straight, dumbo.

[Dan Christensen]

On Tuesday, October 4, 2022 at 2:45:22 AM UTC-4, Fritz Feldhase wrote:
> On Tuesday, October 4, 2022 at 5:19:51 AM UTC+2, Dan Christensen wrote:
>
> > Nowhere does Tao define an "Undefined" predicate.
> So what? Maybe you noticed that his approach is NOT a "formal" one

[snip childish abuse]

>
> > Why would he?
>
> Right. Why should ***he*** (in the context of an analysis textbook)?!
>
> On in the other hand, in the context of a a FORMAL system, ***we*** HAVE TO define our notions (if we want to USE them).
>

[snip]

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

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

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

3. 1 in s01
Axiom

4. ~1 in s0
Axiom

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

[Dan Christensen]

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
>

[snip flawed proof]

You were never very good with logical predicates, Jan Burse. Try to rework you proof without them. They really aren't necessary here. Something along the lines of:

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

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

3. 1 in s01
Axiom

4. ~1 in s0
Axiom

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

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

7. f=g
Premise

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

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

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

Well, that doesn't work either, but I hope it gives you some ideas. (Hee, hee!)

[Mostowski Collapse]

You are spewing nonsense as usual.

A Proof that attempts to reach the same conclusion
from Undefined(f,x,dom1,cod1) and Undefine(g,x,dom2,cod2)
is not the same proof as mine which uses Undefined(f.x)

and Undefine(g,x). How do you want to capitalize from
substitution f=g, A(f) => A(g) using contraposition?
Its just a crank idea. Only a crank would think, the

proof still works, only a crank would use this as
an argument in a discussion, only a crank can go
this far astray, only a crank can pretend being serious,

whereas this is just stupid trolling.

[Dan Christensen]

> A Proof that attempts to reach the same conclusion
> from Undefined(f,x,dom1,cod1) and Undefine(g,x,dom2,cod2)
> is not the same proof as mine which uses Undefined(f.x)
>

[snip nonsense]

Indeed. Your binary predicate leads to a somewhat wonky result, Jan Burse. The fact that it cannot obtained that without you needlessly introducing your wonky predicate should tell you that you got it wrong, but I won't hold my breath.

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 3:22:58 PM UTC+2, Dan Christensen wrote:

> > A Proof that attempts to reach the same conclusion
> > from Undefined(f,x,dom1,cod1) and Undefine(g,x,dom2,cod2)

> > is not the same proof as mine which uses Undefined(f,x)
> >
> Indeed.

Try to learn at least SOME math, crank.

"The set of numbers for which a function is defined is called the domain of the function.
If a number is not in the domain of a function, the function is said to be "undefined" for that number." (Wikipedia)

This quite naturally leads to the definition:

undefined(f, x) :<-> x !e dom(f) (where f is a function).

"f is undefined at x"

For example: Let's consider the function f: IR \ {0} --> IR defined with f(x) = 1/x for all x e IR \ {0}.
Then dom(f) = IR \ {0} and f is undefined at 0 (since 0 !e dom(f)). Using symbols: undefined(f, 0).

And now fuck off, asshole.

[Dan Christensen]

On Wednesday, October 5, 2022 at 10:17:47 AM UTC-4, Fritz Feldhase wrote:
> On Wednesday, October 5, 2022 at 3:22:58 PM UTC+2, Dan Christensen wrote:
>
> > > A Proof that attempts to reach the same conclusion
> > > from Undefined(f,x,dom1,cod1) and Undefine(g,x,dom2,cod2)
> > > is not the same proof as mine which uses Undefined(f,x)
> > >

> > Indeed. Your binary predicate leads to a somewhat wonky result, Jan Burse. The fact that it cannot obtained that without you needlessly introducing your wonky predicate should tell you that you got it wrong, but I won't hold my breath.
>

[snip childish abuse]

>
> "The set of numbers for which a function is defined is called the domain of the function.
> If a number is not in the domain of a function, the function is said to be "undefined" for that number." (Wikipedia)
>
> This quite naturally leads to the definition:
>
> undefined(f, x) :<-> x !e dom(f) (where f is a function).
> "f is undefined at x"

Close, but as we have seen, the domain and codomain sets should be included in the parameters for the "is-undefined" predicate. Otherwise, you can get some quite wonky results (see Jan Burse, aka Mr. Collapse).

Better would be:

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

> For example: Let's consider the function f: IR \ {0} --> IR defined with f(x) = 1/x for all x e IR \ {0}.
> Then dom(f) = IR \ {0} and f is undefined at 0 (since 0 !e dom(f)). Using symbols: undefined(f, 0).
>

[snip childish abuse]

Applying my alternative definition, that would be:

Undefined(f, |R \ {0}, |R, 0).

This gives a much more complete picture of the situation, don't you think?

I hope this helps.

[Mostowski Collapse]

More proof that you are a crank. If you don't like some result,
you call it wonky. Very poor mathematical performance.

[Dan Christensen]

Jan Burse is pissed off that I pointed out and presented two different ways (with and without predicates) to correct his error. How ungrateful!

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 5:51:48 PM UTC+2, Dan Christensen wrote:
> On Wednesday, October 5, 2022 at 10:17:47 AM UTC-4, Fritz Feldhase wrote:

TRY TO LEARN AT LEAST SOME MATH, YOU SILLY CRANK:

> > "The set of numbers for which a function is defined is called the domain of the function.
> > If a number is not in the domain of a function, the function is said to be "undefined" for that number." (Wikipedia)
> >
> > This quite naturally leads to the definition:
> >
> > undefined(f, x) :<-> x !e dom(f) (where f is a function).
> > "f is undefined at x"
> >
> Close, but

TRY TO LEARN AT LEAST SOME MATH, YOU SILLY CRANK:

| "If a number is not in the domain of a function, the function is said to be "undefined" for that number." (Wikipedia)

> Better would be:

THAT YOU TRY TO LEARN AT LEAST SOME MATH, IDIOT!

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 5:56:40 PM UTC+2, Mostowski Collapse wrote:

> More proof that you are a crank. If you don't like some result,
> you call it wonky. Very poor mathematical performance.

Agree.

Moreover he is unwilling (or unable to) to learn.

"A crank is defined as a man who cannot be turned."
— Nature, 8 Nov 1906, 25/2

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 6:10:28 PM UTC+2, Dan Christensen wrote:

> Jan Burse is pissed off that I pointed out and presented two different ways (with and without predicates) to correct his error.

Fuck off, you silly idiot!

[Mostowski Collapse]

What error, crank? You are out of your mind. Its relatively easy
to turn p(v,r) and ~p(w,s) into a contradiction q(v) and ~q(w).

Just use this formula, with free variable a for q(_):

(v=a => p(v,r))&(w=a => ~p(w,s))

Here are some proofs:

(pvr ∧ ¬pws) → ((v=v → pvr) ∧ (w=v → ¬pws)) is valid.
https://www.umsu.de/trees/#p%28v,r%29~1~3p%28w,s%29~5%28v=v~5p%28v,r%29%29~1%28w=v~5~3p%28w,s%29%29

p(v,r) ∧ ¬p(w,s) → (v=w → p(v,r))∧(w=w → ¬p(w,s))
https://www.umsu.de/trees/#p%28v,r%29~1~3p%28w,s%29~5%28v=w~5p%28v,r%29%29~1%28w=w~5~3p%28w,s%29%29

So we should be also able to prove:

f=\=g

from Undefined(f,1,s0,s0) and Undefined(f,1,s01,s01).

Right?

[Mostowski Collapse]

Corr.: Typo

So we should be also able to prove:

f=\=g

from Undefined(f,1,s0,s0) and ~Undefined(g,1,s01,s01).

[Dan Christensen]

> What error?

[snip childish abuse and nonsense]

You left out critical parameters for the domain and codomain sets in your "is-undefined" predicate allowing you to obtain your wonky result. It was impossible to obtain that result when those parameters were added to the argument list, or when not using a predicate/abbreviation. Don't you feel silly, Jan Burse?

[Mostowski Collapse]

Nope the formula doesn't work as such.
Made a typo in the second validation:

p(v,r) ∧ ¬p(w,s) → (v=w → p(v,r))∧(w=w → ¬p(w,s))
https://www.umsu.de/trees/#p%28v,r%29~1~3p%28w,s%29~5%28v=w~5p%28v,r%29%29~1%28w=w~5~3p%28w,s%29%29

Unfortunately this doesn't work:

(pvr ∧ ¬pws) → ¬((v=w → pvr) ∧ (w=w → ¬pws)) is invalid.
https://www.umsu.de/trees/#p(v,r)~1~3p(w,s)~5~3((v=w~5p(v,r))~1(w=w~5~3p(w,s)))

But the idea would be to map v to (v,r) and
w to (w,s) somehow, and look at the truth value
of p, to get the truth q.

Is this possible, to construct such a q?

[Dan Christensen]

On Wednesday, October 5, 2022 at 12:32:30 PM UTC-4, Mostowski Collapse wrote:

> Mostowski Collapse schrieb am Mittwoch, 5. Oktober 2022 um 18:24:59 UTC+2:
> > What error, crank? You are out of your mind. Its relatively easy
> > to turn p(v,r) and ~p(w,s) into a contradiction q(v) and ~q(w).
> >

[snip]

> Corr.: Typo
> So we should be also able to prove:
>
> f=\=g
> from Undefined(f,1,s0,s0) and ~Undefined(g,1,s01,s01).

Please do so.

Dan

[Mostowski Collapse]

Well its obvious that it can be done. Isn't it?
Just use this propositional logic identity:

¬((A → B)∧(¬A→C)) ↔ (A→ ¬B)∧(¬A → ¬C)
https://www.umsu.de/trees/#~3%28%28A~5B%29~1%28~3A~5C%29%29~4%28A~5~3B%29~1%28~3A~5~3C%29

In building the formula. Here is a new attempt:

(v=a→ (w=a→ ?)∧(¬w=a → p(v,r)))∧(¬v=a → (w=a → p(w,s))∧(¬w=a → ?))

Now sure what to set for the two question marks ?
The second question mark is somehow not needed,

since we anyway are only interested in q(v) and ~q(w).
The first question mark can be set to any value,

because in case of v = w, then q(v) and ~q(w) are anyway
in contradiction. Looks solvable somehow.

[Dan Christensen]

On Wednesday, October 5, 2022 at 12:50:46 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 5. Oktober 2022 um 18:38:31 UTC+2:
> > On Wednesday, October 5, 2022 at 12:32:30 PM UTC-4, Mostowski Collapse wrote:
> >
> > > Mostowski Collapse schrieb am Mittwoch, 5. Oktober 2022 um 18:24:59 UTC+2:
> > > > What error, crank? You are out of your mind. Its relatively easy
> > > > to turn p(v,r) and ~p(w,s) into a contradiction q(v) and ~q(w).
> > > >
> > [snip]
> > > Corr.: Typo
> > > So we should be also able to prove:
> > >
> > > f=\=g
> > > from Undefined(f,1,s0,s0) and ~Undefined(g,1,s01,s01).
> > Please do so.
> >

> Well its obvious that it can be done. Isn't it?
> Just use this propositional logic identity:
>
> ¬((A → B)∧(¬A→C)) ↔ (A→ ¬B)∧(¬A → ¬C)
> https://www.umsu.de/trees/#~3%28%28A~5B%29~1%28~3A~5C%29%29~4%28A~5~3B%29~1%28~3A~5~3C%29
>
> In building the formula. Here is a new attempt:
>
> (v=a→ (w=a→ ?)∧(¬w=a → p(v,r)))∧(¬v=a → (w=a → p(w,s))∧(¬w=a → ?))
>
> Now sure what to set for the two question marks ?
> The second question mark is somehow not needed,
>
> since we anyway are only interested in q(v) and ~q(w).
> The first question mark can be set to any value,
>
> because in case of v = w, then q(v) and ~q(w) are anyway
> in contradiction. Looks solvable somehow.

Just do it. Your original proof was only 29 lines.

Dan

[Mostowski Collapse]

pehou...@gmail.com might know the identity I am
using, its from SAT Solving, its an identity about
the ITE (if-then-else) operator. And the identity

is part of the boolean expansion theorem,
see property of cofactor when the formula is negated:
https://en.wikipedia.org/wiki/Boole%27s_expansion_theorem

There are further identities and thus representations:

Sum of Products (SoP)
(A→ B)∧(¬A → C) ↔ (A ∧ B) ∨ (¬A ∧ C)
https://www.umsu.de/trees/#%28A~5B%29~1%28~3A~5C%29~4%28A~1B%29~2%28~3A~1C%29
(Can be also proved by using the definition of ¬(P → Q) == P ∧ ¬Q,
and the theorem below about negation of ITE, gives negative cofactors)

Product of Sums (PoS)
((A→B) ∧ (¬A→C)) ↔ ((A∨C) ∧ (¬A∨B)) is valid.
https://www.umsu.de/trees/#%28A~5B%29~1%28~3A~5C%29~4%28A~2C%29~1%28~3A~2B%29
(Can be also proved by using the definition of P → Q == ¬P ∨ Q)

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 6:50:46 PM UTC+2, Mostowski Collapse wrote:

> > > So we should be also able to prove:
> > >
> > > f=\=g
> > >
> > > from Undefined(f,1,s0,s0) and ~Undefined(g,1,s01,s01).

Well, how do you define /Undefined/() in this case?

Actually, it doesn't make much sense to attach two unrelated "parameters" to the predicate undefined(f, x), which should just express that x !e dom(f) [which depends on exactly 2 "parameters"].

Of course, if we have

Undefined(f, 1, dom(f), codom(f))

and

~Undefined(g, 1, dom(g), codom(g)),

we can get a contradiction from the assumtion f = g (and the "substitution axiom").

For example: If we consider two functions f: {1} --> {1}, f(x) = x, and g: {0} --> {0}, g(x) = x, we have dom(f) = codom(f) = {1} and dom(g} = codom(g) = {0}, and 1 e dom(f), 1 !e dom(g). (Depending on the definition of /Undefined/) we then SHOULD get Undefined(f, 1, dom(f), codom(f)) and ~Undefined(g, 1, dom(g), codom(g)) [otherwise the definition of /Undefined/ would be rather nonsensical]. Hence f =/= g.

[Mostowski Collapse]

I just take the Proofs from Dan-O-Matik:

Undefined(f, 1, s0, s0)
~Undefined(g, 1, s01, s01)

And turn it into two Proofs:

A(f,1)
~A(g,1)

Where A(h,x) is a formula closed formula, using ITE.
And then I am done, I can derive f=\=g.

[Dan Christensen]

On Wednesday, October 5, 2022 at 1:07:09 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, October 5, 2022 at 6:50:46 PM UTC+2, Mostowski Collapse wrote:
>
> > > > So we should be also able to prove:
> > > >
> > > > f=\=g
> > > >
> > > > from Undefined(f,1,s0,s0) and ~Undefined(g,1,s01,s01).
> Well, how do you define /Undefined/() in this case?
>
> Actually, it doesn't make much sense to attach two unrelated "parameters" to the predicate undefined(f, x), which should just express that x !e dom(f) [which depends on exactly 2 "parameters"].
>
> Of course, if we have
>
> Undefined(f, 1, dom(f), codom(f))
>
> and
>
> ~Undefined(g, 1, dom(g), codom(g)),
>
> we can get a contradiction from the assumtion f = g (and the "substitution axiom").
>

There is no dom or codom operator in DC Proof, of most math textbooks as I recall.

This should get you started:

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

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

3. 1 in s01
Axiom

4. ~1 in s0
Axiom

5. ALL(f):ALL(dom):ALL(cod):ALL(a):[Undefined(f,dom,cod,a) <=> ALL(b):[b in dom => f(b) in cod] & ~a in dom]
Axiom

[Mostowski Collapse]

Its irrelevant how you define Undefined(_,_,_,_) as long as we
can derive from it something with a smaller arity, we are done.

[Dan Christensen]

Just do it!!!

Dan

[Mostowski Collapse]

Easy peasy wonky man, rome wasn't built in one day.

[Dan Christensen]

On Wednesday, October 5, 2022 at 1:44:11 PM UTC-4, Mostowski Collapse wrote:
> Easy peasy wonky man, rome wasn't built in one day.

Take your time. Get it right. ;^)

Dan

[Mostowski Collapse]

With this "right" wonky man definition:

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

Its relatively easy to prove f =\= g. Take f : {0} -> {0}, f(x)=x,
and g:{0,1} -> {0,1}, g(x) =1-x, we get immediately:

Undefined(f,s0,s0,1)
~Undefined(g,s0,s0,1)

And therefore:

f=\=g

This is a case where we showed to functions inequal,
with different domain and codomain. The function
axiom of DC Spoiled cannot do that.

[Dan Christensen]

On Wednesday, October 5, 2022 at 6:09:10 PM UTC-4, Mostowski Collapse wrote:
> With this "right" wonky man definition:
>
> 5 ALL(f):ALL(dom):ALL(cod):ALL(a):[Undefined(f,dom,cod,a) <=> ALL(b):[b in dom => f(b) in cod] & ~a in dom]
>
> Its relatively easy to prove f =\= g. Take f : {0} -> {0}, f(x)=x,
> and g:{0,1} -> {0,1}, g(x) =1-x, we get immediately:
>
> Undefined(f,s0,s0,1)
> ~Undefined(g,s0,s0,1)
>

So it should be "relatively easy" to formally prove it, right Jan Burse? We are STILL waiting. What seems to be the problem?

Again, this should get you started:

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

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

3. 1 in s01
Axiom

4. ~1 in s0
Axiom

5. ALL(f):ALL(dom):ALL(cod):ALL(a):[Undefined(f,dom,cod,a) <=> ALL(b):[b in dom => f(b) in cod] & ~a in dom]
Axiom

Take your time. Get it right this time.

[Fritz Feldhase]

On Wednesday, October 5, 2022 at 7:22:14 PM UTC+2, Dan Christensen wrote:
> On Wednesday, October 5, 2022 at 1:07:09 PM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, October 5, 2022 at 6:50:46 PM UTC+2, Mostowski Collapse wrote:
> >
> > > > > So we should be also able to prove:
> > > > >
> > > > > f=\=g
> > > > >
> > > > > from Undefined(f,1,s0,s0) and ~Undefined(g,1,s01,s01).
> > Well, how do you define /Undefined/() in this case?
> >
> > Actually, it doesn't make much sense to attach two unrelated "parameters" to the predicate undefined(f, x), which should just express that x !e dom(f) [which depends on exactly 2 "parameters"].
> >
> > Of course, if we have
> >
> > Undefined(f, 1, dom(f), codom(f))
> >
> > and
> >
> > ~Undefined(g, 1, dom(g), codom(g)),
> >
> > we can get a contradiction from the assumtion f = g (and the "substitution axiom").
> >
> There is no dom or codom operator in DC Proof

and hence no NOTION of "the domain of f" and "the codomain of f" (where f is a function)

> [UNLIKE as in almost all] math textbooks [which refer to /functions/].

Actually, (at least) some "function axioms" like the following would be required in your system

function(f, X, Y) <-> function(f) & dom(f) = X & codom(f) = Y
function(f, X, Y) -> Ax(x e X -> f(x) e Y).
function(f) -> (undefined(f, x) <-> x !e dom(f))
etc.

to be able to formalize standard math claims more or less "directly".

Here "function(f, X, Y)" would stand for "f : X --> Y" from standard math.

Hint: If Tao mentions (considers) a function "f: X --> Y" and talks about "the domain of f", he's talking about X.

TRY TO LEARN AT LEAST SOME MATH, YOU SILLY CRANK.

[Fritz Feldhase]

On Thursday, October 6, 2022 at 1:10:05 AM UTC+2, Dan Christensen wrote:
> On Wednesday, October 5, 2022 at 6:09:10 PM UTC-4, Mostowski Collapse wrote:
> > With this "right" wonky man definition:
> >
> > 5 ALL(f):ALL(dom):ALL(cod):ALL(a):[Undefined(f,dom,cod,a) <=> ALL(b):[b in dom => f(b) in cod] & ~a in dom]
> >
> > Its relatively easy to prove f =\= g. Take f : {0} -> {0}, f(x)=x,
> > and g:{0,1} -> {0,1}, g(x) =1-x, we get immediately:
> >

> > Undefined(f, s0, s0, 1) & ~Undefined(g, s0, s0, 1)

> >
> So it should be "relatively easy" to formally prove it, right Jan Burse? We are STILL waiting. What seems to be the problem?
>
> Again, this should get you started:
> 1. ALL(a):[a in s0 => f(a) in s0]
> Axiom
>
> 2. ALL(a):[a in s01 => g(a) in s01]
> Axiom
>
> 3. 1 in s01
> Axiom

3a. 0 in s01

> 4. ~1 in s0
> Axiom

4a. 0 in s0

> 5. ALL(h):ALL(dom):ALL(cod):ALL(b):[Undefined(h,dom,cod,b) <=> ALL(a):[a in dom => h(a) in cod] & ~b in dom]
> Axiom

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

7. ALL(a):[a in s01 => g(a) = 1 - a]
Axiom

7a. 1 - 0 = 1
Axiom [actually an arithmetic theorem]

8. Undefined(f , s0 , s0, 1) <=> ALL(b):[a in s0 => f(a) in s0] & ~1 in s0
with "specialization" from 5.

9. Undefined(g , s0 , s0, 1) <=> ALL(a):[a in s0 => g(a) in s0] & ~1 in s0
with "specialization" from 5.

10. Undefined(f , s0 , s0, 1)
with 1., 4. from 8.

11. ~ALL(a):[a in s0 => g(a) in s0]
from subproof:
| Assume ALL(a):[a in s0 => g(a) in s0].
| Hence we get 0 in s0 => g(0) in s0 by specialization.
| Hence with 4a. (0 in s0) we get g(0) in s0. [!]
| But from 7, 7a and 3a. we get that g(0) = 1
| and hence with 4. we get ~g(0) in s0. [!]
| Contradicton! Hence ~ALL(a):[a in s0 => g(a) in s0].

12. ~Undefined(g , s0 , s0, 1)
with 9. and 11.

13. Undefined(f, s0, s0, 1) & ~Undefined(g, s0, s0, 1)
from 10. and 12.

Did a make an error? Please check with DC Proof! :-)

[Dan Christensen]

On Wednesday, October 5, 2022 at 7:17:02 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, October 5, 2022 at 7:22:14 PM UTC+2, Dan Christensen wrote:
> > On Wednesday, October 5, 2022 at 1:07:09 PM UTC-4, Fritz Feldhase wrote:
> > > On Wednesday, October 5, 2022 at 6:50:46 PM UTC+2, Mostowski Collapse wrote:
> > >
> > > > > > So we should be also able to prove:
> > > > > >
> > > > > > f=\=g
> > > > > >
> > > > > > from Undefined(f,1,s0,s0) and ~Undefined(g,1,s01,s01).
> > > Well, how do you define /Undefined/() in this case?
> > >
> > > Actually, it doesn't make much sense to attach two unrelated "parameters" to the predicate undefined(f, x), which should just express that x !e dom(f) [which depends on exactly 2 "parameters"].
> > >
> > > Of course, if we have
> > >
> > > Undefined(f, 1, dom(f), codom(f))
> > >
> > > and
> > >
> > > ~Undefined(g, 1, dom(g), codom(g)),
> > >
> > > we can get a contradiction from the assumtion f = g (and the "substitution axiom").
> > >
> > There is no dom or codom operator in DC Proof

> and hence no NOTION of "the domain of f" and "the codomain of f" (where f is a function)
>
> > [UNLIKE as in almost all] math textbooks [which refer to /functions/].
>
> Actually, (at least) some "function axioms" like the following would be required in your system
>
> function(f, X, Y) <-> function(f) & dom(f) = X & codom(f) = Y
> function(f, X, Y) -> Ax(x e X -> f(x) e Y).
> function(f) -> (undefined(f, x) <-> x !e dom(f))

Other than for generating some of your most cherished wonky results (e.g. your "dark elements?"), there doesn't seem to be any real need to formally define domain and codomain operators. (This may even be a good argument for NOT having them.) Textbook authors like Terence Tao would seem to agree.

>
> to be able to formalize standard math claims more or less "directly".
>
> Here "function(f, X, Y)" would stand for "f : X --> Y" from standard math.
>

I have an "is-a-function" predicate among other things that are generated by using the Function Axiom. It is used only for establishing equality of functions with the same domain and codomain.

> Hint: If Tao mentions (considers) a function "f: X --> Y" and talks about "the domain of f", he's talking about X.

But he doesn't formally define any domain operators. Must be frustrating as hell for you.

[Fritz Feldhase]

On Thursday, October 6, 2022 at 2:08:45 AM UTC+2, Dan Christensen wrote:

> But he doesn't formally define any domain operators.

HOLY SHIT! <FACEPALM>

FUCK OFF, YOU SILLY CRANK!

YOU ARE WAY TOO DUMB FOR MATH.

[Fritz Feldhase]

On Thursday, October 6, 2022 at 1:49:58 AM UTC+2, Fritz Feldhase wrote:

> :

> 13. Undefined(f, s0, s0, 1) & ~Undefined(g, s0, s0, 1)
> from 10. and 12.

Now from the assumtion f = g [from substitution] we would either get Undefined(f, s0, s0, 1) & Undefined(g, s0, s0, 1) or ~Undefined(f, s0, s0, 1) & ~Undefined(g, s0, s0, 1), but neither Undefined(f, s0, s0, 1) & ~Undefined(g, s0, s0, 1) nor ~Undefined(f, s0, s0, 1) & Undefined(g, s0, s0, 1)

14. f = g
Assumption

15. Undefined(g, s0, s0, 1) & ~Undefined(g, s0, s0, 1)
from 13. and 14 with substitution

15. ~f = g
from 14. and 15. by RAA.

qed

Remember, the claim by MC was:

| Take f : {0} -> {0}, f(x)=x, and g:{0,1} -> {0,1}, g(x) =1-x,
| we get immediately:
|

| Undefined(f,s0,s0,1) ~Undefined(g,s0,s0,1)
|
| And therefore:
|
| f=\=g
|

| This is a case where we showed two functions inequal,

| with different domain and codomain. The function
| axiom of DC Spoiled cannot do that.

Indeed. Though the following is rather a truism for Tao:

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

Hint: That f =/= g can "formally" be deduced from dom(f) =/= dom(g) (with Tao's substitution axiom).

[Mostowski Collapse]

Moron, you don't need s01. Whats wrong with you?

Can't you even prove these two:

Undefined(f,s0,s0,1)
~Undefined(g,s0,s0,1)

They only need ~1 e s0. 0 e s0, f(0) e s0, ~g(0) e s0.

[Mostowski Collapse]

Here is the full proof, wonky man:

81 ~f=g
Conclusion, 78

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

1 ALL(x):[x ε s0 <=> x=0]
Axiom

2 ~1=0
Axiom

3 f(0)=0
Axiom

4 g(0)=1
Axiom

5 ALL(f):ALL(dom):ALL(cod):ALL(a):[Undefined(f,dom,cod,a) <=> ALL(b):[b

ε dom => f(b) ε cod] & ~a ε dom]
Axiom

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

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

8 ALL(a):[Undefined(f,s0,s0,a) <=> ALL(b):[b ε s0 => f(b) ε s0] & ~a ε s0]
U Spec, 7

9 Undefined(f,s0,s0,1) <=> ALL(b):[b ε s0 => f(b) ε s0] & ~1 ε s0
U Spec, 8

10 [Undefined(f,s0,s0,1) => ALL(b):[b ε s0 => f(b) ε s0] & ~1 ε s0]
& [ALL(b):[b ε s0 => f(b) ε s0] & ~1 ε s0 => Undefined(f,s0,s0,1)]
Iff-And, 9

11 Undefined(f,s0,s0,1) => ALL(b):[b ε s0 => f(b) ε s0] & ~1 ε s0
Split, 10

12 ALL(b):[b ε s0 => f(b) ε s0] & ~1 ε s0 => Undefined(f,s0,s0,1)
Split, 10

13 EXIST(b):[b ε s0 & ~f(b) ε s0]
Premise

14 u ε s0 & ~f(u) ε s0
E Spec, 13

15 u ε s0
Split, 14

16 ~f(u) ε s0
Split, 14

17 u ε s0 <=> u=0
U Spec, 1

18 [u ε s0 => u=0] & [u=0 => u ε s0]
Iff-And, 17

19 u ε s0 => u=0
Split, 18

20 u=0 => u ε s0
Split, 18

21 u=0
Detach, 19, 15

22 ~f(0) ε s0
Substitute, 21, 16

23 ~0 ε s0
Substitute, 3, 22

24 0 ε s0 <=> 0=0
U Spec, 1

25 [0 ε s0 => 0=0] & [0=0 => 0 ε s0]
Iff-And, 24

26 0 ε s0 => 0=0
Split, 25

27 0=0 => 0 ε s0
Split, 25

28 0=0
Reflex

29 0 ε s0
Detach, 27, 28

30 0 ε s0 & ~0 ε s0
Join, 29, 23

31 ~EXIST(b):[b ε s0 & ~f(b) ε s0]
Conclusion, 13

32 ~~ALL(b):~[b ε s0 & ~f(b) ε s0]
Quant, 31

33 ALL(b):~[b ε s0 & ~f(b) ε s0]
Rem DNeg, 32

34 ALL(b):~~[b ε s0 => ~~f(b) ε s0]
Imply-And, 33

35 ALL(b):[b ε s0 => ~~f(b) ε s0]
Rem DNeg, 34

36 ALL(b):[b ε s0 => f(b) ε s0]
Rem DNeg, 35

37 1 ε s0
Premise

38 1 ε s0 <=> 1=0
U Spec, 1

39 [1 ε s0 => 1=0] & [1=0 => 1 ε s0]
Iff-And, 38

40 1 ε s0 => 1=0
Split, 39

41 1=0 => 1 ε s0
Split, 39

42 ~1=0 => ~1 ε s0
Contra, 40

43 ~1 ε s0
Detach, 42, 2

44 1 ε s0 & ~1 ε s0
Join, 37, 43

45 ~1 ε s0
Conclusion, 37

46 ALL(b):[b ε s0 => f(b) ε s0] & ~1 ε s0
Join, 36, 45

47 Undefined(f,s0,s0,1)
Detach, 12, 46

48 ALL(dom):ALL(cod):ALL(a):[Undefined(g,dom,cod,a) <=> ALL(b):[b ε dom
=> g(b) ε cod] & ~a ε dom]
U Spec, 5

49 ALL(cod):ALL(a):[Undefined(g,s0,cod,a) <=> ALL(b):[b ε s0 => g(b) ε
cod] & ~a ε s0]
U Spec, 48

50 ALL(a):[Undefined(g,s0,s0,a) <=> ALL(b):[b ε s0 => g(b) ε s0] & ~a ε s0]
U Spec, 49

51 Undefined(g,s0,s0,1) <=> ALL(b):[b ε s0 => g(b) ε s0] & ~1 ε s0
U Spec, 50

52 [Undefined(g,s0,s0,1) => ALL(b):[b ε s0 => g(b) ε s0] & ~1 ε s0]
& [ALL(b):[b ε s0 => g(b) ε s0] & ~1 ε s0 => Undefined(g,s0,s0,1)]
Iff-And, 51

53 Undefined(g,s0,s0,1) => ALL(b):[b ε s0 => g(b) ε s0] & ~1 ε s0
Split, 52

54 ALL(b):[b ε s0 => g(b) ε s0] & ~1 ε s0 => Undefined(g,s0,s0,1)
Split, 52

55 ~[ALL(b):[b ε s0 => g(b) ε s0] & ~1 ε s0] => ~Undefined(g,s0,s0,1)
Contra, 53

56 ALL(b):[b ε s0 => g(b) ε s0]
Premise

57 0 ε s0 => g(0) ε s0
U Spec, 56

58 0 ε s0 <=> 0=0
U Spec, 1

59 [0 ε s0 => 0=0] & [0=0 => 0 ε s0]
Iff-And, 58

60 0 ε s0 => 0=0
Split, 59

61 0=0 => 0 ε s0
Split, 59

62 0=0
Reflex

63 0 ε s0
Detach, 61, 62

64 g(0) ε s0
Detach, 57, 63

65 1 ε s0
Substitute, 4, 64

66 1 ε s0 <=> 1=0
U Spec, 1

67 [1 ε s0 => 1=0] & [1=0 => 1 ε s0]
Iff-And, 66

68 1 ε s0 => 1=0
Split, 67

69 1=0 => 1 ε s0
Split, 67

70 ~1=0 => ~1 ε s0
Contra, 68

71 ~1 ε s0
Detach, 70, 2

72 1 ε s0 & ~1 ε s0
Join, 65, 71

73 ~ALL(b):[b ε s0 => g(b) ε s0]
Conclusion, 56

74 ~ALL(b):[b ε s0 => g(b) ε s0] | 1 ε s0
Arb Or, 73

75 ~[~~ALL(b):[b ε s0 => g(b) ε s0] & ~1 ε s0]
DeMorgan, 74

76 ~[ALL(b):[b ε s0 => g(b) ε s0] & ~1 ε s0]
Rem DNeg, 75

77 ~Undefined(g,s0,s0,1)
Detach, 55, 76

78 f=g
Premise

79 Undefined(g,s0,s0,1)
Substitute, 78, 47

80 ~Undefined(g,s0,s0,1) & Undefined(g,s0,s0,1)
Join, 77, 79

81 ~f=g
Conclusion, 78

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

[Fritz Feldhase]

On Thursday, October 6, 2022 at 2:25:36 AM UTC+2, Mostowski Collapse wrote:

> Moron, you don't need s01. Whats wrong with you?

Well, on the other hand, the axioms

0 e s0
1 !e s0

and

0 e s01
1 e s01

won't hurt, even if the latter 2 axioms are not really needed. [Though in my little proof, I did refer to s01 and one of these axioms.]

After all, we may (informally) assume that s0 = {0} and s01 = {0, 1}; espacially, if we (informally) assume that s0 is the domain of f and s01 is the domain of g.

Hmmm... In this case, I'd prefer the axioms

0 e s0 & Ax(x =/= 0 -> x !e s0)

and

0 e s01 & 1 e s01 & Ax(x =/= 0 & x =/= 1 -> x !e s01)

This way we've completely characterized s0 and s01 (at least in the context of pure set theory).

Well, in the context of DC Spoof we might (should?) even state these axioms the follwoing way:

Set(s0) & 0 e s0 & Ax(x =/= 0 -> x !e s0)

and

Set(s01) & 0 e s01 & 1 e s01 & Ax(x =/= 0 & x =/= 1 -> x !e s01)

Just my 2 cents.

P.S. Anyway, we managed to prove f =/= g as required (I'd say).

[Dan Christensen]

On Wednesday, October 5, 2022 at 8:13:26 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, October 6, 2022 at 2:08:45 AM UTC+2, Dan Christensen wrote:
>
> > But he doesn't formally define any domain operators.

[snip childish abuse]

Where does Tao formally define a domain and codomain operator?

[Mostowski Collapse]

Well since the goal is to first prove:

47 Undefined(f,s0,s0,1)
Detach, 12, 46

77 ~Undefined(g,s0,s0,1)
Detach, 55, 76

Based on wonky mans "right" definition:

5 ALL(f):ALL(dom):ALL(cod):ALL(a):[Undefined(f,dom,cod,a) <=> ALL(b):[b

ε dom => f(b) ε cod] & ~a ε dom]
Axiom

s01 falls out of the proof, unless you construct f and g
with wonky mans function axiom. But I scrapped from
f and g only what was need for the proof:

3 f(0)=0
Axiom

4 g(0)=1
Axiom

[Mostowski Collapse]

This crankness of wonky man, is on par with AP brain farto,
who thinks his ellipses are oval. Now we have wonky man,
who thinks he doesn't need set theory, and he also thinks

set theory is nowhere used in mathematics. But on the
first problem of formalizing his saying:

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

The result is a cloud of chaos with insane claims, like
Undefined(_,_,_,_) bla bla over Undefined(_,_), and we
see befor our eyes, cards houses erect and crashing

into itself, none of his silly depositions are true!

What is your scientific method, wonky man?

[Fritz Feldhase]

On Thursday, October 6, 2022 at 2:49:42 AM UTC+2, Mostowski Collapse wrote:

> s01 falls out of the proof, unless you construct f and g
> with wonky mans function axiom.

Hmmm... Don't think that wonky man's "function axiom" is needed in my proof.

(In accordance with your informal explanation "Take f : {0} -> {0}, f(x)=x, and g:{0,1} -> {0,1}, g(x) =1-x, ...") I just stated the axioms:

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

7. ALL(a):[a in s01 => g(a) = 1 - a]
Axiom

7a. 1 - 0 = 1
Axiom [actually an arithmetic theorem]

That should suffice (in addition with the axioms concerning 0, 1, s0 and s01).

But I have to admit that I'm too lazy to do that proof with DC Spoof. Sorry, about that.

So 2 different proofs (if so), with slightly different "assumptions" (conditions, expecially concerning g), which both lead to the result f =/= g.

Good enough for me.

[Mostowski Collapse]

DC Spoiled, DC Spoof, its soon Halloween,

its must be DC Spooky!

The only tool that a person has ever built, to not
prove something, but to constantly refute himself.
(Somehow computers were also invented for that,

like the astronomer that takes his telescope and
points to the sky, and doesn't find the planet according
to his hand calculations, DC Spookies is real

meaning of live, is to debunk wonky man)