On Monday, January 3, 2022 at 1:52:01 PM UTC-5, Mostowski Collapse wrote:
> Dan-O-Matik went full berserk:
> > I'm afraid, it is your version of FOL

> Also the prover on my website doesn't originate
> from me. Its the prover written by Jens Otten,
> which goes by then name leanseq_v5.pl:
>
> Build Your Own First-Order Prover
> Invited Tutorial at CADE in Natal/Brazil
> (24 August 2019)
> http://jens-otten.de/tutorial_cade19/
>
> Whats wrong with you?

I'm not the one stuck in the past, Jan Burse. You really have to abandon what doesn't work and move on.

Dan

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

Looks rather like the future than the past.
At least FOL is specified. What about DC Proof,
do you keep some sticky notes on the

fridge in your kitchen with all the specs?

Dan Christensen schrieb:
> On Monday, January 3, 2022 at 1:52:01 PM UTC-5, Mostowski Collapse wrote:
>> Dan-O-Matik went full berserk:
>>> I'm afraid, it is your version of FOL
>
>> Also the prover on my website doesn't originate
>> from me. Its the prover written by Jens Otten,
>> which goes by then name leanseq_v5.pl:
>>
>> Build Your Own First-Order Prover
>> Invited Tutorial at CADE in Natal/Brazil
>> (24 August 2019)
>> http://jens-otten.de/tutorial_cade19/
>>
>> Whats wrong with you?
>
> I'm not the one stuck in the past, Jan Burse. You really have to abandon what doesn't work and move on.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>
>

So DC Proof has something like Emperor penguins from antarctica
as functions, with the exotic USpec. What are they?
There are at least two approaches according two wikipedia for functions:
i) Set-like function, which requires:
(Relation): ∀x∀y (x,y) e f => x e dom & y e cod
ii) An ordered tripple f=(dom, cod,F)
https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach

Both approaches allow querying the domain dom(f) of a function f:
i) Set-like functions, it can be defined, and is a set because of (Relation):
dom(f) := { x | EXIST(y):(x,y) e f }
ii) An ordered tripple f=(dom, cod,F), it can be defined:
dom(f) := π1(f), i.e. projection on the first component of the ordered tripple

So both approaches i) and ii) have a notion dom(f). Why do the
Emperor penguins from antarctica from DC Proof, the functions with
the strange USpec not have a notion dom(f), either through some

definition or through some axiom? Thats quite counter to the current
mathematical practice of either i) or ii), which both do provide querying
the domain of a function.

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 20:04:21 UTC+1:
> Looks rather like the future than the past.
> At least FOL is specified. What about DC Proof,
> do you keep some sticky notes on the
>
> fridge in your kitchen with all the specs?
>
> Dan Christensen schrieb:
> > On Monday, January 3, 2022 at 1:52:01 PM UTC-5, Mostowski Collapse wrote:
> >> Dan-O-Matik went full berserk:
> >>> I'm afraid, it is your version of FOL
> >
> >> Also the prover on my website doesn't originate
> >> from me. Its the prover written by Jens Otten,
> >> which goes by then name leanseq_v5.pl:
> >>
> >> Build Your Own First-Order Prover
> >> Invited Tutorial at CADE in Natal/Brazil
> >> (24 August 2019)
> >> http://jens-otten.de/tutorial_cade19/
> >>
> >> Whats wrong with you?
> >
> > I'm not the one stuck in the past, Jan Burse. You really have to abandon what doesn't work and move on.
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> >
> >

See my reply just now to your similar posting here.

Dan

On Monday, January 3, 2022 at 5:56:50 PM UTC-5, Mostowski Collapse wrote:
> So DC Proof has something like Emperor penguins from antarctica
> as functions, with the exotic USpec. What are they?
>
> There are at least two approaches according two wikipedia for functions:
> i) Set-like function, which requires:
> (Relation): ∀x∀y (x,y) e f => x e dom & y e cod
> ii) An ordered tripple f=(dom, cod,F)
> https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
>
>...

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

But maybe there is some reading help necessary. Kurt Gödel
doesn't use the concept (Function from A to B). He rather
uses (Function over A).

You can imagine a Function over A is the statement f : A -> U,
where U is the universe of discourse. One can prove the
following, namely:

(1) f : A -> B => f : A -> U

You can prove the same in DC Proof I guess, with your
pseudo function notation. i.e. I guess you can prove
in DC Proof the following:

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

But I am not sure whether we can even prove it in DC Proof.
In FOL the above is trivially true, since f is anyway total.
But what clearly holds in Kurt Gödel is this here:

(2) f : A -> U => dom(f) = A

By the chain rule syllogism we get, combining (1) and (2):

(3) f : A -> B => dom(f)=A

On the other hand its very unlikely that one can prove this,
even in a logic that diverts from FOL, and makes the
function symbols behave differently from FOL, like in DC Proof:

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

The problem is that ALL(x):[x e A => ...] doesn't talk about
those x with ~(x e A), so there is not enough information
to deduce dom(f)=A.

Dan Christensen schrieb am Dienstag, 4. Januar 2022 um 06:49:54 UTC+1:
> See my reply just now to your similar posting here.
>
> Dan
> On Monday, January 3, 2022 at 5:56:50 PM UTC-5, Mostowski Collapse wrote:
> > So DC Proof has something like Emperor penguins from antarctica
> > as functions, with the exotic USpec. What are they?
> >
> > There are at least two approaches according two wikipedia for functions:
> > i) Set-like function, which requires:
> > (Relation): ∀x∀y (x,y) e f => x e dom & y e cod
> > ii) An ordered tripple f=(dom, cod,F)
> > https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
> >
> >...

Here is a quizz, which collections are in some bijection?

1) { f | f : Q -> R }, where R the real numbers and Q the rational numbers

2) { f | f : R -> R },

3) { f | f : R -> R, f continuous }

And the same quizz again for:

1) { f | "Dan-O-Matik f : Q -> R" }, where R the real numbers and Q the rational numbers

2) { f | "Dan-O-Matik f : R -> R" },

3) { f | "Dan-O-Matik f : R -> R", f continuous }

Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 10:50:49 UTC+1:
> 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
>
> But maybe there is some reading help necessary. Kurt Gödel
> doesn't use the concept (Function from A to B). He rather
> uses (Function over A).
>
> You can imagine a Function over A is the statement f : A -> U,
> where U is the universe of discourse. One can prove the
> following, namely:
>
> (1) f : A -> B => f : A -> U
>
> You can prove the same in DC Proof I guess, with your
> pseudo function notation. i.e. I guess you can prove
> in DC Proof the following:
>
> ALL(x):[x e A => f(x) e B] => ALL(x):[x e A => EXIST(y):f(x)=y]
>
> But I am not sure whether we can even prove it in DC Proof.
> In FOL the above is trivially true, since f is anyway total.
> But what clearly holds in Kurt Gödel is this here:
>
> (2) f : A -> U => dom(f) = A
>
> By the chain rule syllogism we get, combining (1) and (2):
>
> (3) f : A -> B => dom(f)=A
>
> On the other hand its very unlikely that one can prove this,
> even in a logic that diverts from FOL, and makes the
> function symbols behave differently from FOL, like in DC Proof:
>
> ALL(x):[x e A => EXIST(y):f(x)=y] = dom(f)=A
>
> The problem is that ALL(x):[x e A => ...] doesn't talk about
> those x with ~(x e A), so there is not enough information
> to deduce dom(f)=A.
> Dan Christensen schrieb am Dienstag, 4. Januar 2022 um 06:49:54 UTC+1:
> > See my reply just now to your similar posting here.
> >
> > Dan
> > On Monday, January 3, 2022 at 5:56:50 PM UTC-5, Mostowski Collapse wrote:
> > > So DC Proof has something like Emperor penguins from antarctica
> > > as functions, with the exotic USpec. What are they?
> > >
> > > There are at least two approaches according two wikipedia for functions:
> > > i) Set-like function, which requires:
> > > (Relation): ∀x∀y (x,y) e f => x e dom & y e cod
> > > ii) An ordered tripple f=(dom, cod,F)
> > > https://en.wikipedia.org/wiki/Function_%28mathematics%29#Relational_approach
> > >
> > >...

On Tuesday, January 4, 2022 at 4:50:49 AM UTC-5, Mostowski Collapse wrote:
> In standard mathematics, you can prove:
> f: A --> B => dom(f)=A
>

Again, there is nothing to prove. It's just terminology, Jan Burse. Deal with it.

Dan

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

Well its proofs, proofs, proofs, ... that is all what mathematicians do.
Lets have a look at what this mathematician says:

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

He says the function space X -> X is subset of P(X x X).
Take for X = {0}, then the function space is subset of
P({0} x {0}) = P({(0,0)}) = {{}, {(0,0)}}.

The only function in {{}, {(0,0)}} with domain {0}
is the function {(0,0)}, i.e. the function that sends the
argument 0 to 0. Therefore in ordinary mathematics

we can prove:

EXISTUNIQUE(f): f : {0} -> {0}

Can we also prove?

EXISTUNIQUE(f): "Dan-O-Matik f : {0} -> {0}" ?

Probably no? A function space just pulled out of
the ass, ignoring ordinary mathematics wont do
the job. The DC Proof mentor and creator just talks

nonsense all day long...

Dan Christensen schrieb am Mittwoch, 5. Januar 2022 um 23:41:27 UTC+1:
> On Tuesday, January 4, 2022 at 4:50:49 AM UTC-5, Mostowski Collapse wrote:
> > In standard mathematics, you can prove:
> > f: A --> B => dom(f)=A
> >
> Again, there is nothing to prove. It's just terminology, Jan Burse. Deal with it.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:

> Can we also prove?
>
> EXISTUNIQUE(f): " f : {0} -> {0}" ?
>

Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...

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

Same input, same output. Deal with it, Jan Burse.

Dan

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

The text book proof would end with:

=> f=g

Deal with it, Dan Christensen. You nowhere provide text book math.
Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 04:07:50 UTC+1:
> On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:
>
> > Can we also prove?
> >
> > EXISTUNIQUE(f): " f : {0} -> {0}" ?
> >
>
> Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...
>
> ALL(f):ALL(g):[ALL(a):[a in x => f(a) in x]
> & ALL(a):[a in x => g(a) in x]
> => ALL(a):[a in x => f(a)=g(a)]]
>
> Same input, same output. Deal with it, Jan Burse.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Now try this text book math:

> Here is a quizz, which collections are in some bijection?
>
> 1) { f | f : Q -> R }, where R the real numbers and Q the rational numbers
>
> 2) { f | f : R -> R },
>
> 3) { f | f : R -> R, f continuous }

See also:
https://math.stackexchange.com/questions/477/cardinality-of-set-of-real-continuous-functions

Mostowski Collapse schrieb am Donnerstag, 6. Januar 2022 um 05:44:40 UTC+1:
> The text book proof would end with:
>
> => f=g
>
> Deal with it, Dan Christensen. You nowhere provide text book math.
> Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 04:07:50 UTC+1:
> > On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:
> >
> > > Can we also prove?
> > >
> > > EXISTUNIQUE(f): " f : {0} -> {0}" ?
> > >
> >
> > Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...
> >
> > ALL(f):ALL(g):[ALL(a):[a in x => f(a) in x]
> > & ALL(a):[a in x => g(a) in x]
> > => ALL(a):[a in x => f(a)=g(a)]]
> >
> > Same input, same output. Deal with it, Jan Burse.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

You find your beloved CBS theorem, together with the
correct reading of function spaces, namely set exponentiation:

B^A = { f | f : A -> B }
https://math.stackexchange.com/questions/901735/meaning-of-a-set-in-the-exponent

One can also rephrase the quiz as, cardinalities of:

1) R^Q

2) R^R

3) C(R,R), where C(A,B) are the continues functions from B^A

Things you cannot correctly and concisely prove in DC Proof.
It just doesn't provide text book math that every mathematician
is confluent. Instead it confounds f : A -> B with ALL(x):[x e A =>

f(x) e B] which is utter nonsense. You dont get the same set
exponentiation with the Dan-O-Matik nonsense:

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

Mostowski Collapse schrieb am Donnerstag, 6. Januar 2022 um 05:49:09 UTC+1:
> Now try this text book math:
> > Here is a quizz, which collections are in some bijection?
> >
> > 1) { f | f : Q -> R }, where R the real numbers and Q the rational numbers
> >
> > 2) { f | f : R -> R },
> >
> > 3) { f | f : R -> R, f continuous }
> See also:
> https://math.stackexchange.com/questions/477/cardinality-of-set-of-real-continuous-functions
> Mostowski Collapse schrieb am Donnerstag, 6. Januar 2022 um 05:44:40 UTC+1:
> > The text book proof would end with:
> >
> > => f=g
> >
> > Deal with it, Dan Christensen. You nowhere provide text book math.
> > Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 04:07:50 UTC+1:
> > > On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > Can we also prove?
> > > >
> > > > EXISTUNIQUE(f): " f : {0} -> {0}" ?
> > > >
> > >
> > > Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...
> > >
> > > ALL(f):ALL(g):[ALL(a):[a in x => f(a) in x]
> > > & ALL(a):[a in x => g(a) in x]
> > > => ALL(a):[a in x => f(a)=g(a)]]
> > >
> > > Same input, same output. Deal with it, Jan Burse.
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Wednesday, January 5, 2022 at 11:44:40 PM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 04:07:50 UTC+1:
> > On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:
> >
> > > Can we also prove?
> > >
> > > EXISTUNIQUE(f): " f : {0} -> {0}" ?
> > >
> >
> > Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...
> >
> > ALL(f):ALL(g):[ALL(a):[a in x => f(a) in x]
> > & ALL(a):[a in x => g(a) in x]
> > => ALL(a):[a in x => f(a)=g(a)]]
> >
> > Same input, same output. Deal with it, Jan Burse.

> The text book proof would end with:
>
> => f=g
>

Wrong again, Jan Burse. With functions, it's all about inputs and outputs. Nothing else. Functions f and g are identical if and only if given the same inputs, you will obtain the same outputs.

> Deal with it, Dan Christensen. You nowhere provide text book math.

That's hilarious coming from someone who believes we can make logical inferences about f(x) for x not in the domain of definition of the function f. Get a life!

Dan

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

In standard text book mathematics you can prove:

f e B^A , x not in A => ~EXIST(y):(x,y) in f
https://math.stackexchange.com/questions/3480579/meaning-of-ab-where-a-and-b-are-sets

Thats a logical inference, isn't it? A logical inference
about x not in the domain of definition of f.

But the Function Axiom of DC Proof doesn't allow
it, this here is not anymore derivable:

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

Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 06:01:47 UTC+1:
> On Wednesday, January 5, 2022 at 11:44:40 PM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 04:07:50 UTC+1:
> > > On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > Can we also prove?
> > > >
> > > > EXISTUNIQUE(f): " f : {0} -> {0}" ?
> > > >
> > >
> > > Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...
> > >
> > > ALL(f):ALL(g):[ALL(a):[a in x => f(a) in x]
> > > & ALL(a):[a in x => g(a) in x]
> > > => ALL(a):[a in x => f(a)=g(a)]]
> > >
> > > Same input, same output. Deal with it, Jan Burse.
> > The text book proof would end with:
> >
> > => f=g
> >
> Wrong again, Jan Burse. With functions, it's all about inputs and outputs. Nothing else. Functions f and g are identical if and only if given the same inputs, you will obtain the same outputs.
> > Deal with it, Dan Christensen. You nowhere provide text book math.
> That's hilarious coming from someone who believes we can make logical inferences about f(x) for x not in the domain of definition of the function f. Get a life!
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 6, 2022 at 12:22:40 AM UTC-5, Mostowski Collapse wrote:

> Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 06:01:47 UTC+1:
> > On Wednesday, January 5, 2022 at 11:44:40 PM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 04:07:50 UTC+1:
> > > > On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:
> > > >
> > > > > Can we also prove?
> > > > >
> > > > > EXISTUNIQUE(f): " f : {0} -> {0}" ?
> > > > >
> > > >
> > > > Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...
> > > >
> > > > ALL(f):ALL(g):[ALL(a):[a in x => f(a) in x]
> > > > & ALL(a):[a in x => g(a) in x]
> > > > => ALL(a):[a in x => f(a)=g(a)]]
> > > >
> > > > Same input, same output. Deal with it, Jan Burse.
> > > The text book proof would end with:
> > >
> > > => f=g
> > >
> > Wrong again, Jan Burse. With functions, it's all about inputs and outputs. Nothing else. Functions f and g are identical if and only if given the same inputs, you will obtain the same outputs.

> > > Deal with it, Dan Christensen. You nowhere provide text book math.

> > That's hilarious coming from someone who believes we can make logical inferences about f(x) for x not in the domain of definition of the function f. Get a life!

> In standard text book mathematics you can prove:
>
> f e B^A , x not in A => ~EXIST(y):(x,y) in f
> https://math.stackexchange.com/questions/3480579/meaning-of-ab-where-a-and-b-are-sets
>

Nothing there to support your claim that we can make logical inferences about a function outside of it domain of definition.

> But the Function Axiom of DC Proof doesn't allow
> it, this here is not anymore derivable:
>
> f e B^A , x not in A =/=> ~EXIST(y):fun(x)=y

That is a good thing, Jan Burse. Any definition of a function that allows logical inferences to be made about a function outside of its domain of definition is nonsense--it's Burse's Paradox.

Dan

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

Its not a Burse's Paradox. Its simply an egregious error.
The mistake is on your side, namely writing, where fun
is what pops out of your DC Proof Function Axiom:

fun : A -> B /* egregious error */

Thats not the standard text book meaning of function spaces
A -> B. We require { f | f : A -> B } subset P(A x B). See yourself:

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

Or lookup the relevant literature about B^A yourself. Do your
homework, and stop confusing f : A -> B with ALL(x):[x a A =>
fun(x) e B]. Its not the same.

Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 06:41:50 UTC+1:
> On Thursday, January 6, 2022 at 12:22:40 AM UTC-5, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 06:01:47 UTC+1:
> > > On Wednesday, January 5, 2022 at 11:44:40 PM UTC-5, Mostowski Collapse wrote:
> > >
> > > > Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 04:07:50 UTC+1:
> > > > > On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:
> > > > >
> > > > > > Can we also prove?
> > > > > >
> > > > > > EXISTUNIQUE(f): " f : {0} -> {0}" ?
> > > > > >
> > > > >
> > > > > Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...
> > > > >
> > > > > ALL(f):ALL(g):[ALL(a):[a in x => f(a) in x]
> > > > > & ALL(a):[a in x => g(a) in x]
> > > > > => ALL(a):[a in x => f(a)=g(a)]]
> > > > >
> > > > > Same input, same output. Deal with it, Jan Burse.
> > > > The text book proof would end with:
> > > >
> > > > => f=g
> > > >
>
> > > Wrong again, Jan Burse. With functions, it's all about inputs and outputs. Nothing else. Functions f and g are identical if and only if given the same inputs, you will obtain the same outputs.
>
> > > > Deal with it, Dan Christensen. You nowhere provide text book math.
>
> > > That's hilarious coming from someone who believes we can make logical inferences about f(x) for x not in the domain of definition of the function f. Get a life!
> > In standard text book mathematics you can prove:
> >
> > f e B^A , x not in A => ~EXIST(y):(x,y) in f
> > https://math.stackexchange.com/questions/3480579/meaning-of-ab-where-a-and-b-are-sets
> >
> Nothing there to support your claim that we can make logical inferences about a function outside of it domain of definition.
> > But the Function Axiom of DC Proof doesn't allow
> > it, this here is not anymore derivable:
> >
> > f e B^A , x not in A =/=> ~EXIST(y):fun(x)=y
> That is a good thing, Jan Burse. Any definition of a function that allows logical inferences to be made about a function outside of its domain of definition is nonsense--it's Burse's Paradox.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

Also stop talking utter nonsense like:
> Nothing there to support your claim that we can make
logical inferences about a function outside of it domain of definition.

Well you defined it yourself, what F = B^A is:
Dan Christensen schrieb am Mittwoch, 5. Januar 2022 um 22:23:41 UTC+1:
> 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}.
https://groups.google.com/g/sci.math/c/IWbD8BdJkv8/m/3nY0WjN6BAAJ

If we have f e F, then we have also f e P(A x B).
Its really easy to prove:

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

Just think what the cross product is, and
what the power set is.

Do your homework.

Hint: f e P(A x B) implies f ⊆ A x B.

Mostowski Collapse schrieb am Donnerstag, 6. Januar 2022 um 06:51:43 UTC+1:
> Its not a Burse's Paradox. Its simply an egregious error.
> The mistake is on your side, namely writing, where fun
> is what pops out of your DC Proof Function Axiom:
>
> fun : A -> B /* egregious error */
>
> Thats not the standard text book meaning of function spaces
> A -> B. We require { f | f : A -> B } subset P(A x B). See yourself:
> Zermelo Fraenkel Powerset
> Richard E. BORCHERDS - 30.11.2021
> https://www.youtube.com/watch?v=XCMvljsu84s
> Or lookup the relevant literature about B^A yourself. Do your
> homework, and stop confusing f : A -> B with ALL(x):[x a A =>
> fun(x) e B]. Its not the same.
> Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 06:41:50 UTC+1:
> > On Thursday, January 6, 2022 at 12:22:40 AM UTC-5, Mostowski Collapse wrote:
> >
> > > Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 06:01:47 UTC+1:
> > > > On Wednesday, January 5, 2022 at 11:44:40 PM UTC-5, Mostowski Collapse wrote:
> > > >
> > > > > Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 04:07:50 UTC+1:
> > > > > > On Wednesday, January 5, 2022 at 7:10:57 PM UTC-5, Mostowski Collapse wrote:
> > > > > >
> > > > > > > Can we also prove?
> > > > > > >
> > > > > > > EXISTUNIQUE(f): " f : {0} -> {0}" ?
> > > > > > >
> > > > > >
> > > > > > Easy. In 34 lines. Assuming ALL(a):[a in x <=> a=0], we obtain...
> > > > > >
> > > > > > ALL(f):ALL(g):[ALL(a):[a in x => f(a) in x]
> > > > > > & ALL(a):[a in x => g(a) in x]
> > > > > > => ALL(a):[a in x => f(a)=g(a)]]
> > > > > >
> > > > > > Same input, same output. Deal with it, Jan Burse.
> > > > > The text book proof would end with:
> > > > >
> > > > > => f=g
> > > > >
> >
> > > > Wrong again, Jan Burse. With functions, it's all about inputs and outputs. Nothing else. Functions f and g are identical if and only if given the same inputs, you will obtain the same outputs.
> >
> > > > > Deal with it, Dan Christensen. You nowhere provide text book math..
> >
> > > > That's hilarious coming from someone who believes we can make logical inferences about f(x) for x not in the domain of definition of the function f. Get a life!
> > > In standard text book mathematics you can prove:
> > >
> > > f e B^A , x not in A => ~EXIST(y):(x,y) in f
> > > https://math.stackexchange.com/questions/3480579/meaning-of-ab-where-a-and-b-are-sets
> > >
> > Nothing there to support your claim that we can make logical inferences about a function outside of it domain of definition.
> > > But the Function Axiom of DC Proof doesn't allow
> > > it, this here is not anymore derivable:
> > >
> > > f e B^A , x not in A =/=> ~EXIST(y):fun(x)=y
> > That is a good thing, Jan Burse. Any definition of a function that allows logical inferences to be made about a function outside of its domain of definition is nonsense--it's Burse's Paradox.
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 6, 2022 at 12:51:43 AM UTC-5, Mostowski Collapse wrote:

> > > > Wrong again, Jan Burse. With functions, it's all about inputs and outputs. Nothing else. Functions f and g are identical if and only if given the same inputs, you will obtain the same outputs.
> >
> > > > > Deal with it, Dan Christensen. You nowhere provide text book math.
> >
> > > > That's hilarious coming from someone who believes we can make logical inferences about f(x) for x not in the domain of definition of the function f. Get a life!
> > > In standard text book mathematics you can prove:
> > >
> > > f e B^A , x not in A => ~EXIST(y):(x,y) in f
> > > https://math.stackexchange.com/questions/3480579/meaning-of-ab-where-a-and-b-are-sets
> > >

> > Nothing there to support your claim that we can make logical inferences about a function outside of it domain of definition.

> > > But the Function Axiom of DC Proof doesn't allow
> > > it, this here is not anymore derivable:
> > >
> > > f e B^A , x not in A =/=> ~EXIST(y):fun(x)=y

> > That is a good thing, Jan Burse. Any definition of a function that allows logical inferences to be made about a function outside of its domain of definition is nonsense--it's Burse's Paradox.

> Its not a Burse's Paradox.

You are famous, Jan Burse! You have been immortalized as the discoverer and chief proponent of this wonky paradox.

> Its simply an egregious error.
> The mistake is on your side, namely writing, where fun
> is what pops out of your DC Proof Function Axiom:
>
> fun : A -> B /* egregious error */
>

It's a formalization of ordinary textbook math. It works. And it avoids Burse's Paradox.

> Thats not the standard text book meaning of function spaces
> A -> B. We require { f | f : A -> B } subset P(A x B).

No, we require that f(x) be undefined or meaningless for x not the domain of definition of function f. It's just ordinary textbook math. Deal with it, Jan Burse.

Dan

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

On Thursday, January 6, 2022 at 12:57:58 AM UTC-5, Mostowski Collapse wrote:

> > Nothing there to support your claim that we can make
> logical inferences about a function outside of it domain of definition.
> Well you defined it yourself, what F = B^A is:
> Dan Christensen schrieb am Mittwoch, 5. Januar 2022 um 22:23:41 UTC+1:
> > 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}.

Again, to construct a function space, this subset of P(AxB) would have to be converted to a set of functions: {f | ALL(x):[x =in A => f(x) in B]} using the Function Axiom.

Dan

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

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

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

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

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

They both define the function space A -> B aka B^A. They are used:

F1:

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

F2:

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

Whats wrong with you? Its easy to prove:

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

Dan Christensen schrieb am Donnerstag, 6. Januar 2022 um 07:23:52 UTC+1:
> On Thursday, January 6, 2022 at 12:57:58 AM UTC-5, Mostowski Collapse wrote:
>
> > > Nothing there to support your claim that we can make
> > logical inferences about a function outside of it domain of definition.
> > Well you defined it yourself, what F = B^A is:
> > Dan Christensen schrieb am Mittwoch, 5. Januar 2022 um 22:23:41 UTC+1:
> > > 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}.
> Again, to construct a function space, this subset of P(AxB) would have to be converted to a set of functions: {f | ALL(x):[x =in A => f(x) in B]} using the Function Axiom.
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Thursday, January 6, 2022 at 1:23:52 AM UTC-5, Dan Christensen wrote:
> On Thursday, January 6, 2022 at 12:57:58 AM UTC-5, Mostowski Collapse wrote:
>
> > > Nothing there to support your claim that we can make
> > logical inferences about a function outside of it domain of definition.
> > Well you defined it yourself, what F = B^A is:
> > Dan Christensen schrieb am Mittwoch, 5. Januar 2022 um 22:23:41 UTC+1:
> > > 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}.

> Again, to construct a function space, this subset of P(AxB) would have to be converted to a set of functions: {f | ALL(x):[x =in A => f(x) in B]} using the Function Axiom.

Using DC Proof, given sets X and Y, I was able to construct a set F consisting of those function-like subsets of X*Y using axioms for Cartesian products, power sets and subsets. For each element f of F, I was able to prove the existence of a unique function g: X --> Y such g(a)=b <=> (a, b) in f.

Dan

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

Warning: I am looking at the direction -->, the old topic, and
not at the direction <--, the new topic.

Looks like DC proof is extremly flat chested. There is not
only no power set axiom. Also the function axiom doesn't
have a lot of steam. The function axiom defines a map

from function space to Dan-O-Matik nonsense:

A -> B --> {g | ALL(x):[x =in A => g(x) in B]}

Lets denote what the function axiom gives for f : A -> B
by def(_). Dan-O-Matik can only prove, which IS NOT
INJECTIVITY of the function axiom:

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

But its an easy folklore exercise to obtain a more
stronger result by a better function axiom, namely.
which is INJECTIVITY of the better function axiom:

(**)
def'(g) & def'(g') => ALL(a):[g'(a)=g(a)]

How is this done? Well its relatively easy to use
von Neumann-Gödel-Bernays set theory (NBG) to have
this classes g, where ' is the Peano apostroph:

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

The class g is a function on the domain of discourse,
so that we can use g(x)=y instead of (x,y) e g unrestrictedly.
One can then prove (**) as required.

See also:

The Peano apostroph is also defined here. Kurt Gödel
does it Chapter II, page 16 here, after 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

See also:

In the foundations of mathematics, von Neumann–Bernays–Gödel
set theory (NBG) is an axiomatic set theory that is a conservative
extension of Zermelo–Fraenkel-Choice set theory (ZFC).
https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory

Injectivity can now be examined, since only now
by ALL(a):[g'(a)=g(a)] we have a mapping from
function space to Dan-O-Matik nonsense. Lets

write (_)* for this mapping via Peano apostroph:

A -> B --> {g | ALL(x):[x =in A => g(x) in B]}

Its now easy to show f1,f2 : A -> B and f1=\=f2
that then f1*=\=f2*. So the direction --> is indeed
a map and an injectivity.

But there are also other injective --> mappings possible.
What about the other directio <-- ? Can a reverse mapping
be an injection?

Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 18:12:40 UTC+1:
> Warning: I am looking at the direction -->, the old topic, and
> not at the direction <--, the new topic.
>
> Looks like DC proof is extremly flat chested. There is not
> only no power set axiom. Also the function axiom doesn't
> have a lot of steam. The function axiom defines a map
>
> from function space to Dan-O-Matik nonsense:
>
> A -> B --> {g | ALL(x):[x =in A => g(x) in B]}
>
> Lets denote what the function axiom gives for f : A -> B
> by def(_). Dan-O-Matik can only prove, which IS NOT
> INJECTIVITY of the function axiom:
>
> (*)
> def(g) & def(g') => ALL(a):[a in x => g'(a)=g(a)]
>
> But its an easy folklore exercise to obtain a more
> stronger result by a better function axiom, namely.
> which is INJECTIVITY of the better function axiom:
>
> (**)
> def'(g) & def'(g') => ALL(a):[g'(a)=g(a)]
>
> How is this done? Well its relatively easy to use
> von Neumann-Gödel-Bernays set theory (NBG) to have
> this classes g, where ' is the Peano apostroph:
>
> def'(g) :<=> ∀x∀y( (x,y) e g <=> f'x = y )
>
> The class g is a function on the domain of discourse,
> so that we can use g(x)=y instead of (x,y) e g unrestrictedly.
> One can then prove (**) as required.
>
> See also:
>
> The Peano apostroph is also defined here. Kurt Gödel
> does it Chapter II, page 16 here, after 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
>
> See also:
>
> In the foundations of mathematics, von Neumann–Bernays–Gödel
> set theory (NBG) is an axiomatic set theory that is a conservative
> extension of Zermelo–Fraenkel-Choice set theory (ZFC).
> https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory

Actually this is a nice logic exercise, show that
there is no bijection? At least in the finite case,
by invoking anti-monotonity:

Does this bijection hold?
A -> B <---> { f | ALL(x):[x e A => f(x) e B] }

In the finite case we would have a bijection
with a finite ordinal number, or in other words we
would have that same finite cardinality:

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

Now by anti-monotonity for A ⊆ A' we would
have { f | ALL(x):[x e A' => f(x) e B] } ⊆ { f | ALL(x):[x e A
=> f(x) e B] }. And therefore:

|{ f | ALL(x):[x e A' => f(x) e B] }| = n' & n' =< n.

On the other hand the function space cardinality
is like this, |A -> B| = |B|^|A|. Lets say |A|=k and
|A'|=k' and |B|=j, k=\=k'. So that

we would have:

k < k' => j^k >= j^k'

Quite some nonsense for natural numbers.

Its very unclear why DC Proof even needs a Function Axiom?
Litterally translating Terrence Tao, he says, establishing
a link from a graph to a FOL function symbol:

/* Terrence Tao */
∀x∀y(Xx → (Pxy ↔ f(x)=y))

Its easy to prove then, no axiom needed, FOL validity:

/* Dan-O-Matik Nonsense */
∀x∀y(Ax → (Pxy ↔ f(x)=y)), /* Terrence Tao */
∀x∀y((Ax ∧ Pxy) → By) /* Function Axiom Domain & Codomain */
entails ∀x(Ax → Bf(x)). /* Function Axiom Dan-O-Matik Nonsense */
https://www.umsu.de/trees/#~6x~6y%28Ax~5%28Pxy~4f%28x%29=y%29%29,~6x~6y%28Ax~1Pxy~5By%29|=~6x%28Ax~5Bf%28x%29%29

We can also prove that most of the LHS of the Function Axiom
is unnecessary, again no axiom needed, FOL validity:

/* Seriality is Redundant */
∀x∀y(Ax → (Pxy ↔ f(x)=y)), /* Terrence Tao */
∀x∀y((Ax ∧ Pxy) → By) /* Function Axiom Domain & Codomain */
entails ∀x(Ax → ∃y(By ∧ Pxy)). /* Function Axiom Seriality */
https://www.umsu.de/trees/#~6x~6y%28Ax~5%28Pxy~4f%28x%29=y%29%29,~6x~6y%28Ax~1Pxy~5By%29|=~6x%28Ax~5~7y%28By~1Pxy%29%29

/* Functionality is Redundant */
∀x∀y(Ax → (Pxy ↔ f(x)=y)), /* Terrence Tao */
∀x∀y((Ax ∧ Pxy) → By) /* Function Axiom Domain & Codomain */
entails ∀x∀y∀z((Ax ∧ (By ∧ (Pxy ∧ (Bz ∧ Pxz)))) → y=z). /* Function Axiom Seriality */
https://www.umsu.de/trees/#~6x~6y%28Ax~5%28Pxy~4f%28x%29=y%29%29,~6x~6y%28Ax~1Pxy~5By%29|=~6x~6y~6z%28Ax~1By~1Pxy~1Bz~1Pxz~5y=z%29