The Exponentiation Axiom --> An Inconsistency in DC Proof

[Mostowski Collapse]

Dear All,

I had this starting points:

a) Usually in set theory this here should hold for primitive function spaces:

Definition: 4.2.6 The Exponentiation Axiom (abbreviated Exp) postulates
that for sets a; b the class of all functions from a to b forms a set:
∀a∀b∃c ∀f(f e c <-> (f : a -> b))
https://www1.maths.leeds.ac.uk/~rathjen/book.pdf

b) Dan O Matiks favorite for f : a -> b:

ALL(x):[x ε a=> f(x) ε b]

Here is a DC Proof that a) and b) leads to an inconsistency:

32 ~g(0)=0 & g(0)=0
Join, 29, 31

The prove idea is to construct g : e -> d, using Peano unit and
self application, the later is allowed in DC Proof, and assuming
that 0 is not a function.

/* Some Law from Peano Unit */
1 ALL(x):~x=singleton(x)
Axiom

/* 0 is not a function, therefore ~0 e c */
2 ~0 ε c
Axiom

/* Exponentiation Axiom for { f : {0} -> {0} } */
3 ALL(f):[f ε c <=> ALL(x):[x=0 => f(x)=0]]
Axiom

/* Construction of g : e -> d, when ~(x e c) then g(x)=0 */
4 ALL(x):[~x ε c => g(x)=0]
Axiom

/* Construction of g : e -> d, when x e c then g(x)=singleton(x(x)) */
5 ALL(x):[x ε c => g(x)=singleton(g(x)) & g(x) ε d]
Axiom

6 g ε c
Premise

7 g ε c => g(g)=singleton(g(g)) & g(g) ε d
U Spec, 5

8 g(g)=singleton(g(g)) & g(g) ε d
Detach, 7, 6

9 g(g)=singleton(g(g))
Split, 8

10 g(g) ε d
Split, 8

11 ~g(g)=singleton(g(g))
U Spec, 1, 10

12 g(g)=singleton(g(g)) & ~g(g)=singleton(g(g))
Join, 9, 11

13 ~g ε c
Conclusion, 6

14 g ε c <=> ALL(x):[x=0 => g(x)=0]
U Spec, 3

15 [g ε c => ALL(x):[x=0 => g(x)=0]]
& [ALL(x):[x=0 => g(x)=0] => g ε c]
Iff-And, 14

16 g ε c => ALL(x):[x=0 => g(x)=0]
Split, 15

17 ALL(x):[x=0 => g(x)=0] => g ε c
Split, 15

18 ~g ε c => ~ALL(x):[x=0 => g(x)=0]
Contra, 17

19 ~ALL(x):[x=0 => g(x)=0]
Detach, 18, 13

20 ~~EXIST(x):~[x=0 => g(x)=0]
Quant, 19

21 EXIST(x):~[x=0 => g(x)=0]
Rem DNeg, 20

22 ~[u=0 => g(u)=0]
E Spec, 21

23 ~[~u=0 | g(u)=0]
Imply-Or, 22

24 ~~[~~u=0 & ~g(u)=0]
DeMorgan, 23

25 ~~u=0 & ~g(u)=0
Rem DNeg, 24

26 u=0 & ~g(u)=0
Rem DNeg, 25

27 u=0
Split, 26

28 ~g(u)=0
Split, 26

29 ~g(0)=0
Substitute, 27, 28

30 ~0 ε c => g(0)=0
U Spec, 4

31 g(0)=0
Detach, 30, 2

32 ~g(0)=0 & g(0)=0
Join, 29, 31

[Dan Christensen]

So, one or more or your 5 wonky axioms must be false. Not surprising. What is your point?

Dan

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

[Fritz Feldhase]

On Tuesday, September 13, 2022 at 2:02:17 AM UTC+2, Mostowski Collapse wrote:

Just some short comments. (Worth 2 cents.)

> self application, the later is allowed in DC Proof

Which would also work in the context of set theory (ZFC).

Of course, for no function f we will have f e dom(f) in this case.

Still f(f) is (or may be) a (certain) set. Since we may define .(.) the follwing way:

f(x) := U{y : (x, y) e f}. (*)

In this case we would get

f(f) = U{y : (f, y) e f} = ... = U{} = {}.

[Actually, (*) is not the only possibility to "introduce" the binary "application operation" .(.).]

> /* Exponentiation Axiom for { f : {0} -> {0} } */
> 3 ALL(f):[f ε c <=> ALL(x):[x=0 => f(x)=0]]
> Axiom

I guess this reduces to

ALL(f):[f ε c <=> f(0)=0]]

Well, I personally would prefer to be slightly more specify concerning c. :-P

I'd prefer something like

ALL(f):[f ε c <=> function(f) & f(0)=0]] (**)

But even in this case it seems to me that c will rather be a proper class than a set.

After all (**) would imply that

All sets {(0, 0), {x, x}} (where x is a set) are in c.

Ax(set(x) -> {(0, 0), {x, x}} e c),

Since for any set h = {(0, 0), {x, x}} (for some set x) we have 1. function(f) and 2. h(0) = 0.

Of course, this needn't be a problem, though your proof would not go through in the context of ZFC, I guess. (Or would it, slightly modified?)

> 32 ~g(0)=0 & g(0)=0
> Join, 29, 31

Ok, so we have reached a contradiction.

Now if you hadn't declared (3) an axiom but an _assumption_, your proof would just show/prove (by an application of RAA):

~ALL(f):[f ε c <=> ALL(x):[x=0 => f(x)=0]]

(which indeed might be considered "questionable" - especially in the context of ZFC).

Though the main problems seems to be

| "Dan O Matiks favorite for f : a -> b:
|

| ALL(x):[x ε a=> f(x) ε b]."

After all, the Exponentiation Axiom

∀a∀b∃c ∀f(f e c <-> (f : a -> b))

looks quite innocent. (In the context of set theory, say ZFC, it certainly would be theorem when functions are treaded the usual way.)

Yeah, usually we have the definition b^a = {f e P(a x b) | f : a -> b}. (where a and b are sets).

See: https://proofwiki.org/wiki/Definition:Set_of_All_Mappings

[Dan Christensen]

On Monday, September 12, 2022 at 8:02:17 PM UTC-4, Mostowski Collapse wrote:

[snip]

>
> /* Some Law from Peano Unit */
> 1 ALL(x):~x=singleton(x)
> Axiom
>

I think you will find it impossible to prove the existence of such a function in DC Proof. You would need a domain to start with. Sorry, the "class" V won't do.

> /* 0 is not a function, therefore ~0 e c */
> 2 ~0 ε c

In DC Proof, you can prove the existence of a function, but you cannot prove that something is NOT a function.

[snip]

[Mostowski Collapse]

Its based on this set theory axiom:

Axiom of pairing - In axiomatic set theory
https://en.wikipedia.org/wiki/Axiom_of_pairing

The above says for every x,y there is a unordered pair {x,y}
Now use x=y and you get the Peano Unit:

ALL(x):ALL(x):[x e {y} <=> x = y]

Now use regularity axiom, :

Axiom of regularity - In mathematics
https://en.wikipedia.org/wiki/Axiom_of_regularity

and then you get:

x =\= {x}

I added the later as an axiom.
Do you deny that set theory has this?

[Mostowski Collapse]

Corr.: Typo

The above says for every x,y there is a unordered pair {x,y}

Now use x=y and you get the existence of the Peano Unit
{x} as a set for every x, which can be also defined as:

ALL(a):ALL(b):[a e {b} <=> a = b]

[Dan Christensen]

On Tuesday, September 13, 2022 at 5:09:39 AM UTC-4, Mostowski Collapse wrote:


> Dan Christensen schrieb am Dienstag, 13. September 2022 um 05:17:51 UTC+2:
> > On Monday, September 12, 2022 at 8:02:17 PM UTC-4, Mostowski Collapse wrote:
> > [snip]
> > >
> > > /* Some Law from Peano Unit */
> > > 1 ALL(x):~x=singleton(x)
> > > Axiom
> > >
> > I think you will find it impossible to prove the existence of such a function in DC Proof. You would need a domain to start with. Sorry, the "class" V won't do.
> > > /* 0 is not a function, therefore ~0 e c */
> > > 2 ~0 ε c
> > In DC Proof, you can prove the existence of a function, but you cannot prove that something is NOT a function.
> >

> Its based on this set theory axiom:
>
> Axiom of pairing - In axiomatic set theory
> https://en.wikipedia.org/wiki/Axiom_of_pairing
>

No such axiom in DC Proof.

> The above says for every x,y there is a unordered pair {x,y}
> Now use x=y and you get the Peano Unit:
>
> ALL(x):ALL(x):[x e {y} <=> x = y]
>
> Now use regularity axiom, :
>
> Axiom of regularity - In mathematics
> https://en.wikipedia.org/wiki/Axiom_of_regularity
>
> and then you get:
>
> x =\= {x}
>
> I added the later as an axiom.
> Do you deny that set theory has this?

You introduced some kind of function-like operator with an ambiguous domain. Not good enough in DC Proof.

[Mostowski Collapse]

What is an ambigious domain? I nowhere use a domain
of singleton. Where do you see me using the domain of singleton?
Like this axiom here:

> Axiom of pairing - In axiomatic set theory
> https://en.wikipedia.org/wiki/Axiom_of_pairing

The domain of unordered pairing is any two objects in
the universe of discourse. So for any two objects x,y
there is an object z such that:

ALL(a):[a e z <=> a = x v a = y]

Whats your prolololoblem?

[Ross A. Finlayson]

Why not 4 of the others?

[Mostowski Collapse]

You can formulate this axiom:

x =\= {x}

Also without a the class operator {_}. Shouldn't be
a problem to get rid of this class operator.

Instead of saying this here:

∀x(~x={x})

One could say this here:

∀x∀y(∀z(z e y <=> z=x) => ~x=y)

P.S.: Or in DC Spoiled:

Instead of saying this here:

/* Some Law from Peano Unit */
1 ALL(x):~x=singleton(x)
Axiom

One could say this here:

/* Some Law from Peano Unit */

1 ALL(x):ALL(y):[ALL(z):[z e y <=> z=x] => ~x=y]
Axiom

[Dan Christensen]

> What is an ambigious domain? I nowhere use a domain
> of singleton.

Exactly the problem! Functions require first, at the very least, the names for the domain and codomain sets. Here, the reader can only guess at the domain of this seeming function. This may be permitted in FOL (not sure), but not in DC Proof.

> Like this axiom here:

> > Axiom of pairing - In axiomatic set theory
> > https://en.wikipedia.org/wiki/Axiom_of_pairing

> The domain of unordered pairing is any two objects in
> the universe of discourse. So for any two objects x,y
> there is an object z such that:
>
> ALL(a):[a e z <=> a = x v a = y]
>

I haven't found it necessary since, in most fields of mathematics anyway, there are one or more underlying sets (sets of numbers, points in space, etc.) from which all other objects of interests are constructed. If you want to construct, say, a singleton or a pair of distinct objects, you would use the Subset Axiom. You could even construct a singleton function with one of the underlying sets as the domain.

[Mostowski Collapse]

The inconsistency shows that there is something wrong
in DC Spoiled. You are looking for the wrong cause.
The cause is of course that you allow self application,

and the means to reveal the problem is diagonal argument:

/* Construction of g : e -> d, when x e c then g(x)=singleton(x(x)) */
5 ALL(x):[x ε c => g(x)=singleton(g(x)) & g(x) ε d]
Axiom

g is the same diagonal argument as in Russels Paradox or
in Cantors theorem. Think about it. How should this here hold,
the function space existence, if you have self application?

Mostowski Collapse schrieb am Dienstag, 13. September 2022 um 02:02:17 UTC+2:
> Definition: 4.2.6 The Exponentiation Axiom (abbreviated Exp) postulates
> that for sets a; b the class of all functions from a to b forms a set:
> ∀a∀b∃c ∀f(f e c <-> (f : a -> b))
> https://www1.maths.leeds.ac.uk/~rathjen/book.pdf

Is this even possibly to have a function f, so that f(f) is
meaningful? Which is the case in DC Spoiled, but in FOL
you can even not form f(f). Any candidate function space,

has a g outside of the function space, via diagonalization,
and since I used the stupid, it is also inside the function
space, which then leads to the contradiction:

> Dan O Matiks favorite for f : a -> b:
> ALL(x):[x ε a=> f(x) ε b]

[Mostowski Collapse]

Like you can show via the Regularity Axiom:

x =\= {x}

You can also show that:

f =\= { .... (f,..) ...}

f cannot have a pair inside itself with the first coordinate
the function f itself. Thats impossible in set theory,
Although Peter Aczel might gainsay, and raise his finger,

well and say my set theory has extraordinary sets,
there is no requirement of Regularity Axiom, we might
indeed have such extraordinary functions.

But Peter Aczel writes:

Theorem: 4.2.7 ECSTc+Exp proves the same theorems as
classical Zermelo- Fraenkel Set Theory without the
Foundation Axiom, ZF-. As ZF and ZF- have the same strength,
ECSTc + Exp and ZF have the same strength.

Proof: With classical logic, Replacement implies full Separation
and Exponentiation implies the Powerset Axiom. Details
are left to the exercise.
https://www1.maths.leeds.ac.uk/~rathjen/book.pdf

So maybe can do the diagonalization without requiring
Regularity aka Foundation Axiom? Anybody an idea?

[Mostowski Collapse]

Maybe can carry out the diagonal argument by means
of this productive view of the Russel Paradox, which

doesn't require Regularity aka Foundation Axiom:

Lemma: 3.8.2 (ECST)
For every set A there is a set A_R such that ~(A_R e A).
https://www1.maths.leeds.ac.uk/~rathjen/book.pdf

Letting us plunge off the cliff some assumptions
in showing the DC Spoiled inconsistency.

[Dan Christensen]

> The inconsistency shows that there is something wrong
> in DC Spoiled.

You introduce 5 wonky axioms, find an inconsistency, then pronounce DC Proof itself to be inconsistent??? It doesn't work that way, Jan Burse.

> You are looking for the wrong cause.
> The cause is of course that you allow self application,
>

[snip]

Get back to us if you can make this point without your wonky axioms.

[Dan Christensen]

On Tuesday, September 13, 2022 at 1:23:03 PM UTC-4, Mostowski Collapse wrote:
> Like you can show via the Regularity Axiom:
>

Also not an axiom in DC Proof.

> x =\= {x}
>

[snip]

[Fritz Feldhase]

On Tuesday, September 13, 2022 at 7:15:07 PM UTC+2, Mostowski Collapse wrote:

> Is this even possibly to have a function f, so that f(f) is meaningful?

Yes, if f denotes a set theoretic function (i. e. a set) it is.

> Which is the case in DC Spoiled,

and in any set theoretic framework.

Once more: It certainly will be possible in the context of set theory (ZFC).

Of course, for no function f we will have f e dom(f) in this case.

Still f(f) is a (certain) set.

For examply, we may define .(.) the follwing way:

[Mostowski Collapse]

Well if you have:

> In this case we would get
> f(f) = U{y : (f, y) e f} = ... = U{} = {}.

Then f(f) is not meaningful. And it also
means we cannot make a definition:

g(x) := { x(x) }.

where x=g is possible. But Dan O Matiks
DC Spoiled easily gives me from the above:

g(g) = { g(g) }

Its step 9 in the proof I posted:
> 9 g(g)=singleton(g(g))
> Split, 8

Which would lead much more directly to a contradiction:

{} = { {} }

[Dan Christensen]

On Tuesday, September 13, 2022 at 6:50:54 PM UTC-4, Mostowski Collapse wrote:
> Well if you have:
> > In this case we would get
> > f(f) = U{y : (f, y) e f} = ... = U{} = {}.

Still waiting for you to prove the existence of any function, as defined in DC Proof, that is an element of its domain.

[Fritz Feldhase]

On Wednesday, September 14, 2022 at 12:50:54 AM UTC+2, Mostowski Collapse wrote:
>
> Well if you have:
> >

> > f(x) := U{y : (x, y) e f}. (*)
> >

> > and hence

> >
> > f(f) = U{y : (f, y) e f} = ... = U{} = {}.
> >

> then f(f) is not meaningful.

Yeah, we usually aren't interested in the value of a function for an argument which is not in its domain. In this sense f(f) is not meaningful, right.

But from a formal point of view there's no problem with this notion (at least not in the context of ZFC).

> And it also means we cannot make a definition:
>
> g(x) := { x(x) }.

Well, we have to be careful because of a "dual use" of the "function syntax" here.

To avoid this, instead of "g" we may use a symbol which is not just a "variable name" or "constant" used for sets.

Say a short phrase like "self":

self(x) := { x(x) }

Hence in a formal setting we might even decide to define [., .] instead of .(.):

[f, x] := U{y : (x, y) e f}.

to avoid this "dual use" of .(.). Another idea, something I've seen: some authors write xf instead of f(x).

In this case, I'd use the definition:

xf := U{y : (x, y) e f}.

> where x=g is possible.

Right. "self" cannot be uses like a set variable or set constant.

Consider the symbol "P" for the power set operation. Even though some autors write "P(A)" to denote the powerset of A, "P" does not denote a function (i. e. set).
See: https://en.wikipedia.org/wiki/Power_set

And you are right... there seem to be problems with the way DC Spoof is handling "function symbols".

(All this could be avoided in DC Spoof by handling functions in the usual set theoretic way.)

> But Dan O Matiks
> DC Spoiled easily gives me from the above:
>
> g(g) = { g(g) }

Not good.

> Its step 9 in the proof I posted:
> > 9 g(g)=singleton(g(g))
> > Split, 8
>
> Which would lead much more directly to a contradiction:
>
> {} = { {} }

I see.

[Fritz Feldhase]

On Wednesday, September 14, 2022 at 1:18:59 AM UTC+2, Dan Christensen wrote:

> Still waiting for you to prove the existence of any function, as defined in DC Proof, that is an element of its domain.

We can prove that this is not possible in ZFC. Not so sure about DC Spoof though.

[Dan Christensen]

On Tuesday, September 13, 2022 at 7:34:39 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, September 14, 2022 at 1:18:59 AM UTC+2, Dan Christensen wrote:
>
> > Still waiting for you to prove the existence of any function, as defined in DC Proof, that is an element of its domain.

> We can prove that this is not possible in ZFC. Not so sure about [DC Proof] though.

Could be tricky. The graph set G must be well defined BEFORE the function is named. The name of the function f must be new and not previously used in an active statement. And there must exist y in the codomain such that (f,y) in G.

[Fritz Feldhase]

On Wednesday, September 14, 2022 at 2:51:19 AM UTC+2, Dan Christensen wrote:
> On Tuesday, September 13, 2022 at 7:34:39 PM UTC-4, Fritz Feldhase wrote:
> > On Wednesday, September 14, 2022 at 1:18:59 AM UTC+2, Dan Christensen wrote:
> > >
> > > Still waiting for you to prove the existence of any function, as defined in DC Proof, that is an element of its domain.
> > >
> > We can prove that this is not possible in ZFC. Not so sure about [DC Proof] though.
> >
> Could be tricky. The graph set G must be well defined BEFORE the function is named. The name of the function f must be new and not previously used in an active statement. And there must exist y in the codomain such that (f,y) in G.

Actually, considering functions as mathematical objects which aren't sets (as Terence Tao does in his book) makes things unnecessarily complicated [if doing formal math], imho.

But if you are happy with your tool, who am I to question that?

[Dan Christensen]

I think that in mathematics, the functional notation f(x)=y for x not in the domain of function f should not be considered false, but rather as undefined or indeterminate. This valuable distinction is lost if functions are looked at as merely a set of ordered pairs (or n-tuples).

[Mostowski Collapse]

Ok, what happens if you take this graph in DC Spoiled:

gra = { (gra, 0) }

What function fun will result? Will we have fun(fun) = 0?

[Mostowski Collapse]

BTW: I am doing as you said. You said:

> The graph set G must be well defined BEFORE the function is named.

This is a very strange sentence of yours, since it contains "named",
also a very strange logical viewpoint. If functions where "named"
objects, why do you have function equality axiom? The identity

would be their "name". Like in object orientation where "is"
in Python checks object identity. When I do this here, I can als
"name" a graph or do you deny that?

gra = { (gra, 0) }

> And there must exist y in the codomain such that (f,y) in G.

Do you mean (x,y) and not (f,y). I guess this is a typo. Well
for the above example we have dom={gra} and cod={0}.
Can I apply your function axiom, yes or no?

What will be the result of:

fun(fun) = ?

If it where only a naming, I would expect fun(fun) = fun(gra) = 0.
But I guess this wont happen in DC Spoiled, right? Since we
cannot show fun = gra, right? And therefore also not

fun e cod right? Thats a very annoying axiom, I already have
a name gra = { (gra, 0) }, why should I give it another name, that
even doesn't work correctly?

Thats why Fritz is doing the right thing:
a) Only define _(_), what we call application
b) Don't pretend to create names or some other humbug

[Dan Christensen]

On Wednesday, September 14, 2022 at 2:46:36 PM UTC-4, Mostowski Collapse wrote:
> Ok, what happens if you take this graph [snip childish abuse]
>
> gra = { (gra, 0) }
>
[snip]

A proof of the existence of a such a set would be nice. How about it, Jan Burse? Maybe start with something reasonable like Peano's Axioms since you seem to be assuming the existence of the natural number 0:

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

[Dan Christensen]

On Wednesday, September 14, 2022 at 2:52:48 PM UTC-4, Mostowski Collapse wrote:
> BTW: I am doing as you said. You said:
>
> > The graph set G must be well defined BEFORE the function is named.

> This is a very strange sentence of yours, since it contains "named",
> also a very strange logical viewpoint.

[snip]

As you can see in the Function Axiom, the function in question is "named" by invoking Existential Specification. Now get busy with your construction (i.e. proof of existence) of your supposed graph set g in DC Proof. Hint: You will probably need to use the axioms for Cartesian products, powersets and subsets.

[Mostowski Collapse]

Well since you don't have regularity axiom in DC Spoiled.
Nothing pervents the existence of such a graph.
But please allow me a question, why do you make axioms

for natural numbers. Can you show the existence of natural
numbers in DC Spoiled without axioms? Or the existence
of a dedekind infinite set? You even have the axiom

of infinity missing in DC Spoiled. Nothing you worked with
in DC Spoiled so far, you can prove that it exists in DC Spoiled.

LMAO!

[Mostowski Collapse]

Using Kuratowski pair, we can rewrite gra = { (gra, 0) }
as gra = { { {gra}, {gra, 0} } }. Which leads to this system
of set equations:

gra = { s1 }
s1 = { s2, s3 }
s2 = { gra }
s3 = { gra, 0 }

Which has a unique solution according to this paper.
But I am not sure whether Kuratowski pair works in
AFA, or something else needs to be used?

PREDICATIVITY, CIRCULARITY, AND ANTI-FOUNDATION
M. RATHJEN - 2012
https://www1.maths.leeds.ac.uk/~rathjen/russelle.pdf

[Dan Christensen]

On Wednesday, September 14, 2022 at 8:29:09 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Mittwoch, 14. September 2022 um 23:34:26 UTC+2:
> > On Wednesday, September 14, 2022 at 2:52:48 PM UTC-4, Mostowski Collapse wrote:
> > > BTW: I am doing as you said. You said:
> > >
> > > > The graph set G must be well defined BEFORE the function is named.
> >
> > > This is a very strange sentence of yours, since it contains "named",
> > > also a very strange logical viewpoint.
> > [snip]
> >
> > As you can see in the Function Axiom, the function in question is "named" by invoking Existential Specification. Now get busy with your construction (i.e. proof of existence) of your supposed graph set g in DC Proof. Hint: You will probably need to use the axioms for Cartesian products, powersets and subsets.

> Well since you don't have regularity axiom in DC Proof.

> Nothing pervents the existence of such a graph.

Then you have no excuses for not proving its existence. Get busy!

> But please allow me a question, why do you make axioms
>
> for natural numbers.

You have to start by assuming the existence some set(s) in order to construct other sets like your graph set g. DC Proof does not assume the existence of any object(s), not even the empty set. You mentioned 0, a natural number. The set of natural numbers would seem to be natural choice for you, but any set(s) would do.

> Can you show the existence of natural

> numbers in DC Proof without axioms?

[snip]

Not without introducing additional axioms, e.g. the existence of a Dedekind infinite set.

Of course, you can't introduce just any old wonky axioms as you have done here. Peano's Axioms, of course, are not just any wonky axioms. If you can derive a contradiction from them alone, there would be a serious problem.

[Dan Christensen]

On Wednesday, September 14, 2022 at 8:39:27 PM UTC-4, Mostowski Collapse wrote:
> Using Kuratowski pair, we can rewrite gra = { (gra, 0) }
> as gra = { { {gra}, {gra, 0} } }. Which leads to this system
> of set equations:
>
> gra = { s1 }
> s1 = { s2, s3 }
> s2 = { gra }
> s3 = { gra, 0 }
>

[snip]

I think this needs a pairing axiom as in ZFC. Again, there is no such axiom in DC Proof. It isn't required in ordinary mathematics, e.g. linear algebra or real analysis. For your assignment, you can use only the axioms on the Sets and Logic menus in DC Proof.

[Mostowski Collapse]

See my replies just now to your identical postings at sci.math.

[Mostowski Collapse]

Here is a shorter proof, there was also a typo in axiom
4 which I have now corrected, I wrote g(x) instead x(x),
further I only need one direction of (Exp):

1 ALL(x):~x=singleton(x)
Axiom

2 ALL(f):[ALL(x):[x=0 => f(x)=0] => f ε c]
Axiom

3 ALL(x):[x=0 => g(x)=0]
Axiom

4 ALL(x):[x ε c => g(x)=singleton(x(x)) & x(x) ε d]
Axiom

5 ALL(x):[x=0 => g(x)=0] => g ε c
U Spec, 2

6 g ε c
Detach, 5, 3

7 g ε c => g(g)=singleton(g(g)) & g(g) ε d
U Spec, 4

8 g(g)=singleton(g(g)) & g(g) ε d
Detach, 7, 6

9 g(g)=singleton(g(g))
Split, 8

10 g(g) ε d
Split, 8

11 ~g(g)=singleton(g(g))
U Spec, 1, 10

12 g(g)=singleton(g(g)) & ~g(g)=singleton(g(g))
Join, 9, 11

[Fritz Feldhase]

On Thursday, September 15, 2022 at 6:26:49 PM UTC+2, Mostowski Collapse wrote:
> Here is a shorter proof, there was also a typo in axiom
> 4 which I have now corrected, I wrote g(x) instead x(x),
> further I only need one direction of (Exp):

Just some comments.

> 1 ALL(x):~x=singleton(x)
> Axiom

In the context of ZFA we might have sets x such that x=singleton(x).

Without that axiom you cannot derive "your" contradiction.

So it seems that DC Spoof is just (or especially?) not "compatible" with ZFC.

Not good, of course.

But...

Some minor details:

> 2 ALL(f):[ALL(x):[x=0 => f(x)=0] => f ε c]
> Axiom

Shorter:
2 ALL(f):[f(0) = 0 => f ε c]

> Axiom

> 3 ALL(x):[x=0 => g(x)=0]
> Axiom

Shorter:
> 3 g(0)=0]
> Axiom

Now...

> 4 ALL(x):[x ε c => g(x)=singleton(x(x)) & x(x) ε d]
> Axiom

I guess that one is "problematic". Since it implies

ALL(x):[x ε c => g(x)=singleton(x(x))]

which will collide with the definition of .(.) in the way I did. [Since this definition implies x(x) = {} for any x.
But since {x(x)} isn't empty, x(x) = {x(x)} CAN'T hold for any x. Now if g ε c (which it is, due to your axioms above)
then this axiom "implies" (quite directly) a contradiction.]

So maybe this axiom is to blame?
___________________________________

On the other hand, if we are working in ZFA ... couldn't there be a function g: {0} --> {0}, such that
g(0) = 0 and g(g) = {g(g)}?

Say, we have a Quine Atom q = {q}. And let's assume that we have defined .(.) using the following approach:

_______the y such that (x, y) e f if f is a function and x e dom(f)
f(x) = {
_______ q otherwise

Now we define g: {0} --> {0} with g(0) = 0. Then g e c, but also g(g) = {g(g)}, since g !e dom(g) and hence g(g) = q, with q = {q}.

[Dan Christensen]

On Thursday, September 15, 2022 at 2:34:58 PM UTC-4, Fritz Feldhase wrote:
[snip]

> Just some comments.
>
> > 1 ALL(x):~x=singleton(x)
> > Axiom
>
> In the context of ZFA we might have sets x such that x=singleton(x).
>
> Without that axiom you cannot derive "your" contradiction.
>

> So it seems that DC Proof is just (or especially?) not "compatible" with ZFC.
>
> Not good, of course.
>

A proof checker based on ZFC and "standard" FOL would be quite useless to students first learning the basic methods of proof. Better to use the same methods used, implicitly at least, in most math textbooks.

> But...
>
> Some minor details:
> > 2 ALL(f):[ALL(x):[x=0 => f(x)=0] => f ε c]
> > Axiom
> Shorter:
> 2 ALL(f):[f(0) = 0 => f ε c]
> > Axiom
>
> > 3 ALL(x):[x=0 => g(x)=0]
> > Axiom
> Shorter:
> > 3 g(0)=0]
> > Axiom
>
> Now...
> > 4 ALL(x):[x ε c => g(x)=singleton(x(x)) & x(x) ε d]
> > Axiom
> I guess that one is "problematic". Since it implies
>
> ALL(x):[x ε c => g(x)=singleton(x(x))]
>
> which will collide with the definition of .(.) in the way I did. [Since this definition implies x(x) = {} for any x.
> But since {x(x)} isn't empty, x(x) = {x(x)} CAN'T hold for any x. Now if g ε c (which it is, due to your axioms above)
> then this axiom "implies" (quite directly) a contradiction.]
>
> So maybe this axiom is to blame?

You think?

> ___________________________________
>
> On the other hand, if we are working in ZFA ... couldn't there be a function g: {0} --> {0}, such that
> g(0) = 0

Yes. It's graph set would be {(0, 0)}.

> and g(g) = {g(g)}?

[snip]

If g=/=0, then your definition of g would not be applicable. g(g) would then be undefined or indeterminate.

[Mostowski Collapse]

I nowhere wrote g : {0} -> {0}.
I only wrote: ALL(x):[x=0 => g(x)=0]

[Mostowski Collapse]

The inconsistency is based on a) and b):

Mostowski Collapse schrieb am Dienstag, 13. September 2022 um 02:02:17 UTC+2:
> a) Usually in set theory this here should hold for primitive function spaces:
> Definition: 4.2.6 The Exponentiation Axiom (abbreviated Exp) postulates
> ...
> b) Dan O Matiks favorite for f : a -> b:
> ALL(x):[x ε a=> f(x) ε b]
https://groups.google.com/g/sci.logic/c/I2NEjtolSGc/m/kRG4k-ieBQAJ

The ALL(x):[x=0 => g(x)=0] is a shorthand
for ALL(x):[x ε {0} => g(x) ε {0}] which is not
the same as g : {0} -> {0}.

In set theory, g : {0} -> {0}, would indeed imply
g = { (0,0) }, but ALL(x):[x ε {0} => g(x) ε {0}] only
implies (0,0) ε g, which is weaker.

You cannot prove (If DC Spoiled can prove this,
it is seriously broken):

(0,0) ε g => g = { (0,0) }

It could be also the case that g = { (0,0), (🌷,🌷) }
or whatever has (0,0) as a member.

[Dan Christensen]

On Thursday, September 15, 2022 at 3:46:21 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
> The inconsistency is based on a) and b):
>
> Mostowski Collapse schrieb am Dienstag, 13. September 2022 um 02:02:17 UTC+2:
> > a) Usually in set theory this here should hold for primitive function spaces:
> > Definition: 4.2.6 The Exponentiation Axiom (abbreviated Exp) postulates
> > ...

> > b) Dan's favorite for f : a -> b:

> > ALL(x):[x ε a=> f(x) ε b]
> https://groups.google.com/g/sci.logic/c/I2NEjtolSGc/m/kRG4k-ieBQAJ
>

[snip]

You are still grasping at straws here, Jan Burse. We are STILL waiting for your proof that DC Proof is somehow inconsistent. No wonky axioms this time. Note: Peano's Axioms are NOT wonky. Neither is the existence of, say, a non-empty set. Or even an empty set. Something along those line would be acceptable. Now, do your homework, Jan Burse.

[Fritz Feldhase]

On Thursday, September 15, 2022 at 9:19:26 PM UTC+2, Dan Christensen wrote:

> > So it seems that DC Proof is just (or especially?) not "compatible" with ZFC.
> >
> > Not good, of course.
> >
> A proof checker based on ZFC and "standard" FOL would be quite useless to students first learning the basic methods of proof.

If you say so. Seems that you are a teacher who knows his stuff.

On the other hand, your tool should at least be "compatible" with ZFC.

> If g =/= 0, then your definition of g would not be applicable.

You do not understand that definition. It's ALWAYs applicable.

> g(g) would then be undefined or <bla>

No, it wouldn't and it isn't.

How hard can it be to understand BASIC set theory?

Hint:

z(x) := U{y : (x, y) e z}

dom(z) := {x : Ey((x, y) e z}

Now if g !e dom(g), then g(g) = {}.

Not that hard, is it?

In addition, with

function(z) :<-> EXEY(z c X x Y) & AxAy1Ay2((x, y1) e z & (x, y2) e z -> y1 = y2)

we get for any function(f):

AxAy(x e dom(f) -> (f(x) = y <-> (x, y) e f)).

You see, IF some x is in dom(f), THEN we may consider f(x) = y and (x, y) e f as equivalent.

For any f in ZFC f(f) = {}. But this does NOT "mean" that f e dom(f). (Actually, it isn't and it can't be in ZFC.)

Especially for you: "f(f)" is just a formal expression (a term) which denotes the empty set {}.

In the context of FOPL (with set theory) we clearly prefer to have

AfAxAy(f(x) = y v ~f(x) = y).

and hence especially, say,

g(g) = 0 v ~g(g) = 0 ,

even though g !e dom(g).

g(g) IN THIS CONTEXT doesn't make much sense from a "mathematical" point of view - but from a "formal" ("logical") point of view it does.

[Dan Christensen]

On Thursday, September 15, 2022 at 6:14:29 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, September 15, 2022 at 9:19:26 PM UTC+2, Dan Christensen wrote:
>
> > > So it seems that DC Proof is just (or especially?) not "compatible" with ZFC.
> > >
> > > Not good, of course.
> > >
> > A proof checker based on ZFC and "standard" FOL would be quite useless to students first learning the basic methods of proof.
> If you say so. Seems that you are a teacher who knows his stuff.
>
> On the other hand, your tool should at least be "compatible" with ZFC.
>

There are features (quirks?) of ZFC and FOL that are largely ignored in math textbooks without introducing any known inconsistencies.

> > If g =/= 0, then your definition of g would not be applicable.
>
> You do not understand that definition. It's ALWAYs applicable.
>

By inapplicable, I mean that when x is not in the domain of function f, we can infer nothing about f(x). Basic high-school math.

> > g(g) would then be undefined or <bla>
>
> No, it wouldn't and it isn't.
>
> How hard can it be to understand BASIC set theory?
>
> Hint:
>
> z(x) := U{y : (x, y) e z}
>
> dom(z) := {x : Ey((x, y) e z}
>
> Now if g !e dom(g), then g(g) = {}.
>
> Not that hard, is it?
>

More common is something like: ALL(a):ALL(b):[a in dom & b in cod => [f(a)=b <=> (a,b) in G]].

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

When x not in dom, we cannot use this definition to infer anything about f(x), i.e. f(x)=y would be indeterminate or undefined.

> In addition, with
>
> function(z) :<-> EXEY(z c X x Y) & AxAy1Ay2((x, y1) e z & (x, y2) e z -> y1 = y2)
>
> we get for any function(f):
>
> AxAy(x e dom(f) -> (f(x) = y <-> (x, y) e f)).
>

That would be another way to do it. Not my preference.

> You see, IF some x is in dom(f), THEN we may consider f(x) = y and (x, y) e f as equivalent.
>
> For any f in ZFC f(f) = {}. But this does NOT "mean" that f e dom(f). (Actually, it isn't and it can't be in ZFC.)
>
> Especially for you: "f(f)" is just a formal expression (a term) which denotes the empty set {}.
>
> In the context of FOPL (with set theory) we clearly prefer to have
>
> AfAxAy(f(x) = y v ~f(x) = y).
>

This gives us no information about f(x). It simply affirms the Law of the Excluded Middle which is true of any proposition.

> and hence especially, say,
>
> g(g) = 0 v ~g(g) = 0 ,
>
> even though g !e dom(g).
>
> g(g) IN THIS CONTEXT doesn't make much sense from a "mathematical" point of view - but from a "formal" ("logical") point of view it does.

[Fritz Feldhase]

On Friday, September 16, 2022 at 3:33:04 AM UTC+2, Dan Christensen wrote:

> More common is something like: ALL(a):ALL(b):[a in dom & b in cod => [f(a)=b <=> (a,b) in G]].

Holy shit! Certainly NOT, you silly crank.

Are you on drugs?

Anyway, more common would be:

AaAb: a in dom(f) -> [f(a) = b <-> (a, b) in f].

Ooops... I already wrote that.

> > AxAy(x e dom(f) -> (f(x) = y <-> (x, y) e f)).

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

Complete nonsense.

Aa: a in dom(f) -> f(a) e cod(f).

Your free floating "dom" and "cod" are complete nonsense (i. e. crank stuff).

> When x not in dom,

in dom(f) i. e. __in the domain of f__

HOLY SHIT!!!

> we cannot use this definition to infer anything about f(x),

Your bad.

That's why *we* use a definition like

z(x) := U{y : (x, y) e z} .

THEN:

> f(x) would be

{}

for any x !e dom(f).

I already told you that fact. What's the matter with you, Dan? Are you demented?

> > In addition, with
> >
> > function(z) :<-> EXEY(z c X x Y) & AxAy1Ay2((x, y1) e z & (x, y2) e z -> y1 = y2)
> >
> > we get for any function(f):
> >
> > AxAy(x e dom(f) -> (f(x) = y <-> (x, y) e f)).
> >
> That would be another way to do

Of course. Namely, the "standard way".

> > You see, IF some x is in dom(f), THEN we may consider f(x) = y and (x, y) e f as equivalent.
> >
> > For any f in ZFC f(f) = {}. But this does NOT "mean" that f e dom(f). (Actually, it isn't and it can't be in ZFC.)
> >
> > Especially for you: "f(f)" is just a formal expression (a term) which denotes the empty set {}.
> >
> > In the context of FOPL (with set theory) we clearly prefer to have
> >
> > AfAxAy(f(x) = y v ~f(x) = y).
> >
> This gives us no information about f(x).

No, it doesn't. So what?

> It simply affirms the Law of the Excluded Middle which is true of any proposition.

*lol* Is it?! You silly idiot just claimed that

"f(x)=y would be indeterminate or undefined"

for x !e dom(f).

Using "my" definition we have

> > especially, say,
> >
> > g(g) = 0 v ~g(g) = 0 ,
> >
> > even though g !e dom(g).
> >
> > g(g) IN THIS CONTEXT doesn't make much sense from a "mathematical" point of view - but from a "formal" ("logical") point of view it does.

No comment. That fits.

Fuck off, crank.

EOD

[Dan Christensen]

On Thursday, September 15, 2022 at 11:49:03 PM UTC-4, Fritz Feldhase wrote:
> On Friday, September 16, 2022 at 3:33:04 AM UTC+2, Dan Christensen wrote:
>
> > More common is something like: ALL(a):ALL(b):[a in dom & b in cod => [f(a)=b <=> (a,b) in G]].

[snip childish abuse]

Not unlike:

"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y , such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true [...] Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
--Terence Tao, "Analysis I," p. 49

Note the absence of dom and cod functions and the notion of a function as merely a set of ordered pairs.

> Anyway, more common would be:
>
> AaAb: a in dom(f) -> [f(a) = b <-> (a, b) in f].
>

Maybe in the philosophy department where they don't think it is necessary to distinguish the indeterminate from the false.

> Ooops... I already wrote that.
> > > AxAy(x e dom(f) -> (f(x) = y <-> (x, y) e f)).

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

> Complete nonsense.
>

Quite common AFAICT. In the math department anyway.

> Aa: a in dom(f) -> f(a) e cod(f).
>
> Your free floating "dom" and "cod" are complete nonsense

[snip abuse]

You are reduced to quibbling about trifles.

> > When x not in dom,

> in dom(f) i. e. __in the domain of f__
>

[snip abuse]

More quibbling??? <sigh>

> > we cannot use this definition to infer anything about f(x),

> Your bad.
>
> That's why *we* use a definition like
>
> z(x) := U{y : (x, y) e z} .
>
> THEN:
>
> > f(x) would be
>
> {}
>
> for any x !e dom(f).
>

[snip childish abuse]

Cute, but I think I will stick to the more mainstream notions of indeterminate and undefined function values.

> > > In addition, with
> > >
> > > function(z) :<-> EXEY(z c X x Y) & AxAy1Ay2((x, y1) e z & (x, y2) e z -> y1 = y2)
> > >
> > > we get for any function(f):
> > >
> > > AxAy(x e dom(f) -> (f(x) = y <-> (x, y) e f)).
> > >

> > That would be another way to do it.

> Of course. Namely, the "standard way".

Not so much in the math department.

> > > You see, IF some x is in dom(f), THEN we may consider f(x) = y and (x, y) e f as equivalent.
> > >
> > > For any f in ZFC f(f) = {}. But this does NOT "mean" that f e dom(f). (Actually, it isn't and it can't be in ZFC.)
> > >
> > > Especially for you: "f(f)" is just a formal expression (a term) which denotes the empty set {}.
> > >
> > > In the context of FOPL (with set theory) we clearly prefer to have
> > >
> > > AfAxAy(f(x) = y v ~f(x) = y).
> > >

> > This gives us no information about f(x).

> No, it doesn't.

Good. We agree.

> > It simply affirms the Law of the Excluded Middle which is true of any proposition.

> *lol* Is it?! You [snip abuse] just claimed that

> "f(x)=y would be indeterminate or undefined"
> for x !e dom(f).
>

Yes. If we cannot determine the truth value of f(x)=y, then we say that it is "indeterminate" or "undefined." Saying it could be either true or false is pointless.

> Using "my" definition we have
> > > especially, say,
> > >
> > > g(g) = 0 v ~g(g) = 0 ,
> > >
> > > even though g !e dom(g).
> > >
> > > g(g) IN THIS CONTEXT doesn't make much sense from a "mathematical" point of view - but from a "formal" ("logical") point of view it does.

> No comment.

I agreed with you that g(g) doesn't make much (or any) sense from a mathematical point view.

[Ben Bacarisse]

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

> On Thursday, September 15, 2022 at 11:49:03 PM UTC-4, Fritz Feldhase wrote:
>> On Friday, September 16, 2022 at 3:33:04 AM UTC+2, Dan Christensen wrote:
>>
>> > More common is something like: ALL(a):ALL(b):[a in dom & b in cod => [f(a)=b <=> (a,b) in G]].
>
> [snip childish abuse]
>
> Not unlike:
>
> "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a
> property pertaining to an object x ∈ X and an object y ∈ Y , such that
> for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true
> [...] Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> --Terence Tao, "Analysis I," p. 49
>
> Note the absence of dom and cod functions and the notion of a function
> as merely a set of ordered pairs.

I thought I'd check that "[...]" as it was a bit suspicious. Would Tao
really not make explicit what X and Y are in relation to f? No. The
part you snipped includes

[...] Then we define the function f : X → Y defined by P on the domain X
and range Y [...]

Writing f : X → Y when talking about X and Y is the same as writing X =
don(f), Y = cod(f) or simply using dom(f) and cod(f) independently. DC
Proof should either have some way to specify that f : X → Y, or
something like the dom(f) and cod(f) you object to is needed.

You cite this work a lot, but you need to take care because Tao is
writing rather casually. For example, he says that

"it is possible to start with a function f : X → Y and construct its
graph {(x, f(x)) : x ∈ X}, which describes the function completely"

but (using Tao's definition of equality) two different functions can
have the same graph so "describes completely" is being used in a rather
loose way. If the graph really /did/ describe a function completely,
then a function could, quite reasonably, be considered a set of ordered
pairs (though one could still, somewhat pointlessly, define it to be
something other than its graph).

--
Ben.

[Dan Christensen]

On Friday, September 16, 2022 at 10:07:31 AM UTC-4, Ben Bacarisse wrote:
> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>
> > On Thursday, September 15, 2022 at 11:49:03 PM UTC-4, Fritz Feldhase wrote:
> >> On Friday, September 16, 2022 at 3:33:04 AM UTC+2, Dan Christensen wrote:
> >>
> >> > More common is something like: ALL(a):ALL(b):[a in dom & b in cod => [f(a)=b <=> (a,b) in G]].
> >
> > [snip childish abuse]
> >
> > Not unlike:
> >
> > "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a
> > property pertaining to an object x ∈ X and an object y ∈ Y , such that
> > for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true
> > [...] Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
> > --Terence Tao, "Analysis I," p. 49
> >
> > Note the absence of dom and cod functions and the notion of a function
> > as merely a set of ordered pairs.
> I thought I'd check that "[...]" as it was a bit suspicious. Would Tao
> really not make explicit what X and Y are in relation to f? No. The
> part you snipped includes
>
> [...] Then we define the function f : X → Y defined by P on the domain X
> and range Y [...]
>
> Writing f : X → Y when talking about X and Y is the same as writing X =

> dom(f), Y = cod(f) or simply using dom(f) and cod(f) independently.

The dom(f) and cod(f) notation seems to refer to functions on some unspecified domain. Tao does not use this notation.

> DC
> Proof should either have some way to specify that f : X → Y, or
> something like the dom(f) and cod(f) you object to is needed.
>

I use a 3-place predicate Function.

For functions of 1 variable, I use the following axiom:

ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
=> [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):[Function(fun,dom,cod) <----------------- Here

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

> You cite this work a lot, but you need to take care because Tao is
> writing rather casually. For example, he says that
>
> "it is possible to start with a function f : X → Y and construct its
> graph {(x, f(x)) : x ∈ X}, which describes the function completely"
> but (using Tao's definition of equality) two different functions can
> have the same graph so "describes completely" is being used in a rather
> loose way.

[snip]

f: X --> Y together with the graph set {(x, f(x)) : x ∈ X} do completely describe the function.

[Ben Bacarisse]

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

> On Friday, September 16, 2022 at 10:07:31 AM UTC-4, Ben Bacarisse wrote:
>> Dan Christensen <Dan_Chr...@sympatico.ca> writes:
>>
>> > On Thursday, September 15, 2022 at 11:49:03 PM UTC-4, Fritz Feldhase wrote:
>> >> On Friday, September 16, 2022 at 3:33:04 AM UTC+2, Dan Christensen wrote:
>> >>
>> >> > More common is something like: ALL(a):ALL(b):[a in dom & b in cod => [f(a)=b <=> (a,b) in G]].
>> >
>> > [snip childish abuse]
>> >
>> > Not unlike:
>> >
>> > "Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a
>> > property pertaining to an object x ∈ X and an object y ∈ Y , such that
>> > for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true
>> > [...] Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."
>> > --Terence Tao, "Analysis I," p. 49
>> >
>> > Note the absence of dom and cod functions and the notion of a function
>> > as merely a set of ordered pairs.
>> I thought I'd check that "[...]" as it was a bit suspicious. Would Tao
>> really not make explicit what X and Y are in relation to f? No. The
>> part you snipped includes
>>
>> [...] Then we define the function f : X → Y defined by P on the domain X
>> and range Y [...]
>>
>> Writing f : X → Y when talking about X and Y is the same as writing X =
>> dom(f), Y = cod(f) or simply using dom(f) and cod(f) independently.
>
> The dom(f) and cod(f) notation seems to refer to functions on some
> unspecified domain. Tao does not use this notation.

The notation is not the issue. Neither f : X → Y nor dom(f) and cod(f)
are suitable as DC Proof stands.

>> DC
>> Proof should either have some way to specify that f : X → Y, or
>> something like the dom(f) and cod(f) you object to is needed.
>>
>
> I use a 3-place predicate Function.
>
> For functions of 1 variable, I use the following axiom:
>
> ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod) & Set'(gra)
> => [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):[Function(fun,dom,cod) <----------------- Here
>
> & ALL(a1):ALL(b):[a1 in dom & b in cod => [fun(a1)=b <=> (a1,b) in gra]]]]]

Do you think this treatment of functions is suitable for students? I
don't think I've ever seen something so simple expressed in such a
complicated way (assuming it's correct).

--
Ben.

[Dan Christensen]

Required sets:

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

Requirements for the functionality of the graph set:

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

Naming the new function:

> > => EXIST(fun): [Function(fun,dom,cod)
> >

Defining the new function in terms of the given graph set:

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

> Do you think this treatment of functions is suitable for students?

Certainly not for beginners. Formally proving the existence of function is a fairly advanced topic. I don't recall ever having to do so in any pure math course. Formal proofs were never required. Functions were simply "defined" as required. I include the function axioms for completeness. And for something to write about at my blog for more advanced students. These axioms are not required for my tutorial.

[Jeff Barnett]

Did you ever take a high school or 1st year collage calculus course?
Perhaps you then define derivative and and anti-derivative functions.
And part of the tricks involved were saying where they were defined and
issues of real and complex values. Or in high school and early
university did you ever form "functional equations" and try to solve
them? You even do some of these things in a basic trigonometry class.
--
Jeff Barnett

[Dan Christensen]

On Friday, September 16, 2022 at 5:52:42 PM UTC-4, Jeff Barnett wrote:
[snip]

What point are you trying to make here, Jeff? That there is no such thing as functions being undefined or indeterminate for some values/inputs? If so, that would put you very much outside of mainstream mathematics. That is not necessarily a bad thing in itself, but that is the issue here as I see it.

[Jeff Barnett]

If that is how you interpret what I wrote, you have serious problems
with English as well as the obvious problems understanding mathematics
and logic. The point is that non-serious as well as serious students
take classes where they learn to create and define functions as well as
have the onus of accurately describing them as part of the class work.
You claim (I suppose ..) you want to help them yet are entirely unaware
of what they are taught and how. You also ignore advise from folks who
have been on both sides of the teacher/student divide most of their life.

You remind me of a fellow, David J., in my high school chemistry class
who seemed fairly intelligent but never listened to what he was told and
made light of everything. For example, teacher kept warning him to think
a little bit when he was in the lab; he had caused a series of minor
problems through non-attention, often while spewing gibberish. One day
he was walking around and saw some really grunge looking stuff on the
counter so he decided to do a good deed: He throw the stuff in the sink
and simultaneously leaned over to turn on the water. That wasn't
necessary because the sink was already stoppered and had water in it. We
all stood and clapped and hooted when that disgusting piece of sodium
hit the water. David needed medical attention but was quite lucky that
somehow his eyes were either closed or not looking at the center of the
explosion. It makes me wonder, Dan: Did you ever take a chemistry class?

He was like you. When he saw or perceived a problem. He took charge and
grabbed the bull by the horns. And that is why he spent the majority of
his life walking around with a chunk cartilage up his ass.
--
Jeff Barnett

[Dan Christensen]

[snip]

> The point is that non-serious as well as serious students
> take classes where they learn to create and define functions as well as
> have the onus of accurately describing them as part of the class work.

Nice climbdown, but it hasn't been my experience that in courses like linear algebra or real analysis, students are required to formally prove the existence of any particular functions using the axioms of set theory. Nevertheless, that capability is built into DC Proof for students who may wish to do so.

> You claim (I suppose ..) you want to help them yet are entirely unaware
> of what they are taught and how. You also ignore advise from folks who
> have been on both sides of the teacher/student divide most of their life.
>

[snip irrelevant nonsense]

You mean folks like Terence Tao? https://en.wikipedia.org/wiki/Terence_Tao

"Definition 3.3.1 (Functions). Let X, Y be sets, and let P(x, y) be a property pertaining to an object x ∈ X and an object y ∈ Y , such that for every x ∈ X, there is exactly one y ∈ Y for which P(x, y) is true (this is sometimes known as the vertical line test). Then we define the function f : X → Y defined by P on the domain X and range Y to be the object which, given any input x ∈ X, assigns an output f(x) ∈ Y, defined to be the unique object f(x) for which P(x, f(x)) is true. Thus, for any x ∈ X and y ∈ Y, y = f(x) ⇐⇒ P(x, y) is true."

--Terence Tao, "Analysis I," p. 49

"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 [with respect to the domain X], if and only if f(x) = g(x) for all x ∈ X. (If f(x) and g(x) agree for some values of x, but not others, then we do not consider f and g to be equal.)"
--Terence Tao, "Analysis I," p. 51

Not unlike axioms available on the Sets menu of DC Proof. Must be frustrating as hell for you.

[Dan Christensen]

Example: You can formally prove the existence of an identity function on any given set (101 lines in DC Proof), but very few if any textbook authors would include even an informal proof, the result being so "intuitively obvious." Such proofs are not covered in the DC Proof tutorial, but are left as an exercise for the motivated user with many examples at my math blog.

[Dan Christensen]

See: https://www.dcproof.com/IdentityFunction.htm

[Fritz Feldhase]

On Sunday, September 18, 2022 at 5:38:01 AM UTC+2, Dan Christensen wrote:

> Example: You can formally prove the existence of an identity function on any given set

In the context of ZFC (with some definitions for basic set-theoretic notions, say, ". x .", "(., .)", "U", etc.):

Let f = {(x, x) e A x A : x e A}.

Then f is a function with domain A such that f(x) = x for all x e A.

Proof: f is a set of ordered pairs and f is functional, hence f is a function. dom(f) = A and for all x e dom(f): f(x) = x. qed

Some definitions which might help to fill the gaps:

ordered_pair(p) :<-> ExEy(p = (x, y))
functional(h) :<-> AxAyAz((x, y) e h & (x, z) e h -> y = z)
function(h) :<-> ordered_pair(h) & functional(h)
dom(h) := {x e UUh : Ey((x, y) e h}
f(x) := U{y e UUh : (x, y) e h}

[Dan Christensen]

On Sunday, September 18, 2022 at 11:28:50 PM UTC-4, Fritz Feldhase wrote:
> On Sunday, September 18, 2022 at 5:38:01 AM UTC+2, Dan Christensen wrote:
>
> > Example: You can formally prove the existence of an identity function on any given set
> In the context of ZFC (with some definitions for basic set-theoretic notions, say, ". x .", "(., .)", "U", etc.):
>
> Let f = {(x, x) e A x A : x e A}.
>

[snip]

That is a definition, not a proof of existence. You want to end your proof with EXIST(f): ...

In my proof, I start by assuming that x is a set:

1. Set(x)
Premise

At the end that I conclude:

101. ALL(x):[Set(x) => EXIST(f):[Function(f,x,x) & ALL(a):[a in x => f(a)=a]]]
Conclusion, 1

I make use of the following axioms of set theory in DC Proof:

- Cartesian Product (Line 2)

- Subset (Line 10)

- Function (Line 14)

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

[Mostowski Collapse]

So you cannot prove in DC Spoiled:

x =\= y => id_x =\= id_y

LoL

[Mostowski Collapse]

You must be extremly proud of the nonsense that you have
created in the form of DC Spoiled, making you blind to the
fact that you cannot solve this easy text book exercise.

[Dan Christensen]

On Monday, September 19, 2022 at 7:08:46 AM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Montag, 19. September 2022 um 05:54:40 UTC+2:
> > On Sunday, September 18, 2022 at 11:28:50 PM UTC-4, Fritz Feldhase wrote:
> > > On Sunday, September 18, 2022 at 5:38:01 AM UTC+2, Dan Christensen wrote:
> > >
> > > > Example: You can formally prove the existence of an identity function on any given set
> > > In the context of ZFC (with some definitions for basic set-theoretic notions, say, ". x .", "(., .)", "U", etc.):
> > >
> > > Let f = {(x, x) e A x A : x e A}.
> > >
> > [snip]
> >
> > That is a definition, not a proof of existence. You want to end your proof with EXIST(f): ...
> >
> > In my proof, I start by assuming that x is a set:
> >
> > 1. Set(x)
> > Premise
> >
> > At the end that I conclude:
> >
> > 101. ALL(x):[Set(x) => EXIST(f):[Function(f,x,x) & ALL(a):[a in x => f(a)=a]]]
> > Conclusion, 1
> >
> > I make use of the following axioms of set theory in DC Proof:
> >
> > - Cartesian Product (Line 2)
> >
> > - Subset (Line 10)
> >
> > - Function (Line 14)
> >
> > https://www.dcproof.com/IdentityFunction.htm

> So you cannot prove in DC Proof:

>
> x =\= y => id_x =\= id_y
>

In DC Proof, as in Terrence Tao's best-selling textbook, "Analysis I", you can only compare functions with the same domains and codomains. You could, of course, compare their graph sets.

[Mostowski Collapse]

You wrote:
> you can only compare functions with the same domains and codomains

Well thats not completely true. For x=\=y you can prove:

Surjective(id_x,x,x)
~Surjective(id_y,x,x)

And therefore indirectly via your subst rule in DC Spoiled:

id_x =\= id_y

[Mostowski Collapse]

Lets make it like this. For x=\=y you can prove:

Bijection(id_x,x,x)
~Bijection(id_y,x,x)

And therefore indirectly via your subst rule in DC Spoiled:

id_x =\= id_y

[Mostowski Collapse]

Or maybe you cannot prove:

y=\=x => ~Bijection(id_y,x,x)

Right, you cannot prove the above?
What is it if its not not a Bijection?
Maybe a dark Bijection from Wolfgang Mückenheim?

LoL

[Dan Christensen]

On Monday, September 19, 2022 at 11:08:18 AM UTC-4, Mostowski Collapse wrote:
> Lets make it like this. For x=\=y you can prove:
>
> Bijection(id_x,x,x)
> ~Bijection(id_y,x,x)

Your proof?

[Dan Christensen]

On Monday, September 19, 2022 at 11:16:10 AM UTC-4, Mostowski Collapse wrote:
> Or maybe you cannot prove:
>
> y=\=x => ~Bijection(id_y,x,x)
>

Not true in general. What is your point, Jan Burse?

[Dan Christensen]

On Monday, September 19, 2022 at 11:06:20 AM UTC-4, Mostowski Collapse wrote:
> You wrote:
> > you can only compare functions with the same domains and codomains
> Well thats not completely true. For x=\=y you can prove:
>
> Surjective(id_x,x,x)
> ~Surjective(id_y,x,x)
>

Your proof?

[Ross A. Finlayson]

On Tuesday, September 13, 2022 at 10:31:48 AM UTC-7, Mostowski Collapse wrote:
> Maybe can carry out the diagonal argument by means
> of this productive view of the Russel Paradox, which
>
> doesn't require Regularity aka Foundation Axiom:
>
> Lemma: 3.8.2 (ECST)
> For every set A there is a set A_R such that ~(A_R e A).
> https://www1.maths.leeds.ac.uk/~rathjen/book.pdf
>
> Letting us plunge off the cliff some assumptions
> in showing the DC Spoiled inconsistency.
> Mostowski Collapse schrieb am Dienstag, 13. September 2022 um 19:23:03 UTC+2:
> > Like you can show via the Regularity Axiom:
> >
> > x =\= {x}
> >
> > You can also show that:
> >
> > f =\= { .... (f,..) ...}
> >
> > f cannot have a pair inside itself with the first coordinate
> > the function f itself. Thats impossible in set theory,
> > Although Peter Aczel might gainsay, and raise his finger,
> >
> > well and say my set theory has extraordinary sets,
> > there is no requirement of Regularity Axiom, we might
> > indeed have such extraordinary functions.
> >
> > But Peter Aczel writes:
> >
> > Theorem: 4.2.7 ECSTc+Exp proves the same theorems as
> > classical Zermelo- Fraenkel Set Theory without the
> > Foundation Axiom, ZF-. As ZF and ZF- have the same strength,
> > ECSTc + Exp and ZF have the same strength.
> >
> > Proof: With classical logic, Replacement implies full Separation
> > and Exponentiation implies the Powerset Axiom. Details
> > are left to the exercise.
> > https://www1.maths.leeds.ac.uk/~rathjen/book.pdf
> >
> > So maybe can do the diagonalization without requiring
> > Regularity aka Foundation Axiom? Anybody an idea?

Does it already have a theory of real functions?

[Dan Christensen]

On Monday, September 19, 2022 at 12:32:17 PM UTC-4, Ross A. Finlayson wrote:
> On Tuesday, September 13, 2022 at 10:31:48 AM UTC-7, Mostowski Collapse wrote:
> > Maybe can carry out the diagonal argument by means
> > of this productive view of the Russel Paradox, which
> >
> > doesn't require Regularity aka Foundation Axiom:
> >
> > Lemma: 3.8.2 (ECST)
> > For every set A there is a set A_R such that ~(A_R e A).
> > https://www1.maths.leeds.ac.uk/~rathjen/book.pdf

Nothing new. The only axiom of set theory required is the Subset Axiom (line 4).

From A worked example in my tutorial, 10+ years ago, plus addendum:

THEOREM

The set of all things cannot exist.

~EXIST(s):[Set(s) & ALL(a):ains]


PROOF

Suppose to the contrary...

1 Set(u) & ALL(a):a in u
Premise

2 Set(u)
Split, 1

3 ALL(a):a in u
Split, 1

Apply the Subset Axiom for u

4 EXIST(sub):[Set(sub) & ALL(a):[a in sub <=> a in u & ~a in a]]
Subset, 2

Define: r, the subset of all things that are not elements of themselves.

5 Set(r) & ALL(a):[a in r <=> a in u & ~a in a]
E Spec, 4

6 Set(r)
Split, 5

7 ALL(a):[a in r <=> a in u & ~a in a]
Split, 5

Apply the definition of r to itself

8 r in r <=> r in u & ~r in r
U Spec, 7

9 [r in r => r in u & ~r in r] & [r in u & ~r in r => r in r]
Iff-And, 8

10 r in r => r in u & ~r in r
Split, 9

11 r in u & ~r in r => r in r
Split, 9


Prove: ~r in r

Suppose to the contrary...

12 r in r
Premise

13 r in u & ~r in r
Detach, 10, 12

14 r in u
Split, 13

15 ~r in r
Split, 13

Obtain the contradiction...

16 r in r & ~r in r
Join, 12, 15

Apply the Conclusion Rule.

As Required:

17 ~r in r
Conclusion, 12

Apply the defintion of u to r

18 r in u
U Spec, 3

19 r in u & ~r in r
Join, 18, 17

20 r in r
Detach, 11, 19

We obtain the contradicition...

21 ~r in r & r in r
Join, 17, 20

Therefore, there cannot exist a set u as defined in the
initial premise.

22 ~EXIST(u):[Set(u) & ALL(a):a in u]
Conclusion, 1

**********************************************************

Addendum

23 ~~ALL(u):~[Set(u) & ALL(a):a in u]
Quant, 22

24 ALL(u):~[Set(u) & ALL(a):a in u]
Rem DNeg, 23

25 ALL(u):~~[Set(u) => ~ALL(a):a in u]
Imply-And, 24

26 ALL(u):[Set(u) => ~ALL(a):a in u]
Rem DNeg, 25

27 ALL(u):[Set(u) => ~~EXIST(a):~a in u]
Quant, 26

28 ALL(u):[Set(u) => EXIST(a):~a in u]
Rem DNeg, 27

[Mostowski Collapse]

Thats rather trivial in set theory. A map f is
a bijection f : A -> B, Bijection(f, A, B), if the
following holds:

a) f : A -> B
dom(f) = A & rng(f) ⊆ B

b) Injectivity:
ALL(x):ALL(y):ALL(z):[(x,y) e f & (x,z) e f => y = z]

c) Surjectivity:
ALL(y):[y e B => EXIST(x):[(x,y) e f]]

Now when you have id_X = { (x,x) | x e X }, then
we obviously have:

Bijection(id_X, X, X)

But if Y =\= X, then we have:

~Bijection(id_Y, X, X)

Because a) already fails, dom(id_Y) = Y =\= X.

LoL

[Mostowski Collapse]

Corr.: The better phrasing is "iff" instead "if",
but you know mathematicians are sloppy:

Thats rather trivial in set theory. A map f is

a bijection f : A -> B, Bijection(f, A, B), iff the
following holds, i.e. conjunction of a), b) and c):

...

[Fritz Feldhase]

On Wednesday, September 21, 2022 at 9:02:42 AM UTC+2, Mostowski Collapse wrote:

> a) f : A -> B
> dom(f) = A & rng(f) ⊆ B
>
> b) Injectivity:
> ALL(x):ALL(y):ALL(z):[(x,y) e f & (x,z) e f => y = z]

Not quite. That just ensures that a relation f is a function. (But we assumed that already.)

Injectivity:
ALL(x):ALL(y):ALL(z):[(x,z) e f & (y,z) e f => x = y]