DC Proof 2.0 Update for 2022-04-15

[Dan Christensen]

A new version of DC Proof 2.0 was released yesterday. It includes:

1. Bug fix for Arbitrary Consequent Rule that ignored certain error conditions.

2. Re-introduced requirements for non-empty domain and codomain sets in function axioms. Adventurous users are still able to introduce their own versions of axioms at the beginning of proofs.


NEW FUNCTION AXIOM (1 variable)

ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)

& EXIST(a1):a1 in dom & EXIST(a1):a1 in cod <---- NEW

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

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

where

dom = domain set
cod = codomain set
gra = graph set
fun = function operator


NEW FUNCTION EQUALITY AXIOM (1 variable)

ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)

& EXIST(a):a in dom & EXIST(a):a in cod <---- NEW

& ALL(a):[a in dom => f1(a) in cod]
& ALL(a):[a in dom => f2(a) in cod]

=> [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]


NEW FUNCTION SPACE AXIOM (1 variable)

ALL(dom):ALL(cod):[Set(dom) & Set(cod)

& EXIST(a1):a1 in dom & EXIST(a1):a1 in cod <---- NEW

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


Here is an example applying the new Function and Equality Axioms:

THEOREM

On any non-empty set x there exists a unique identity function id: x --> x

ALL(x):[Set(x) & EXIST(a):a in x

=> EXIST(id):[ALL(a):[a in x => id(a)=a]

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

FORML PROOF

https://www.dcproof.com/IdentityFunctionsUnique.htm (136 lines)

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]

Your nonsense doesn't make any sense.
Take id1 : {1,2} -> {1,2} is id1={(1,1),(2,2)}
id2 : {2,3} -> {2,3} is id2={(2,2),(3,3)}
id3 : {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.

And using the Ben Trick, prove via Dans ad-hoc Axiom:

id2=id3 Hint: Use dom/cod = {1,2}
id1=id3 Hint: Use dom/cod = {2,3}

Then using DC Proof substition:

id1=id2

LoL

[Dan Christensen]

On Saturday, April 16, 2022 at 6:28:17 PM UTC-4, Mostowski Collapse wrote:
> Your nonsense doesn't make any sense.
> Take id1 : {1,2} -> {1,2} is id1={(1,1),(2,2)}
> id2 : {2,3} -> {2,3} is id2={(2,2),(3,3)}
> id3 : {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.
>
> And using the Ben Trick, prove via Dans ad-hoc Axiom:
>
> id2=id3 Hint: Use dom/cod = {1,2}

Maybe you didn't know, but {1, 2} =/= {1, 2, 3}

[Mostowski Collapse]

take
id1: {1,2} -> {1,2} is id1 = {(1,1),(2,2)}.
id2: {2,3} -> {2,3} is id2 = {(2,2),(3,3)}.

id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.

You can prove:

ALL(a):[a in {1,2} => id1(a) in {1,2}]
ALL(a):[a in {1,2} => id3(a) in {1,2} ]
ALL(a):[a in {1,2} => id1(a)=id3(a)]]]

Which implies, according to your ad-hoc axiom:

id1 = id3

You can prove:

ALL(a):[a in {2,3} => id2(a) in {2,3}]
ALL(a):[a in {2,3} => id3(a) in {2,3} ]
ALL(a):[a in {2,3} => id2(a)=id3(a)]]]

Which implies, according to your ad-hoc axiom:

id2 = id3

Now use subst from your DC Proof, and you can derive:

id1 = id2

[Dan Christensen]

On Saturday, April 16, 2022 at 8:14:52 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> take
> id1: {1,2} -> {1,2} is id1 = {(1,1),(2,2)}.
> id2: {2,3} -> {2,3} is id2 = {(2,2),(3,3)}.
> id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.
> You can prove:
>
> ALL(a):[a in {1,2} => id1(a) in {1,2}]
> ALL(a):[a in {1,2} => id3(a) in {1,2} ]
> ALL(a):[a in {1,2} => id1(a)=id3(a)]]]
>
> Which implies, according to your ad-hoc axiom:
>
> id1 = id3
>

Recall:

ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
& EXIST(a):a in dom & EXIST(a):a in cod

& ALL(a):[a in dom => f1(a) in cod]
& ALL(a):[a in dom => f2(a) in cod]

=> [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]

Equality of functions f1 and f2 is always equality with respect to a COMMON domain and codomain. Deal with it, Jan Burse.

[Fritz Feldhase]

On Sunday, April 17, 2022 at 4:01:21 AM UTC+2, Dan Christensen wrote:
>
> Equality of functions f1 and f2 is always equality with respect to a COMMON domain and codomain. Deal with it, Jan Burse.

What an idiotic approach. You are thick as a brick.

Hint: "In our definition of the equality of functions, we have assumed that the two functions have the same domain and codomain. Two functions that do not have the same domain and codomain are not equal."

Source: https://mathstats.uncg.edu/sites/pauli/112/HTML/secfuneq.html

[Dan Christensen]

Hint 2: "Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X."
--Terence Tao, "Analysis I, 3rd Ed.," p. 51

Look familiar?

Dan

[Mostowski Collapse]

{1,2} is a common domain of:

> id1: {1,2} -> {1,2} is id1 = {(1,1),(2,2)}.

> id3: {1,2,3} -> {1,2,3} is id3 = {(1,1),(2,2),(3,3)}.

Every dom is a common domain of f1 : dom1 -> cod1 and f2 : dom2 -> cod2,
and can be used in your axiom in case we have:

dom ⊆ dom1 and dom ⊆ dom2

Do you finally see the "bug" in your ad hoc axiom. Or are you simply
too stupid Dan-O-Matik Ultra Moron?

P.S.: You can check yourself if this is provable:
ALL(a):[a in dom1 => f1(a) in cod1 ]
ALL(a):[a in dom2 => f2(a) in cod2 ]

Then this is also provable:
ALL(a):[a in dom => f1(a) in cod1 ]
ALL(a):[a in dom => f2(a) in cod2 ]

This is called CONTRAVARIANCE in the domain.
We told you already a 1000-times.

[Mostowski Collapse]

The more general law about bounded quantifiers is simply:

ALL(a):[A(a) => B(a)] & ALL(a):[C(a) => A(a)] => ALL(a):[C(a) => B(a)]

The schema is called BARBARA, and it is one of Aristoteles Syllogisms.

How stupid are you Dan-O-Matik on a scale of 1-1000? 9000 Stupid?

https://de.wikipedia.org/wiki/Modus_Barbara

[Fritz Feldhase]

Yeah. I already told you: A stupid approach (when used in the context of a formal system).

Hint: "In our definition of the equality of functions, we have assumed that the two functions have the same domain and codomain. Two functions that do not have the same domain and codomain are not equal."

The final clause is important.

In the light of this fact, one might prefer the following approach (which is quite common):

"f=g ⟺ f and g have the same domain and codomain, and f(x)=g(x) for all x in the domain" ,

especially in a formal context.

[Mostowski Collapse]

We are back to some fundamental problem that Dan-O-Matik
never mastered so far. Namely "definite descriptions" à la Russel.
Your phrase says:

"have THE same domain and codomain"

So you need some function dom(f) that gives "THE domain" of
the functions f. And then you could formulate something
as follows:

ALL(d):ALL(f):[d=dom(f) => ....]

But Dan-O-Matik alwasys uses, which is ambiguous:

ALL(dom):ALL(f):[....]

Which leads to nowhere. As long as you don't have a notion
of "the domain", its futil to try to formalize equality. This is what
needs to be resolved firms,

to turn "the domain" into a "definite description" à la Russel.
P.S.: Its not possible to be resolved with FOL function symbols,
because FOL function symbols are f : V -> V, where V is

the domain of discourse, they have anyway dom(f)=V.

[Mostowski Collapse]

So we have a real cluster of problems:
- Definite Descriptions
- BARBARA
- What else?

I would say Dan-O-Matik is cluster fucked up. It will
take ages until he masters function spaces. Whereby it
could be so easy, just read Nikolas Burbaki, before

reading Terrence Tao.

[Mostowski Collapse]

Because Dan-O-Matik is cluster fucked up, its especially
difficult to argue with him, he jumps from his BARBARA
fallacies to his Definite Description fallacies,

back and forth, and commits dozen other fallacies,
like the use of first order function symbols f : V -> V,
so that it is quite difficult discuss

functions spaces and equality. Because he did never
study the Greek, seen in that he has BARBARA not
present, and because he never read Nikolas Burbaki,

one could equally well talk to a wall now. He also
tries some fraud in that he attempts formulating
his ad hoc axioms with "if" instead "iff", thinking

they become less wrong.

Rika trying to convince Satoko to leave Hinamizawa
https://www.reddit.com/r/Higurashinonakakoroni/comments/nnnfpy/rika_talking_to_a_wall/

[Ben]

Dan Christensen <Dan_Chr...@sympatico.ca> writes:

> Recall:
>
> ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> & EXIST(a):a in dom & EXIST(a):a in cod
> & ALL(a):[a in dom => f1(a) in cod]
> & ALL(a):[a in dom => f2(a) in cod]
>
> => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
>
> Equality of functions f1 and f2 is always equality with respect to a
> COMMON domain and codomain. Deal with it, Jan Burse.

You are not taking this seriously. Your axiom entails this:

ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]

Many pairs of functions on the same domain and to the same codomain have
f(0)=g(0)=0 but are not equal. You can't have intended this, surely?

The old axiom (that allowed for functions from {}) proved

ALL(f):ALL(g):[~f=g => f=g]

but now, to get nonsense, all that's needed is set with at least one
element. You have not fixed the basic problem.

--
Ben.

[Dan Christensen]

On Sunday, April 17, 2022 at 5:00:32 PM UTC-4, Ben wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > Recall:
> >
> > ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> > & EXIST(a):a in dom & EXIST(a):a in cod
> > & ALL(a):[a in dom => f1(a) in cod]
> > & ALL(a):[a in dom => f2(a) in cod]
> >
> > => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
> >
> > Equality of functions f1 and f2 is always equality with respect to a
> > COMMON domain and codomain. Deal with it, Jan Burse.
> You are not taking this seriously. Your axiom entails this:
>
> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
>
> Many pairs of functions on the same domain and to the same codomain have
> f(0)=g(0)=0 but are not equal. You can't have intended this, surely?
>

See my reply to you on this matter at sci.math just now.

Dan

[Ben]

You didn't answer the question there. Did you intend your axiom to
entail ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]? It looks dodgy to me.

--
Ben.

[Fritz Feldhase]

On Sunday, April 17, 2022 at 4:09:00 PM UTC+2, Mostowski Collapse wrote:

> So you need some function dom(f) that gives "THE domain" of
> the functions f. And then you could formulate something
> as follows:
>
> ALL(d):ALL(f):[d=dom(f) => ....]
>
> But Dan-O-Matik alwasys uses, which is ambiguous:
>
> ALL(dom):ALL(f):[....]
>
> Which leads to nowhere. As long as you don't have a notion
> of "the domain", its futil to try to formalize equality. This is what

> needs to be resolved first.

Agree. Here my ad hoc "first take" (not aiming at "functions" due to Bourbaki):

X --> Y :<-> f is a set of ordered pairs & f is functional & dom(f) = X & img(f) c Y
"f is a (set-theoretic) function with domain X and codomain Y."

(Note that the codomain for a (set-theoretic) function is not unique.)

With

ord_pair(p) :<-> ExEy(p = <x, y>) "p is an ordered pair"
f is a set of ordered pairs :<-> Az(z e f -> ord_pair(z))
f is functional :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z)
dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

We now may define

function(f) :<-> EXEY: f: X --> Y (for any set f)

and

f(x) := U{y e UUf : <x, y> e f} (for any set f)

This finally allows to state the THEOREM:

AfAg(function(f) & function(g) -> (f = g <-> dom(f) = dom(g) & Ax(x e dom(x) -> f(x) = g(x)))).

We now may extend this approach aiming at full blown "mathematical function" (a la Bourbaki).

To be continued. Stay tuned.

[Mostowski Collapse]

Actually what implies dom(f)=X is seriality:

A binary relation is serial (also called left-total) if
∀ x ∈ X , ∃ y ∈ Y , ( x , y ) ∈ R .
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

dom(f) = X means the function is maximally **total** on X.
For partial functions on X you would only have dom(f) ⊆ X.
Well you find the notion total, see above, also used on

Wikipedia, i.e. left-total. One of the bugs of your nonsense:

/* Dan-O-Matik Nonsense */
ALL(a):[a e X => f(a) e Y]

That it doesn't imply that X is the largest set where f is total,
i.e. it doesn't imply dom(f)=X. But there is a real cluster of bugs,
since for example you use first order function symbols,

which anyway have dom(f) = V. Since this is provable:

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

LMAO!

[Dan Christensen]

On Sunday, April 17, 2022 at 8:49:01 PM UTC-4, Ben wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Sunday, April 17, 2022 at 5:00:32 PM UTC-4, Ben wrote:
> >> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
> >>
> >> > Recall:
> >> >
> >> > ALL(dom):ALL(cod):ALL(f1):ALL(f2):[Set(dom) & Set(cod)
> >> > & EXIST(a):a in dom & EXIST(a):a in cod
> >> > & ALL(a):[a in dom => f1(a) in cod]
> >> > & ALL(a):[a in dom => f2(a) in cod]
> >> >
> >> > => [f1=f2 <=> ALL(a):[a in dom => f1(a)=f2(a)]]]
> >> >
> >> > Equality of functions f1 and f2 is always equality with respect to a
> >> > COMMON domain and codomain. Deal with it, Jan Burse.
> >> You are not taking this seriously. Your axiom entails this:
> >>
> >> ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]
> >>
> >> Many pairs of functions on the same domain and to the same codomain have
> >> f(0)=g(0)=0 but are not equal. You can't have intended this, surely?
> >
> > See my reply to you on this matter at sci.math just now.

> You didn't answer the question there. Did you intend your axiom to
> entail ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g]?

No. Again, you can prove:

ALL(x):ALL(f):ALL(g):[Set(x) & ALL(a):[a in x <=> a=0]
& ALL(a):[a in x => f(a) in x]
& ALL(a):[a in x => g(a) in x]
=> f=g]

[Ben]

and also ALL(f):ALL(g):[f(0)=0 & g(0)=0 => f=g].

I've posted a proof in the other thread. Is there a way to get text out
of DC Proof? It does not appear to be easy.

--
Ben.

[Dan Christensen]

See my comment there.

> Is there a way to get text out
> of DC Proof? It does not appear to be easy.
>

The proof that appears on the main screen is rich text. The best way to display it to convert it to HTML text and upload it to your website. I copy and paste it to MS Word and save it as a web page, then upload it to my website. That preserves all the lovely formatting -- different sizes and colours of fonts and spacing.

[Fritz Feldhase]

On Sunday, April 17, 2022 at 6:16:29 AM UTC+2, Dan Christensen wrote:

> "Definition 3.3.7 (Equality of functions). Two functions f : X → Y, g : X → Y with the same domain and range are said to be equal, f = g, if and only if f(x) = g(x) for all x ∈ X."
> --Terence Tao, "Analysis I, 3rd Ed.," p. 51

Actually, We can get that as a theorem in the context of the "set theoretic" approach.

Though it seems that you are too dumb to get it.

I'll formulate it once more. Just for fun.

Some motivating preliminary definitions:

ordered_pair(p) :<-> ExEy(p = <x, y>)
set_of_ordered_pairs(f) :<-> Set(f) & Ap(p e f -> ordered_pair(p))
functional(f) :<-> AxAyAz(<x, y> e f & <x, z> e f -> y = z)

Now we may define the core notions:

function(f) :<-> set_of_ordered_pairs(f) & functional(f)

dom(f) := {x e UUf : Ey(<x, y> e f)}
img(f) := {y e UUf : Ex(<x, y> e f)}

Finally we may define some rather helpful notions in connection with functions:

f: X --> Y :<-> function(f) & dom(f) = X & img(f) c Y
"f is a function from X to Y."

f(x) := U{y e UUf : <x, y> e f}

"the value of f at x"

These notions allow to deal with "functions" (at a basic level).

For example, we can derive (in a set theoreric context) the theorem

AfAXAY((f: X --> Y) -> Ax(x e X -> f(x) e Y))

as well as, say, the theorem:

AfAgAXAY((f: X --> Y) & (g: X --> Y) -> (f = g <-> Ax(x e X -> f(x) = g(x)))).

"[Any] two functions f : X → Y, g : X → Y [...] are [...] equal, f = g, if and only if f(x) = g(x) for all x ∈ X."

[Dan Christensen]

Removed troublesome Function Equality Axiom. The equality of functions f1 and f2 on their common domain can still, as always, be indicated by:

ALL(a):[a in dom => f1(a)=f2(a)]

[Fritz Feldhase]

On Tuesday, April 19, 2022 at 6:58:14 PM UTC+2, Dan Christensen wrote:

*sigh*

You really don't get it, do you?

> The equality of functions f1 and f2 on their common domain can still [...] be indicated by:

> ALL(a):[a in dom => f1(a)=f2(a)]

No, it can't.

What you MEAN is that for any two (set theoretic) functions f, g with dom(f) = dom(g) "equaility can be indicated by"

Ax(x e dom(f) -> f(x) = g(x)).

Which is true.

Hint: Since it's possible to chose an arbitrary set for /dom/, not necessarily dom = dom(f).

[Mostowski Collapse]

But why would one use Ax(x e dom(f) -> f(x) = g(x)), when
we already have in ZF(C) by extensionality:

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

function(f) and function(g) is only a special case. Unfortuntely
DC Proof cannot use the above, since what is missing in DC Proof:

Ax(x e dom(f) -> Ay((x,y) e f <-> f(x)=y))

He only has:

> NEW FUNCTION AXIOM (1 variable)

> [fun(a1)=b <=> (a1,b) in gra]]]]

Two different functions fun and gra. So he introduce the notation
f(a) not as a notation, but via some transfer.

[Mostowski Collapse]

And then he runs into the problem that he cannot prove,
because his axiom is too "if" and not enough "iff":

EXISTUNIQUE(fun): .... [fun(a1)=b <=> (a1,b) in gra]]]]

Since he doesn't say ~(a e dom) => fun(a)={}, whereby
the Fritz approach would have ~(a e dom) => f(a)={}.

LMAO!

[Fritz Feldhase]

On Tuesday, April 19, 2022 at 11:15:23 PM UTC+2, Mostowski Collapse wrote:

I see. Adopting the "set theoretic" approch (the "kludge") we can prove/do all the things DC Poop can't do.

For example, we can prove for any function f:

Ax(x e dom(f) -> Ay(f(x) = y <-> <x, y> e f))

We don't need an additional axioms for that.

> [...] he doesn't say ~(a e dom) => fun(a)={}, whereby

> the Fritz approach would have ~(a e dom) => f(a)={}.

Yeah, of course, no one is interested in f(x) for x !e dom(f). Still it's good to know that f(x) is "defined" for a l l x. Especially in a formal context.

Extremely funny: The kludge allows to prove theorems like: For any functions f, g: f = g <-> dom(f) = dom(g) & Ax(x e dom(f) -> f(x) = g(x)).

While DC Proof can't deal with "function equality" at all. :-)

Thiugh my aim is to define/introduce functions a la Bourbaki, for them we would have

f = g <-> dom(f) = dom(g) & codom(f) & codom(g) & Ax(x e dom(f) -> f(x) = g(x)).

Too much kludge for DC though, I guess

[Ben]

So no. OK.

--
Ben.

[Python]

Dan has very low standards when it comes to software development...
DC is not open source (so no way to validate the correction of
its proof engine), only runs on MS Windows (which is outrageous
these days) and cannot inter-operate with anything.

[Ben]

Yes. I used it only because he was resistant to any other sort of
reasoning, but was painful to use. There's endless mouse moving,
clicking and scrolling. There's no way to import axioms. There's no
way to structure sequences and re-use them. (I had to run through the
same tedious dozen steps twice because an antecedent had the same
condition twice except for a different free variable.) You can't even
"split" a bi-conditional -- you have to click to turn it into an & and
the split that (I don't mind the two steps being recorded, it's the
endless clicking that got me down). The list goes on...

Does anyone actually use it to teach logic?

--
Ben.