On Saturday, April 30, 2022 at 11:18:14 AM UTC-4, Mostowski Collapse wrote:
> Why, if gra is set of ordered pairs, then there is also a set
> of elements of the second ordinate?

I think you want:

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

Dan

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

Nope, rng(f) is intrinsic, not extrinsic. Similar
for dom(f), it is intrinsic for set-like function,
but dom(f) is less seen in the theorem.

So its only this:

ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[fritz(gra,a) e y]]

And a definition, i.e. an axiom:

ALL(gra):ALL(a):ALL(b):[fritz(gra,a)=b <=> ...]

The particular proof depends on how you define fritz. But
firtz should satisfy Russells Definite Descriptions:

ALL(gra):ALL(a):[[EXISTUNIQUE(b):(a,b) e gra] =>
ALL(b):[fritz(gra,a) = b <=> (a,b) e gra]]]

Dan Christensen schrieb am Samstag, 30. April 2022 um 18:09:57 UTC+2:
> On Saturday, April 30, 2022 at 11:18:14 AM UTC-4, Mostowski Collapse
wrote:
> > Why, if gra is set of ordered pairs, then there is also a set
> > of elements of the second ordinate?
> I think you want:
>
> ALL(x):ALL(y):ALL(g):[Set(x) & Set(y) & Set'(g)
> & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
> => EXIST(z):[Set(z) & ALL(b):[b in z <=> b in y & EXIST(a):[a in x &
(a,b) in g]]]]
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, April 30, 2022 at 12:29:40 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Samstag, 30. April 2022 um 18:09:57 UTC+2:
> > On Saturday, April 30, 2022 at 11:18:14 AM UTC-4, Mostowski Collapse
> wrote:
> > > Why, if gra is set of ordered pairs, then there is also a set
> > > of elements of the second ordinate?
> > I think you want:
> >
> > ALL(x):ALL(y):ALL(g):[Set(x) & Set(y) & Set'(g)
> > & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
> > => EXIST(z):[Set(z) & ALL(b):[b in z <=> b in y & EXIST(a):[a in x &
> (a,b) in g]]]]

> Nope, rng(f) is intrinsic, not extrinsic. Similar
> for dom(f), it is intrinsic for set-like function,
> but dom(f) is less seen in the theorem.
>
> So its only this:
>
> ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[fritz(gra,a) e y]]
>
> And a definition, i.e. an axiom:
>
> ALL(gra):ALL(a):ALL(b):[fritz(gra,a)=b <=> ...]
>

Ummm... Let's just say, it's not something I would want to build into DC Proof. You can, of course, insert your own axioms at the beginning of your proofs and play around with them. I routinely insert Peano's Axioms at the beginning of my own proofs. Using them, I have proven the existence of the addition, multiplication, exponentiation and factorial functions on N. It works.

Dan

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

You should be able to prove:

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

Don't you? All set theories can do that:

When pairs are Kuratowski Pairs, you can use Fritz UU,
you only need Z, Zermelo Set Theory.

When pairs are more abstractly, you only need ZF, Zermelo
Fraenkel Set Theory.

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 18:29:40 UTC+2:
> Nope, rng(f) is intrinsic, not extrinsic. Similar
> for dom(f), it is intrinsic for set-like function,
> but dom(f) is less seen in the theorem.
>
> So its only this:
>
> ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[fritz(gra,a) e y]]
>
> And a definition, i.e. an axiom:
>
> ALL(gra):ALL(a):ALL(b):[fritz(gra,a)=b <=> ...]
>
> The particular proof depends on how you define fritz. But
> firtz should satisfy Russells Definite Descriptions:
>
> ALL(gra):ALL(a):[[EXISTUNIQUE(b):(a,b) e gra] =>
> ALL(b):[fritz(gra,a) = b <=> (a,b) e gra]]]
> Dan Christensen schrieb am Samstag, 30. April 2022 um 18:09:57 UTC+2:
> > On Saturday, April 30, 2022 at 11:18:14 AM UTC-4, Mostowski Collapse
> wrote:
> > > Why, if gra is set of ordered pairs, then there is also a set
> > > of elements of the second ordinate?
> > I think you want:
> >
> > ALL(x):ALL(y):ALL(g):[Set(x) & Set(y) & Set'(g)
> > & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
> > => EXIST(z):[Set(z) & ALL(b):[b in z <=> b in y & EXIST(a):[a in x &
> (a,b) in g]]]]
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, April 30, 2022 at 1:22:08 PM UTC-4, Mostowski Collapse wrote:
> You should be able to prove:
>
> ALL(g):[Set'(g) => EXIST(x):[Set(x) & EXIST(y):[Set(y) & ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
>

You only need it because you start constructing functions without even knowing to start what the domain and codomain are. Not very smart.

Before I construct a function I must first establish the existence the set(s) intended to be its domain and codomain, even if only to name them. Common usage. If you are going construct an add function, for example, you must first know on what set. So there may be no need of this axiom/theorem of yours.

Dan

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

Or do you claim your g's have some "dark elements",
i.e. ordered pairs, that prevent that collectively
the ordinates of the ordered pairs fit into sets y and x?
Or maybe the g's are so big, that the ordinates do

not fit into sets y and x. Do the g's then still deserve
the name of being sets of ordered pairs?
This is very puzzling, whats missing in DC Proof?
So far the fog has only increased, and

we still couldn't figure out function spaces...

P.S.: Although I and now more convinced there is
something wrong with the baguettes and the french,
like in this fallacy:

The french eat baguette
Therefore
Baquette eaters are french

You probably only say when something goes
into Set', but you have nowhere an axiom in DC
Proof that says what comes out of Set'

Right?

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 19:22:08 UTC+2:
> You should be able to prove:
>
> ALL(g):[Set'(g) => EXIST(x):[Set(x) & EXIST(y):[Set(y) & ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
>
> Don't you? All set theories can do that:
>
> When pairs are Kuratowski Pairs, you can use Fritz UU,
> you only need Z, Zermelo Set Theory.
>
> When pairs are more abstractly, you only need ZF, Zermelo
> Fraenkel Set Theory.
> Mostowski Collapse schrieb am Samstag, 30. April 2022 um 18:29:40 UTC+2:
> > Nope, rng(f) is intrinsic, not extrinsic. Similar
> > for dom(f), it is intrinsic for set-like function,
> > but dom(f) is less seen in the theorem.
> >
> > So its only this:
> >
> > ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[fritz(gra,a) e y]]
> >
> > And a definition, i.e. an axiom:
> >
> > ALL(gra):ALL(a):ALL(b):[fritz(gra,a)=b <=> ...]
> >
> > The particular proof depends on how you define fritz. But
> > firtz should satisfy Russells Definite Descriptions:
> >
> > ALL(gra):ALL(a):[[EXISTUNIQUE(b):(a,b) e gra] =>
> > ALL(b):[fritz(gra,a) = b <=> (a,b) e gra]]]
> > Dan Christensen schrieb am Samstag, 30. April 2022 um 18:09:57 UTC+2:
> > > On Saturday, April 30, 2022 at 11:18:14 AM UTC-4, Mostowski Collapse
> > wrote:
> > > > Why, if gra is set of ordered pairs, then there is also a set
> > > > of elements of the second ordinate?
> > > I think you want:
> > >
> > > ALL(x):ALL(y):ALL(g):[Set(x) & Set(y) & Set'(g)
> > > & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
> > > => EXIST(z):[Set(z) & ALL(b):[b in z <=> b in y & EXIST(a):[a in x &
> > (a,b) in g]]]]
> > > Dan
> > >
> > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > Visit my Math Blog at http://www.dcproof.wordpress.com

I guess the resolution for DC Proof is always:

The french eat baguette
Therefore
Baquette eaters are french or dark elements

Which is somehow true if you define dark elements
as ~french. I guess this is a tautology:

ALL(a):[F(a) => B(a)] => ALL(a):[B(a) => F(a) v ~F(a)]

Well you even don't need that french are
baguette eaters. You already have:

ALL(a):[B(a) => F(a) v ~F(a)]

How convenient...

LoL

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 20:36:46 UTC+2:
> Or do you claim your g's have some "dark elements",
> i.e. ordered pairs, that prevent that collectively
> the ordinates of the ordered pairs fit into sets y and x?
> Or maybe the g's are so big, that the ordinates do
>
> not fit into sets y and x. Do the g's then still deserve
> the name of being sets of ordered pairs?
> This is very puzzling, whats missing in DC Proof?
> So far the fog has only increased, and
>
> we still couldn't figure out function spaces...
>
> P.S.: Although I and now more convinced there is
> something wrong with the baguettes and the french,
> like in this fallacy:
> The french eat baguette
> Therefore
> Baquette eaters are french
> You probably only say when something goes
> into Set', but you have nowhere an axiom in DC
> Proof that says what comes out of Set'
>
> Right?
> Mostowski Collapse schrieb am Samstag, 30. April 2022 um 19:22:08 UTC+2:
> > You should be able to prove:
> >
> > ALL(g):[Set'(g) => EXIST(x):[Set(x) & EXIST(y):[Set(y) & ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
> >
> > Don't you? All set theories can do that:
> >
> > When pairs are Kuratowski Pairs, you can use Fritz UU,
> > you only need Z, Zermelo Set Theory.
> >
> > When pairs are more abstractly, you only need ZF, Zermelo
> > Fraenkel Set Theory.
> > Mostowski Collapse schrieb am Samstag, 30. April 2022 um 18:29:40 UTC+2:
> > > Nope, rng(f) is intrinsic, not extrinsic. Similar
> > > for dom(f), it is intrinsic for set-like function,
> > > but dom(f) is less seen in the theorem.
> > >
> > > So its only this:
> > >
> > > ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[fritz(gra,a) e y]]
> > >
> > > And a definition, i.e. an axiom:
> > >
> > > ALL(gra):ALL(a):ALL(b):[fritz(gra,a)=b <=> ...]
> > >
> > > The particular proof depends on how you define fritz. But
> > > firtz should satisfy Russells Definite Descriptions:
> > >
> > > ALL(gra):ALL(a):[[EXISTUNIQUE(b):(a,b) e gra] =>
> > > ALL(b):[fritz(gra,a) = b <=> (a,b) e gra]]]
> > > Dan Christensen schrieb am Samstag, 30. April 2022 um 18:09:57 UTC+2:
> > > > On Saturday, April 30, 2022 at 11:18:14 AM UTC-4, Mostowski Collapse
> > > wrote:
> > > > > Why, if gra is set of ordered pairs, then there is also a set
> > > > > of elements of the second ordinate?
> > > > I think you want:
> > > >
> > > > ALL(x):ALL(y):ALL(g):[Set(x) & Set(y) & Set'(g)
> > > > & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
> > > > => EXIST(z):[Set(z) & ALL(b):[b in z <=> b in y & EXIST(a):[a in x &
> > > (a,b) in g]]]]
> > > > Dan
> > > >
> > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, April 30, 2022 at 2:36:46 PM UTC-4, Mostowski Collapse wrote:
> Or do you claim your g's have some "dark elements",
> i.e. ordered pairs, that prevent that collectively
> the ordinates of the ordered pairs fit into sets y and x?

It has nothing to do with anything fitting. It's just a wonky result made necessary by your wonky approach to functionality. Basic rule: The first step in constructing a function is to establish by axiom, premise or inference set(s) for the intended domain and codomain. You have it backwards.

Dan

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

So of what use is Set'(_) if it has dark elements.
Its totally useless, you cannot bootstrap function
spaces from it, as one would do in a math book.

At least the experienced struggle so far tells me:
- We still don't have f : X->Y, function space
- We still don't have f=g function equality
-

My impression, its only a little word, instead of "if"
some "iff" at the right place, eh voila, we are doing
math, and not poop-ology.

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 20:42:06 UTC+2:
> I guess the resolution for DC Proof is always:
> The french eat baguette
> Therefore
> Baquette eaters are french or dark elements
>
> Which is somehow true if you define dark elements
> as ~french. I guess this is a tautology:
>
> ALL(a):[F(a) => B(a)] => ALL(a):[B(a) => F(a) v ~F(a)]
>
> Well you even don't need that french are
> baguette eaters. You already have:
>
> ALL(a):[B(a) => F(a) v ~F(a)]
>
> How convenient...
>
> LoL
> Mostowski Collapse schrieb am Samstag, 30. April 2022 um 20:36:46 UTC+2:
> > Or do you claim your g's have some "dark elements",
> > i.e. ordered pairs, that prevent that collectively
> > the ordinates of the ordered pairs fit into sets y and x?
> > Or maybe the g's are so big, that the ordinates do
> >
> > not fit into sets y and x. Do the g's then still deserve
> > the name of being sets of ordered pairs?
> > This is very puzzling, whats missing in DC Proof?
> > So far the fog has only increased, and
> >
> > we still couldn't figure out function spaces...
> >
> > P.S.: Although I and now more convinced there is
> > something wrong with the baguettes and the french,
> > like in this fallacy:
> > The french eat baguette
> > Therefore
> > Baquette eaters are french
> > You probably only say when something goes
> > into Set', but you have nowhere an axiom in DC
> > Proof that says what comes out of Set'
> >
> > Right?
> > Mostowski Collapse schrieb am Samstag, 30. April 2022 um 19:22:08 UTC+2:
> > > You should be able to prove:
> > >
> > > ALL(g):[Set'(g) => EXIST(x):[Set(x) & EXIST(y):[Set(y) & ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
> > >
> > > Don't you? All set theories can do that:
> > >
> > > When pairs are Kuratowski Pairs, you can use Fritz UU,
> > > you only need Z, Zermelo Set Theory.
> > >
> > > When pairs are more abstractly, you only need ZF, Zermelo
> > > Fraenkel Set Theory.
> > > Mostowski Collapse schrieb am Samstag, 30. April 2022 um 18:29:40 UTC+2:
> > > > Nope, rng(f) is intrinsic, not extrinsic. Similar
> > > > for dom(f), it is intrinsic for set-like function,
> > > > but dom(f) is less seen in the theorem.
> > > >
> > > > So its only this:
> > > >
> > > > ALL(gra):[Set'(gra) => EXIST(y):[Set(y) & ALL(a):[fritz(gra,a) e y]]
> > > >
> > > > And a definition, i.e. an axiom:
> > > >
> > > > ALL(gra):ALL(a):ALL(b):[fritz(gra,a)=b <=> ...]
> > > >
> > > > The particular proof depends on how you define fritz. But
> > > > firtz should satisfy Russells Definite Descriptions:
> > > >
> > > > ALL(gra):ALL(a):[[EXISTUNIQUE(b):(a,b) e gra] =>
> > > > ALL(b):[fritz(gra,a) = b <=> (a,b) e gra]]]
> > > > Dan Christensen schrieb am Samstag, 30. April 2022 um 18:09:57 UTC+2:
> > > > > On Saturday, April 30, 2022 at 11:18:14 AM UTC-4, Mostowski Collapse
> > > > wrote:
> > > > > > Why, if gra is set of ordered pairs, then there is also a set
> > > > > > of elements of the second ordinate?
> > > > > I think you want:
> > > > >
> > > > > ALL(x):ALL(y):ALL(g):[Set(x) & Set(y) & Set'(g)
> > > > > & ALL(a):ALL(b):[(a,b) in g => a in x & b in y]
> > > > > => EXIST(z):[Set(z) & ALL(b):[b in z <=> b in y & EXIST(a):[a in x &
> > > > (a,b) in g]]]]
> > > > > Dan
> > > > >
> > > > > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > > > > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, April 30, 2022 at 2:49:04 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> So of what use is Set'(_) if it has dark elements.

That is your area of expertise, Jan Burse. I can only guess what you might use them for.

Poor Jan Burse here believes he can make logical inferences about functions outside of their domains of definition--his "dark elements." Very sad.

Dan

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

You cannot prove:

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

So I guess there are g's that satisfy Set'(g) and
where its not clear, i.e. in the dark, whether
they have a set of first ordinates and a set

of second ordinate. Right? Why do you call
it then Set', thats a category mistake.
By a collection of Cartesian products we do

not understand a set with dark elements, instead of calling it:

Set'(g)

You should call it:

Poop(g)

You are using the wrong names.

Dan Christensen schrieb:
> On Saturday, April 30, 2022 at 2:49:04 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
>> So of what use is Set'(_) if it has dark elements.
>
> That is your area of expertise, Jan Burse. I can only guess what you might use them for.
>
> Poor Jan Burse here believes he can make logical inferences about functions outside of their domains of definition--his "dark elements." Very sad.
>
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com
>

Maybe Poop(_) is to harsh, something like Half-Set'(_)
would also do. But it is not a well defined concept.
Its like you would use Half-Comprehension, the usual

comprehension says (your subset axiom):

ALL(x):EXIST(y):ALL(a):[a e y <=> a e x & P(a)]
And you can prove:
/* Provable */
ALL(x):EXISTUNIQUE(y):ALL(a):[a e y <=> a e x & P(a)]

Now imagine you would only have a half-subset axiom:

ALL(x):EXIST(y):ALL(a):[a e y <= a e x & P(a)]
You cannot anymore prove:
/* Not Provable */
ALL(x):EXISTUNIQUE(y):ALL(a):[a e y <= a e x & P(a)]

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 21:03:51 UTC+2:
> You cannot prove:
> ALL(g):[Set'(g) =>
> EXIST(x):[Set(x) & EXIST(y):[Set(y) &
> ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
> So I guess there are g's that satisfy Set'(g) and
> where its not clear, i.e. in the dark, whether
> they have a set of first ordinates and a set
>
> of second ordinate. Right? Why do you call
> it then Set', thats a category mistake.
> By a collection of Cartesian products we do
>
> not understand a set with dark elements, instead of calling it:
>
> Set'(g)
>
> You should call it:
>
> Poop(g)
>
> You are using the wrong names.
>
> Dan Christensen schrieb:
> > On Saturday, April 30, 2022 at 2:49:04 PM UTC-4, Mostowski Collapse (aka Jan Burse) wrote:
> >> So of what use is Set'(_) if it has dark elements.
> >
> > That is your area of expertise, Jan Burse. I can only guess what you might use them for.
> >
> > Poor Jan Burse here believes he can make logical inferences about functions outside of their domains of definition--his "dark elements." Very sad.
> >
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com
> >

On Saturday, April 30, 2022 at 3:03:51 PM UTC-4, Mostowski Collapse wrote:
> You cannot prove:
> ALL(g):[Set'(g) =>
> EXIST(x):[Set(x) & EXIST(y):[Set(y) &
> ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
> So I guess...

There is no guess work if get the order right: First get your domain and codomain set. Then your graph set. Only then can you infer the existence of the required function operator.

For practice, try to use your wonky backwards method to construct the add function. I can't tell you the domain. Just use you dom( ) function to figure it out from your set of ordered pairs. ;^)

Dan

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

Now you make a hilarious claim about a certain order of proofs.
You repeatedly use words you don't know what they mean.
You imply that your order is justified:

- by the desire of some "constructivity"?
- by the method of instantiating extrinsic properties
- by the method of non-wellformed concepts
-

You forget in your delirium of nonsense that:

- math is not only about constructive stuff
- to prove constructive stuff, its not related to proof order
- instantiating extrinsics lead the ad-hoc axiom disaster,
inconsistencies f=g & ~f=g
- non-wellformed concepts leads to gaps in common math,
you cannot prove existence of a range

Dan Christensen schrieb am Samstag, 30. April 2022 um 21:26:34 UTC+2:
> On Saturday, April 30, 2022 at 3:03:51 PM UTC-4, Mostowski Collapse wrote:
> > You cannot prove:
> > ALL(g):[Set'(g) =>
> > EXIST(x):[Set(x) & EXIST(y):[Set(y) &
> > ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
> > So I guess...
>
> There is no guess work if get the order right: First get your domain and codomain set. Then your graph set. Only then can you infer the existence of the required function operator.
>
> For practice, try to use your wonky backwards method to construct the add function. I can't tell you the domain. Just use you dom( ) function to figure it out from your set of ordered pairs. ;^)
> Dan
>
> Download my DC Proof 2.0 freeware at http://www.dcproof.com
> Visit my Math Blog at http://www.dcproof.wordpress.com

So how to spot a crank? Well if he uses the word "construct"
or "constructive" and refers to proof order.

Usually you find things like yes/no excluded middle or
yes/no uniformity or yes/no coutable choice,
https://ncatlab.org/nlab/show/intermediate%20value%20theorem

as the switch from non-constructive to constructive. I
have never heard that order makes a dent.

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 21:57:09 UTC+2:
> Now you make a hilarious claim about a certain order of proofs.
> You repeatedly use words you don't know what they mean.
> You imply that your order is justified:
>
> - by the desire of some "constructivity"?
> - by the method of instantiating extrinsic properties
> - by the method of non-wellformed concepts
> -
>
> You forget in your delirium of nonsense that:
>
> - math is not only about constructive stuff
> - to prove constructive stuff, its not related to proof order
> - instantiating extrinsics lead the ad-hoc axiom disaster,
> inconsistencies f=g & ~f=g
> - non-wellformed concepts leads to gaps in common math,
> you cannot prove existence of a range
> Dan Christensen schrieb am Samstag, 30. April 2022 um 21:26:34 UTC+2:
> > On Saturday, April 30, 2022 at 3:03:51 PM UTC-4, Mostowski Collapse wrote:
> > > You cannot prove:
> > > ALL(g):[Set'(g) =>
> > > EXIST(x):[Set(x) & EXIST(y):[Set(y) &
> > > ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
> > > So I guess...
> >
> > There is no guess work if get the order right: First get your domain and codomain set. Then your graph set. Only then can you infer the existence of the required function operator.
> >
> > For practice, try to use your wonky backwards method to construct the add function. I can't tell you the domain. Just use you dom( ) function to figure it out from your set of ordered pairs. ;^)
> > Dan
> >
> > Download my DC Proof 2.0 freeware at http://www.dcproof.com
> > Visit my Math Blog at http://www.dcproof.wordpress.com

On Saturday, April 30, 2022 at 3:57:09 PM UTC-4, Mostowski Collapse wrote:

> Dan Christensen schrieb am Samstag, 30. April 2022 um 21:26:34 UTC+2:
> > On Saturday, April 30, 2022 at 3:03:51 PM UTC-4, Mostowski Collapse wrote:
> > > You cannot prove:
> > > ALL(g):[Set'(g) =>
> > > EXIST(x):[Set(x) & EXIST(y):[Set(y) &
> > > ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
> > > So I guess...
> >
> > There is no guess work if get the order right: First get your domain and codomain set. Then your graph set. Only then can you infer the existence of the required function operator.
> >
> > For practice, try to use your wonky backwards method to construct the add function. I can't tell you the domain. Just use you dom( ) function to figure it out from your set of ordered pairs. ;^)

> Now you make a hilarious claim about a certain order of proofs.
> You repeatedly use words you don't know what they mean.
> You imply that your order is justified:
>
> - by the desire of some "constructivity"?
> - by the method of instantiating extrinsic properties
> - by the method of non-wellformed concepts
> -
>

So, you couldn't even get started on your homework assignment with your backwards approach. It's one thing to concoct "systems" for your philosophy seminars, and quite another to get actual results on the ground. I hope you have learned your lesson, 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

Its not **my** approach. All of logic is order independent.
You can most of the time approach a problem from different
sides. Thats utter nonsense to turn a proof assistant

into a template wizard, and then claim we need to this
this way and we need to do this this way. Because logic
doesn't care how the end user uses a tool. The logical

consequences of a deductive systems are defined as
everything that can be proved.

Cn(X) = { Y | X |- Y }

And a deductive system is consistent, if you have
no A with A e Cn({}) and ~A e Cn({}). Your ad-hoc axiom
of function equality showed that your idea of

a proof assistent as a template wizard, and your idea
of a new concept such as function equality, just some
shitty new template doesn't work.

Its the wrong approach to do proof assistants and
the wrong approach to do mathematics.

Dan Christensen schrieb am Samstag, 30. April 2022 um 22:26:48 UTC+2:
> So, you couldn't even get started on your homework assignment with your backwards approach. It's one thing to concoct "systems" for your philosophy seminars, and quite another to get actual results on the ground. I hope you have learned your lesson, 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 Saturday, April 30, 2022 at 4:26:48 PM UTC-4, Dan Christensen wrote:
> On Saturday, April 30, 2022 at 3:57:09 PM UTC-4, Mostowski Collapse wrote:
>
> > Dan Christensen schrieb am Samstag, 30. April 2022 um 21:26:34 UTC+2:
> > > On Saturday, April 30, 2022 at 3:03:51 PM UTC-4, Mostowski Collapse wrote:
> > > > You cannot prove:
> > > > ALL(g):[Set'(g) =>
> > > > EXIST(x):[Set(x) & EXIST(y):[Set(y) &
> > > > ALL(a):ALL(b):[(a,b) in g => a in x & b in y] ]]]
> > > > So I guess...
> > >
> > > There is no guess work if get the order right: First get your domain and codomain set. Then your graph set. Only then can you infer the existence of the required function operator.
> > >
> > > For practice, try to use your wonky backwards method to construct the add function. I can't tell you the domain. Just use you dom( ) function to figure it out from your set of ordered pairs. ;^)
> > Now you make a hilarious claim about a certain order of proofs.
> > You repeatedly use words you don't know what they mean.
> > You imply that your order is justified:
> >
> > - by the desire of some "constructivity"?
> > - by the method of instantiating extrinsic properties
> > - by the method of non-wellformed concepts
> > -
> >
> So, you couldn't even get started on your homework assignment with your backwards approach. It's one thing to concoct "systems" for your philosophy seminars, and quite another to get actual results on the ground. I hope you have learned your lesson, Jan Burse.

This is how it is done, Jan Burse: https://dcproof.com/ConstructAddFunction..htm

Note how I STARTED with the domain NxN (n2) and codomain N (n). It would have been impossible otherwise. Then I constructed the graph set (add) using the domain and codomain sets Finally, I introduced the function operator (fadd) defining it terms of the domain, codomain and graph sets.

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

For exampe the foundational approach of ZFC is totally
different. You are not allowed to introduce a single new
axiom aka template. You are only allowed to

introduce so called definitions. And by some reasoning,
see Shoenfinkel for example, you can show that if ZFC is
consistent, your definitions are also consistent.

When you write, this is practically a no-go:

Dan Christensen schrieb am Samstag, 30. April 2022 um 19:19:22 UTC+2:
> You can, of course, insert your own axioms at the beginning
of your proofs and play around with them.
https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/UJ_-2ZgLAwAJ

Especially for constructive mathematics there are
now frameworks, of course different from ZFC/Shoenfield,
that do not allow to add any axiom.

Just check out what Coq, Isabelle/HOL, etc.. provide.

LoL

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 22:35:38 UTC+2:
> Its not **my** approach. All of logic is order independent.
> You can most of the time approach a problem from different
> sides. Thats utter nonsense to turn a proof assistant
>
> into a template wizard, and then claim we need to this
> this way and we need to do this this way. Because logic
> doesn't care how the end user uses a tool. The logical
>
> consequences of a deductive systems are defined as
> everything that can be proved.
>
> Cn(X) = { Y | X |- Y }
>
> And a deductive system is consistent, if you have
> no A with A e Cn({}) and ~A e Cn({}). Your ad-hoc axiom
> of function equality showed that your idea of
>
> a proof assistent as a template wizard, and your idea
> of a new concept such as function equality, just some
> shitty new template doesn't work.
>
> Its the wrong approach to do proof assistants and
> the wrong approach to do mathematics.
> Dan Christensen schrieb am Samstag, 30. April 2022 um 22:26:48 UTC+2:
> > So, you couldn't even get started on your homework assignment with your backwards approach. It's one thing to concoct "systems" for your philosophy seminars, and quite another to get actual results on the ground. I hope you have learned your lesson, 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

Also Metamath has a definitional framework. And
they do mathematics mostly by definitions. The usual
building blocks of mathematics is:

- definition
- lemma
- theorem

This building block is usually not so much needed:

- axiom

But you have it in DC Proof, Logic, 2nd menu item.

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 22:44:16 UTC+2:
> For exampe the foundational approach of ZFC is totally
> different. You are not allowed to introduce a single new
> axiom aka template. You are only allowed to
>
> introduce so called definitions. And by some reasoning,
> see Shoenfinkel for example, you can show that if ZFC is
> consistent, your definitions are also consistent.
>
> When you write, this is practically a no-go:
> Dan Christensen schrieb am Samstag, 30. April 2022 um 19:19:22 UTC+2:
> > You can, of course, insert your own axioms at the beginning
> of your proofs and play around with them.
> https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/UJ_-2ZgLAwAJ
>
> Especially for constructive mathematics there are
> now frameworks, of course different from ZFC/Shoenfield,
> that do not allow to add any axiom.
>
> Just check out what Coq, Isabelle/HOL, etc.. provide.
>
> LoL
> Mostowski Collapse schrieb am Samstag, 30. April 2022 um 22:35:38 UTC+2:
> > Its not **my** approach. All of logic is order independent.
> > You can most of the time approach a problem from different
> > sides. Thats utter nonsense to turn a proof assistant
> >
> > into a template wizard, and then claim we need to this
> > this way and we need to do this this way. Because logic
> > doesn't care how the end user uses a tool. The logical
> >
> > consequences of a deductive systems are defined as
> > everything that can be proved.
> >
> > Cn(X) = { Y | X |- Y }
> >
> > And a deductive system is consistent, if you have
> > no A with A e Cn({}) and ~A e Cn({}). Your ad-hoc axiom
> > of function equality showed that your idea of
> >
> > a proof assistent as a template wizard, and your idea
> > of a new concept such as function equality, just some
> > shitty new template doesn't work.
> >
> > Its the wrong approach to do proof assistants and
> > the wrong approach to do mathematics.
> > Dan Christensen schrieb am Samstag, 30. April 2022 um 22:26:48 UTC+2:
> > > So, you couldn't even get started on your homework assignment with your backwards approach. It's one thing to concoct "systems" for your philosophy seminars, and quite another to get actual results on the ground. I hope you have learned your lesson, 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 can check out this book, its all definitions,
he does some methematics in set theory as
part of his book:

Mathematical Logic
Joseph R. Shoenfield
https://www.amazon.com/-/de/dp/1568811357

If you have a newer version of the book, it says on some first page:

Joseph R. Schoenfield died on November 15, 2000,
while this book was being reprinted.

Mostowski Collapse schrieb am Samstag, 30. April 2022 um 22:48:21 UTC+2:
> Also Metamath has a definitional framework. And
> they do mathematics mostly by definitions. The usual
> building blocks of mathematics is:
>
> - definition
> - lemma
> - theorem
>
> This building block is usually not so much needed:
>
> - axiom
>
> But you have it in DC Proof, Logic, 2nd menu item.
> Mostowski Collapse schrieb am Samstag, 30. April 2022 um 22:44:16 UTC+2:
> > For exampe the foundational approach of ZFC is totally
> > different. You are not allowed to introduce a single new
> > axiom aka template. You are only allowed to
> >
> > introduce so called definitions. And by some reasoning,
> > see Shoenfinkel for example, you can show that if ZFC is
> > consistent, your definitions are also consistent.
> >
> > When you write, this is practically a no-go:
> > Dan Christensen schrieb am Samstag, 30. April 2022 um 19:19:22 UTC+2:
> > > You can, of course, insert your own axioms at the beginning
> > of your proofs and play around with them.
> > https://groups.google.com/g/sci.math/c/SOIECV0E-Dc/m/UJ_-2ZgLAwAJ
> >
> > Especially for constructive mathematics there are
> > now frameworks, of course different from ZFC/Shoenfield,
> > that do not allow to add any axiom.
> >
> > Just check out what Coq, Isabelle/HOL, etc.. provide.
> >
> > LoL
> > Mostowski Collapse schrieb am Samstag, 30. April 2022 um 22:35:38 UTC+2:
> > > Its not **my** approach. All of logic is order independent.
> > > You can most of the time approach a problem from different
> > > sides. Thats utter nonsense to turn a proof assistant
> > >
> > > into a template wizard, and then claim we need to this
> > > this way and we need to do this this way. Because logic
> > > doesn't care how the end user uses a tool. The logical
> > >
> > > consequences of a deductive systems are defined as
> > > everything that can be proved.
> > >
> > > Cn(X) = { Y | X |- Y }
> > >
> > > And a deductive system is consistent, if you have
> > > no A with A e Cn({}) and ~A e Cn({}). Your ad-hoc axiom
> > > of function equality showed that your idea of
> > >
> > > a proof assistent as a template wizard, and your idea
> > > of a new concept such as function equality, just some
> > > shitty new template doesn't work.
> > >
> > > Its the wrong approach to do proof assistants and
> > > the wrong approach to do mathematics.
> > > Dan Christensen schrieb am Samstag, 30. April 2022 um 22:26:48 UTC+2:
> > > > So, you couldn't even get started on your homework assignment with your backwards approach. It's one thing to concoct "systems" for your philosophy seminars, and quite another to get actual results on the ground. I hope you have learned your lesson, 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

Mostowski Collapse wrote:
> Its the wrong approach to do proof assistants and the wrong approach to
> do mathematics.
>
> Dan Christensen schrieb am Samstag, 30. April 2022 um 22:26:48 UTC+2:
>> So, you couldn't even get started on your homework assignment with your

you two like nazi pigs and lovers. Which may kiss my ass, we use for
transportation in my country. Soon not event the nazis will fight for the
oligarchs. The nazis are stupid, but not stupid that much.

On Saturday, April 30, 2022 at 4:44:16 PM UTC-4, Mostowski Collapse wrote:
> For exampe the foundational approach of ZFC is totally
> different.

It would be quite useless as an educational aid otherwise. IIUC you can get degree in pure math without ever looking at the ZFC axioms (possible exception: AC). Why do you think that is, 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 Saturday, April 30, 2022 at 4:44:16 PM UTC-4, Mostowski Collapse wrote:
> For exampe the foundational approach of ZFC is totally
> different.

DC Proof would be quite useless as an educational aid otherwise. IIUC you can get degree in pure math without ever looking at the ZFC axioms (possible exception: AC). Why do you think that is, 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 Saturday, April 30, 2022 at 4:44:16 PM UTC-4, Mostowski Collapse wrote:
> For exampe the foundational approach of ZFC is totally
> different.

DC Proof would be quite useless as an educational aid otherwise. IIUC you can get degree in pure math without ever looking at the ZFC axioms (possible exception: AC). Why do you think that is, 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