Proposed Function Space Axiom for DC Proof

[Dan Christensen]

I am considering a new Function Space axiom for DC Proof of the form:

1. ALL(a):ALL(b):[Set(a) & Set(b) => EXIST(c):[Set(c) & ALL(f):[f in c <=> ALL(d):[d in a => f(d) in b]]]]
(Function Space)

To justify it, consider my proof of the theorem:

Given sets x and y we can construct the set fs consisting of all those function-like subsets of the Cartesian product of x and y. For each element f in fs, we can prove the existence of a unique function g: x --> y such that g(a)=b <=> (a, b) in f.

Formal proof: https://www.dcproof.com/FunctionSpace.htm (138 lines, re-posted from earlier this month)

Your comments?

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]

Take a={} the empty set, and you suddently can prove
that the universal class is a set. Which makes your
system inconsistent.

If a={} then this here:

ALL(f):[f in c <=> ALL(d):[d in a => f(d) in b]]]

turns into this here:
ALL(f):[f in c <=> ALL(d):[d in {} => f(d) in b]]]

which is equivalent to:
ALL(f):[f in c <=> ALL(d):[false => f(d) in b]]]

which is equivalent to:
ALL(f):[f in c <=> true]

which is equivalent to:
ALL(f):[f in c]

On the other hand in standard mathematics, there
is only exactly one function with a={} the empty set,
namely the function f={}.

LoL

[Dan Christensen]

On Saturday, January 15, 2022 at 2:29:20 PM UTC-5, Mostowski Collapse wrote:
> Take a={} the empty set, and you suddently can prove
> that the universal class is a set. Which makes your
> system inconsistent.
>
> If a={} then this here:
> ALL(f):[f in c <=> ALL(d):[d in a => f(d) in b]]]
> turns into this here:
> ALL(f):[f in c <=> ALL(d):[d in {} => f(d) in b]]]
>
> which is equivalent to:
> ALL(f):[f in c <=> ALL(d):[false => f(d) in b]]]
>
> which is equivalent to:
> ALL(f):[f in c <=> true]
>
> which is equivalent to:
> ALL(f):[f in c]
>

I think you will find you cannot obtain this result in DC Proof. Give it a try.

[Mostowski Collapse]

Why not, is there no empty set in DC poop?
Or does vacously true not anymore work?

Which of the steps do not work?

[Dan Christensen]

On Saturday, January 15, 2022 at 1:49:48 PM UTC-5, Dan Christensen wrote:
> I am considering a new Function Space axiom for DC Proof of the form:
>
> 1. ALL(a):ALL(b):[Set(a) & Set(b) => EXIST(c):[Set(c) & ALL(f):[f in c <=> ALL(d):[d in a => f(d) in b]]]]
> (Function Space)
>
> To justify it, consider my proof of the theorem:
>
> Given sets x and y we can construct the set fs consisting of all those function-like subsets of the Cartesian product of x and y. For each element f in fs, we can prove the existence of a unique function g: x --> y such that g(a)=b <=> (a, b) in f.
>
> Formal proof: https://www.dcproof.com/FunctionSpace.htm (138 lines, re-posted from earlier this month)
>
> Your comments?
>

Restricted domain to non-empty sets. Function space doesn't exist in ordinary set theory--it blows up--if domain is empty.

If the codomain is empty, so is the function space:

ALL(x):ALL(y):ALL(fs):[Set(x) & Set(y) & Set(fs)
& EXIST(a):a in x
& ALL(f):[f in fs <=> ALL(a):[a in x => f(a) in y]]
& ~EXIST(a):a in y

=> ~EXIST(f):f in fs]

Proof: https://www.dcproof.com/FunctionSpaceEmptyCodomain.htm (22 lines)

Example with domain and codomain = {z}. Function space is also a singleton: f(z)=z

ALL(x):ALL(z):[Set(x) & ALL(a):[a in x <=> a=z]

=> EXIST(fs):[Set(fs) & ALL(f):[f in fs <=> ALL(d):[d in x => f(d) in x]] & ALL(f):[f in fs <=> f(z)=z]]]

Proof: https://dcproof.com/FunctionSpaceSingletons.htm (48 lines)

[Mostowski Collapse]

You dont understand the implications of anti-monotonicity?

Your new function space existence axiom leads to
to non-well founded sets. Thats easy to show.
Another proof uses disjoint union, defined as:

X+Y := { (a,0) | a e X } u { (b,1) | b e Y } ⊆ (X ∪ Y) x {0,1}

For every function space of your sort, i.e. A -? B. For arbitrary
set S, T, because of anti-monotonicity, we have from S ⊆ T,
that A+S ⊆ A+T, and therefore A+T -? B ⊆ A+S -? B.

Now take any infinite INCREASING chain S0 ⊊ S1 ⊊ S2 ...
You get an infinite DECREASING chain:

.... A+S2 -? B ⊊ A+S1 -? B ⊊ A+S0 -? B

LoL

[Mostowski Collapse]

Also as usual you are talking non sense:

> Function space doesn't exist in ordinary set theory--it blows up--if domain is empty.

In set theory, because the function space is defined as:

A -> B = { f e P(A x B) | forall x in A existunique y in B (x,y) e f }

Its easy to show that A = {} implies A -> B = {{}}.

Proof: A = {} implies A x B = {},
A x B = {} implies P(A x B) ={{}},
take f = {}, forall x in A existunique y in B (x,y) e f is vacously true

What non-sense are you halucinating now about set theory and some blow up?

[Mostowski Collapse]

How flat chested is DC Proof? It doesn't have a power set axiom?

These two collections are provably equal, i.e. F1 = F2:

F1 = {f in P(AxB) : For all x in A, there exists unique y in B such that (x, y) in f}.

F2 = {f ⊆ A x B : For all x in A, there exists unique y in B such that (x, y) in f}.

They both define the function space A -> B aka set exponentiation B^A.

You find them mentioned here:

F1:

Zermelo Fraenkel Powerset
Richard E. BORCHERDS - 30.11.2021
https://www.youtube.com/watch?v=XCMvljsu84s

F2:

In the relational approach, a function f: X→Y is a binary relation between
X and Y that associates to each element of X exactly one element of Y.
Any subset of the Cartesian product of two sets X and Y defines a binary
relation R ⊆ X × Y between these two sets.
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

Whats wrong with you? Its then easy to prove:

f e B^A , x not in A => ~EXIST(y):(x,y) in f

[Mostowski Collapse]

But we don't know whether A+Sn+1 -? B ⊊ A+Sn -? B
or A+Sn+1 -? B = A+Sn -? B from Sn ⊊ Sn+1,

So requirement of well founded ness, could
lead to the conclusion that the decreasing chain
is in fact not a proper decreasing chain. But

we would possibly then get a contradiction,
since we nevertheless can show your pseudo
function spaces different for Sn =\= Sn+1?

We dont know, there is no definition of equality
in DC Proof yet for function symbols. This here
is yet undefined:

/* DC Poop question */
f = g <=> ?

When f and g are function symbols. On the
other hand in set theory, for f,g e A -> B,
because f and g are sets and not function symbols,

equality is defined, its just set extensionality:

f = g <=> ∀x( x e f <=> y e g)

Also in set theory one can prove:

A ≠ A', f e A -> B & g e A' -> B => f ≠ g

There is no anti-monotonicity.

[Dan Christensen]

On Sunday, January 16, 2022 at 5:04:42 AM UTC-5, Mostowski Collapse wrote:
> You dont understand the implications of anti-monotonicity?
>
> Your new function space existence axiom leads to
> to non-well founded sets.

It leads to the kind of sets one sees in most textbook math proofs. Using my proposed axiom for functions spaces, you can infer the existence of the set of all functions mapping non-empty set X to set Y. In my example, I obtain that set of all functions mapping {z} to itself, namely {f : f(z)=z}.

https://dcproof.com/FunctionSpaceSingletons.htm

[Mostowski Collapse]

No, the text book set is different. A^B , the set exponentiation,
which gives { f | f : A -> B } is not anti-monotonic.

Ask MSE, MO, etc.. whether set exponentiation is anti monotonic.
I don't have a MSE, MO, etc.. account anymore,

but I guess you should still have one, don't you.

[Dan Christensen]

On Sunday, January 16, 2022 at 12:40:09 PM UTC-5, Mostowski Collapse wrote:
> No, the text book set is different. A^B , the set exponentiation,
> which gives { f | f : A -> B } is not anti-monotonic.
>

I'm not defining any kind of exponentiation here. Given any non-empty set X and set Y, I am simply inferring the existence of a set

{f | ALL(a):[a in X => f(a) in Y]}

I see no problem with it so far. I will continue testing it though. Thanks again for pointing out the problem with an empty domain.

[Mostowski Collapse]

Corr.: Wrong argument order, we have:

B^A = { f | f : A -> B }

The set exponention is monotonic in its first argument
B, we have indeeded the following:

B ⊆ B' => B^A ⊆ B'^A

But the set exponentiation is not monotonic or anti-monotonic
in its second argument. One can prove that different
exponentiations are disjoint:

A ≠ A' & B ≠ {} => B^A ∩ B^A' = {}

You cannot prove the same for your function space notion.
But it holds for the text book function space.

Ask the above on MSE, MO, etc..

[Mostowski Collapse]

The problem with your function space notion,
you get that the universal class is a set.
Thats easy to prove. Even now that you exclude

B = {}, it is still provable. It has nothing to do
with B = {}, thats only a border case, where its
the most easiest to show that you get the

universal class.

[Dan Christensen]

On Sunday, January 16, 2022 at 12:54:38 PM UTC-5, Dan Christensen wrote:
> On Sunday, January 16, 2022 at 12:40:09 PM UTC-5, Mostowski Collapse wrote:
> > No, the text book set is different. A^B , the set exponentiation,
> > which gives { f | f : A -> B } is not anti-monotonic.
> >
> I'm not defining any kind of exponentiation here. Given any non-empty set X and set Y, I am simply inferring the existence of a set
>
> {f | ALL(a):[a in X => f(a) in Y]}
>
> I see no problem with it so far. I will continue testing it though. Thanks again for pointing out the problem with an empty domain.

Another test. Looks good. https://dcproof.com/FunctionSpaceTwoElementDomain.htm

[Dan Christensen]

On Sunday, January 16, 2022 at 1:47:57 PM UTC-5, Dan Christensen wrote:
> On Sunday, January 16, 2022 at 12:54:38 PM UTC-5, Dan Christensen wrote:
> > On Sunday, January 16, 2022 at 12:40:09 PM UTC-5, Mostowski Collapse wrote:
> > > No, the text book set is different. A^B , the set exponentiation,
> > > which gives { f | f : A -> B } is not anti-monotonic.
> > >
> > I'm not defining any kind of exponentiation here. Given any non-empty set X and set Y, I am simply inferring the existence of a set
> >
> > {f | ALL(a):[a in X => f(a) in Y]}
> >
> > I see no problem with it so far. I will continue testing it though. Thanks again for pointing out the problem with an empty domain.

> Another test. Looks good. https://dcproof.com/FunctionSpaceTwoElementDomain.htm

A test with functions of 2 variables: https://dcproof.com/FunctionSpaceTwoVariables.htm

[Mostowski Collapse]

Strange that you don't see a pattern behind your nonsense.
I hope so that you can prove f e { g | A(g) } when A(f).
Thats for every set builder style axiom the case.

The following ZFC axioms are set builder style axioms:
- Pairing axiom: It says { x | x=y v x=z } is a set.
- Power set axiom: It says { x | x ⊆ y } is a set.
- Subset axiom: It says { x | x e y & A } is a set.
- Union axiom: It says { x | ∃z(z e y & x e z) } is a set.
- What else?

Your new function space axiom from DC Proof:
- Dan-O-Matik Function Space: It says { f | ∀x(x e A => f(x) e B } is a set.
- What else?`

There is only one difference between ZFC and DC Proof.

****************************************************************
ZFC has not yet been shown inconsistent. But DC Proof
can be easily shown inconsistent with his new Dan-O-Matik
Function Space axiom. Thats really easy.
****************************************************************

Dan-O-Matik will not believe me, he claimed a few seconds
ago the empty set cannot be derived in DC Proof.
But DC Proof has the Subset axiom, so its easy to

derive the empty set together with his set based
Peano axioms. How difficult can it be to relate a
anti-monotonic construct with the universal class?

ZFC Pairing axiom, Power set axiom, Subset axiom
Union axiom, are all not anti-monotonic. Some are
even monotonic. Gödel discusses monotonicity

in his booklet about the gen. CH.

LoL

[Dan Christensen]

On Sunday, January 16, 2022 at 4:18:24 PM UTC-5, Mostowski Collapse wrote:
> Strange that you don't see a pattern behind your nonsense.
> I hope so that you can prove f e { g | A(g) } when A(f).
> Thats for every set builder style axiom the case.
>
> The following ZFC axioms are set builder style axioms:
> - Pairing axiom: It says { x | x=y v x=z } is a set.
> - Power set axiom: It says { x | x ⊆ y } is a set.
> - Subset axiom: It says { x | x e y & A } is a set.
> - Union axiom: It says { x | ∃z(z e y & x e z) } is a set.
> - What else?
>
> Your new function space axiom from DC Proof:
> - Dan-O-Matik Function Space: It says { f | ∀x(x e A => f(x) e B } is a set.
> - What else?`
>
> There is only one difference between ZFC and DC Proof.
>
> ****************************************************************
> ZFC has not yet been shown inconsistent. But DC Proof
> can be easily shown inconsistent with his new Dan-O-Matik
> Function Space axiom. Thats really easy.

Post your proof, Jan Burse. Recall that to show a formal system is inconsistent, you must derive a pair of contradictory theorems in that system without introducing additional axioms. You can use the Sets and Logic menus.

> ****************************************************************
>
> Dan-O-Matik will not believe me, he claimed a few seconds
> ago the empty set cannot be derived in DC Proof.
> But DC Proof has the Subset axiom, so its easy to
>
> derive the empty set together with his set based
> Peano axioms.

Peano's axioms are not built into the set theory in DC Proof (see the Sets and Logic menus). None of them postulates the existence of any set or other object. The user would have to introduce additional axioms to do so.

[Mostowski Collapse]

Well you invited me yourself to use your Peano,
that you are repeatedly spamming on sci.math
and sci.logic, you wrote:

Dan Christensen schrieb am Freitag, 14. Januar 2022 um 18:46:47 UTC+1:
> [...]. Peano's Axioms, which effectively define the natural
numbers, are self-evident and very intuitive and can be introduced
by the user at the beginning of any proof.
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/ykyUHkBpAgAJ

Now the party is canceled.
What happend to your invitation?
Cold feet? Mental meltdown?

LoL

[Mostowski Collapse]

Everybody can prove (maybe the next dcproof6.exe will
not anymore allow to do so, seem that all of
my posts sooner or later lead to more and more

restricted inference rules of DC Proof):

Set(n) |- EXIST(x):Set(x)

See for yourself:

Sn entails ∃xSx
https://www.umsu.de/trees/#Sn|=~7xSx

So I only need:

1. Set(n)
Axiom

To derive the empty set via your Subset axiom (but
I suspect with dcproof6.exe, we will be closer to
Augsburg Crank institute and the empty set

will be banned, and my proof wont work anymore).

[Mostowski Collapse]

If you are having didactical problems with your
Peano axioms, well we are telling you that they
are nonsense already for ages.

At least they are not the first order Peano axioms,
the set-less variant. In the set-less variant one wouldn't
introduce n, and only have an axiom schema:

P(0) & forall x (P(x) => P(x+1))
--------------------------------------------------
forall x P(x)

Obviously the domain of discourse is now the Peano
structure. But you use a set-like version of Peano axioms,
so its unavoidable that there is an interaction

with your set theory. But you refuse to use ZFC insteand
and make omega derivable from ZFC, as I showed an
alternative. Instead you now make complaints about

your own Peano take, and its inevitable interaction
with your Set theory? How funny. LoL

Not happy with what you did?

[Dan Christensen]

On Sunday, January 16, 2022 at 6:00:43 PM UTC-5, Mostowski Collapse wrote:
> Everybody can prove (maybe the next dcproof6.exe will
> not anymore allow to do so, seem that all of
> my posts sooner or later lead to more and more
>
> restricted inference rules of DC Proof):
>
> Set(n) |- EXIST(x):Set(x)
>
> See for yourself:
>
> Sn entails ∃xSx
> https://www.umsu.de/trees/#Sn|=~7xSx
>
> So I only need:
>
> 1. Set(n)
> Axiom
>
> To derive the empty set via your Subset axiom (but
> I suspect with dcproof6.exe, we will be closer to
> Augsburg Crank institute and the empty set
>

Seeing no proof, I can only assume you were lying when you said DC Proof was inconsistent. When will you learn, Jan Burse?

[Mostowski Collapse]

How should I do a proof? There was no official announcement
yet of dcproof6.exe , only a request for comments of some

WONKY function space axiom. You wrote:
> I am considering a new Function Space axiom for DC Proof of the form:

Is your considering phase over? Do you know whether your
DC Proof cabaret is opening with a new sensation or not.

I will be happy to work on an inconsistency when I can do some hands on.

Dan Christensen schrieb am Montag, 17. Januar 2022 um 01:19:11 UTC+1:
> Seeing no proof

[Mostowski Collapse]

I nowhere said I would only use set theory of DC Proof.
DC Proof refers to the full package. If I can derive

an inconsistency from Peano, this would be even
more fun. Showing Peano inconsistent or have a logic

tool that does that, is quite some feat.

[Dan Christensen]

On Sunday, January 16, 2022 at 8:41:36 PM UTC-5, Mostowski Collapse wrote:
> How should I do a proof? There was no official announcement
> yet of dcproof6.exe , only a request for comments of some
> WONKY function space axiom. You wrote:
> > I am considering a new Function Space axiom for DC Proof of the form:
> Is your considering phase over? Do you know whether your
> DC Proof cabaret is opening with a new sensation or not.
>
> I will be happy to work on an inconsistency when I can do some hands on.
>

Why did you say it was inconsistent when you had no proof? I think that's called lying.

[Dan Christensen]

On Sunday, January 16, 2022 at 4:18:24 PM UTC-5, Mostowski Collapse wrote:
> Strange that you don't see a pattern behind your nonsense.
> I hope so that you can prove f e { g | A(g) } when A(f).
> Thats for every set builder style axiom the case.
>
> The following ZFC axioms are set builder style axioms:
> - Pairing axiom: It says { x | x=y v x=z } is a set.
> - Power set axiom: It says { x | x ⊆ y } is a set.
> - Subset axiom: It says { x | x e y & A } is a set.
> - Union axiom: It says { x | ∃z(z e y & x e z) } is a set.
> - What else?
>
> Your new function space axiom from DC Proof:
> - Dan-O-Matik Function Space: It says { f | ∀x(x e A => f(x) e B } is a set.
> - What else?`
>
> There is only one difference between ZFC and DC Proof.
>
> ****************************************************************
> ZFC has not yet been shown inconsistent. But DC Proof

> can be easily shown inconsistent ...

Not that easily, it seems. Apparently Jan Burse here actually has NO PROOF of this outrageous claim. It's called LYING.

Dan

[Mostowski Collapse]

Studends beware, DC Proof function space are a logic
roller coaster, you can prove that there is butterfly color
that isn't a color. Take Dan-Matik function space

F : { f | ALL(x):[x e butterfly -> f(x) e color] }

Now we can proof:

EXIST(y):EXIST(g):[g e F & ~g(y) e color]

[Dan Christensen]

Sorry, Jan Burse, but this, too, requires a proof. Must be frustrating as hell for you.

BTW, we are STILL waiting for your proof of the inconsistency of DC Proof. It has been several years now.

Dan

[Mostowski Collapse]

Well you can prove that for every set s,
there is an element x not in s?

ALL(s):EXIST(y):[~y e s]

Russell does it like this, it does not need
pairing and it does not need union, it does not
need power set, it does not need regularity:

y := { x e s | ~(x e x) }

Now ask, is y e s? Assume it were so:

There are two cases:
Case 1: If ~(y e y), then it where that,
the comprehension axiom selects y as well,
and we would get, y e y, a contradiction.

Case 2: If (y e y), now we can also see that y is
subset s, therefore if y e y, it were also y e s,
and then by definition of s, it were ~(y e y), a contradiction.

So I guess we need DC Proof Subset Axiom
as a start to derive the above Lemma?

[Mostowski Collapse]

The Tree Tool by Wolfgang Schwartz can prove
the Russel Construction in a blink:

∀s∃y∀x(Exy ↔ ¬Exx) /* Subset Axiom */
entails ∀s∃y¬Eys. /* Lemma */
https://www.umsu.de/trees/#~6s~7y~6x%28Exy~4~3Exx%29|=~6s~7y~3Eys

This lemma is later needed in the butterfly
color proof experiment.

[Mostowski Collapse]

Powerset is not needed for Russels

construction, I wrote:

> Russell does it like this, it does not need
> pairing and it does not need union, it does not
> need power set, it does not need regularity:

Only subset is needed.
What is wrong with you?

Dan Christensen schrieb am Montag, 17. Januar 2022 um 22:28:51 UTC+1:
> > So I guess we need DC Proof Subset Axiom

> See the Power Set option on the Sets menu. No more excuses, Jan Burse!

[Mostowski Collapse]

Oops this is the correct proof in Wolfgang Schwartz tool,
my previous post was the Barber Paradox and not
the Russell constuction:

/* u∈v is encoded as Euv */
∀s∃y∀x(Exy ↔ (Exs ∧ ¬Exx))
entails ∀s∃y¬Eys.
https://www.umsu.de/trees/#~6s~7y~6x%28Exy~4Exs~1~3Exx%29|=~6s~7y~3Eys

Now the formula is also used in the proof, and the
proof is a little bit more longer.

[Dan Christensen]

See the SUBSET option on the Sets menu. No more excuses, Jan Burse!

[Mostowski Collapse]

The rest is relatively easy, take some h e F,
you can construct this set:

H = { (x,y) | x e butterfly & y e color & g(x)=y }

Now by Russell construction there is an a,
with ~(a e butterfly) and by the same construction
there is some a b, with ~(b e color).

Now construct this set:

G = H u { (a,b) }

By your Function Axiom there is a function g.
Its easy to show:

i) g e F
ii) ~g(a) e color

Therefore EXIST(y):EXIST(g):[g e F & ~g(y) e color] .

Q.E.D.

[Dan Christensen]

On Monday, January 17, 2022 at 5:29:13 PM UTC-5, Mostowski Collapse wrote:
> The rest is relatively easy, take some h e F,
> you can construct this set:
>
> H = { (x,y) | x e butterfly & y e color & g(x)=y }
>
> Now by Russell construction there is an a,
> with ~(a e butterfly) and by the same construction
> there is some a b, with ~(b e color).
>
> Now construct this set:
>
> G = H u { (a,b) }
>
> By your Function Axiom there is a function g.
> Its easy to show:
>

Please show us, Jan Burse.

[Mostowski Collapse]

There is a bug in this proof:
https://dcproof.com/FunctionSpaceSingletons.htm

Where do you show existence of a = {z} ?

[Mostowski Collapse]

Without existence of Singleton, your proof of existence
of FunctionSpaceSingleton is only conditional. You
didn't prove existence of FunctionSpaceSingleton .

Seeing no proof, I can only assume you were lying when

you claimed a proof of FunctionSpaceSingleton .
Please show us, Dan Christensen.

On the other hand, in ZFC an existence proof is relatively easy.

[Dan Christensen]

It is assumed in the premise on line 2. I just needed a simple test case. The next one has a set with two elements.

BTW, the first line should be an axiom, not a premise. It doesn't make any difference to the end result since it has no free variables and was not discharged.

So, no bug.

[Mostowski Collapse]

Existence of singleton is not assumed.
And existence of singleton function is not derived from singleton existence assumption.

You only prove:

ALL(x):ALL(z):[Set(x) & ALL(a):[a e x <=> a=z] =>

You don't prove:

ALL(a):ALL(z):EXIST(x):[Set(x) & ALL(a):[a e x <=> a=z] =>

The later would be the singleton existence assumption.
Ideally you don't need this assumption, ideally its in your set theory.

[Mostowski Collapse]

Corr.: Typo

/* Singelton Existence */
ALL(z):EXIST(x):[Set(x) & ALL(a):[a e x <=> a=z]]

See also ZFC:

The set {A,A} is abbreviated {A}, called the singleton containing A.
https://en.wikipedia.org/wiki/Axiom_of_pairing#Consequences

So we don't know whether the Dan-O-Matik function space:

{ f | ALL(x):[x e {z} => f(x) e {z}] }

Really exists for all z. It only exists if {z} exists.
Its the same nonsense like your Dedekind Proof.

We don't know whether a Peano structure really
exists in DC Proof. Dedekind existence is missing.

[Mostowski Collapse]

Interesting twist the Russell construction also shows
that there is not universal set, since we have:

∀s∃y¬y∈s ⇔ ¬∃s∀y y∈s

Now I can do the Russell construction also in my FOL prover.
Had to add bi-conditional, otherwise too much typing,
and otherwise also too much proving:

?- prove0('∀s∃y∀x(x∈y ⇔ x∈s ∧ ¬x∈x) ⇒ ∀s∃y¬y∈s', 3, unicode), !.
http://www.xlog.ch/izytab/moblet/en/docs/18_live/34_bil2022/paste22/package.html

So we can prove for every set there is an element y outside
of the set. Only the Subset axiom is needed:

1. ∀s ∃y ∀x (x ∈ y ⇔ x ∈ s ∧ ¬x ∈ x) ⇒ ∀s ∃y ¬y ∈ s
2. ∀s ∃y ¬y ∈ s (T⇒2 1)
3. ¬∀s ∃y ∀x (x ∈ y ⇔ x ∈ s ∧ ¬x ∈ x) (T⇒1 1)
4. ∃y ¬y ∈ a (T∀ 2)
5. ¬∃y ∀x (x ∈ y ⇔ x ∈ a ∧ ¬x ∈ x) (F∀ 3)
6. ¬∀x (x ∈ b ⇔ x ∈ a ∧ ¬x ∈ x) (F∃ 5)
7. ¬b ∈ a (T∃ 4)
8. ¬(b ∈ b ⇔ b ∈ a ∧ ¬b ∈ b) (F∀ 6)
9. ¬(b ∈ b ∧ b ∈ a ∧ ¬b ∈ b) (F⇔1 8)
10. ¬(b ∈ a ∧ ¬b ∈ b) (F∧2 9)
11. ¬b ∈ b (F∧1 9)
12. ¬¬b ∈ b (F∧2 10)
13. ¬b ∈ a (F∧1 10)
14. b ∈ b (F¬ 12)
✓ (ax 11, 14)
9. b ∈ b ∨ b ∈ a ∧ ¬b ∈ b (F⇔2 8)
10. b ∈ a ∧ ¬b ∈ b (T∨2 9)
11. b ∈ b (T∨1 9)
12. b ∈ a (T∧1 10)
✓ (ax 7, 12)
12. ¬b ∈ b (T∧2 10)
✓ (ax 12, 11)

[Mostowski Collapse]

The butterfly paradox is not provable for set-like function,
its only an artefact of Dan-O-Matik function spaces,
his existence axiom and his function axiom. And

provided we could do the singleton extension G =
H u { (a,b) }. In set-like functions there is a substantial
problem how to translated the following:

EXIST(y):EXIST(g):[g e F & ~g(y) e color] .

According to Russells On Denoting "not the X is Y" has
near or far scope translation. Similiarly we can
translate the above two ways.

i) Near Scope Translation
EXIST(y):EXIST(g):[g e F & ~EXIST(z):[(y,z) e g & z e color]] .
ii) Far Scope Translation
EXIST(y):EXIST(g):[g e F & EXIST(z):[(y,z) e g & ~z e color] .

Me thinks i) is provably false because g e F implies
EXIST(z):[(y,z) e g & z e color] is true, provided butterfly is
non-empty, and if butterfly is empty, F is empty, false again.

Me thinks ii) is also provably false because g e F and
(y,z) e g implies z e color is true.

[Dan Christensen]

On Tuesday, January 18, 2022 at 4:14:29 AM UTC-5, Mostowski Collapse wrote:
> Existence of singleton is not assumed.

In this case.

> And existence of singleton function is not derived from singleton existence assumption.
>
> You only prove:
>
> ALL(x):ALL(z):[Set(x) & ALL(a):[a e x <=> a=z] =>
>

I prove that for every singleton {z}, there exists a function space comprised of those functions mapping {z} to itself.

ALL(x):ALL(z):[Set(x) & ALL(a):[a in x <=> a=z]
=> EXIST(fs):[Set(fs) & ALL(f):[f in fs <=> ALL(d):[d in x => f(d) in x]] & ALL(f):[f in fs <=> f(z)=z]]]

> You don't prove:
>
> ALL(a):ALL(z):EXIST(x):[Set(x) & ALL(a):[a e x <=> a=z] =>
>

So what?

[Dan Christensen]

On Tuesday, January 18, 2022 at 8:59:30 AM UTC-5, Mostowski Collapse wrote:
> The butterfly paradox is not provable for set-like function,

> its only an artefact of DC Proof function spaces,

> his existence axiom and his function axiom.

Still waiting for you to complete that proof, Jan Burse.

Dan

[Timothy Golden]

On Saturday, January 15, 2022 at 1:49:48 PM UTC-5, Dan Christensen wrote:
> I am considering a new Function Space axiom for DC Proof of the form:
>

> 1. ALL(a):ALL(b):[Set(a) & Set(b) => EXIST(c):[Set(c) & ALL(f):[f in c <=> ALL(d):[d in a => f(d) in b]]]]
> (Function Space)
>
> To justify it, consider my proof of the theorem:
>
> Given sets x and y we can construct the set fs consisting of all those function-like subsets of the Cartesian product of x and y. For each element f in fs, we can prove the existence of a unique function g: x --> y such that g(a)=b <=> (a, b) in f.
>
> Formal proof: https://www.dcproof.com/FunctionSpace.htm (138 lines, re-posted from earlier this month)
>
> Your comments?

Not sure what happened to the function thread; Guess I lost it. Dan, I'm not sure how much formalities need to be taken some of the time.
I am all for your freedom to construct something that completely disagrees; even with standard functional analysis. The by-products of such a theory A and another pure and free-standing theory B, and if we are to be general then there ought to be room for the threes and the fours and of course the One. If the one is to be stated it is unification. Thence we are taught that the twos are binary falsehood and truth. That the three can at this place in time form a trio in discretes is branched against another option to treat the three as the first continuous loop. This then in the fours develops a bubble that in the fives of course continues onward into volumetric proportions. Something puzzling does occur at the five yet it was present in the three and the two-form; the one-form; the four form however lacks the peculiarity. The four-form is quite sad and disappointing, really. Looking back on history perhaps we will see this expressed by others. Nah. The family P1P2P3P4P5P6P7 have been taken in magnitudinal form which provides ordinary vector space. Their unitized image is readily available. The purity of the unitized image is sufficient and indeed ordinary arithmetic products are rotationally behaved. These products are highly rotational; they obey modulo-n principles. P6 are of a class just their own in their natural pairing, inversions, and triples. Their kaleidoscopic properties are best of the lower lot, at least. Now I see this isn't saying much, but that is from top down thinkers, I would think. From the bottom up, sir. From the top down, sir. From the other side, sir. The other way, sir. Sorry, sir. You lost me, sir.

I think it is interesting that the function has taken form in computer programming stronger really than it has in mathematics. These overburdened cases of disbelievable functions is troublesome. Why should a second derivative suffice in characterizing nature? We are taught that our force fields of energy result in accelerations. This is known as the kinetic form, and it is claimed to be reused within thermodynamics. I find this theory not laughable, but falsifiable none the less.

If mathematics suffers a similar fate, and I do see that, and without hate, honestly, but with obvious confrontational energy, as in there is another way forward. This power I believe we all feel yet within mathematics it seems the laws are so narrow that the room to work is sparsely available.
There is something about operator theory, related to the Cartesian product, that is not quite right. Functional analysis per se rests its hat here. That functions are like operators is clear. They compute something, and yet in the guts of the theory something fowl is brooding. It's smell is of estrogen really, and hopefully the eggs are well kept.

[Mostowski Collapse]

Q: How do you use DC poop to prove Landau's:

∀x∀y(x + y = y + x)

A1: Not at all, it doesn't use x e N. LoL

A2: With x e N, going ZigZag between FOL function symbols
and set like functions, by the "help" of the Function Axiom,
producing 1000 lines of proof.

I don't call this "help". Its rather a patch for an otherwise
botched system, that cannot work how mathematical
text books or Landau would prove the matter.

[Dan Christensen]

On Thursday, January 20, 2022 at 2:28:56 PM UTC-5, Mostowski Collapse wrote:
> Q: How do you use DC Proof to prove

>
> ∀x∀y(x + y = y + x)
>

https://dcproof.com/AddComm.htm

[Chris M. Thomasson]

On 1/20/2022 11:28 AM, Mostowski Collapse wrote:
> Q: How do you use DC poop to prove Landau's:
>
> ∀x∀y(x + y = y + x)

[...]

For some reason this makes me think of using a physical scale as some
sort of aid for a "proof". The scale shall balance, therefore x + y
equals y + x. Say:

x = 1 unit weight
y = 2 unit weights

placing an x _and_ a y on the left hand side of the scale shall balance
when we place a y _and_ an x on the right hand side.

Too crude?

[FromTheRafters]

Chris M. Thomasson explained on 1/21/2022 :

https://math.stackexchange.com/questions/2677192/prove-addition-is-commutative-using-axioms-definitions-and-induction

...but he wants DC Proof to do it.

[Jim Burns]

"Too crude?" is a fair question.

We want a proof to be a reliable statement-path
from what we already know to new knowledge.
But we know x+y = y+x already. It's not new.
_Whatever_ our candidate proof of x+y = y+x is,
we won't get the wrong answer. What would it
mean to be unreliable in this case?

I suggest taking the form of the candidate proof and
re-writing it for a different topic, one in which
it would give the wrong answer. If you can do that,
it wasn't reliable in its previous incarnation,
either.

What do we have that _does not_ commute?
Rotations in 3-space is a nice, physical example.
Perhaps a different example springs to your mind.

Take a standard 6-die.

(i)
Roll it to the right and roll it up.

\ 3 / \ 3 / \ 5 /
5 1 2 6 5 1 6 4 1
/ 4 \ / 4 \ / 2 \

(ii)
Alternatively, roll it up and roll it to the right.

\ 3 / \ 1 / \ 1 /
5 1 2 5 4 2 3 5 4
/ 4 \ / 6 \ / 6 \

Observe that the die is in the same position?
No! The die is not in the same position.

The candidate proof of x+y = y+x could be stated

(i)
Add x units to the left pan and add y units to
the left pan.

(ii)
Add y units to the right pan and add x units
to the right pan.

Observe that the left and right pans balance.

And, yes, the pans balance. We know they do.

But, if we _didn't_ know they do, if we only
knew we were applying two operations in two
orders, like up(right(die)) and right(up(die)),
we couldn't say for sure that the two outcomes
would be the same.

This proof only looks convincing because we start out
convinced. Because x+y = y+x is not _new_ knowledge.
But we want proofs to be able to give us new knowledge.

----
There's a nice graphic here that summarizes the
connections between these properties. With proofs.
https://en.wikipedia.org/wiki/Proofs_involving_the_addition_of_natural_numbers

These proofs won't work for rotations in 3-space.
They all lead back to D1,D2,D3,D4, and they don't
apply to rotations in 3-space.

D1.
x + 0 = x

D2.
x + Sy = S(x + y)

D3.
x*0 = 0

D4.
x*Sy = x*y + x

L5. (D1,D2,induction)
0 + x = x

L6. (D1,D2,induction)
Sx + y = S(x + y)

L7. (D1,D2,L5,L6,induction)

x + y = y + x

L8. (D1,D2,induction)
(x + y) + z = x + (y + z)

L9. (D1,D2,D3,D4,L8,induction)
x*(y + z) = x*y + x*z

L10. (D1,D3,D4,induction)
0*x = x

L11. (D1,D2,D3,D4,L7,L8,induction)
Sx*y = x*y + y

L12. (D3,D4,L10,L11,induction)
x*y = y*x

L13. (D3,D4,L9,induction)
(x*y)*z = x*(y*z)