New DC Proof Function Space axiom:

One variable:

1. ALL(dom):ALL(cod):[Set(dom) & EXIST(a1):a1 in dom & Set(cod)
=> EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):[a1 in dom => f(a1) in cod]]]]
Fn Space

Two variables:

2. ALL(dom):ALL(cod):[Set'(dom) & EXIST(a1):EXIST(a2):(a1,a2) in dom & Set(cod)
=> EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):ALL(a2):[(a1,a2) in dom => f(a1,a2) in cod]]]]
Fn Space

Dan

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

Are you suffering the John Gabriel syndrome???

On Saturday, January 22, 2022 at 2:31:43 PM UTC-5, Dan Christensen wrote:
> New DC Proof Function Space axiom:
>
> One variable:
>
> 1. ALL(dom):ALL(cod):[Set(dom) & EXIST(a1):a1 in dom & Set(cod)
> => EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):[a1 in dom => f(a1) in cod]]]]
> Fn Space
>
> Two variables:
>
> 2. ALL(dom):ALL(cod):[Set'(dom) & EXIST(a1):EXIST(a2):(a1,a2) in dom & Set(cod)
> => EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):ALL(a2):[(a1,a2) in dom => f(a1,a2) in cod]]]]
> Fn Space
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Your comprehension:

ALL(f):[f in fsp <=> ALL(a1):[a1 in dom => f(a1) in cod]]]]

Leads to a proper class, even if dom and cod are non-empty.
Which then leads to an inconsistency.

Dan Christensen schrieb am Samstag, 22. Januar 2022 um 20:31:43 UTC+1:
> New DC Proof Function Space axiom:
>
> One variable:
>
> 1. ALL(dom):ALL(cod):[Set(dom) & EXIST(a1):a1 in dom & Set(cod)
> => EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):[a1 in dom => f(a1) in cod]]]]
> Fn Space
>
> Two variables:
>
> 2. ALL(dom):ALL(cod):[Set'(dom) & EXIST(a1):EXIST(a2):(a1,a2) in dom & Set(cod)
> => EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):ALL(a2):[(a1,a2) in dom => f(a1,a2) in cod]]]]
> Fn Space
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Thats quite straight forward to show. Take dom={y} and cod={y}.
Now take an arbitrary set S, with y e S. We can prove:

ALL(a1):[a1 in S => f(a1) in {y}] => ALL(a1):[a1 in {y} => f(a1) in {y}]

Here is a prove, encoding x in y as Exy:

(EyS ∧ ∀a(EaS → f(a)=y)) → ∀a(a=y → f(a)=y) is valid.
https://www.umsu.de/trees/#EyS~1~6a%28EaS~5f%28a%29=y]~5~6a%28a=y~5f%28a%29=y%29

So a Dan-O-Matik function f : S -> {y} is also a Dan-O-Matik
function f : {y} -> {y}. So that we get:

{ f | f : S -> {y} Dan-O-Matik } ⊆ { f | f : {y} -> {y} Dan-O-Matik }

Thats in stark contrast to the usual function space in math
text books, where there is only a single function
f : S -> {y}, namely the set of pairs f = { (x,y) | x e S }, and

further on math text books f1=\=f2 for S1=\=S2.
So a Dan-O-Matik function space { f | f : {y} -> {y} Dan-O-Matik }
is already a proper class, since S was arbitrary?

Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 17:44:50 UTC+1:
> Your comprehension:
> ALL(f):[f in fsp <=> ALL(a1):[a1 in dom => f(a1) in cod]]]]
> Leads to a proper class, even if dom and cod are non-empty.
> Which then leads to an inconsistency.
> Dan Christensen schrieb am Samstag, 22. Januar 2022 um 20:31:43 UTC+1:
> > New DC Proof Function Space axiom:
> >
> > One variable:
> >
> > 1. ALL(dom):ALL(cod):[Set(dom) & EXIST(a1):a1 in dom & Set(cod)
> > => EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):[a1 in dom => f(a1) in cod]]]]
> > Fn Space
> >
> > Two variables:
> >
> > 2. ALL(dom):ALL(cod):[Set'(dom) & EXIST(a1):EXIST(a2):(a1,a2) in dom & Set(cod)
> > => EXIST(fsp):[Set(fsp) & ALL(f):[f in fsp <=> ALL(a1):ALL(a2):[(a1,a2) in dom => f(a1,a2) in cod]]]]
> > Fn Space
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Sunday, January 23, 2022 at 11:52:54 AM UTC-5, Mostowski Collapse wrote:
> Thats quite straight forward to show. Take dom={y} and cod={y}.
> Now take an arbitrary set S, with y e S. We can prove:
>

> ALL(a1):[a1 in S => f(a1) in {y}] => ALL(a1):[a1 in {y} => f(a1) in {y}]
>

Not sure what your are getting at here, but in DC Proof, there is no axiom or theorem to the effect that ALL(a):EXIST(b):[Set(b) & a in b].
> Here is a prove, encoding x in y as Exy:
>
> (EyS ∧ ∀a(EaS → f(a)=y)) → ∀a(a=y → f(a)=y) is valid.

Translating the antecedent: [y in s & ALL(a):[a in s => f(a) = y]] =>???

Makes no sense.

Dan

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

On Sunday, January 23, 2022 at 11:52:54 AM UTC-5, Mostowski Collapse wrote:
> Thats quite straight forward to show. Take dom={y} and cod={y}.
> Now take an arbitrary set S, with y e S. We can prove:
>

> ALL(a1):[a1 in S => f(a1) in {y}] => ALL(a1):[a1 in {y} => f(a1) in {y}]
>

Not sure what your are getting at here, but in DC Proof, there is no axiom or theorem to the effect that ALL(a):EXIST(b):[Set(b) & a in b].

> Here is a prove, encoding x in y as Exy:
>
> (EyS ∧ ∀a(EaS → f(a)=y)) → ∀a(a=y → f(a)=y) is valid.

Translating the antecedent: [y in S & ALL(a):[a in S => f(a) = y]]

This makes no sense.

Dan

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

WHATS WRONG WITH YOU???

The antecedent says:

y in S:
y e S as I said, S is an arbitrary set that contains y.

ALL(a):[a in S => f(a) = y]]:
as I said, f : S -> {y} Dan-O-Matik style.

So the proof gives, you can add Set(S), doesn't change the proof:

y e S
f : S -> {y} Dan-O-Matik style.
∴ f : {y} -> {y}, Dan-O-Matik style.

So your singleton function space { f | f : {y} -> {y} }, contains
all f : S -> {y} functions as well. Thats a very strange thing,

because it makes { f | f : {y} -> {y} } a proper class, not
a set anymore. Subsequently your logic is unsatisfiable.

Dan Christensen schrieb am Sonntag, 23. Januar 2022 um 21:59:25 UTC+1:
> On Sunday, January 23, 2022 at 11:52:54 AM UTC-5, Mostowski Collapse wrote:
> > Thats quite straight forward to show. Take dom={y} and cod={y}.
> > Now take an arbitrary set S, with y e S. We can prove:
> >
>
>
> > ALL(a1):[a1 in S => f(a1) in {y}] => ALL(a1):[a1 in {y} => f(a1) in {y}]
> >
> Not sure what your are getting at here, but in DC Proof, there is no axiom or theorem to the effect that ALL(a):EXIST(b):[Set(b) & a in b].
> > Here is a prove, encoding x in y as Exy:
> >
> > (EyS ∧ ∀a(EaS → f(a)=y)) → ∀a(a=y → f(a)=y) is valid.
> Translating the antecedent: [y in S & ALL(a):[a in S => f(a) = y]]
>
> This makes no sense.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

BTW ∴ is the tea plantation sign:

> y e S
> f : S -> {y} Dan-O-Matik style.
> ∴ f : {y} -> {y}, Dan-O-Matik style.

See also:
https://en.wikipedia.org/wiki/Therefore_sign

Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 22:52:09 UTC+1:
> WHATS WRONG WITH YOU???
>
> The antecedent says:
>
> y in S:
> y e S as I said, S is an arbitrary set that contains y.
>
> ALL(a):[a in S => f(a) = y]]:
> as I said, f : S -> {y} Dan-O-Matik style.
>
> So the proof gives, you can add Set(S), doesn't change the proof:
>
> y e S
> f : S -> {y} Dan-O-Matik style.
> ∴ f : {y} -> {y}, Dan-O-Matik style.
>
> So your singleton function space { f | f : {y} -> {y} }, contains
> all f : S -> {y} functions as well. Thats a very strange thing,
>
> because it makes { f | f : {y} -> {y} } a proper class, not
> a set anymore. Subsequently your logic is unsatisfiable.
> Dan Christensen schrieb am Sonntag, 23. Januar 2022 um 21:59:25 UTC+1:
> > On Sunday, January 23, 2022 at 11:52:54 AM UTC-5, Mostowski Collapse wrote:
> > > Thats quite straight forward to show. Take dom={y} and cod={y}.
> > > Now take an arbitrary set S, with y e S. We can prove:
> > >
> >
> >
> > > ALL(a1):[a1 in S => f(a1) in {y}] => ALL(a1):[a1 in {y} => f(a1) in {y}]
> > >
> > Not sure what your are getting at here, but in DC Proof, there is no axiom or theorem to the effect that ALL(a):EXIST(b):[Set(b) & a in b].
> > > Here is a prove, encoding x in y as Exy:
> > >
> > > (EyS ∧ ∀a(EaS → f(a)=y)) → ∀a(a=y → f(a)=y) is valid.
> > Translating the antecedent: [y in S & ALL(a):[a in S => f(a) = y]]
> >
> > This makes no sense.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

That the { f | f: {y} -> {y} } function space exists, where
f :{y} -> {y} is read Dan-O-Matik style, is not my idea,

it from your blogging here:
https://dcproof.com/FunctionSpaceSingletons.htm

In your Peano, there are the singletons {0}, {1}, {2}, etc..
since the set N exists, just use {n} = { x e N | x = n }.

Now this function space is a proper class, because it
also contains every f : S -> {y}. Thats a strange thing.

Shouldn't happen in text book mathematics.

Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 22:55:00 UTC+1:
> BTW ∴ is the tea plantation sign:
> > y e S
> > f : S -> {y} Dan-O-Matik style.
> > ∴ f : {y} -> {y}, Dan-O-Matik style.
> See also:
> https://en.wikipedia.org/wiki/Therefore_sign
> Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 22:52:09 UTC+1:
> > WHATS WRONG WITH YOU???
> >
> > The antecedent says:
> >
> > y in S:
> > y e S as I said, S is an arbitrary set that contains y.
> >
> > ALL(a):[a in S => f(a) = y]]:
> > as I said, f : S -> {y} Dan-O-Matik style.
> >
> > So the proof gives, you can add Set(S), doesn't change the proof:
> >
> > y e S
> > f : S -> {y} Dan-O-Matik style.
> > ∴ f : {y} -> {y}, Dan-O-Matik style.
> >
> > So your singleton function space { f | f : {y} -> {y} }, contains
> > all f : S -> {y} functions as well. Thats a very strange thing,
> >
> > because it makes { f | f : {y} -> {y} } a proper class, not
> > a set anymore. Subsequently your logic is unsatisfiable.
> > Dan Christensen schrieb am Sonntag, 23. Januar 2022 um 21:59:25 UTC+1:
> > > On Sunday, January 23, 2022 at 11:52:54 AM UTC-5, Mostowski Collapse wrote:
> > > > Thats quite straight forward to show. Take dom={y} and cod={y}.
> > > > Now take an arbitrary set S, with y e S. We can prove:
> > > >
> > >
> > >
> > > > ALL(a1):[a1 in S => f(a1) in {y}] => ALL(a1):[a1 in {y} => f(a1) in {y}]
> > > >
> > > Not sure what your are getting at here, but in DC Proof, there is no axiom or theorem to the effect that ALL(a):EXIST(b):[Set(b) & a in b].
> > > > Here is a prove, encoding x in y as Exy:
> > > >
> > > > (EyS ∧ ∀a(EaS → f(a)=y)) → ∀a(a=y → f(a)=y) is valid.
> > > Translating the antecedent: [y in S & ALL(a):[a in S => f(a) = y]]
> > >
> > > This makes no sense.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, January 22, 2022 at 2:31:43 PM UTC-5, Dan Christensen wrote:

Rolled back to version of 2022-01-02 (dcsetup5.exe). Fixing bug and making improvements. Will announce new release here at sci.math.

Dan

Dan Christensen wrote:

> On Saturday, January 22, 2022 at 2:31:43 PM UTC-5, Dan Christensen
> wrote:
>
> Rolled back to version of 2022-01-02 (dcsetup5.exe). Fixing bug and
> making improvements. Will announce new release here at sci.math.

no shit Sherlock.

Belarus President Alexander Lukashenko - plandemic has been created by
"International Criminals"
https://www.bitchute.com/video/kcqVTleRn2sR/

but I can tell you the entire story. In capitalist europe, it's sharp
forbidden selling a product *in_connection_with_another_product*.

yet, they sold each and every fucking computer with
*Windoze_preinstalled*.

Now guess, the uneducated *mass_murderer* bill gaytes, involved the
governments to buy and inject each and every fucking person in those
countries with his injections, called "vaccines". Profit *20:1*, fuck you
all.

If you can't stand up against obvious government crimes against humanity,
for the sake of capitalism, you are a nobody.

don't go out protesting *singing*, you have to arrest those bankers sons
of a bitches. When I see them go out in thousands singing, makes me sick.

Will your function objects have an update? If f is a
function, then I can derive a new function f' as follows:

/ b if x=a
f'(x) = <
\ f'(x) if x ≠ a

We can write for f' for example f[a|->b]. Will your function
objects have equality, so that we can for example prove

this commutativity:

a1≠a2 => f[a1|->b1][a2|->b2] = f[a2|->b2][a1|->b1]

LoL

Dan Christensen schrieb am Montag, 24. Januar 2022 um 22:41:42 UTC+1:
> On Saturday, January 22, 2022 at 2:31:43 PM UTC-5, Dan Christensen wrote:
> Rolled back to version of 2022-01-02 (dcsetup5.exe). Fixing bug and making improvements. Will announce new release here at sci.math.
>
> Dan

In set theory one could define f[a|->b] for example as:

f[a|->b] := f \ ({a} x V) u ({a} x {b})

One can show by the ZFC comprehension axiom that f[a|->b]
exists set-like if f is set-like itself. First computing f1:

f1 = f \ ({a} x V)

Thats just f1 = { (x,y) | (x,y) e f & x≠a }. Now computing f',
here we need the unordered pairing twice and the union axiom:

f' = f1 u ({a} x {b})

Thats just f' = U {f1,{(a,b)}}. We didn't say what ordered
pairs are. Does it matter?

Mostowski Collapse schrieb am Dienstag, 25. Januar 2022 um 01:16:59 UTC+1:
> Will your function objects have an update? If f is a
> function, then I can derive a new function f' as follows:
>
> / b if x=a
> f'(x) = <
> \ f'(x) if x ≠ a
>
> We can write for f' for example f[a|->b]. Will your function
> objects have equality, so that we can for example prove
>
> this commutativity:
>
> a1≠a2 => f[a1|->b1][a2|->b2] = f[a2|->b2][a1|->b1]
>
> LoL
> Dan Christensen schrieb am Montag, 24. Januar 2022 um 22:41:42 UTC+1:
> > On Saturday, January 22, 2022 at 2:31:43 PM UTC-5, Dan Christensen wrote:
> > Rolled back to version of 2022-01-02 (dcsetup5.exe). Fixing bug and making improvements. Will announce new release here at sci.math.
> >
> > Dan