How difficult is contraposition for DC Proof and Dan Christensen?

[Mostowski Collapse]

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

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

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

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

A <=> B

Can be separated into:

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

Or alternatively separated into:

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

LoL

[Mostowski Collapse]

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

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

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

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

LMAO!

[Dan Christensen]

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

From DC Proof:

1. A => B
Premise

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

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

I hope this helps.

Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[Mostowski Collapse]

And why cant you answer this question:

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

(SameDomCod => Postive_Def)

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

(~SameDomCod => Negative_Def)

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

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

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

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

[Mostowski Collapse]

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

but more explicit:

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

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

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

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

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

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

[Dan Christensen]

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

[snip text already addressed here]

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

[Mostowski Collapse]

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

(SameDomCod => Postive_Def)

What about the other direction <=, as contraposition:

(~SameDomCod => Negative_Def)

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

should be equal if we have:

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

Or written as:

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

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

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

A = {f1, f2, f3}

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

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

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

[Dan Christensen]

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

As required.

A and B are not function spaces. You need another example.

[snip]

[Mostowski Collapse]

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

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

{f1, f2, f3} ⊆ F

{f1, f2, f3, f4} ⊆ F

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

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

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

LoL

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

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

[Dan Christensen]

On Wednesday, September 7, 2022 at 7:10:36 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 8. September 2022 um 00:55:21 UTC+2:
> > On Wednesday, September 7, 2022 at 3:38:56 PM UTC-4, Mostowski Collapse wrote:
> > > Well the built-in axiom only covers the direction =>:
> > >
> > > (SameDomCod => Postive_Def)
> > >

> > As required.

> > > What about the other direction <=, as contraposition:
> > >
> > > (~SameDomCod => Negative_Def)
> > >
> >
> >
> > > There seems to be a sever gap in DC Proof, which has

> > > consequences for function spaces. If you have two <------------------------ Here

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

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

Still grasping at straws, Jan Burse? You said nothing about a union of function spaces. You said, "If you have two function spaces F and G..."

And your redefinition of F is certainly NOT a function space.

> {f1, f2, f3} ⊆ F
>
> {f1, f2, f3, f4} ⊆ F
>

Maybe you didn't know, but:

"In mathematics, a function space is a set of functions between two fixed sets."
https://en.wikipedia.org/wiki/Function_space

> Do you think function spaces are something to
> put into a vitrine and only look at? They can be
>
> used like any other set.

[snip abuse]

I know what is and is not a function space.

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

Still not function spaces, Jan Burse. Try again.

[Mostowski Collapse]

Pitty DC Proof cannot prove:

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

LoL

[Dan Christensen]

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

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

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

[Dan Christensen]

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

See full, formal proof at sci.logic

[Mostowski Collapse]

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

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

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

Where the function equality axiom of Dan Christensen gives me:

f1 = f2

Simple example:

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

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

Mostowski Collapse schrieb am Donnerstag, 8. September 2022 um 02:00:09 UTC+2:
> Pitty DC Proof cannot prove:
>
> Proposition: 4.2.5 If A is a set and F : A -> B then F is a set.

> http://www1.maths.leeds.ac.uk/~rathjen/book.pdf
>
> LoL
https://groups.google.com/g/sci.logic/c/UGlOyyBYVLU/m/Lv4mduDABAAJ

[Mostowski Collapse]

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

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

Therefore:

f1 =\= f2.

LoL

[Dan Christensen]

See my reply just now to your identical postings at sci.logic

Dan

On Friday, September 9, 2022 at 10:28:05 AM UTC-4, Mostowski Collapse wrote:
> The problem with your higher order substitution, the

[snip childish abuse]

[Dan Christensen]

See my replies to your identical postings at sci. logic

Dan

On Friday, September 9, 2022 at 2:39:24 PM UTC-4, Mostowski Collapse wrote:
> A formula A(_) that does the discrimination is relatively
> easy.

[snip]

[Dock Biondi]

Mostowski Collapse wrote:

> Or alternatively separated into: (A => B) & (~A => ~B) LoL

in fake_money shithole switzerland you can get 3 years in prison for
screwing too much for heat in your radiator. It just tells how much gas
and oil these wankers stole from Russia.

[Mostowski Collapse]

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

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

Can you prove in DC Spoiled this standard theorem:

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

[Dan Christensen]

See my reply just now to your identical posting at sci.logic

Dan

[Mostowski Collapse]

You can introduce this axiom:

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

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

the favorite form of definition for the genius Dan Christensen:

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

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

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

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

to prove function inequality, like this:

f =/= g

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

but I guess using UNDEFINED works also.

[Dan Christensen]

See my reply just now to your identical posting at sci.logic

Dan

On Saturday, October 1, 2022 at 9:08:09 PM UTC-4, Mostowski Collapse wrote:
> You can introduce this axiom:
>
> 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Present(h,x) <=> x ε dom]]
> Axiom
>

[snip]

[Mostowski Collapse]

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

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

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

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

are in the special liking scope of Dan Christiansen):

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

We can then prove as expected:

29 ~f=g
Conclusion, 26

[Dan Christensen]

On Sunday, October 2, 2022 at 5:11:55 AM UTC-4, Mostowski Collapse wrote:
[snip]

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

Missing arguments. Should be "Undefined(h,dom,cod,x)". That should solve your problem.

[Burt Rotolo]

Dan Christensen wrote:

> On Sunday, October 2, 2022 at 5:11:55 AM UTC-4, Mostowski Collapse
> wrote: [snip]

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

> Missing arguments. Should be "Undefined(h,dom,cod,x)". That should solve
> your problem.

you two nazis are committing *state_terrorism* blowing up costly and
essential pipelines in other countries, which are not yours. You
disgusting worthless criminals.

[Fritz Feldhase]

On Sunday, October 2, 2022 at 6:49:09 PM UTC+2, Dan Christensen wrote:
> On Sunday, October 2, 2022 at 5:11:55 AM UTC-4, Mostowski Collapse wrote:
> >
> > 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]]
> > Axiom
> >

> Missing arguments. <bla>

Nothing is missing, you silly idiot - except your brain.

[Dan Christensen]

So, have you "volunteered" to die in Ukraine for Putin's massive ego, Nazi boy?

[Dan Christensen]

On Sunday, October 2, 2022 at 2:16:06 PM UTC-4, Fritz Feldhase wrote:
> On Sunday, October 2, 2022 at 6:49:09 PM UTC+2, Dan Christensen wrote:
> > On Sunday, October 2, 2022 at 5:11:55 AM UTC-4, Mostowski Collapse wrote:
> > >
> > > 5 ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]]
> > > Axiom
> > >

> > Missing arguments. Should be "Undefined(h,dom,cod,x)". That should solve your problem.
>

> Nothing is missing

[snip childish abuse]

Wrong again, Fritz. The arguments for domain and codomain are missing. I'm beginning to think he did it on purpose so he could get that wonky result of his.

[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 a pussy

that cannot live the consequences of his doing. The consequences
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:47:12 PM UTC-4, Mostowski Collapse wrote:
[snip]

>

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

It would enable you to avoid your wonky result, Jan Burse. Clearly, for some bizarre reason, you WANT a wonky result.

Oh, well... I tried.

[Fritz Feldhase]

On Sunday, October 2, 2022 at 11:32:22 PM UTC+2, Dan Christensen wrote:
> On Sunday, October 2, 2022 at 3:47:12 PM UTC-4, Mostowski Collapse wrote:
> >
> > Defining "Undefined(f,x,dom,cod)" is nowhere required.
> >

> It would enable you to avoid your [...] result, Jan Burse.

Wow, what a silly comment. :-)

Yeah, defining primes as "all odd natural numbers such that ..." would also enable us to avoid many results in number theory. *lol*

Are you demented, Dan?

> Clearly, for some [...] reason, you WANT [your] result.

Indeed! After all, the "result" is a _formal proof_ for Tao's claim:

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

[Dan Christensen]

On Sunday, October 2, 2022 at 6:11:10 PM UTC-4, Fritz Feldhase wrote:
> On Sunday, October 2, 2022 at 11:32:22 PM UTC+2, Dan Christensen wrote:
> > On Sunday, October 2, 2022 at 3:47:12 PM UTC-4, Mostowski Collapse wrote:
> > >
> > > Defining "Undefined(f,x,dom,cod)" is nowhere required.
> > >

> > It would enable you to avoid your wonky result, Jan Burse. Clearly, for some bizarre reason, you WANT a wonky result. Oh, well... I tried.
>

> Wow, what a silly comment.

How about:

1. Function(f,s0,s0)
Axiom

2. Function(g,s01,s01)
Axiom

3. 1 in s01
Axiom

4. ~1 in s0
Axiom

Tweaking your definition just a bit, we have...

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

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

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

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

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

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

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

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

13. ~1 in 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 in dom]]
U Spec, 5

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

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

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

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

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

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

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

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

24. 1 in 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! Your wheels just fell off. On the very last line, too! Those pesky domain and codomain parameters!

:^( <---Jan ("Boo, hoo!")

:^( <--- Fritz ("F********************K!!!!")

[Fritz Feldhase]

On Monday, October 3, 2022 at 1:52:18 AM UTC+2, Dan Christensen wrote:

> Tweaking your definition just a bit

rendering it nonsensical and hence useless (for the task at hand).

Remember: You asked for a _formal proof_ supporting Tao's claim:

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

Hint: We do not need the notion "undefined" for that.

Actually, the simple fact

1 !e dom(f) & 1 e dom(g) [and hence dom(f) =/= dom(g)]

will suffice, you silly asshole.

Hint: If dom(f) =/= dom(g), then f =/= g: "f and g are not [...] the same function, f =/= g, because they have different domains." (Terence Tao)

[Fritz Feldhase]

On Monday, October 3, 2022 at 3:32:07 AM UTC+2, Fritz Feldhase wrote:

> Actually, the simple fact
>
> 1 !e dom(f) & 1 e dom(g) [and hence dom(f) =/= dom(g)]
>
> will suffice, you silly asshole.
>

> Hint: If dom(f) =/= dom(g), then f =/= g. [Tao: "f and g are not [...] the same function, f =/= g, because they have different domains."]

Look, dumbo: the substitution axiom implies:

if f = g, then dom(f) = dom(g).

Hence by contraposition we get:

if dom(f) =/= dom(g), then f =/= g.

Not that hard, is it?

[Dan Christensen]

On Sunday, October 2, 2022 at 9:32:07 PM UTC-4, Fritz Feldhase wrote:
> On Monday, October 3, 2022 at 1:52:18 AM UTC+2, Dan Christensen wrote:
>
> > Tweaking your definition just a bit
> rendering it nonsensical and hence useless (for the task at hand).
>

That task being to produce a wonky result from a flawed definition? You did accomplish that much!

Here is the original wonky definition from Jan Burse (aka Mr. Collapse) that leads to another wonky result:

ALL(h):ALL(dom):ALL(cod):[Function(h,dom,cod) => ALL(x):[Undefined(h,x) <=> ~x ε dom]] -----> f=/=g

Corrected version:

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

Note: Defining an "Undefined" predicate in the first place, is not really necessary. If you want to say that a function f: X --> Y is undefined for some element in x0 in its domain, you need only write "ALL(a):[a in X => f(a) in Y] & ~x0 in X."

Only by ignoring the parameters for the domain (dom) and codomain (cod) sets was it possible to obtain his required wonky result. Really kind of sad. And soooooo transparent.

> Remember: You asked for a _formal proof_ supporting Tao's claim:
> | "f and g are not [...] the same function, f =/= g, because they have different domains."

Again, very disingenuous, Fritz. In your desperation, you were hanging your hat on some informal commentary by Tao that even he suggests could, strictly speaking, be seen as "careless." (In the same paragraph). In your desperation, you were hoping that he was actually disavowing his formal definition:

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

In your desperation, you were hoping that this definition did NOT actually mean that, strictly speaking, we can determine whether f=g or f=/=g ONLY IF their domain and codomain sets are the same.

Soooooo VERY pathetic, Fritz.

Alas your silly little project has now blown up in your face. Don't you feel silly? Put an end to it and just admit you were wrong and I was right.

[Dan Christensen]

It seems you can only obtain the required wonky result if you ignore certain critical parameters, i.e. the domain and codomain sets. Oh, well...

[Fritz Feldhase]

On Monday, October 3, 2022 at 4:40:53 AM UTC+2, Dan Christensen wrote:
> On Sunday, October 2, 2022 at 10:14:50 PM UTC-4, Fritz Feldhase wrote:
> > On Monday, October 3, 2022 at 3:32:07 AM UTC+2, Fritz Feldhase wrote:
> > >
> > > Actually, the simple fact
> > >
> > > 1 !e dom(f) & 1 e dom(g) [and hence dom(f) =/= dom(g)]
> > >
> > > will suffice, you silly asshole.
> > >
> > > Hint: If dom(f) =/= dom(g), then f =/= g. [Tao: "f and g are not [...] the same function, f =/= g, because they have different domains."]
> >
> > Look, dumbo: the substitution axiom implies:
> >
> > if f = g, then dom(f) = dom(g).
> >
> > Hence by contraposition we get:
> >
> > if dom(f) =/= dom(g), then f =/= g.
> >
> > Not that hard, is it?
> >

> It seems you can only obtain the required [...] result if you ignore certain critical parameters, i.e. the domain and codomain sets.

Huh?! Did you take drugs, or what?

Hint: We obtain the "required result" by explicitly taking into account the domains of f and g [taking into account the codomains of f and g is not necessary in this case].

Again: "f and g are not [...] the same function, f =/= g, ___because they have different domains___." (Terence Tao, Analysis I)

[Dan Christensen]

On Sunday, October 2, 2022 at 10:58:19 PM UTC-4, Fritz Feldhase wrote:

> > It seems you can only obtain the required [...] result if you ignore certain critical parameters, i.e. the domain and codomain sets.
>

[snip childish abuse]

>
> Hint: We obtain the "required result" by explicitly taking into account the domains of f and g [taking into account the codomains of f and g is not necessary in this case].

Pay attention, Fritz.

Your definition of "Undefined" here leads to the wonky result that f=/=g:

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

When you define "Undefined(h,x)" as here, you are saying that the truth value of "Undefined" depends ONLY on h and x. And that it is independent of other variables. That is where you went wrong. It is ALSO dependent of the variables dom and cod. You can't deny it. When you ignore this, as you do, you get the wonky result that f=/=g. That is why you need the additional parameters--to avoid such nonsensical results.

>
> Again: "f and g are not [...] the same function, f =/= g, ___because they have different domains___." (Terence Tao, Analysis I)

Already debunked here. (Scroll up) Why must you keep repeating your failed arguments?

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

On Monday, October 3, 2022 at 2:44:05 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 don't), I recommend defining the following abbreviation:

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

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

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

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

> (From DC Proof in dcpsetup17.exe)
>

As in Terence Tao's definition of function:

"Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range are said to be equal, f = g [with respect to the domain X], if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values of x, but not others, then we do not consider f and g to be equal.)"

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

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

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

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

Dan

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

[Fritz Feldhase]

On Monday, October 3, 2022 at 7:12:55 PM UTC+2, Dan Christensen wrote:
>
> 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.

Then something is missing in your "system", you silly idiot!

After all, Tao states: "f and g are not [...] the same function, f =/= g, ___because they have different domains___." (Terence Tao, Analysis I)

[Dan Christensen]

On Monday, October 3, 2022 at 1:28:28 PM UTC-4, Fritz Feldhase wrote:
> On Monday, October 3, 2022 at 7:12:55 PM UTC+2, Dan Christensen wrote:
> >
> > 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.

[snip childish abuse]

>
> After all, Tao states: "f and g are not [...] the same function, f =/= g, ___because they have different domains___." (Terence Tao, Analysis I)

Again, please read the rest of the paragraph for the context, Fritz. You can't seriously be suggesting that Tao is renouncing his formal definition. You can't be THAT desperate, can you?

"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

Again, it is clear from this definition that we can determine that functions are equal or not ONLY when they have the same domains and codomains.

Dan

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

[Dan Christensen]

On Monday, October 3, 2022 at 1:12:55 PM UTC-4, Dan Christensen wrote:
> On Monday, October 3, 2022 at 2:44:05 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 don't), I recommend defining the following abbreviation:
>
> ALL(f):ALL(dom):ALL(cod):ALL(x):[Undefined(f,dom,cod,x) <=> ALL(a):[a in f => f(a) in dom] & ~x in dom]
>

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

[Mostowski Collapse]

Dan Christensen halucinated:

Dan Christensen schrieb am Montag, 3. Oktober 2022 um 20:30:45 UTC+2:
> 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.

https://groups.google.com/g/sci.logic/c/InGcDaFcuKE/m/LbM9ZJFvAQAJ

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]

See my reply just now to your nearly identical posting at sci.logic.

Dan

On Monday, October 3, 2022 at 6:55:04 PM UTC-4, Mostowski Collapse wrote:

[snip childish abuse]

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

[snip]

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

On Wednesday, October 5, 2022 at 3:15:50 AM UTC-4, Mostowski Collapse wrote:
> 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)
>

[snip nonsense]

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

Dan

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

[Mostowski Collapse]

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

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

See my reply just now to your identical posting at sci.logic

Dan

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

[Dan Christensen]

On Wednesday, October 5, 2022 at 8:44:09 PM UTC-4, Mostowski Collapse wrote:
> 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
>

[snip]

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

Umm... you have 2 functions with the SAME domain and codomain. And you have f(0)=/=g(0), so, by the definition of function equality, we can determine that f=/=g. But the whole point of this exercise was to compare functions with DIFFERENT domains or codomains.

Try again, Jan Burse.

[Fritz Feldhase]

On Thursday, October 6, 2022 at 3:35:00 AM UTC+2, Dan Christensen wrote:

> Umm... you have 2 functions with the SAME domain and codomain. And <bla>

Nonsense.

[Dan Christensen]

On Wednesday, October 5, 2022 at 8:44:09 PM UTC-4, Mostowski Collapse wrote:

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

[snip]

Better might be:

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

This would force the user to first establish the domain and codomain of the function in question.

[Mostowski Collapse]

Well you will become known as introducing the concept
of "critical parameter" to logic. BTW: Never heard of such!

Its more that you are often toning up. Your collaboration
with sci.logic always runs always by the same pattern:

- [snip childish abuse and nonsense]
- Otherwise, you can get some quite wonky results
- is pissed off that I pointed out and presented two different ways
- Pay attention, Try again (Hee Hee)
- It seems obvious to me, and, I would think, to anyone with any kind of math background. Oh, well ...
- Must be frustrating as hell for you.
-

With ultimately, after weeks and weeks:

- Hm, yes, I have to retract
-

And then the circle of life of DC Spooky begins again.
Old habits never die, isn't it wonky man?

LoL

[Mostowski Collapse]

Lets say I define square number (working in natural numbers):

SquareNumber(x) :<=> EXIST(y):[y*y = x]

Is this wrong because I didn't define:

SquareNumber(y,x) :<=> y*y = x

Forgot the critical parameter y?

LMAO!

[Dan Christensen]

See my reply just now to your identical posting as sci.logic.

Dan

On Thursday, October 6, 2022 at 10:55:42 AM UTC-4, Mostowski Collapse wrote:
> Lets say I define square number (working in natural numbers):
>
> SquareNumber(x) :<=> EXIST(y):[y*y = x]
>
> Is this wrong because I didn't define:
>
> SquareNumber(y,x) :<=> y*y = x
>

[snip]

[Mostowski Collapse]

There was no reply, you only changed topic. You
didn't read what I wrote: (working in natural numbers)

We still don't know what you mean by critical parameter:
- Is a critical parameter an extrinsic parameter
- Is a critical parameter an intrinsic parameter

The words "extrinsic" and "intrinsic" have a meaning, see
your stackoverflow question about surjectivity and

set theory. Does "critical" also have a mening?

[Mostowski Collapse]

ju...@diegidio.name schrieb am Sonntag, 20. Juni 2021 um 16:19:11 UTC+2:
> Let U be the universe of all numbers.

Thats something for wonky man. He also makes a recurring
error to start modelling the universe of discourse, as a
set inside the universe of disourse.

As soon as you do that, it seems you have elements that
then jump out of your universe of discourse. Assume you want
to have a universe of discourse of natural numbers, but

you make the error to also introduce sets of natural numbers,
etc.. etc.., i.e. you go a little bit too far what you otherwise
allow in your universe of discourse. Eh volia, you

open pandoras box:

/* Previous Result http://www.dcproof.com/UniversalSet.htm */
1 ALL(s):[Set(s) => EXIST(a):~a ε s]
Axiom

2 Set(nat)
Axiom

3 Set(nat) => EXIST(a):~a ε nat
U Spec, 1

4 EXIST(a):~a ε nat
Detach, 3, 2

Oopsi, what is this thing outside of N?

Whats is the classical way, for example in FOL, to not
be subject of this paradox, the wonky man paradox?

[Dan Christensen]

On Friday, October 7, 2022 at 8:02:09 PM UTC-4, Mostowski Collapse wrote:
> ju...@diegidio.name schrieb am Sonntag, 20. Juni 2021 um 16:19:11 UTC+2:
> > Let U be the universe of all numbers.
>
> Thats something for wonky man. He also makes a recurring
> error to start modelling the universe of discourse, as a
> set inside the universe of disourse.
>
> As soon as you do that, it seems you have elements that
> then jump out of your universe of discourse.

Wrong again, Jan Burse. Maybe you are confusing math with philosophy, but, again, in mathematics there is rarely if ever a notion of an overarching domain (or universe) of discourse. Just admit your were wrong, Jan Burse. Yes, I know, you would rather die. Oh, well...

Dan

[Urbano Stilo]

he is a development country.

[Mostowski Collapse]

The problem is you don't know what FOL is. Your
DC Spoiled is not FOL. And you cannot prove this
FOL theorem, namely the Drinker Paradox:

/* Not Provable in DC Spoiled, but Provable in FOL */
∃x(D(x) => ∀yD(y))

FOL is a modern development between 1900 - 1950.
In this periods a couple of publications appeared which
started classifying logics more clearly. One booklet

was Hilbert & Ackermann, Grundzüge der Theoretischen
Logik, which defined more clearly what FOL is. But you
find it also here in Gödels lecture, the simplest logics are:

1.1 Propositional logic
1.2 Predicate logic
Logic Lectures: Gödel's Basic Logic Course at Notre Dame
https://arxiv.org/abs/1705.02601

Neither of them can quatify function symbols as
DC Spoiled does. His lecture has a critical tone, and
you find sections like "Failure of traditional logic". First

thing Gödel does is this here:

1.2.5 Theorems and derived rules of the system for predicate logic
[74] ∀xPhi(x) ⊃ ∃xPhi(x) Syllogism

Which doesn't work in empty domain.

LoL

[Dan Christensen]

On Saturday, October 8, 2022 at 5:01:25 PM UTC-4, Mostowski Collapse wrote:
[snip]

> /* Not Provable in DC Proof, but Provable in FOL */
> ∃x(D(x) => ∀yD(y))
>

Maybe that's some consolation for the fact that there is no assumption of a non-empty domain of discussion in math textbooks. Must be frustrating as hell for you, but it just isn't required in mathematics.

In DC Proof, as in most math textbooks, however, we have the set-theoretic equivalent:

EXIST(x):[ x in d=> ALL(y):y in d]

What's more, the consequent can be ANY proposition whatsoever. Deal with it, Jan Burse.

[Michel Marconi]

Dan Christensen wrote:

> On Saturday, October 8, 2022 at 5:01:25 PM UTC-4, Mostowski Collapse
> wrote:[snip]
>
>> /* Not Provable in DC Proof, but Provable in FOL */
>> ∃x(D(x) => ∀yD(y))
>
> Maybe that's some consolation for the fact that there is no assumption
> of a non-empty domain of discussion in math textbooks. Must be
> frustrating as hell for you, but it just isn't required in mathematics.

your proofs shows up you don't know what a proof is. You are insignificant.

[Mostowski Collapse]

So you cannot proof in FOL with DC Proof:

/* Drinker Paradox, Not Provable in DC Proof, but Provable in FOL */
∃x(D(x) => ∀yD(y))

Right? Well I thought so, that you botched it.

[Mostowski Collapse]

Dan Christensen halucinated even more Sonntag, 9. Oktober 2022 um 00:21:58 UTC+2:

> What's more, the consequent can be ANY proposition whatsoever

https://groups.google.com/g/sci.math/c/hEQjzBmQIIw/m/T35rYRp8BQAJ

Thats just utter nonsense that makes it even worse,
and shows that you didn't understand the drinker paradox,
it obviously doesn't work for the Drinker Paradox.

You can try yourself:

∃x(Dx→Q) is invalid.
https://www.umsu.de/trees/#~7x%28D%28x%29~5Q%29

The point of the drinker paradox is exactly that Q is
not arbitary. Just check out the usual proof by cases,
where two cases are used. One of the cases needs that

Q is not arbitrary. What the hell are you doing wonky man?

For the two cases see here:

"The proof begins by recognising it is true that either
everyone in the pub is drinking (in this particular round
of drinks), or at least one person in the pub isn't drinking."
https://paradox.fandom.com/wiki/Drinker_paradox

[Mostowski Collapse]

Dan Christensen is currently banging his head in the
other direction. Although Set(U) and ALL(a):[a e U]
leads to a contradiction, on the other hand when we

use predicate symbols, this here isn't contradictory per se:

ALL(a):U(a)

It is even not related to empty domain issues. Its just
the fact that a predicate can be "full". It also
causes a counter model here:

∃x(Dx→Q) is invalid.
https://www.umsu.de/trees/#~7x%28D%28x%29~5Q%29

Another way to say "full", is to write ∀yD(y),
which is what makes the Drinker Paradox work,
namely that we don't have an arbitrary Q,

but that we have ∀yD(y). In the Drinker Paradox
you can translate "full" into "everybody
is drinking (in this round)".

[Dan Christensen]

On Saturday, October 8, 2022 at 6:44:49 PM UTC-4, Mostowski Collapse wrote:


> Dan Christensen schrieb am Sonntag, 9. Oktober 2022 um 00:21:58 UTC+2:
> > On Saturday, October 8, 2022 at 5:01:25 PM UTC-4, Mostowski Collapse wrote:
> > [snip]
> >
> > > /* Not Provable in DC Proof, but Provable in FOL */
> > > ∃x(D(x) => ∀yD(y))
> > >
> >
> > Maybe that's some consolation for the fact that there is no assumption of a non-empty domain of discussion in math textbooks. Must be frustrating as hell for you, but it just isn't required in mathematics.
> >
> > In DC Proof, as in most math textbooks, however, we have the set-theoretic equivalent:
> >
> > EXIST(x):[ x in d=> ALL(y):y in d]
> >
> > What's more, the consequent can be ANY proposition whatsoever. Deal with it, Jan Burse.

> So you cannot proof in FOL with DC Proof:
>
> /* Drinker Paradox, Not Provable in DC Proof, but Provable in FOL */
> ∃x(D(x) => ∀yD(y))
>

As in most math textbooks, in DC Proof there is no assumption of a non-empty domain of discourse. The rules of logic and axioms of set theory also do not postulate (explicitly or otherwise) the existence of any object(s), not even the empty set. As such, without additional assumptions or axioms, nothing can be proven be proven to exist. As soon as we postulate the existence of any set S, however, we can infer the existence of another object x such that if x is an element of S, then can infer any proposition whatever. Stated formally in the notation of DC Proof, we can have the theorem:

ALL(s):[Set(s) => EXIST(x):[x in s => Q]]

where Q is any proposition, be it true or false.

Q could, for example, be ALL(y):y in s, thus obtaining the set theoretic equivalent of your theorem.

[Dan Christensen]

On Saturday, October 8, 2022 at 7:07:04 PM UTC-4, Mostowski Collapse wrote:

[snip]

>

> You can try yourself:
>
> ∃x(Dx→Q) is invalid.
> https://www.umsu.de/trees/#~7x%28D%28x%29~5Q%29
>

[snip]

As I recall, that software does not have any kind of set theory built into it, so I don't know how useful it would be in evaluating:

ALL(s):[Set(s) => EXIST(x):[x in s => Q]]

To make it specific to your version of DP, you could substitute Q = ALL(y): y in s

[Mostowski Collapse]

ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is not the Drinker
paradox, you bilstering idiot. Its only the Russel paradox, so
that it shows an outside element, you need subset axiom

to prove it, you just replaced negation by more general => Q:

∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a¬Eas) is valid.
https://www.umsu.de/trees/#~6k~7u%28Su~1~6a%28Eau~4%28Eak~1~3Eaa%29%29%29~5~6s%28Ss~5~7a~3Eas%29

∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a(Eas → Qxs)) is valid.
https://www.umsu.de/trees/#~6k~7u%28Su~1~6a%28Eau~4Eak~1~3Eaa%29%29~5~6s%28Ss~5~7a%28Eas~5Qxs%29%29

S = your Set
E = your Membership
∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) = instance of Subset Axiom
∀s(Ss → ∃a¬Eas) = outside element
∀s(Ss → ∃a(Eas → Qxs)) = outside element again

It needs the Subset Axiom from some SET theory.
So its a proof in FOL+SET, you cannot prove it without SET, in FOL only:

∀s(Ss → ∃a¬Eas) is invalid.
https://www.umsu.de/trees/#~6s%28Ss~5~7a~3Eas%29

∀s(Ss → ∃a(Eas → Qxs)) is invalid.
https://www.umsu.de/trees/#~6s%28Ss~5~7a%28Eas~5Qxs%29%29

On the other hand the Drinker paradox works in FOL only:

∃a(Da → ∀bDb) is valid.
https://www.umsu.de/trees/#~7a%28Da~5~6bDb%29

Got it moron?

[Michel Marconi]

Dan Christensen wrote:

> On Saturday, October 8, 2022 at 7:07:04 PM UTC-4, Mostowski Collapse
> wrote:[snip]
>
>> You can try yourself:
>> ∃x(Dx→Q) is invalid. https://www.umsu.de/trees/#~7x%28D%28x%29~5Q%29
>>
> [snip]

you two are a nigga.

[Michel Marconi]

Mostowski Collapse wrote:

> ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is not the Drinker paradox,
> you bilstering idiot. Its only the Russel paradox, so that it shows an
> outside element, you need subset axiom
>
> to prove it, you just replaced negation by more general => Q:
>
> ∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a¬Eas) is valid.

are you a Dindo Nothen nigga?

[Dan Christensen]

On Sunday, October 9, 2022 at 4:56:01 AM UTC-4, Mostowski Collapse wrote:
> ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is not the Drinker
> paradox, you bilstering idiot. Its only the Russel paradox, so
> that it shows an outside element, you need subset axiom
>
> to prove it, you just replaced negation by more general => Q:
>
> ∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a¬Eas) is valid.
> https://www.umsu.de/trees/#~6k~7u%28Su~1~6a%28Eau~4%28Eak~1~3Eaa%29%29%29~5~6s%28Ss~5~7a~3Eas%29
>
> ∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) → ∀s(Ss → ∃a(Eas → Qxs)) is valid.
> https://www.umsu.de/trees/#~6k~7u%28Su~1~6a%28Eau~4Eak~1~3Eaa%29%29~5~6s%28Ss~5~7a%28Eas~5Qxs%29%29
>
> S = your Set
> E = your Membership
> ∀k∃u(Su ∧ ∀a(Eau ↔ (Eak ∧ ¬Eaa))) = instance of Subset Axiom
> ∀s(Ss → ∃a¬Eas) = outside element
> ∀s(Ss → ∃a(Eas → Qxs)) = outside element again
>
> It needs the Subset Axiom from some SET theory.
> So its a proof in FOL+SET, you cannot prove it without SET, in FOL only:
>
> ∀s(Ss → ∃a¬Eas) is invalid.
> https://www.umsu.de/trees/#~6s%28Ss~5~7a~3Eas%29
>

Sorry, not good enough, Jan Burse. You will have to identify which if any line of my proof is an invalid inference. Or derive some kind of internal contradiction (like Russell's Paradox) in DC Proof. Or somehow disprove ALL(s):[Set(s) => EXIST(x):[x in s => Q]]. Get busy.

[Mostowski Collapse]

I nowhere claimed that you cannot prove your nonsense.
But this still doesn't make it correct.

The formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is even
not the Drinker Paradox. It would be the drinker

paradox if x in s where D(x) and Q were ALL(y):D(y).

[Mostowski Collapse]

Do pay attention, Dan Christensen! DP is not
a special case of this theorem. DP is foremost a
kindergarden thought experiment concerning

the universal predicate. "The everybody is drinking"
in the pub is a metaphore for the universal predicate.

ALL(x):U(x)

But there is no universal set in set theory. So
DP is not a special of something in set theory.
You failed at a simple kindergarden thought

experiment posed by Raymond Smullyan.
Raymond Smullyan got you tricked!

LMAO!

[Mostowski Collapse]

Why don't you ask here:

Mathematics Stack Exchange
https://math.stackexchange.com/

MathOverflow
https://mathoverflow.net/

Whether there is anybody on this planet that believes
that your formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]

is the Drinker Paradox. Could be fun!

[Dan Christensen]

On Sunday, October 9, 2022 at 4:28:10 PM UTC-4, Mostowski Collapse wrote:
> I nowhere claimed that you cannot prove your nonsense.
> But this still doesn't make it correct.
>
> The formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is even
> not the Drinker Paradox. It would be the drinker
>
> paradox if x in s where D(x) and Q were ALL(y):D(y).

No one has ever accused you of being too imaginative, have they, Jan Burse? Using x in D instead D(x) seems to cause your head to explode. It works, maybe even better. Think of it as a generalization.

Also, predicate logic does have its limitations, even with something as mundane the Barber Paradox. See another of my blog postings on this topic at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/

[Mostowski Collapse]

Your proof proves nonsense. For example:

5 EXIST(a):~a e drinkers
Detach, 4, 2
http://www.dcproof.com/DrinkersThm1.htm

There is nowhere an assumption of this kind in the Drinker Paradox.

Get lost wonky man.

[Dan Christensen]

On Monday, October 10, 2022 at 2:31:48 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 10. Oktober 2022 um 19:25:14 UTC+2:
> > On Sunday, October 9, 2022 at 4:28:10 PM UTC-4, Mostowski Collapse wrote:
> > > I nowhere claimed that you cannot prove your nonsense.
> > > But this still doesn't make it correct.
> > >
> > > The formula ALL(s):[Set(s) => EXIST(x):[x in s => Q]] is even
> > > not the Drinker Paradox. It would be the drinker
> > >
> > > paradox if x in s where D(x) and Q were ALL(y):D(y).
> > No one has ever accused you of being too imaginative, have they, Jan Burse? Using x in D instead D(x) seems to cause your head to explode. It works, maybe even better. Think of it as a generalization.
> >
> > Also, predicate logic does have its limitations, even with something as mundane the Barber Paradox. See another of my blog postings on this topic at https://dcproof.wordpress.com/2017/01/11/the-barber-paradox-revisited-why-we-need-sets/

> Your proof proves nonsense. For example:
>
> 5 EXIST(a):~a e drinkers
> Detach, 4, 2
> http://www.dcproof.com/DrinkersThm1.htm
>

Nothing "nonsensical" about that, Jan Burse. Here, "drinkers" is a set. Since no set can include everything (from RP), there must exist something that is NOT an element of "drinkers." Get it now, Jan Burse??? Did think so. Oh, well...

[Mostowski Collapse]

Its nonsensical to think that the Barber Paradox implies
that there is a barber that is not a man. This would be this
first order quantifier logic fallacy:

¬∃x(L(x)∧M(x))→∃x¬M(x)
https://www.umsu.de/trees/#~3~7x%28L%28x%29~1M%28x%29%29~5~7x~3M%28x%29

Your phrasing in http://www.dcproof.com/BP12.htm
might suggest that you are subject to this fallacy.
So you got tricked by what Wikipedia

calls a loaded question:

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

Trying to solve a loaded question, and not point out that it is
loaded with some assumption that cannot be solved, is
of course not a very smart move.

[Mostowski Collapse]

¬∃x(Lx ∧ Mx) → ∃x¬Mx is invalid.
https://www.umsu.de/trees/#~3~7x%28L%28x%29~1M%28x%29%29~5~7x~3M%28x%29

Its not generally valid.

[Mostowski Collapse]

I guess wonky man is subject to a similar confusion
concerning the Drinker Paradox, just some fallacious

thinking when the paradox involves first order quantifier
logic, because of quantifier dislexia, similar to WM.

[Dan Christensen]

On Tuesday, October 11, 2022 at 3:33:09 AM UTC-4, Mostowski Collapse wrote:
> Its nonsensical to think that the Barber Paradox implies
> that there is a barber that is not a man.

That's not what my BP theorem says. It says: The barber can shave those and only those men in the village who do not shave themselves if and only if that barber is not a man.

More formally:

ALL(v):ALL(barber):ALL(m):[Set(v)
& barber in v
& Set(m)
& ALL(a):[a in m => a in v]

=> [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
& ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]

<=> ~barber in m]]

where

v = the set of all villagers

m = the set of all men in the village

s = the shaving relation on v, a set of ordered pairs, (x,y) in s means x shaves y

[Mostowski Collapse]

Not a smart move, trying to prove a loaded question.
You lost your mind already years ago wonky man.

[Dan Christensen]

On Tuesday, October 11, 2022 at 2:37:26 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Dienstag, 11. Oktober 2022 um 18:05:57 UTC+2:
> > On Tuesday, October 11, 2022 at 3:33:09 AM UTC-4, Mostowski Collapse wrote:
> > > Its nonsensical to think that the Barber Paradox implies
> > > that there is a barber that is not a man.


> > That's not what my BP theorem says. It says: The barber can shave those and only those men in the village who do not shave themselves if and only if that barber is not a man.
> >
> > More formally:
> >
> > ALL(v):ALL(barber):ALL(m):[Set(v)
> > & barber in v
> > & Set(m)
> > & ALL(a):[a in m => a in v]
> >
> > => [EXIST(s):[ALL(a):ALL(b):[(a,b) in s => a in v & b in v]
> > & ALL(a):[a in m => [(barber,a) in s <=> ~(a,a) in s]]]
> >
> > <=> ~barber in m]]
> >
> > where
> >
> > v = the set of all villagers
> >
> > m = the set of all men in the village
> >
> > s = the shaving relation on v, a set of ordered pairs, (x,y) in s means x shaves y

> Not a smart move, trying to prove a loaded question.

What question would that be, Jan Burse? You really seem to be losing it here.

Dan

[Mandy Stabile]

two nazis of "uKraine" admitting they don't undrestand anything, much less
each other.

[Dan Christensen]

I take it you haven't managed to escape Putin's Nazi regime. It's probably too late. Have you considered going into hiding in the far north or east? A few of your fellow countrymen have managed to get a boat across the Strait to Alaska. You better come with up a good story about your past few months here, Nazi boy. The US border service may throw you in jail and put you on trial for war crimes.

[Mandy Stabile]

Dan Christensen wrote:

> On Tuesday, October 11, 2022 at 3:07:54 PM UTC-4, Mandy Stabile wrote:
>> > On Tuesday, October 11, 2022 at 2:37:26 PM UTC-4, Mostowski Collapse
>> > wrote:
>> > What question would that be, Jan Burse? You really seem to be losing
>> > it here.
>
>> two nazis of "uKraine" admitting they don't undrestand anything, much
>> less each other.
>
> I take it you haven't managed to escape Putin's Nazi regime. It's
> probably too late. Have you considered going into hiding in the far
> north or east?

https://www.bitchute.com/channel/eval_argument/

Kalibr missile flying over Southern Ukraine

Results of a Kalibr missile strike on power station in Ivano-Frankovsk,
Ukraine

Kalibr Missile Strike on electrical substation in Lvov, Ukraine

Another view of Kalibr missile strike on US-backed terrorists in Kiev

Outstanding video of "foreign legion" terrorists becoming fertilizer.

Light Kalibration of Kiev

People by US embassy in Moscow demand to nuke Washington DC.

Aftermath of strikes on Kiev

Volodimor Ziolenski (or his body double) makes a cute selfy

Kiev getting slightly Kalibrated

Hacked webstream: Terrorists in Washington Authorized attack on Crimean
Bridge

US-backed terrorists in Dnepropetrovsk get a message from Kremlin

Wars are stupid. Better exterminate pests who start them.

Surreal view of massive loss of Ukrainian lives (graphic VDA)

Strike on American mercs in Zaporozhye

Heart-wrenching video from AFU soldiers

BREAKING: Russians are Demanding to Nuke Washington

[Mostowski Collapse]

You were never the smartes shed in the box.
This here is probably the biggest perversion
anybody has done to a paradox:

http://www.dcproof.com/BP12.htm

Its just useless garbage. There is no set m, in
the original paradox. Its just villagers. And
of course barber e v. Now please redo

your nonsense theorem.

(Hint woman don't need to shave, at least
for this paradox shave would mean to cutoff
a beard from a man, since the profession of

a barber is defined:

A barber is a person whose occupation is mainly
to cut, dress, groom, style and shave **men's** and
**boys'** hair or beards.
https://en.wikipedia.org/wiki/Barber

also in the present context the barber is a man
of course. So you don't need to go into gender
studies, and invent a Pink Unicorn,

there is just V = M and M(b), to arrive at or consider
~M(b) is obviously inconsistent garbage)

[Mostowski Collapse]

You are really a moron Dan Christensen, you don't understand
the verb shave, you state nonsense such as:

EXIST(s):[ALL(a):ALL(b):[(a,b) e s => a e v & b e v]
http://www.dcproof.com/BP12.htm

So in your take shave has domain and codomain V villagers,
which in your setting can have males and femals? Thats already
wrong, how can you deposit nonsense like EXIST(s):[ALL(a):

ALL(b):[(a,b) e s => a e v & b e v]. Or in words the moron Dan
Christensen might understand. The shave relation is a relation
where the codomain is men. The verb "shave" applies to men only!

cod(S) = { y | EXIST(x): (x,y) e S } = M

And since the paradox asks also about the shaving of
the barber himself, which hints that he is also a man,
there is something fishy with an answer such as:

"that barber is not a man."

http://www.dcproof.com/BP12.htm

Its just plain crazy nonsense.

[Dan Christensen]

Tell it to the judges at your trial, Nazi Boy. They will NOT be impressed.

[Dan Christensen]

On Tuesday, October 11, 2022 at 5:41:09 PM UTC-4, Mostowski Collapse wrote:
> You are really a moron Dan Christensen, you don't understand
> the verb shave, you state nonsense such as:
>

[snip more childish abuse]

All this abuse because you can't derive this basic result in set theory. Must be frustrating as hell for you, Jan Burse.

[Mostowski Collapse]

You are so brain damaged wonky man, that you
don't see the analogue between these two?

- No Barber (Barber Paradox)
- No Universal Set (Russel Paradox)

You got carried away by a loaded question. The
Barber Pardox is a loaded question that assumes

the existence of the barber, which is false.

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

Not a smart move to follow the wrong lead of
a loaded question instead of dismissing it on
grounds of a wrong lead.

Not a smart move at all.

[Mostowski Collapse]

How to get to the Universal Set from the Barber,
just replace shaving Sxy with Set membership Eyx,
you get that this Universal Set cannot exist:

¬∃x∀y(Eyx ↔ ¬Eyy) is valid.
https://www.umsu.de/trees/#~3~7x~6y%28Eyx~4~3Eyy%29

The above ∀y(Eyx ↔ ¬Eyy) can be read that x would
be the Universal Set of all simply regular sets, i.e.
all sets y such that ~(y e y). Works also with a

potentially empty domain. Unlike the Drinker Paradox
which requires a non-empty domain:

¬∃x(Dx ∧ ∀y(Dy → (Eyx ↔ ¬Eyy))) is valid.
https://www.umsu.de/trees/#~3~7x%28Dx~1~6y%28Dy~5%28Eyx~4~3Eyy%29%29%29