Re: Minor updates to DC Proof 2.0

[Dan Christensen]

Minor updates to DC Proof 2.0

(1) The text of the Function Axiom has been shortened and no longer overloads the function name. For functions of 1 variable, we now have:

ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
=> [ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
=> [(a1,b1) in f & (a1,b2) in f => b1=b2]]

=> EXIST(fun):ALL(a1):ALL(b):[a1 in dom & b in cod => [fun(a1)=b <=> (a1,b) in f]]]]
(Function)

f = set of ordered n-tuples
dom = domain
cod = codomain
fun = function name

Previous version:

ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
=> [ALL(a1):ALL(b):[(a1,b) in f => a1 in dom & b in cod]
& ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
& ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
=> [(a1,b1) in f & (a1,b2) in f => b1=b2]]

=> ALL(a1):ALL(b):[a1 in dom & b in cod => [f(a1)=b <=> (a1,b) in f]]]]
(Function)

(2) Corrected error message for Reflexivity Rule.

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]

I do not think this axiom makes any sense. It does not
satisfy Occams Razor. Why talk about functions "from A to B"
when its enough to talk about functions "over A", like

Kurt Gödel does in Chapter II, page 16 here, Definition 4.63:

Consistency of the Continuum Hypothesis. (AM-3), Volume 3
Annals of Mathematics Studies Band 264
https://www.orellfuessli.ch/shop/home/artikeldetails/A1004884502

You could go with a much simpler axiom, replace the
(Function from dom to cod) by this here:

ALL(f):ALL(dom):[Set'(f) & Set(dom)
=> [ALL(a1):[a1 in dom => EXIST(b):[(a1,b) in f]]

& ALL(a1):ALL(b1):ALL(b2):[a1 in dom

=> [(a1,b1) in f & (a1,b2) in f => b1=b2]]

=> EXIST(fun):ALL(a1):ALL(b):[a1 in dom => [fun(a1)=b <=> (a1,b) in f]]]]
(Function over dom)

It would then be a corrolary, no axiom of replacement needed
for this type of corrolary:

ALL(cod):[Set(cod) & ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
=> ALL(a1):[a1 in dom => fun(a1) in cod]]

LoL

[Mostowski Collapse]

Shit Orell Füssli wants 67.90 CHF for the booklet.
10 years ago a used one was only 5.90 CHF at Klio.

Like all the muses, Clio is a daughter of Zeus and the
Titaness Mnemosyne, goddess of memory.
https://www.klio-buch.ch/index.ahtml

[Dan Christensen]

On Monday, January 3, 2022 at 5:19:58 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 3. Januar 2022 um 05:41:34 UTC+1:
> > Minor updates to DC Proof 2.0
> >
> > (1) The text of the Function Axiom has been shortened and no longer overloads the function name. For functions of 1 variable, we now have:
> >
> > ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
> > => [ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
> > & ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
> > => [(a1,b1) in f & (a1,b2) in f => b1=b2]]
> >
> > => EXIST(fun):ALL(a1):ALL(b):[a1 in dom & b in cod => [fun(a1)=b <=> (a1,b) in f]]]]
> > (Function)
> >
> > f = set of ordered n-tuples
> > dom = domain
> > cod = codomain
> > fun = function name
> >
> > Previous version:
> >
> > ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
> > => [ALL(a1):ALL(b):[(a1,b) in f => a1 in dom & b in cod]
> > & ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
> > & ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
> > => [(a1,b1) in f & (a1,b2) in f => b1=b2]]
> >
> > => ALL(a1):ALL(b):[a1 in dom & b in cod => [f(a1)=b <=> (a1,b) in f]]]]
> > (Function)
> >

> You could go with a much simpler axiom, replace the
> (Function from dom to cod) by this here:
>
> ALL(f):ALL(dom):[Set'(f) & Set(dom)
> => [ALL(a1):[a1 in dom => EXIST(b):[(a1,b) in f]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in dom
> => [(a1,b1) in f & (a1,b2) in f => b1=b2]]
> => EXIST(fun):ALL(a1):ALL(b):[a1 in dom => [fun(a1)=b <=> (a1,b) in f]]]]
> (Function over dom)
>

Doesn't look very workable. In math textbooks, the signature of a function always explicitly specifies both the domain and codomain of a functions, e.g. f: A --> B. But, if you want to use another axiom, you can introduce it at the beginning of proofs requiring a proof of the existence of a particular function. Try it out. Prove the existence of the left inverse of any injective function:

ALL(x):ALL(y):ALL(f):[Set(x)
& Set(y)
& ALL(c):[c in x => f(c) in y]
& ALL(c):ALL(d):[c in x & d in x => [f(c)=f(d) => c=d]]

=> EXIST(rf):EXIST(g):[ALL(a):[a in rf => g(a) in x]
& ALL(a):[a in rf => f(g(a))=a]]]

It took me 121 lines with my new axiom. Can you beat that with yours?

[Mostowski Collapse]

Still hunted by shadows Dr. Frankenstein? Its easier to prove with
the shorter (Function over dom) axiom. Do you see a codomain
appear in the main theorem?

ALL(a):[a in rf => f(g(a))=a]]]

You need the codomain y to construct the range rf. But from then
on, I am pretty sure you get a shorter proof, with the (Function over dom)
axiom. But I didn't try yet.

LoL

[Scot Dino]

Mostowski Collapse wrote:

> ALL(a):[a in rf => f(g(a))=a]]]
> You need the codomain y to construct the range rf. But from then on, I
> am pretty sure you get a shorter proof, with the (Function over dom)
> axiom. But I didn't try yet. LoL
>
> Dan Christensen schrieb am Montag, 3. Januar 2022 um 14:46:16 UTC+1:

you two guys are *buttfuck_manure*, promoting lethal injections in people
and kids. If you can't arrest your buttfuck manure government, clauss
schwab, bill gaytes etc, shut the fuck up.

[Mostowski Collapse]

If you would have the axiom of replacement, you would
even not need the codomain y, you could construct the
range rf, from the domain x only.

[Dan Christensen]

On Monday, January 3, 2022 at 11:23:36 AM UTC-5, Mostowski Collapse wrote:
> Still hunted by shadows Dr. Frankenstein? Its easier to prove with
> the shorter (Function over dom) axiom.

Let's see your proof, Jan Burse.

> Do you see a codomain
> appear in the main theorem?
> ALL(a):[a in rf => f(g(a))=a]]]
> You need the codomain y to construct the range rf.

Indeed.

> But from then
> on, I am pretty sure you get a shorter proof, with the (Function over dom)
> axiom. But I didn't try yet.
>

I won't hold my breath.

[Dan Christensen]

It seems you are out to wipe out gullible Trump supporters with your scare mongering tactics. You must really hate them.

[Dan Christensen]

On Monday, January 3, 2022 at 11:30:22 AM UTC-5, Mostowski Collapse wrote:
> If you would have the axiom of replacement, you would
> even not need the codomain y, you could construct the
> range rf, from the domain x only.

Whatever it takes, Jan Burse. Let's see your proof.

Dan

[Mostowski Collapse]

Your anouncement is incomplete. What about the ALL(x) of DC Proof?
Did it also change. For example I can prove in DC Proof:

1 ALL(x):P(x)
Premise

2 ALL(x):P(x) => ALL(x):P(x)
Conclusion, 1

Can I also prove ALL(x):P(x) => ALL(x):[P(x) & P(f(x))] ?

P.S.: The HTML generator should automatically place a comment
with the version of the tool. Also its annoying that all versions are
name the same, dcproof2.exe, dcproof3.exe and dcproof4.exe all

are named DC Proof 2.0 in the window title. And also the splash
screen always shows DC Proof 2.0. Ever heard that versions
numbers could be updated?

Only when I use About DC Proof I see a little more info:

Release Date: 2019-09-14

[Dan Christensen]

On Monday, January 3, 2022 at 12:33:57 PM UTC-5, Mostowski Collapse wrote:
> Your anouncement is incomplete. What about the ALL(x) of DC Proof?
> Did it also change.

Again, just the text generated by the Function Axiom (as above), and an error message put out by the Reflexivity Axiom.

> For example I can prove in DC Proof:
>
> 1 ALL(x):P(x)
> Premise
>
> 2 ALL(x):P(x) => ALL(x):P(x)
> Conclusion, 1
>
> Can I also prove ALL(x):P(x) => ALL(x):[P(x) & P(f(x))] ?
>

In DC Proof, you need to define the function f, at the very least specifying its domain and codomain. Unlike standard FOL, such "messy details" must be made explicit in every proof, not just in some introductory notes in some dusty volume on a library shelf.

> P.S.: The HTML generator should automatically place a comment
> with the version of the tool. Also its annoying that all versions are
> name the same, dcproof2.exe, dcproof3.exe and dcproof4.exe all
>
> are named DC Proof 2.0 in the window title. And also the splash
> screen always shows DC Proof 2.0. Ever heard that versions
> numbers could be updated?
>

The About DC Proof screen gives the release date. There have been no major changes since version 2 was released maybe ten years ago. I usually announce any new releases here, even minor ones here. You need to pay closer attention, Jan Burse.

[Mostowski Collapse]

And what is the new rule for ALL(x) exactly?

Some handwaving that is even not found in

some introductory notes in some dusty volume

on a library shelf? And also not found on

your website. Maybe you keep a sticky note
in your kitchen close to the onions?

Dan Christensen schrieb:

[Dan Christensen]

On Monday, January 3, 2022 at 2:01:49 PM UTC-5, Mostowski Collapse wrote:
> And what is the new rule for ALL(x) exactly?
>

That hasn't changed in about ten years. Every axiom and rule in DC Proof is documented in the User Reference Guide (click on Help).

[Mostowski Collapse]

You are a horrible liar:

There is a new error message for U Spec Rule:
f(z) must be an element of a set

Shame on you!!!

Dan Christensen schrieb:

[Mostowski Collapse]

Here is evidence that you are a liar:

In dcproof2.exe I can prove:

1 ALL(x):P(x)
Premise

2 EXIST(y):[~P(y) | ~P(f(y))]
Premise

3 ~P(z) | ~P(f(z))
E Spec, 2

4 P(z)
U Spec, 1

5 P(f(z))
U Spec, 1, 3

6 ~[~~P(z) & ~~P(f(z))]
DeMorgan, 3

7 ~[P(z) & ~~P(f(z))]
Rem DNeg, 6

8 ~[P(z) & P(f(z))]
Rem DNeg, 7

9 P(z) & P(f(z))
Join, 4, 5

10 ~[P(z) & P(f(z))] & [P(z) & P(f(z))]
Join, 8, 9

11 ~EXIST(f):EXIST(y):[~P(y) | ~P(f(y))]
Conclusion, 2

12 ~~ALL(f):~EXIST(y):[~P(y) | ~P(f(y))]
Quant, 11

13 ALL(f):~EXIST(y):[~P(y) | ~P(f(y))]
Rem DNeg, 12

14 ALL(f):~~ALL(y):~[~P(y) | ~P(f(y))]
Quant, 13

15 ALL(f):ALL(y):~[~P(y) | ~P(f(y))]
Rem DNeg, 14

16 ALL(f):ALL(y):~~[~~P(y) & ~~P(f(y))]
DeMorgan, 15

17 ALL(f):ALL(y):[~~P(y) & ~~P(f(y))]
Rem DNeg, 16

18 ALL(f):ALL(y):[P(y) & ~~P(f(y))]
Rem DNeg, 17

19 ALL(f):ALL(y):[P(y) & P(f(y))]
Rem DNeg, 18

20 ALL(x):P(x) => ALL(f):ALL(y):[P(y) & P(f(y))]
Conclusion, 1

In dcproof4.exe I get stuck here:


1 ALL(x):P(x)
Premise

2 EXIST(y):[~P(y) | ~P(f(y))]
Premise

3 ~P(z) | ~P(f(z))
E Spec, 2

4 P(z)
U Spec, 1

I cannot make the next step:

5 P(f(z))
U Spec, 1, 3

Because of new error message:

f(z) must be an element of a set

Mostowski Collapse schrieb:

[Dan Christensen]

On Monday, January 3, 2022 at 2:09:50 PM UTC-5, Mostowski Collapse wrote:
> You are a horrible liar:
>
> There is a new error message for U Spec Rule:
> f(z) must be an element of a set
>

YIKES! You are really going off the deep end here, Jan Burse! Nothing seems to be working for you today.

I made no changes to the U Spec Rule. Just the Function and Reflexivity Axioms. I coded and tested the changes yesterday as I have described them here. Get a life!

[Mostowski Collapse]

You think you made no changes. But you can try yourself:
With dcproof2.exe you come past step 4:

1 ALL(x):P(x)
Premise

2 EXIST(y):[~P(y) | ~P(f(y))]
Premise

3 ~P(z) | ~P(f(z))
E Spec, 2

4 P(z)
U Spec, 1

5 P(f(z))
U Spec, 1, 3

With dcproof4.exe you don't come past step 4. Do you
want me to make a video or a screenshot?

Dan Christensen schrieb:

[Dan Christensen]

On Monday, January 3, 2022 at 2:20:00 PM UTC-5, Mostowski Collapse wrote:

> In dcproof4.exe I get stuck here:
>
>
> 1 ALL(x):P(x)
> Premise
>
> 2 EXIST(y):[~P(y) | ~P(f(y))]
> Premise
>
> 3 ~P(z) | ~P(f(z))
> E Spec, 2
>
> 4 P(z)
> U Spec, 1
>
> I cannot make the next step:
>
> 5 P(f(z))
> U Spec, 1, 3
>
> Because of new error message:
> f(z) must be an element of a set

That has been this rule for maybe a year or two, and still is. I have used it many times recently and got just that message. There would have to be a previous, active statement of the form f(x) in y to allow this specification. I announced this minor change at sci.math and sci.logic when I made it.

GET A LIFE, JAN BURSE!!!

[Mostowski Collapse]

Here are screenshots, since you don't believe me:

I can get till step 4:
<screenshot 1>
But I cannot get past step 4:
<screenshot 2>
Was using dcproof4.exe. With dcproof2.exe there was no such problem:
<screenshot 2>
https://medium.com/@janburse_2989/things-that-dont-work-anymore-in-dc-proof-b22d7bdc4762

Have Fun! Have Fun figuring out what you have changed,
and what you don't remember having changed.

LoL

Mostowski Collapse schrieb:

[Mostowski Collapse]

Liar a few seconds ago you wrote:

Dan Christensen schrieb:

> And what is the new rule for ALL(x) exactly?
That hasn't changed in about ten years.

Dan Christensen schrieb:

[Dan Christensen]

On Monday, January 3, 2022 at 2:28:30 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb:
> > On Monday, January 3, 2022 at 2:09:50 PM UTC-5, Mostowski Collapse wrote:
> >> You are a horrible liar:
> >>
> >> There is a new error message for U Spec Rule:
> >> f(z) must be an element of a set
> >>
> >
> > YIKES! You are really going off the deep end here, Jan Burse! Nothing seems to be working for you today.
> >
> > I made no changes to the U Spec Rule. Just the Function and Reflexivity Axioms. I coded and tested the changes yesterday as I have described them here. Get a life!
> >

> You think you made no changes. But you can try yourself:
> With dcproof2.exe you come past step 4:
>
> 1 ALL(x):P(x)
> Premise
> 2 EXIST(y):[~P(y) | ~P(f(y))]
> Premise
>
> 3 ~P(z) | ~P(f(z))
> E Spec, 2
>
> 4 P(z)
> U Spec, 1
>
> 5 P(f(z))
> U Spec, 1, 3
> With dcproof4.exe you don't come past step 4. Do you
> want me to make a video or a screenshot?
>

Yeah, that would be fun! HA, HA, HA!!!

Dan

[Mostowski Collapse]

Youre a fucked up liar! A few seconds ago you wrote:

Dan Christensen schrieb:

> > And what is the new rule for ALL(x) exactly?
> That hasn't changed in about ten years.

U Spec applied to ALL(x) is a ALL(x) rule, isn't it?
In natural deduction there are introduction and
elimination rules. And U Spec is an elimination rule.

Maybe I should have asked what are the rules, plural
for ALL(x) exactly. So that Dan-O-Matik understands
what people want to know about a proof tool.

They want to know them rules!!! For FOL you can
lookup the rules everywhere. But what are the exact
rules for this exotic tool DC Proof. They

are nowhere documented.

Mostowski Collapse schrieb:

[Dan Christensen]

On Monday, January 3, 2022 at 2:06:07 PM UTC-5, Dan Christensen wrote:
> On Monday, January 3, 2022 at 2:01:49 PM UTC-5, Mostowski Collapse wrote:
> > And what is the new rule for ALL(x) exactly?
> >
> That hasn't changed in about ten years. Every axiom and rule in DC Proof is documented in the User Reference Guide (click on Help).

Should be "two years."

[Dan Christensen]

On Monday, January 3, 2022 at 2:47:51 PM UTC-5, Mostowski Collapse wrote:

>
> They want to know them rules!!! For FOL you can
> lookup the rules everywhere. But what are the exact
> rules for this exotic tool DC Proof. They
>
> are nowhere documented.

Pay attention, Jan Burse. Once again, every axiom and rule is documented in the User Reference Guide. Click on Help. (In your case, maybe you should click on Psychiatric Help.) The tutorial demonstrates how to use most of them with worked examples and exercises with hints and full solutions.

[Mostowski Collapse]

dcproof2.exe says:

Restriction: No new variables may be introduced by Universal
Specification. Each variable here must have previously been introduced
by active Premise or Existential Specification statements. In the DC
Proof format, this means that only 'red' variables already found in
previous, active statements may be selected.

dcproof3.exe says:

Restrictions: (1) No new free variables can be introduced. (2) If any
functional expression (e.g. f(x)) is specified, it must be an element of
a set (e.g. f(x) e n). The functional expression f(x), after all, is
meaningful only in the context of it being an element of a set. (Similar
to restrictions for Reflexivity.)

Does this make DC Proof functions correct? I don't think so.
Now they are neither set-like functions nor FOL function symbols.

If they were set-like functions, one could prove:

1)
ALL(f):EXIST(dom):ALL(x):[x e dom <=> EXIST(y):(x,y) e f]

But I cannot prove 1) from ALL(x):[x e dom => f(x) e cod]

If they were FOL functoon symbols, one could prove:

ALL(x):P(x) => ALL(x):[P(x) & P(f(x))]

So what are the exotic functions from DC Proof?


Dan Christensen schrieb:

[Mostowski Collapse]

I cannot prove (in DC Proof):

ALL(x):[x e dom => f(x) e cod] =>
EXIST(s):ALL(x):[x e s <=> EXIST(y):(x,y) e f]

The later is what Kurt Gödel requires by his concept of
(Function over Domain), see for yourself, its all ink on paper:

Kurt Gödel does in Chapter II, page 16 here, Definition 4.63:

Consistency of the Continuum Hypothesis. (AM-3), Volume 3
Annals of Mathematics Studies Band 264
https://www.orellfuessli.ch/shop/home/artikeldetails/A1004884502

For a set-like function f, we can always query dom(f).
So what are the exotic functions of DC Proof? They
are neither FOL function symbols nor set-like functions.

What are they? Emperor penguins from antarctica?

[Dan Christensen]

On Monday, January 3, 2022 at 3:10:23 PM UTC-5, Mostowski Collapse wrote:
> dcproof2.exe says:
>
> Restriction: No new variables may be introduced by Universal
> Specification. Each variable here must have previously been introduced
> by active Premise or Existential Specification statements. In the DC
> Proof format, this means that only 'red' variables already found in
> previous, active statements may be selected.
>
> dcproof3.exe says:
>
> Restrictions: (1) No new free variables can be introduced. (2) If any
> functional expression (e.g. f(x)) is specified, it must be an element of
> a set (e.g. f(x) e n). The functional expression f(x), after all, is
> meaningful only in the context of it being an element of a set. (Similar
> to restrictions for Reflexivity.)
>
> Does this make DC Proof functions correct? I don't think so.
> Now they are neither set-like functions nor FOL function symbols.
>
> If they were set-like functions, one could prove:
>
> 1)
> ALL(f):EXIST(dom):ALL(x):[x e dom <=> EXIST(y):(x,y) e f]
>

Weird! You won't see anything like that in many math textbooks. Most likely something like:

ALL(a):[a in dom => f(a) in cod]

or

f: dom --> cod

where f = function name, dom = domain of f, cod = codomain of f.

> Here, f is defined only for elements of dom. We can make not inferences about f(x) for x not in dom, i.e. f(x) is undefined or meaningless for x not in dom.

> But I cannot prove 1) from ALL(x):[x e dom => f(x) e cod]
>

I guess that makes your system quite useless to mathematicians, but who cares, right, Jan Burse?

> If they were FOL functoon symbols, one could prove:
> ALL(x):P(x) => ALL(x):[P(x) & P(f(x))]
> So what are the exotic functions from DC Proof?
>

The same "exotic functions" found in just about every math textbook in every middle school, high school and college on the planet.

[Mostowski Collapse]

Whats wrong with you, THERE IS NO MY SYSTEM!!!!

Its not a question on my system. First of all there is
no my system. FOL is not my system. And second the
behaviour of FOL, and the behaviour of FOL+ZFC is

very well know. For example in FOL+ZFC one can always
prove, I am now using FOL ∀/∃ and not anymore DC Proof
ALL/EXIST:

/* Provable in FOL+ZFC */
∀f∃s∀x(x e s <=> ∃y (x,y) e f)

On the other hand we have:

/* Not Provable in DC Proof */
ALL(f):EXIST(s):ALL(x):[x e s <=> EXIST(y):(x,y) e f]

In DC Proof f alone does not imply Set'(f). So the above
cannot be derived. On the other hand in FOL+ZFC it can
be easily derived, which gives then rise to the

notation dom(f). So what would happen if we have Set'(f)
and ALL(x):[x e dom => f(x) e cod]. We wont get this here:

ALL(x):[x e dom <=> EXIST(y):(x, y) e f]

Because:
(1) The DC Proof Function Axiom works from set-like functions to
Emperor penguins from antarctica, the DC Proof function symbols.
(2) There is no axiom for the other direction, to go from
Emperor penguins from antarctica to set like functions.

In as far USpec rule is a little arbitrary f(x) e s doesn't mean
that we had ALL(x):[x e dom => f(x) e cod] which Dan-O-Matik wrongly
identifies with the notation f : dom -> cod. It could be some other

s, so there is no way to reflect f back to dom(f) in DC Proof. Its
not possible from f : dom -> cod interpreted as ALL(x):[x e dom =>
f(x) e cod] to determine the correct intended dom(f) = dom.

On the other hand in standard mathematic practice f: dom->cod
also means the following, I am now using FOL ∀/∃ and not
anymore DC Proof ALL/EXIST:

(Relation): ∀x∀y (x,y) e f => x e dom & y e cod
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

So these Emperor penguins from antarctica are quite remote
to anything from current mathematic practice. The new USpec
rule doesn't address that the root problem is still a wrong

translation of f : dom -> cod. A similare root cause that bugged
Russells "the X is Y". Now we have still not yet found a correct
translation of f : dom -> cod for DC Proof. The translation was

always done wrongly into some ideas of ALL(x):[x e dom => f(x) e cod].
This was never fixed, instead the USpec rule got broke two
years or so. So the church of DC Proof had one window broken,

since f : dom -> cod was never translated correctly. But instead
of fixing the translation, USpec rule got broken, so that the church
of DC Proof has now a further window broken,

so after two years or so the church of DC Proof went from one broken
window, to two broken windows.

[Dan Christensen]

On Monday, January 3, 2022 at 3:16:00 PM UTC-5, Mostowski Collapse wrote:

> I cannot prove (in DC Proof):
>
> ALL(x):[x e dom => f(x) e cod] =>
> EXIST(s):ALL(x):[x e s <=> EXIST(y):(x,y) e f]

Not sure why you would want to, but you can get very close using the Subset Axiom (line 5) as follows:

1. Set(dom) & Set(cod) & ALL(a):[a in dom => f(a) in cod]
(Premise)

2. Set(dom)
(Split, 1)

3. Set(cod)
(Split, 1)

4. ALL(a):[a in dom => f(a) in cod]
(Split, 1)

5. EXIST(s):[Set(s) & ALL(a):[a in s <=> a in dom & EXIST(b):[b in cod & f(a)=b]]]
(Subset, 2)

6. ALL(dom):ALL(cod):ALL(f):[Set(dom) & Set(cod) & ALL(a):[a in dom => f(a) in cod]

=> EXIST(s):[Set(s) & ALL(a):[a in s <=> a in dom & EXIST(b):[b in cod & f(a)=b]]]]
(Conclusion, 1)

[Dan Christensen]

On Monday, January 3, 2022 at 5:41:09 PM UTC-5, Mostowski Collapse wrote:

>
> /* Not Provable in DC Proof */
> ALL(f):EXIST(s):ALL(x):[x e s <=> EXIST(y):(x,y) e f]
>

See my previous posting here.

> In DC Proof f alone does not imply Set'(f).

The purpose of the Function Axiom in DC Proof is to construct, i.e. prove the existence of functions with certain properties by first constructing the required set of ordered n-tuples.

For any given function f: A --> B, you can easily construct {(x,y) in AxB: f(x)=y}

[snip]

> A similare root cause that bugged
> Russells "the X is Y". Now we have still not yet found a correct
> translation of f : dom -> cod for DC Proof. The translation was
>
> always done wrongly into some ideas of ALL(x):[x e dom => f(x) e cod].

Still in denial about that bald king of France. (HA, HA!!) As I recall, you never quite understood the principle of vacuous truth:

~P => [P => Q] in propositional logic

ALL(a):~P(a) => ALL(a):[P(a) => Q(a)] in predicate logic

[Mostowski Collapse]

DC Proof is subject to "Fake it till you make it". You claim:

Dan Christensen schrieb am Dienstag, 4. Januar 2022 um 06:45:47 UTC+1:
> For any given function f: A --> B, you can easily construct {(x,y) in AxB: f(x)=y}

Its not provable in DC Proof. You cannot prove in DC Proof:

ALL(x):[x e A => f(x) e B] => dom(f)=A

Because there is even no notion dom(f) in DC Proof.

P.S.:On the other hand in standard mathematics, you can prove:
f: A --> B => dom(f)=A

Just check out Kurt Gödel, like 100 years ago:
https://archive.org/details/dli.ernet.469738/page/n1/mode/2up

[Dan Christensen]

On Tuesday, January 4, 2022 at 4:27:27 AM UTC-5, Mostowski Collapse wrote:
> DC Proof is subject to "Fake it till you make it". You claim:
> Dan Christensen schrieb am Dienstag, 4. Januar 2022 um 06:45:47 UTC+1:
> > For any given function f: A --> B, you can easily construct {(x,y) in AxB: f(x)=y}
> Its not provable in DC Proof.

Wrong. Here is the conclusion of my 53 line formal proof using DC Proof:

53. ALL(x):ALL(y):ALL(f):[Set(x) & Set(y) & ALL(a):[a in x => f(a) in y]
=> EXIST(fxy):[Set'(fxy)
& ALL(a):ALL(b):[(a,b) in fxy
<=> a in x & b in y & f(a)=b]]]
(Conclusion, 1)

> You cannot prove in DC Proof:
>
> ALL(x):[x e A => f(x) e B] => dom(f)=A
>

True. Nowhere have I defined a function dom. But what could be more useless in writing mathematical proofs? Before you can even consider the existence of a function, you must START with set(s) that will be the domain and codomain.

> P.S.:On the other hand in standard mathematics, you can prove:
> f: A --> B => dom(f)=A
>

Not in the standard mathematics of most textbook proofs. Contrary to what you might think, what you call "mathematical logic" is NOT a required course in many pure math programs (e.g. at MIT). Ever wonder why that is the case?

[Mostowski Collapse]

You should be able to prove this here:

["Dan-O-Matik f: A -> B"] => dom(f)=A

Otherwise your tool is useless.
dom(f) is pretty standard:

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

If you cannot prove the above, then you can
also not prove that the dualspace has the same
finite dimension as the vectorspace:

dim(V)=n => dim(V*)=n

Try proving it with your confounded function notion:

The standard definition:

hom(V, F) := { f : V -> F |
∀x e V ∀y e V (f(x+y)=f(x)+f(y)) &
∀a e F ∀x e V a*f(x)=f(a*x) }

hom(V,F) abbreviated as V*:
https://en.wikipedia.org/wiki/Dual_space

What would happen if we take Dan-O-Matik-ism?

hom(V, F) := { "Dan-O-Matik f: V -> F" |
∀x e V ∀y e V (f(x+y)=f(x)+f(y)) &
∀a e F ∀x e V a*f(x)=f(a*x) }

Dan Christensen schrieb:

[Mostowski Collapse]

I didn't try it yet. A simpler challenge
from standard mathematics is this here:

|A|=n => |{ f : A -> 2 }| = 2^n

Can we also prove in DC Proof?

|A|=n => |{ "Dan-O-Matik f : A -> 2" }| = 2^n

Mostowski Collapse schrieb:

[Dan Christensen]

On Wednesday, January 5, 2022 at 8:21:01 AM UTC-5, Mostowski Collapse wrote:
> You should be able to prove this here:
>
> ["Dan-O-Matik f: A -> B"] => dom(f)=A
>
> Otherwise your tool is useless.
> dom(f) is pretty standard:
>
> https://en.wikipedia.org/wiki/Domain_of_a_function
>

No proofs there, Jan Burse. Grasping at straws as always. Really quite pathetic.

If we have ALL(a): [a in x => f(a) in y] , then we can say that f is a function with domain x and codomain y. There is nothing to prove. It is just terminology. Deal with it.

[Jahn Brown]

Mostowski Collapse wrote:

> You should be able to prove this here:
>
> ["Dan-O-Matik f: A -> B"] => dom(f)=A

you stupid troll, i saw once a bitch from the world bank, saying that
they only are waiting you, everybody, people to get "vaccinated". You
idiot. Arrest that motherlover clauss schwab, immediately. You stupid
fags.

and arrest all the partners of the *world_economic_forum*, ie mozilla,
the mozilla is a partner to the *world_economic_forum*, waiting you to
get vaccinated.

[Dan Christensen]

You certainly seem to be having an impact on gullible Trump supporters. They are dropping like flies.

[Michael Moroney]

On 1/5/2022 12:16 PM, Dan Christensen wrote:

That must be its goal. It's likely a Putin agent (or perhaps a CCP
agent) trying to manipulate the political climate by killing off the
Trumpeteers.

[Jahn Brown]

Dan Christensen wrote:

>> and arrest all the partners of the *world_economic_forum*, ie mozilla,
>> the mozilla is a partner to the *world_economic_forum*, waiting you to
>> get vaccinated.
>
> You certainly seem to be having an impact on gullible Trump supporters.
> They are dropping like flies.

Bill Clinton: 4,000 Government sponsored Medical Experiments on Citizens
https://www.bitchute.com/video/50EqaQN2xXh6/

Bill Gates' Military Tribunal and Execution
https://www.bitchute.com/video/8BVem5ofMmQ6/

[Jahn Brown]

Michael Moroney wrote:

>>> and arrest all the partners of the *world_economic_forum*, ie mozilla,
>>> the mozilla is a partner to the *world_economic_forum*, waiting you to
>>> get vaccinated.
>>
>> You certainly seem to be having an impact on gullible Trump supporters.
>> They are dropping like flies.
>>
> That must be its goal. It's likely a Putin agent (or perhaps a CCP
> agent) trying to manipulate the political climate by killing off the
> Trumpeteers.

they intently put plutonium into your medication, my friend. What is it I
don't understand??

[Dan Christensen]

On Wednesday, January 5, 2022 at 12:34:44 PM UTC-5, Jahn Brown wrote:
> Michael Moroney wrote:
>
> >>> and arrest all the partners of the *world_economic_forum*, ie mozilla,
> >>> the mozilla is a partner to the *world_economic_forum*, waiting you to
> >>> get vaccinated.
> >>
> >> You certainly seem to be having an impact on gullible Trump supporters.
> >> They are dropping like flies.
> >>
> > That must be its goal. It's likely a Putin agent (or perhaps a CCP
> > agent) trying to manipulate the political climate by killing off the
> > Trumpeteers.

But they are about the only ones dumb enough to buy into your disinformation and not get vaccinated. A true shame.

[Jahn Brown]

Dan Christensen wrote:

>> >> You certainly seem to be having an impact on gullible Trump
>> >> supporters.
>> >> They are dropping like flies.
>> >>
>> > That must be its goal. It's likely a Putin agent (or perhaps a CCP
>> > agent) trying to manipulate the political climate by killing off the
>> > Trumpeteers.
>
> But they are about the only ones dumb enough to buy into your
> disinformation and not get vaccinated. A true shame.

buying into what you stupid son of a bitch, get "vaccinated" with genetic
alteration toxic crap, just to get again "vaccinated"??

you stinking sub-human excrement, the humans evolved along MILLIONS of
years with OWN immune system, not being fucked up by an eugenicist mass
murder, who openly says the world is overpopulated, in spite that Europe
knowingly was going down in reproduction. You stinking shit, are going to
be arrested, judged and probably executed.

[Mostowski Collapse]

You don't know the scroll of truth? Don't you?

The scroll of truth is every wikipedia article
has exceptions to the top of its article, that
you find when you scroll down to the end of

the wikipedia article. For example domain need
not be a set, read the scroll of truth for yourself:

" In mathematics, the domain of a function is the set of inputs accepted by the function. "
[...]
https://en.wikipedia.org/wiki/Domain_of_a_function
" it is sometimes convenient in set theory to permit the domain of a function to be a proper class X "
https://en.wikipedia.org/wiki/Domain_of_a_function#Set_theoretical_notions

An example of a function that hasn't a set-like domain
is the operator *, that sends a vector space V to its dual
space V*. Or do you claim the vector spaces do

make up a set? The finite vector spaces would make up
a set if the field is fixed to lets say R. Then you can use
cross product and infinite uniion to show that

the finite vector spaces over R are also a set. But if the
field is not fixed, are the vector spaces then a set or
a class? Do you know that Dan-O-Matik?

[Dan Christensen]

On Wednesday, January 5, 2022 at 2:53:08 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 5. Januar 2022 um 16:46:57 UTC+1:
> > If we have ALL(a): [a in x => f(a) in y] , then we can say that f is a function with domain x
> > and codomain y. There is nothing to prove. It is just terminology. Deal with it.

> You don't know the scroll of truth? Don't you?
>
> The scroll of truth is every wikipedia article
> has exceptions to the top of its article, that
> you find when you scroll down to the end of
>
> the wikipedia article. For example domain need
> not be a set, read the scroll of truth for yourself:
>
> " In mathematics, the domain of a function is the set of inputs accepted by the function. "
> [...]
> https://en.wikipedia.org/wiki/Domain_of_a_function
> " it is sometimes convenient in set theory to permit the domain of a function to be a proper class X "

"Sometimes" maybe, but not in DC Proof. There are no "proper classes" in DC Proof set theory. Just sets and functions. Not unlike ZFC in this regard.

>> An example of a function that hasn't a set-like domain
> is the operator *, that sends a vector space V to its dual
> space V*.

There is no such V in DC Proof set theory. No objects are presumed to exist a priori in DC Proof, not even the empty set. The user would have to introduce additional axioms about this V at the beginning of their proofs.

[Mostowski Collapse]

Dan-O-Matik could learn something, he just explains
function spaces A -> B here in passing in the first seconds:

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

Task for Dan-O-Matik can you prove:

{ f | "Dan-O-Matik f : A -> B" } ⊆ P(A x B)

Thats litterally the requirement of set-like function spaces,
I want to explain Dan-O-Matik already for weeks,

but Dan-O-Matik refuses, denies, cranks it up, etc..

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 11:19:58 UTC+1:
> I do not think this axiom makes any sense. It does not
> satisfy Occams Razor. Why talk about functions "from A to B"
> when its enough to talk about functions "over A", like

>
> Kurt Gödel does in Chapter II, page 16 here, Definition 4.63:
>
> Consistency of the Continuum Hypothesis. (AM-3), Volume 3
> Annals of Mathematics Studies Band 264
> https://www.orellfuessli.ch/shop/home/artikeldetails/A1004884502
>

> You could go with a much simpler axiom, replace the
> (Function from dom to cod) by this here:
>
> ALL(f):ALL(dom):[Set'(f) & Set(dom)
> => [ALL(a1):[a1 in dom => EXIST(b):[(a1,b) in f]]
> & ALL(a1):ALL(b1):ALL(b2):[a1 in dom
> => [(a1,b1) in f & (a1,b2) in f => b1=b2]]
> => EXIST(fun):ALL(a1):ALL(b):[a1 in dom => [fun(a1)=b <=> (a1,b) in f]]]]
> (Function over dom)
>
> It would then be a corrolary, no axiom of replacement needed
> for this type of corrolary:
>
> ALL(cod):[Set(cod) & ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
> => ALL(a1):[a1 in dom => fun(a1) in cod]]
>
> LoL
> Dan Christensen schrieb am Montag, 3. Januar 2022 um 05:41:34 UTC+1:
> > Minor updates to DC Proof 2.0
> >
> > (1) The text of the Function Axiom has been shortened and no longer overloads the function name. For functions of 1 variable, we now have:
> >
> > ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
> > => [ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
> > & ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
> > => [(a1,b1) in f & (a1,b2) in f => b1=b2]]
> >
> > => EXIST(fun):ALL(a1):ALL(b):[a1 in dom & b in cod => [fun(a1)=b <=> (a1,b) in f]]]]
> > (Function)
> >
> > f = set of ordered n-tuples
> > dom = domain
> > cod = codomain
> > fun = function name
> >
> > Previous version:
> >
> > ALL(f):ALL(dom):ALL(cod):[Set'(f) & Set(dom) & Set(cod)
> > => [ALL(a1):ALL(b):[(a1,b) in f => a1 in dom & b in cod]
> > & ALL(a1):[a1 in dom => EXIST(b):[b in cod & (a1,b) in f]]
> > & ALL(a1):ALL(b1):ALL(b2):[a1 in dom & b1 in cod & b2 in cod
> > => [(a1,b1) in f & (a1,b2) in f => b1=b2]]
> >
> > => ALL(a1):ALL(b):[a1 in dom & b in cod => [f(a1)=b <=> (a1,b) in f]]]]
> > (Function)
> >
> > (2) Corrected error message for Reflexivity Rule.

[Mostowski Collapse]

This video also adresses some "conceptualism" nonsense of
WM, who thinks the ZFC power axiom makes P(omega) full.

The video goes also into Kurt Gödels, see reference below,
V = L, and then Cohen something. All the time dealing with

what the powerset could be inside a model. Nice!

[Dan Christensen]

On Wednesday, January 5, 2022 at 3:59:51 PM UTC-5, Mostowski Collapse wrote:

>
> Can you prove:
>
> { f | "f : A -> B" } ⊆ P(A x B)
>

You could easily construct F = {f in P(AxB) : For all x in A, there exists unique y in B such that (x, y) in f}.

For each f in F, we can then show that there exists g: A --> B such that for all x in A, we have (x, g(x)) in f.

[Mostowski Collapse]

Your Function Axiom doesn't make any sense.
You dont get the same set exponentiation with
the Dan-O-Matik nonsense:

B^A =\= { f | ALL(x):[x e A => fun(x) e B] }

Proof:
We can construct a f, with f not in B^A and Function Axiom
result fun, such that ALL(x):[x e A => fun(x) e B].
Just pick an arbitrary g in B^A and an arbitrary element

z not in A and not in B, then construct f = g u {(z,z)}.
Then the Function Axiom yields:

ALL(x):[x e A u {z} => fun(x) e B u {z}]

But its also easy to prove:

ALL(x):[x e A => fun(x) e B]

Just apply the Function Axiom to g, and obtain
gun, and observe that this can be derived:

ALL(x):[x e A => gun(x) = fun(x)]

[Mostowski Collapse]

Ha Ha, egregious error. Dan-O-Matik writes:
> For each f in F, we can then show that there exists g: A --> B such that for all x in A, we have (x, g(x)) in f.

But f in F already means f : A --> B. So what is his
g : A --> B then? Well its exactly not g : A --> B.

Its only ALL(x):[x e A => g(x) e B]. Your error is so
ingrained confusing the two, its hilarious.

[Mostowski Collapse]

In the context of DC Proof, g will be fun, and the Function
Axiom of DC Proof will only say ALL(x):[x e A => fun(x) e B].

Also the precondition of Function Axiom requires something
weaker that f e F. But the Function Axiom also works for f e F.
But f e F is the text book f : A -> B. The Function Axiom of

DC Proof doesn't require the text book f : A -> B, no requirement
f e P(A x B), it only requires "For all x in A, there exists unique y in
B such that (x, y) in f". But even if the DC Proof Function Axiom

would require the stronger f e F aka f : A -> B. Still the
outcome ALL(x):[x e A => fun(x) e B] would be as weak as before,
so that we cannot say fun : A -> B, for what drops out of

the DC Proof Function Axiom. Thats just nonsense.

[Dan Christensen]

On Thursday, January 6, 2022 at 12:12:34 AM UTC-5, Mostowski Collapse wrote:
> Your Function Axiom doesn't make any sense.

It is your system that doesn't make sense, Jan Burse. It makes no sense that you are making logical inferences in proofs about f(x) for x outside of the domain of definition for function f -- i.e. Burse's Paradox.

> You dont get the same set exponentiation

Irrelevant. Given sets x and y, and their Cartesian product xy, we can construct a set fs consisting of all those function-like subsets
of xy. 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. And no Burse's Paradox!

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

& [ALL(a):[a in x => EXIST(b):[b in y & (a,b) in f]]
& ALL(a):ALL(b1):ALL(b2):[a in x & b1 in y & b2 in y => [(a,b1) in f & (a,b2) in f => b1=b2]]]]

& ALL(f):[f in fs => EXIST(g):[ALL(a):[a in x => g(a) in y]
& ALL(a1):ALL(b):[a1 in x & b in y => [g(a1)=b <=> (a1,b) in f]]

& ALL(g'):[ALL(a):[a in x => g'(a) in y]
& ALL(a1):ALL(b):[a1 in x & b in y => [g'(a1)=b <=> (a1,b) in f]]

=> ALL(a):[a in x => g'(a)=g(a)]]]]]]

Link to HTML version of the formal proof (138 lines) to be posted later today.

[Dan Christensen]

https://www.dcproof.com/FunctionSpace.htm

[Dan Christensen]

On Thursday, January 6, 2022 at 5:14:18 PM UTC-5, Dan Christensen wrote:

> > Given sets x and y, and their Cartesian product xy, we can construct a set fs consisting of all those function-like subsets
> > of xy. 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. And no Burse's Paradox!
> >
> > ALL(x):ALL(y):[Set(x) & Set(y)
> > => EXIST(fs):[ALL(f):[f in fs <=> Set'(f)
> > & ALL(a):ALL(b):[(a,b) in f => a in x & b in y]
> >
> > & [ALL(a):[a in x => EXIST(b):[b in y & (a,b) in f]]
> > & ALL(a):ALL(b1):ALL(b2):[a in x & b1 in y & b2 in y => [(a,b1) in f & (a,b2) in f => b1=b2]]]]
> >
> > & ALL(f):[f in fs => EXIST(g):[ALL(a):[a in x => g(a) in y]
> > & ALL(a1):ALL(b):[a1 in x & b in y => [g(a1)=b <=> (a1,b) in f]]
> >
> > & ALL(g'):[ALL(a):[a in x => g'(a) in y]
> > & ALL(a1):ALL(b):[a1 in x & b in y => [g'(a1)=b <=> (a1,b) in f]]
> >
> > => ALL(a):[a in x => g'(a)=g(a)]]]]]]
> >
> > Link to HTML version of the formal proof (138 lines) to be posted later today.

> https://www.dcproof.com/FunctionSpace.htm

It is also possible to work backwards from ALL(a):[a in x => f(a) in y] to get a unique set of ordered pairs {(a, b) | a in x & b in y & f(a)=b}

Nothing at all profound about that. Intuitively obvious as they say. But it does demonstrate how to work with functions in DC Proof 2.0 in much that same way as you would in textbook math proofs.

https://www.dcproof.com/FunctionNotation.htm

[Mostowski Collapse]

Its also possible, its also possible, ... its also possible to show
that if the moon is made of cheese that then pigs can fly. You just
prove nonsense after nonsense. There is no bijection between:

A -> B (*)

and this collection:

{ f | ALL(x):[x e A => f(x) e B }

Because there is no bijection you can also not use the
two interchangeably. Your function axiom gives an injection
from A -> B into the collection. Since it allows to construct

an element from the collection for an element from A -> B.
But you know yourself what is needed for a bijection. You
proved yourself the Cantor-Schröder-Bernstein theorem.

So what is need for example would be an injection from
the collection back to A -> B. But it is easy to show that
there is no such injection.

(*) I am taking A -> B to be exactly this, and nothing else:
A -> B := { f e P(A x B) : For all x e A exist a unique y in B such that (x,y) e f }

[Mostowski Collapse]

So far with your latest proof, you only showed how to
get an element from A -> B for an element of the collection.
But you didn't show that this method is injective.

By injective, we mean really injective. Showing that
for f1 and f2 in the collection, and f1=\=f2 that then
the element from A -> B is also different.

Whereby f1=\=f2 is defined as existence of a separating element:

EXIST(x):f1(x)=\=f2(x)

The quantifier MUST range over the universe of discourse.

[Dan Christensen]

On Saturday, January 8, 2022 at 7:46:19 AM UTC-5, Mostowski Collapse wrote:

> So far with your latest proof, you only showed how to
> get an element from A -> B for an element of the collection.
> But you didn't show that this method is injective.
>

Again, I have shown that, given sets x and y, and their Cartesian product xy, we can construct a set fs consisting of all those function-like subsets of xy. 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. This it is a kind of functional mapping. And that, for each of those functions g, there exists a unique pre-image in fs this mapping. Thus, this mapping is one-to-one. It is effectively injective.

[Mostowski Collapse]

I mean by your latest remark, you started thinking of
the other direction of your function axiom:

Dan Christensen schrieb am Freitag, 7. Januar 2022 um 23:02:08 UTC+1:
> It is also possible to work backwards from ALL(a):[a in x => f(a) in y] to
get a unique set of ordered pairs {(a, b) | a in x & b in y & f(a)=b}

https://groups.google.com/g/sci.math/c/IWbD8BdJkv8/m/OHHB51B_AQAJ

For one f you get such a unique set of course. This
shows there is a backward mapping into the function space:

A -> B

From this collection:

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

But you nowhere show that this backward mapping is
injective. And without an injective backward mapping
there will be no bijection between the two. Since there

is no bijection, it is an error to use the two notions
A -> B and your Dan-O-Matik nonsense interchangeably.
They are not the same spaces. Never ever.

[Mostowski Collapse]

Corr::

From this collection:
{ f | ALL(x):[x in A => f(x) in B] }

[Dan Christensen]

On Saturday, January 8, 2022 at 11:02:44 AM UTC-5, Mostowski Collapse wrote:
> I mean by your latest remark, you started thinking of
> the other direction of your function axiom:
> Dan Christensen schrieb am Freitag, 7. Januar 2022 um 23:02:08 UTC+1:
> > It is also possible to work backwards from ALL(a):[a in x => f(a) in y] to
> get a unique set of ordered pairs {(a, b) | a in x & b in y & f(a)=b}
> https://groups.google.com/g/sci.math/c/IWbD8BdJkv8/m/OHHB51B_AQAJ
>
> For one f you get such a unique set of course. This
> shows there is a backward mapping into the function space:
>
> A -> B
>
> From this collection:
>
> { f | ALL(a):[a in x => f(a) in y] }
>
> But you nowhere show that this backward mapping is
> injective.

These proofs, of course, make use of the Function Axiom in DC Proof that models the notion of a function that is used in most textbook math proofs. It avoids Burse's Paradox that allows you to make questionable inferences about functions outside of their domain of definition.

You cannot deny that, using DC Proof, you can prove that for each function-like set of ordered pairs (as I call them), there corresponds a unique function of one variable? (See formal proof here: https://www.dcproof.com/FunctionSpace.htm - 138 lines)

You also cannot deny that, using DC Proof, you can prove that for each function of one variable, there corresponds a unique function-like set of ordered pairs? (See formal proof here: https://www.dcproof.com/FunctionNotation.htm - 134 lines)

I suppose it is up to you if you want to continue to make questionable inferences about functions outside of their domain of definition, contrary to standard mathematical practice. It is definitely NOT a strong selling point for YOUR alternative system whatever you may call it, Jan Burse.

[Mostowski Collapse]

Your Dan-O-Matik idea is anti-monotonic. The classical notion
is not anti-monotonic.

You only need the binary relation property (see wikipedia) of the
classical notion to show that it is not provable, to get an idea that
it is not provable:

/* Not Provable */
A ⊆ A', f ⊆ A' x B => f ⊆ A x B

Seriality and functional would go through, but binary relation
is the crux. The tree tool can find a counter-model, and show that
it is not provable.

(∀x(Ax → Cx) ∧ ∀x∀y(Fxy → (Cx ∧ By))) → ∀x∀y(Fxy → (Ax ∧ By)) is invalid.
Countermodel:
Domain: { 0 }
A: { }
C: { 0 }
F: { (0,0) }
B: { 0 }
https://www.umsu.de/trees/#~6x%28Ax~5Cx%29~1~6x~6y%28Fxy~5Cx~1By%29~5~6x~6y%28Fxy~5Ax~1By%29

[Dan Christensen]

On Saturday, January 8, 2022 at 5:51:57 PM UTC-5, Mostowski Collapse wrote:
> Your Dan-O-Matik idea is anti-monotonic. The classical notion
> is not anti-monotonic.
>
> You only need the binary relation property (see wikipedia) of the
> classical notion to show that it is not provable, to get an idea that
> it is not provable:
>
> /* Not Provable */
> A ⊆ A', f ⊆ A' x B => f ⊆ A x B
>
> Seriality and functional would go through, but binary relation
> is the crux. The tree tool can find a counter-model, and show that
> it is not provable.
>
> (∀x(Ax → Cx) ∧ ∀x∀y(Fxy → (Cx ∧ By))) → ∀x∀y(Fxy → (Ax ∧ By)) is invalid.

Where are you getting this nonsense???

Do you deny that you can prove that for each function-like set of ordered pairs (as I call them), there corresponds a unique function of one variable? (See formal proof here: https://www.dcproof.com/FunctionSpace.htm - 138 lines)

Do you deny that you can prove that for each function of one variable, there corresponds a unique function-like set of ordered pairs? (See formal proof here: https://www.dcproof.com/FunctionNotation.htm - 134 lines)

[Mostowski Collapse]

Dan-O-Matik halucinated:
> that 2 is a subset of 4 as at your link

You don't have to choose 2 and 4 this way.
You can also choose differently. The main point
would be to show that this collection exists:

{0,1,2,3,...}

Can you show existence of natural numbers in DC Proof.
In set theory omega exists so the class of infinite countable
well ordered sets without limit points is non empty.

Is the class of your Peano structures non-empty? I
doubt that you can executed the proof, because of
your recent changes. You cannot prove anymore:

> This is the proof that worked in dcproof2.exe, but
> does not work anymore in dcproof5.exe:
> [...]
> 8 ~Field(constr(a))
> U Spec, 6, 7
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/LGiS4I8UAwAJ

My speculation, technically you possibly cannot executed
the required proof anymore in DC Proof.

[Ubaldo Dortas]

Mostowski Collapse wrote:

> Dan-O-Matik halucinated:
>> that 2 is a subset of 4 as at your link
>
> You don't have to choose 2 and 4 this way.
> You can also choose differently. The main point would be to show that
> this collection exists:

SPAIN POLICE OFFICERS IN VALENCIA: "WE ARE WITH THE PEOPLE, NOT WITH
CORRUPT POLITICIANS. WE ARE IN CONTACT WITH PORTUGAL, ITALY, FRANCE,
AUSTRIA, SWITZERLAND, SWEDEN, GERMANY AND THE NETHERLANDS TO UNITE ALL
THE POLICE IN EUROPE! DOWN WITH THE HEALTH PASSPORT"

[Dan Christensen]

On Friday, January 14, 2022 at 12:47:52 PM UTC-5, Mostowski Collapse wrote:
> Dan-O-Matik halucinated:
> > that 2 is a subset of 4 as at your link
>
> You don't have to choose 2 and 4 this way.
> You can also choose differently. The main point
> would be to show that this collection exists:
>
> {0,1,2,3,...}
>
> Can you show existence of natural numbers in DC Proof.
> In set theory omega exists so the class of infinite countable
> well ordered sets without limit points is non empty.
>

It's much simpler in DC Proof. The user simply introduces the relatively self-evident Peano's Axioms at the beginning of any proof for N, S and 0 (or 1) using the Create Axiom option on the Logic menu.

1. Set(n)
(Axiom)

2. 0 in n
(Axiom)

3. ALL(a):[a in n => s(a) in n]
(Axiom)

4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
(Axiom)

5. ALL(a):[a in n => ~s(a)=0]
(Axiom)

6. ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in a => s(b) in a]
=> ALL(b):[b in n => b in a]]]
(Axiom)

These axioms takes the place of the ZFC Axiom of Infinity, a pedagogical nightmare IMHO. The set of natural numbers is a well known, easy to define, infinite set. No ordinals, omegas, classes, etc.

[Dan Christensen]

If wishes were horses...

[Ubaldo Dortas]

It says a lot about NATO if the secretary General protects and arms
countries such as the Ukraine, with large Neo-Nazi supporters and a
dictator for president. Almost as much as what is says about the attacks
on Yugoslavia, Libya, Syria, Afghanistan and Iraq.

[Mostowski Collapse]

Its a kind if axiom of infinity without the EXIST(n),
so its more canonical than ZFC, because you introduce

a name for n, the natural numbers. In ZFC there is
no name omega, you can unravel omega into a nameless

definite. Your axioms say:

> 2. 0 in n
> (Axiom)
>
> 3. ALL(a):[a in n => s(a) in n]
> (Axiom)
>
> 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> (Axiom)
>
> 5. ALL(a):[a in n => ~s(a)=0]
> (Axiom)
>

Why would you bash the axiom infinity when you
use the same. In set theory, you have an EXIST(n),

around 2 & 3, which then reads:

/* Zermelos Axiom of Infinity */
EXIST(n):[0 in n & ALL(a):[a in n => s(a) in n]]

And 4 & 5 can be derived from how you define s(_),
but it can be also unfolded, and us nameless.

Whats wrong with you?

Dan Christensen schrieb:

[Mostowski Collapse]

I mean we have internet nowadays, you can lookup
the axiom yourself:

/* Zermelos Axiom of Infinity */

exists S (0 in S & forall x (x in S => s(x) in S))
https://de.wikipedia.org/wiki/Unendlichkeitsaxiom

Compare with your axioms 2 and 3 wrapped in EXIST(n),
it is the same:

/* Dan-O-Matik Quantified */

EXIST(n):[0 in n & ALL(a):[a in n => s(a) in n]]

Its then possible to repeat the Zermelo construction
from 1908 in a way so that it gives induction schema.
You prove the same with >250 lines in your Dedekind

to Peano proof, but its more easier to prove.
Just define, i.e. define Omega N, where S is some
S from Zermelos Axiom of Infinity exists S I(S):

/* Definition of N in set theory */
N = { x e S | forall S' I(S') => x e S' }

Now you can show if for some set A subset N,
if I(A) then N subset A. Left as an exercise.

Which is your induction axiom:

some set A subset N

ALL(b):[b in a => b in n]

if I(A)

[0 in a & ALL(b):[b in a => s(b) in a]

then N subset A

ALL(b):[b in n => b in a]

The point of set theory is that you dont need
to give a canonical name like N, you can
always define it via comprehension.

And your induction follows.

Mostowski Collapse schrieb:

[Mostowski Collapse]

Here is a derivation of the induction schema,
in Wolfgang Schwartz Tree Tool:

/* Encoding Exy for x in y */
∀x(Exn ↔ ∀s(Is → Exs)), /* Definition of Omega aka n */
∀y(Eya → Eyn), /* A subset N */
Ia /* I(A) */
entails ∀y(Eyn → Eya). /* N subset A */
https://www.umsu.de/trees/#~6x%28Exn~4~6s%28Is~5Exs%29%29,~6y%28Eya~5Eyn%29,Ia|=~6y%28Eyn~5Eya%29

The proof is only 14 steps. Compare with your
pedagogical nightmare of >250 steps of DC poop.

LoL

P.S.: I(S) stands for (0 in S & forall x
(x in S => s(x) in S)), but its content is
not need in the proof.

P.P.S.: Because the content of I(S) is
not really needed, you can construct this
way a lot of other closures as well,

not only omega. And you get a lot of
different induction schematas. For example
the schema of hereditary finite sets etc.. etc..

Mostowski Collapse schrieb:

[Mostowski Collapse]

This simpler also works, you don't need the full
definition of the set N to derive the induction schema,
and that A subset N is also superflous,

the important part is:

/* Encoding Exy for x ∈ y */
∀x(ExN → ∀s(Is → Exs)), IA entails ∀y(EyN → EyA).
https://www.umsu.de/trees/#~6x%28Exn~5~6s%28Is~5Exs%29%29,~6y%28Eya~5Eyn%29,Ia|=~6y%28Eyn~5Eya%29

Now its not 14 steps proof, but 12 steps proof.
Works also in my tool, did not yet upload this version.
The new version supports infix ∈ notation:

1. ∀x (x ∈ N ⇒ ∀s (I(s) ⇒ x ∈ s)) ∧ I(A) ⇒ ∀y (y ∈ N ⇒ y ∈ A)
2. ∀y (y ∈ N ⇒ y ∈ A) (T⇒ 1)
3. ¬ (∀x (x ∈ N ⇒ ∀s (I(s) ⇒ x ∈ s)) ∧ I(A)) (T⇒ 1)
4. ¬ I(A) (F∧ 3)
5. ¬ ∀x (x ∈ N ⇒ ∀s (I(s) ⇒ x ∈ s)) (F∧ 3)
6. a ∈ N ⇒ a ∈ A (T∀ 2)
7. a ∈ A (T⇒ 6)
8. ¬ a ∈ N (T⇒ 6)
9. ¬ (a ∈ N ⇒ ∀s (I(s) ⇒ a ∈ s)) (F∀ 5)

10. a ∈ N (F⇒ 9)
✓

10. ¬ ∀s (I(s) ⇒ a ∈ s) (F⇒ 9)
11. ¬ (I(A) ⇒ a ∈ A) (F∀ 10)

12. I(A) (F⇒ 11)
✓

12. ¬ a ∈ A (F⇒ 11)
✓

[Dan Christensen]

> Its a kind if axiom of infinity without the EXIST(n),
> so its more canonical than ZFC, because you introduce
>
> a name for n, the natural numbers.

If you want to add existential quantifies if it would make your feel better, but why bother?

> In ZFC there is
> no name omega, you can unravel omega into a nameless
>
> definite. Your axioms say:
> > 2. 0 in n
> > (Axiom)
> >
> > 3. ALL(a):[a in n => s(a) in n]
> > (Axiom)
> >
> > 4. ALL(a):ALL(b):[a in n & b in n => [s(a)=s(b) => a=b]]
> > (Axiom)
> >
> > 5. ALL(a):[a in n => ~s(a)=0]
> > (Axiom)
> >
> Why would you bash the axiom infinity when you
> use the same. In set theory, you have an EXIST(n),
>
> around 2 & 3, which then reads:
>
> /* Zermelos Axiom of Infinity */
> EXIST(n):[0 in n & ALL(a):[a in n => s(a) in n]]
>
> And 4 & 5 can be derived from how you define s(_),
> but it can be also unfolded, and us nameless.
>

Makes no sense. Will stick to the standard practice of writing out Peano's Axioms without existential quantifiers.

[Mostowski Collapse]

Its not anymore pacticed. The insight that I(_) can be
generic and that there are many many differnet induction
schemas, has lead to a new breed of theorem prover.

Your students will learn nothing. Set theory and other
research has paved the way to these new approaches.
Check out the Coq theorem prover, Peano is just the

directive "inductive":

Inductive nat : Set :=
| O : nat
| S : nat -> nat.
https://coq.inria.fr/refman/language/core/inductive.html

How does genericity of I(_) pay off? Well you can also
do for example the following and define a list:

Inductive list (A:Set) : Set :=
| nil : list A
| cons : A -> list A -> list A.
https://coq.inria.fr/refman/language/core/inductive.html

Existence of such inductive structures can also
be proved without set theory, like for example
with the Knaster–Tarski Theorem:

"Since complete lattices cannot be empty (they must
contain a supremum/infimum of the empty set), the
theorem in particular guarantees the existence of at
least one fixed point of f, and even the existence of a
least (or greatest) fixed point. In many practical cases,
this is the most important implication of the theorem."
https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem

[Dan Christensen]

On Friday, January 14, 2022 at 5:40:08 PM UTC-5, Mostowski Collapse wrote:
> Its not anymore pacticed.

Then may you should write to Wolfram and set them straight. (HA, HA, HA!!!)

https://mathworld.wolfram.com/PeanosAxioms.html

You are such a liar.

Dan

[Mostowski Collapse]

Of course Peano axioms have an encyclopedia entry, but
its not anymore practiced.

How do you now solve this problem, where natural
numbers and real numbers appear:

ALL(n):ALL(x):[n e N & x e R & x > 0 => 1 + n*x =< (1+x)^n]
https://shemesh.larc.nasa.gov/fm/pvs/TheMartian/

You can define rational numbers with the directive "inductive":
Define some quotient for equality.

Inductive rat: Set :=
| / : nat -> nat -> rat
https://coq.inria.fr/refman/language/core/inductive.html

And then you could define reals:
Define some predicate to check Cauchy property
and some quotient for equality.

Inductive cauchy: Set :=
| lim : (nat -> rat) -> cauchy

LMAO

[Mostowski Collapse]

Coq is more interested in constructive reals, so you find
for example a Cauchy sequence with a modulus:

Definition QCauchySeq (xn : Z -> Q)
: Prop
:= forall (k : Z) (p q : Z),
Z.le p k
-> Z.le q k
-> Qabs (xn p - xn q) < 2 ^ k.
https://coq.inria.fr/stdlib/Coq.Reals.Cauchy.ConstructiveCauchyReals.html

You could go set like with this inductive type:

Inductive cauchy: Set :=
| lim : (nat -> rat) -> cauchy

It is a constructor which takes a function argument.
In set theory, if you had proper functions, like function
space nat -> rat as in set theory exponentiation rat^nat,

you could stay with sets. But you have some nonsense
Function Axiom and a tendency to ingnore that a function
is a binary relation between domain and codomain,

so your reals would horribly blow up, and you would
need to carry around a lot of extra parameters.

LoL

[Dan Christensen]

On Friday, January 14, 2022 at 6:00:26 PM UTC-5, Mostowski Collapse wrote:
> Of course Peano axioms have an encyclopedia entry, but
> its not anymore practiced.
>

Liar.

> How do you now solve this problem, where natural
> numbers and real numbers appear:
>
> ALL(n):ALL(x):[n e N & x e R & x > 0 => 1 + n*x =< (1+x)^n]
> https://shemesh.larc.nasa.gov/fm/pvs/TheMartian/
>

Peano's axioms are used to define the natural numbers. The field axioms, etc. can define the real numbers. Deal with it, Jan Burse.

[Dan Christensen]

On Friday, January 14, 2022 at 6:08:57 PM UTC-5, Mostowski Collapse wrote:

> But you have some nonsense
> Function Axiom and a tendency to ingnore that a function
> is a binary relation between domain and codomain,
>

You tend to ignore the fact that we can make no logical inferences about functions outside of their domain of definition. Such statements are simply undefined or meaningless. My Function Axiom prevents that kind of nonsense. No wonder you are so obsessed with it. You are as bad as WM with his mysterious "dark numbers." Get a life, Jan Burse!

[Mostowski Collapse]

You can prove in FOL not only

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

You can also prove:

ALL(x):EXIST(y):(f(x)=y & ALL(z):(f(x)=z => y=z)

So your statement "can make no logical inferences about functions
outside of their domain of definition" is simply wrong. At least its
wrong for FOL function symbols,

FOL function symbols are total over the domain of discourse.
So your claim "Such statements are simply undefined or meaningless"
is bull shit, we can prove totality, thats the first proof,

the second proof even says that the value of a function not
only exists, it is also unique for the whole range of the
domain of discourse.

For some proofs see here:

∀x∃yf(x)=y is valid.
https://www.umsu.de/trees/#~6x~7yf%28x%29=y

∀x∃y(f(x)=y ∧ ∀z(f(x)=z → y=z)) is valid.
https://www.umsu.de/trees/#~6x~7y%28f%28x%29=y~1~6z%28f%28x%29=z~5y=z%29%29

[Mostowski Collapse]

No Dan-O-Matik ALL(x):[x e a => f(x) e b] involved in the
proofs, even if there were a Dan-O-Matik ALL(x):[x e a => f(x) e b],
the proofs would be still valid in FOL,

on the other hand I guess they are not anymore valid in DC
poop, with or without Dan-O-Matik ALL(x):[x e a => f(x) e b].
Since dcproof5.exe changed its rules.

But how much of **standard** mathematics is sacrificed in
DC poop by this tweaking?

- We didnt see yet an existence proof of a Peano structure in DC poop.
- We didnt see yet Cauchy sequence construction of real numbers
- What else?

[Mostowski Collapse]

How do you want to show existence of Cauchy sequences
if there is no powerset axiom. Can you show in DC Poop
the following, i.e. existence of function space:

EXIST(F):ALL(f):[f e F <=> f e N -> Q]

The usual proof has existence of N from Zermelos
axiom of infinity, then existence some rational number
construction Q, and existence of Q^N, i.e. set

exponentiation. So you cannot show existence
of real numbers from Cauchy sequences construction
in DC poop. How funny because already you cannot

show existence of some Peano numbers.

LMAO!

P.S.: Recall that powerset is instrumental in defining
a function space A -> B, it is defined as:

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

See also:

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

[Dan Christensen]

On Saturday, January 15, 2022 at 4:37:40 AM UTC-5, Mostowski Collapse wrote:
> You can prove in FOL not only
>
> ALL(x):EXIST(y):f(x)=y
>

If so, FOL is in dire need of a serious tweaking. If so, maybe it's silliness like this that explains why so-called mathematical logic is not a required course in many pure math programs (e.g. at MIT). In the logic of most textbook math proofs, as in DC Proof, you can't have a function without at least attaching a name to its domain (D) and codomain (C), e.g. ALL(x):[x in D => f(x) in C]. Otherwise "f(x)" is quite meaningless if f is supposed to be a function.

[Dan Christensen]

On Saturday, January 15, 2022 at 4:53:29 AM UTC-5, Mostowski Collapse wrote:
> How do you want to show existence of Cauchy sequences
> if there is no powerset axiom.

Huh??? Just select the "Power Set" option on the "Sets" menu on the DC Proof main screen. to obtain:

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

I hope this helps.

[Dan Christensen]

On Saturday, January 15, 2022 at 4:53:29 AM UTC-5, Mostowski Collapse wrote:

> Can you show in DC Proof

> the following, i.e. existence of function space:
>
> EXIST(F):ALL(f):[f e F <=> f e N -> Q]
>

You could use the following, re-posted from earlier this month, to achieve the equivalent:

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, posted earlier this month)

Informally, you might say that fs is the set of functions mapping x to y.

[Dan Christensen]

On Saturday, January 15, 2022 at 1:11:21 PM UTC-5, Dan Christensen wrote:
> On Saturday, January 15, 2022 at 4:53:29 AM UTC-5, Mostowski Collapse wrote:
>
> > Can you show in DC Proof
> > the following, i.e. existence of function space:
> >
> > EXIST(F):ALL(f):[f e F <=> f e N -> Q]
> >
> You could use the following, re-posted from earlier this month, to achieve the equivalent:
>
> 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, posted earlier this month)
>
> Informally, you might say that fs is the set of functions mapping x to y.

Hmmm... This might justify introducing an axiom of the form:

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

Comments?

[Mostowski Collapse]

Looks like you are in deep trouble with function spaces,
is this the warterloo of DC Proof, is it its amagedon?

LoL

[Mostowski Collapse]

Not enough. You possibly need also the unordered
pairing axiom. How do you want to prove that for a,b the set

{{},{a},{b},{a,b}} exists?

But if you have unordered pairing axiom, you can also build
the above set manually, without the powerset axiom, takes
more steps though, O(2^n) proof steps. The powerset axiom is

only needed for infinite sets. But its pretty useless without the
unordered pairing axiom. Because you cannot show that for
a,b the set

{a,b} exists?

Which you could feed into the power set, to shorten the
O(2^n) proof steps into O(n) proof steps.

> Huh??? Just select the "Power Set" option on the "Sets" menu on the DC Proof main screen. to obtain:
> 1. ALL(a):[Set(a) => EXIST(b):[Set(b) & ALL(c):[c in b <=> Set(c) & ALL(d):[d in c => d in a]]]]
(Power Set)

[Mostowski Collapse]

How is equality of function symbols defined in DC Poop?
In set theory we have for set-like functions:

f = g <=> ∀z(z e f <=> z e g)

When we use the unconstrainted shorthand f(x)≈y
stands for (x,y) e f, which is a partial equality.

Then we can express it also as, but it requires that
we already know that f,g only consist of pairs:

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

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

[Dan Christensen]

On Sunday, January 16, 2022 at 5:47:34 AM UTC-5, Mostowski Collapse wrote:
> How is equality of function symbols defined in DC Proof?

As in most math textbooks, f and g are the same functions if they always give the same output for the same input.

> In set theory we have for set-like functions:
>
> f = g <=> ∀z(z e f <=> z e g)
>

This works for arbitrary sets f and g. Equating functions to sets (i.e. their graph set), unfortunately, leads to Burse's Paradox: the notion that we can make logical inferences about functions outside of their domain of definition. There is more to a function than its graph set. At the very least, a domain and codomain set must be specified, even if only to attach a specific name to them.