Basic math is not possible with DC Proof

[Mostowski Collapse]

Here is a challenge, some basic math:
"The image of a non empty domain is non empty"

Or formally, s≠0 stands for EXIST(c):[c e s]:

ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

The above is provable in ZF, right?
I doubt it can be proved in DC Proof.

[Mostowski Collapse]

P.S.: Was using the weaker form ALL(x):[x e a => f(x) e b]
instead of ALL(x):[x e a <=> f(x) e b], strictly the image

f[a] would be only that b with ALL(x):[x e a <=> f(x) e b].
But lets see whether the simpler can be proved?

[Mostowski Collapse]

Corr.:
Oh my, the stronger would be ALL(y):[y e b <=> EXIST(x):[x e a & f(x)=y]]
Anyway lets stick to the problem with the weaker, which would say:
"The image of a non empty set is contained in a non empty set"

[Dan Christensen]

On Tuesday, November 23, 2021 at 8:56:37 PM UTC-5, Mostowski Collapse wrote:
> Here is a challenge, some basic math:
> "The image of a non empty domain is non empty"
>

THEOREM

ALL(x):ALL(f):ALL(y):ALL(z):[ALL(a):[a in x => f(a) in y]
& EXIST(a):a in x
& ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
=> EXIST(a):a in z]

PROOF

1 ALL(a):[a in x => f(a) in y]
& EXIST(a):a in x
& ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
Premise

2 ALL(a):[a in x => f(a) in y]
Split, 1

3 EXIST(a):a in x
Split, 1

4 ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
Split, 1

5 x0 in x
E Spec, 3

6 x0 in x => f(x0) in y
U Spec, 2

7 f(x0) in y
Detach, 6, 5

8 f(x0) in z <=> f(x0) in y & EXIST(b):[b in x & f(b)=f(x0)]
U Spec, 4, 7

9 [f(x0) in z => f(x0) in y & EXIST(b):[b in x & f(b)=f(x0)]]
& [f(x0) in y & EXIST(b):[b in x & f(b)=f(x0)] => f(x0) in z]
Iff-And, 8

10 f(x0) in y & EXIST(b):[b in x & f(b)=f(x0)] => f(x0) in z
Split, 9

11 f(x0)=f(x0)
Reflex, 7

12 x0 in x & f(x0)=f(x0)
Join, 5, 11

13 EXIST(b):[b in x & f(b)=f(x0)]
E Gen, 12

14 f(x0) in y & EXIST(b):[b in x & f(b)=f(x0)]
Join, 7, 13

15 f(x0) in z
Detach, 10, 14

16 EXIST(a):a in z
E Gen, 15

17 ALL(x):ALL(f):ALL(y):ALL(z):[ALL(a):[a in x => f(a) in y]
& EXIST(a):a in x
& ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
=> EXIST(a):a in z]
Conclusion, 1

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]

You didn't prove:

ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

You assume ALL(a):[a in x => f(a) in y] .
Do you see some assumption ALL(a):[a in x => f(a) in y] in the above?

[Dan Christensen]

I proved, "The image of a non empty domain is non empty." Deal with it, Jan Burse.

[Mostowski Collapse]

There is a second error. Your existence quantifier is wrongly
placed or missing. You dont have EXIST(z) anywhere
after the implication sign =>:

7 ALL(x):ALL(f):ALL(y):ALL(z):[ALL(a):[a in x => f(a) in y]
& EXIST(a):a in x
& ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
=> EXIST(a):a in z]
Conclusion, 1

You did not prove what I wrote:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:

> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

The above is provable in FOL+ZF.
It is not provable in DC Proof alone.

[Dan Christensen]

> There is a second error. Your existence quantifier is wrongly
> placed or missing. You dont have EXIST(z) anywhere
> after the implication sign =>:
> 7 ALL(x):ALL(f):ALL(y):ALL(z):
>
> [ALL(a):[a in x => f(a) in y]
>

[f is a function with domain x and codomain y]

>
> & EXIST(a):a in x
>

[the domain of f is non-empty]

>
> & ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]]
>

[z is the image of x under f]

>
> => EXIST(a):a in z]
>

[z is non-empty]

>
> Conclusion, 1
> You did not prove what I wrote:

You wanted to prove, "The image of a non empty domain is non empty." Perhaps you do not fully understand what that means, but that is what I have proven. (See my comments in [ ]'s inserted above.) Maybe you should reacquaint yourself with the terminology? See: https://en.wikipedia.org/wiki/Function_(mathematics)

[Mostowski Collapse]

I don't want to prove something from Wikipedia.
It doesn't have an english phrasing, its just a formula.
The full english phrasing would be:

- For every non empty set
there exists a set
that is a super set of an image of the former set
and that is non empty

So the task is to prove this theorem:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:

> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

[Mostowski Collapse]

In the case of DC Proof, you possibly want a closed
higher order formula, so it would be:

ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]

[Mostowski Collapse]

You can also switch sides of the conjunction &:

ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[EXIST(c):[c e b] & ALL(x):[x e a => f(x) e b]]]

Then the phrasing is a little shorter, using bounded quantifier phrasing twice:

- For every non empty set

there exists an non empty set

that is a super set of an image of the former set

You can also phrase the ALL(f) quantifier:

- For every function and for every non empty set
there exists an non empty set
that is a super set of the function image of the former set

[Dan Christensen]

On Wednesday, November 24, 2021 at 11:33:38 AM UTC-5, Mostowski Collapse wrote:
> In the case of DC Proof, you possibly want a closed
> higher order formula, so it would be:
>
> ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]

It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.

Dan

[Mostowski Collapse]

Well its basic math. Its a basic theorem, because
its a simple theorem. It uses only some simple notions:
- non empty set
- image by a function

It would be non-basic math, aka advanced math, if
the theorem were more complex.

The theorem can be proved in FOL+ZF.
But it cannot be proved in DC Proof.

Do you know why?

[Mostowski Collapse]

Here is a tableaux proof of the theorem in FOL+ZF, using Exy for x e y:

∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is valid.
https://www.umsu.de/trees

The LHS is an instance of the axiom schema of replacement from ZF.

Woa! Thats quite amazing that trees can find it.

[Dan Christensen]

On Wednesday, November 24, 2021 at 6:02:45 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 24. November 2021 um 19:05:22 UTC+1:
> > On Wednesday, November 24, 2021 at 11:33:38 AM UTC-5, Mostowski Collapse wrote:
> > > In the case of DC Proof, you possibly want a closed
> > > higher order formula, so it would be:
> > >
> > > ALL(f):ALL(a):[EXIST(c):[c e a] => EXIST(b):[ALL(x):[x e a => f(x) e b] & EXIST(c):[c e b]]]
> >
> > It seems you have truly caught the Muckenheim disease, Jan Burse. That's not basic math. It's basic nonsense. Get back to us when you are feeling better.
> >

> Well its basic math. Its a basic theorem, because
> its a simple theorem. It uses only some simple notions:
> - non empty set
> - image by a function
>
>

This is basic math about "the image of a non empty domain [being] non-empty":

ALL(x):ALL(f):ALL(y):ALL(z):
[ALL(a):[a in x => f(a) in y] (f is a function with domain x and codomain y)
& EXIST(a):a in x (x is non-empty)
& ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] (z is the image of x under f)

=> EXIST(a):a in z] (z is non-empty)

Your version is pure nonsense, Jan Burse. Deal with it.

[Mostowski Collapse]

You didn't prove what was require.

[Mostowski Collapse]

Just recall what Russell said about "the X is Y".
You translate it again into "some X is Y":

ALL(z):[ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] => EXIST(a):a in z]]

Can be vacously true if there is no z that is the
image. So you didn't learn anything from "the bald king"
example? Still doing the same errors? Just

think how "the image is translated". If you really
want to translate the english definite description,
you would need to use the strong:

EXISTUNIQUE(z):[ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] & EXIST(a):a in z]]

I offered you the weaker EXIST instead EXISTUNIQUE:

Mostowski Collapse schrieb am Mittwoch, 24. November 2021 um 02:56:37 UTC+1:
> Or formally, s≠0 stands for EXIST(c):[c e s]:

> ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
https://groups.google.com/g/sci.logic/c/tVUtBSQUhiE/m/bLEb_i6BBAAJ

But you wont be able to prove either in DC Proof. You
wont be able to prove the EXIST nor the EXISTUNIQUE
without extra axioms. Like you showed your inability to

grasp the translation of Russells "the X is Y" in theory. Also
in practice for basic math, you insist on utter nonsense
allowing for vacouse truth, instead of

make a proper existence proof.

Whats wrong with you?

[Mostowski Collapse]

Because you didn't understand Russells "the X is Y",
you keep continuing proving "some X is Y" nonsense.
Latest example "some Dedekind is Peano".

It even seems your DC proof tool is made to prove
such nonsense. You are totally inable to prove the
existence of omega from some foundation.

But the example I gave litterally can be even proved
from an other tool that doesn't need download and
that even works for the macintosh:

> Here is a tableaux proof of the theorem in FOL+ZF, using Exy for x e y:
> ∀a∃b∀x(Exb ↔ ∃y(Eya ∧ f(y)=x)) → ∀a(∃zEza → ∃b(∃zEzb ∧ ∀y(Eya → Ef(y)b))) is valid.
> https://www.umsu.de/trees
> The LHS is an instance of the axiom schema of replacement from ZF.

The axiom schema of replacement was introduce
by Abraham Fraenkel, the F in ZF signifies this axiom
schema. Its quite a powerful axiom schema.

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

To make a proper proof we would also need to
prove that f(y)=x is a definite description, namely
that we also have:

ALL(y):EXISTUNIQUE(x):f(y)=x

Only then we are allowed to apply the axiom
schema. But the above is left as an exercise.

[Mostowski Collapse]

And Lazy-O-Matik, why didn't you prove:

EXIST(z):ALL(a):[a in z <=> a in y & EXIST(b):[b in x & f(b)=a]] ?

Too lazy to invoke your own DC Proof subset axiom?

LMAO!

[Dan Christensen]

Recall that you requested only proof that, "The image of a non empty domain is non empty." The notion of the image of the domain (of a function), was a given. Deal with it, Jan Burse.

Dan

[Mostowski Collapse]

*****************************************************
Hello Dan-O-Matik, WAKE UP, see below at end of post
how x e a has switched sides, same for x e b?
*****************************************************

Dan Christensen schrieb am Donnerstag, 2. Dezember 2021 um 18:46:31 UTC+1:
> Perhaps, you didn't know, but every set is a superset of itself.
> And if A <=> B, then A => B. I hope this helps.

You are extremly crazy right now, just because you don't
read what is before your eyes. Can you show how you go from 1):

/* not provable */
1) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]

To this here 2), when 1) isn't provable?

/* provable */
2) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a <=> f(x) e b] & b≠0]]

You forget that 1) is not in the form of the axiom schema of replacement.
The exists quatifier is missing. To be in the form of the axiom schema of
replacement it would need to read:

/* provable */
3) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e b <=> EXIST(y):[y e a & f(y)=x]] & b≠0]]

How do you want to go from 3) to 2) by chaning <=> into =>.
You are crazy. What about the EXIST quantifier? Did you
also see that x e a has switched sides, same for x e b?

[Mostowski Collapse]

Corr.:

/* provable */
2) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

[Mostowski Collapse]

You are correct in your "thinking" so informally something
happens going from codomain to superset of codomain.

But formally its not so simple going from A<=>B to A=>B,
because already the direction is somehow wrong.

Can you prove my formula in DC Proof, yes or no?

[Dan Christensen]

On Thursday, December 2, 2021 at 3:26:31 PM UTC-5, Mostowski Collapse wrote:
> You are correct in your "thinking" so informally something
> happens going from codomain to superset of codomain.
>
> But formally its not so simple going from A<=>B to A=>B,
> because already the direction is somehow wrong.
>
> Can you prove my formula in DC Proof, yes or no?
> Mostowski Collapse schrieb am Donnerstag, 2. Dezember 2021 um 21:16:32 UTC+1:
> > Corr.:
> > /* provable */
> > 2) ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]

In DC Proof, as in just about every math textbook, functional notation is about a relation between the elements in a pair of sets: the so-called domain and codomain sets. Both sets must, at the very least, be named. They may be a set of numbers or points in space, or just an arbitrary, possibly empty set. A function f mapping elements of an arbitrary set x to elements of an arbitrary set y can be formally defined as follows:

ALL(a):[a in x => f(a) in y]

where x is the domain set and y is the codomain set.

If x0 in x (i.e. x is not empty), then f(x0) in y (i.e. y is not empty). This is an extremely trivial result, roughly equivalent to your much less intuitive "theorem" here. Maybe that's why ZFC set theory is so rarely if ever required in university pure math programs (e.g. at MIT).

[Mostowski Collapse]

Dan-O-Matik halucinated his own little crazy world:
> Given s0={0}, f:s0-->s0 and ~1=0, we have: f(0)=0 and f(1) is indeterminate (undefined)
> Formal Proof: https://www.dcproof.com/FunctionUndefined.htm (23 lines)

This is not correct mathematics. If you say f : X -> Y, you
want the domain of f to be determined to be X.
If you have for f : {0} -> {0}, f(1) inderminate, then dom(f)

can be either {0} or {0,1}. You need to have f(1) undefined,
so that the domain is always {0}. You can check any standard
reference in mathematics, for example:

Basic Set Theory - Azriel Levy
https://www.amazon.de/dp/0486420795

The booklet is only 20 bucks or so.

[Dan Christensen]

On Friday, December 3, 2021 at 3:39:50 AM UTC-5, Mostowski Collapse wrote:
> Dan-O-Matik halucinated his own little crazy world:
> > Given s0={0}, f:s0-->s0 and ~1=0, we have: f(0)=0 and f(1) is indeterminate (undefined)
> > Formal Proof: https://www.dcproof.com/FunctionUndefined.htm (23 lines)
>
> This is not correct mathematics. If you say f : X -> Y, you
> want the domain of f to be determined to be X.
> If you have for f : {0} -> {0}, f(1) inderminate, then dom(f)
>
> can be either {0} or {0,1}. You need to have f(1) undefined,
> so that the domain is always {0}. You can check any standard
> reference in mathematics, for example:
>

See my reply just now to your identical posting here.

Dan

[Mostowski Collapse]

I didn't say invalid axiom, I said incorrect definition.
You incorrectly define f : X -> Y. Your definition is not
the text book math definition of function space.

[Mostowski Collapse]

So we have now two unresolved problems for DC proof:
1) Still no proof of ALL(a):[a≠0 => EXIST(b):[ALL(x):[x e a => f(x) e b] & b≠0]]
2) Still no correct definition of F : X -> Y

Here is my prediction what we will discuss X-mas:
3) Denial of 3 ⊆ 5 for von Neuman ordinals
4) The moon is made of cheese

LoL

[Daniel Pehoushek]

sigmund freud said
only fags really care
sigmund really cared
freud was a fag

daniel

[Mostowski Collapse]

Dan-O-Matik, your school skipper definition is not
a correct definition. Your definition does not imply:

ALL(a):ALL(b):[F(a,b) => P(a) & Q(b)].

Even the tree tool can find a counter example:

∀a(Pa → ∃b(Qb ∧ (Fab ∧ ∀c(Qc → (Fac → c=b))))) → ∀a∀b(Fab → (Pa ∧ Qb)) is invalid.
Countermodel:
Domain: { 0 }
P: { }
Q: { 0 }
F: { (0,0) }
https://www.umsu.de/trees

Your easy definition is an easily wrong definition.

[Mostowski Collapse]

Just check wikipedia:

Any subset of the Cartesian product of two sets X and Y defines a
binary relation R ⊆ X × Y between these two sets.
[...]
A function is a **binary relation** that is functional and serial.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

Wikipedia also notes your blooper (refering to R ⊆ X × Y):

It is immediate that an arbitrary relation may contain pairs that
violate the necessary conditions for a function given above.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

Also the word "functional" is used differently in wikipedia so that
it might also cover partial functions, i.e. when serial is missing.
Basically the EXISTUNIQUE quantifier is split up into, now doing

it class wise like Dan-O-Matik started doing it:

/* serial = existence */
ALL(a):[P(a) => EXIST(b):[Q(b) & F(a,b)]]

/* functional = uniqueness */
ALL(a):[P(a) => ALL(b):[Q(b) => ALL(c):[Q(c) => [F(a,b) & F(a,c) => b = c]]]]