Handling Ordered Pairs in DC Proof 2.0

[Dan Christensen]

On Tuesday, August 23, 2022 at 1:02:22 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:

> How do you prove this valid theorem [in DC Proof 2.0]
>
> ALL(y):ALL(z):[EXIST(x):[x = (y,z) & P(x)] <=> P((y,z))]
>
> You cannot even enter it.
>

True. In DC Proof, the parser will eliminate what it sees as redundant brackets. "P((y,z))" as above will be automatically trimmed to "P(y,z)"

In mathematics, however, we don't usually talk about arbitrary objects like this. Rather, we talk about elements of sets and functions mapping one set to another.

In set theory, you can prove:

ALL(y): ALL(z): [y in r & z in r => EXIST(x): [x in r2 & [P(x) <=> P(pt(y,z))]]]

Where we define the function pt as follows:

ALL(a):ALL(b):[a in r & b in r => EXIST(c):[c in r2 & pt(a,b)=c]]

(For example, you might think of r as the set of real numbers R, and the r2 as the set of points in the R^2 plane. The pt function would then map ordered pairs of real numbers to points in the R^2 plane.)

PROOF

1. Set(r)
Axiom

2. Set(r2)
Axiom

3. ALL(a):ALL(b):[a in r & b in r => EXIST(c):[c in r2 & pt(a,b)=c]]
Axiom

4. y in r & z in r
Premise

5. ALL(b):[y in r & b in r => EXIST(c):[c in r2 & pt(y,b)=c]]
U Spec, 3

6. y in r & z in r => EXIST(c):[c in r2 & pt(y,z)=c]
U Spec, 5

7. EXIST(c):[c in r2 & pt(y,z)=c]
Detach, 6, 4

8. x in r2 & pt(y,z)=x
E Spec, 7

9. x in r2
Split, 8

10. pt(y,z)=x
Split, 8

11 P(x)
Premise

12. P(x) => P(x)
Conclusion, 11

13. P(x) => P(pt(y,z))
Substitute, 10, 12

14. P(pt(y,z)) => P(x)
Substitute, 10, 12

15. [P(x) => P(pt(y,z))] & [P(pt(y,z)) => P(x)]
Join, 13, 14

16. P(x) <=> P(pt(y,z))
Iff-And, 15

17. x in r2 & [P(x) <=> P(pt(y,z))]
Join, 9, 16

18. ALL(y):ALL(z):[y in r & z in r
=> EXIST(x):[x in r2 & [P(x) <=> P(pt(y,z))]]]
Conclusion, 4

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]

> In mathematics, however, we don't usually talk about arbitrary objects like this.

Oh, we don't say (x_1, x_2) =/= (y_1, y_2) for certain x_1, x_2, y_1, y_2 e IR in the context of IR^2? Are you serious?

So we don't claim that e_1 =/= e_2 with e_1 := (1, 0) and e_2 := (0, 1)?

Ever heard of /linear algebra/, man?

See: https://en.wikipedia.org/wiki/Linear_algebra

> Rather, we talk about elements of sets and functions mapping one set to another.

Huh?! So you think that we don't consider set of (ordererd) pairs, like {(x, y) : x e X & y e Y} in math? Are you serious?

Ever heard of n-tupels? Or vectors?

No sets of n-tupels (or vectors) in math?

Hint: "Mathematicians usually write tuples by listing the elements within parentheses "( )" and separated by commas; for example, (2, 7, 4, 1, 7) denotes a 5-tuple. [...] The term tuple can often occur when discussing other mathematical objects, such as vectors."

Source: https://en.wikipedia.org/wiki/Tuple

Holy shit!

_____________________________________________

Yes, it's true that mathematicans often write

F(x, y)

instead of

F((x, y))

but that's just a convention for convenience.

In a formal system it SHOULD be possible to write F((x, y)).

How about writing/using "<x, y>" instead of "(x, y)" to avoid problems with parsing of expressions?

[Dan Christensen]

On Tuesday, August 23, 2022 at 2:45:55 PM UTC-4, Fritz Feldhase wrote:
> > In mathematics, however, we don't usually talk about arbitrary objects like this.
> Oh, we don't say (x_1, x_2) =/= (y_1, y_2) for certain x_1, x_2, y_1, y_2 e IR in the context of IR^2? Are you serious?
>

We can, instead, say the pt(x_1, x_2) =/= pt(y_1,y_2), etc.

> So we don't claim that e_1 =/= e_2 with e_1 := (1, 0) and e_2 := (0, 1)?
>

The pt function would have be a bijection. pt(a,b)=pt(c,d) <=> a=c & b=d

> Ever heard of /linear algebra/, man?
>
> See: https://en.wikipedia.org/wiki/Linear_algebra
> > Rather, we talk about elements of sets and functions mapping one set to another.
> Huh?! So you think that we don't consider set of (ordererd) pairs, like {(x, y) : x e X & y e Y} in math? Are you serious?
>
> Ever heard of n-tupels? Or vectors?
>

Why would something like the above pt function not work for vectors?

> No sets of n-tupels (or vectors) in math?
>

The Cartesian Product Axiom is used to construct sets of ordered pairs.

> Hint: "Mathematicians usually write tuples by listing the elements within parentheses "( )" and separated by commas; for example, (2, 7, 4, 1, 7) denotes a 5-tuple. [...] The term tuple can often occur when discussing other mathematical objects, such as vectors."
>
> Source: https://en.wikipedia.org/wiki/Tuple
>
> Holy shit!
>
> _____________________________________________
>
> Yes, it's true that mathematicans often write
>
> F(x, y)
>
> instead of
>
> F((x, y))

Or F(pt(x,y))?

>
> but that's just a convention for convenience.
>
> In a formal system it SHOULD be possible to write F((x, y)).
>

Not necessarily AFAICT.

> How about writing/using "<x, y>" instead of "(x, y)" to avoid problems with parsing of expressions?

Why not pt(x,y)?

[Mostowski Collapse]

Again some irrelevant bull shiting.
Its not the same you moron.
Where is the equality?

ALL(y):ALL(z):[EXIST(x):[x = (y,z) <-------------- !!!! equality !!!!
& P(x)] <=> P((y,z))]

One can even not enter an expression x = (y,z) in moronic DC Proof:
https://www.rubycap.ch/dcproof17_nopaireq.png

[Mostowski Collapse]

Now use pt(_,_) instead (_,_) and you can even not replicate this proof:

Here is a proof in Wolfgang Schwartz tree tool, I use
p(_,_) for pair (_,_), because he currently doesn't have pairs
syntax, but this doesn't matter, the theorem is valid:

∀y∀z(∃x(x=p(y,z) ∧ Px) ↔ Pp(y,z)) is valid.
https://www.umsu.de/trees/#~6y~6z%28~7x%28x=p%28y,z%29~1P%28x%29%29~4P%28p%28y,z%29%29%29

Whats wrong with you?

[Mostowski Collapse]

Also its again one of your charlatan nonsense, only
because your theorem has EXIST in it, doesn't mean
it is the same. I could also ask for a proof with ALL:

ALL(y):ALL(z):[ALL(x):[x = (y,z) => P(x)] <=> P((y,z))]

Thats also a valid sententence you cannot currently prove in
DC Proof. But Wolfgang Schwartz tree tool can prove it:

∀y∀z(∀x(x=p(y,z) → Px) ↔ Pp(y,z)) is valid.

https://www.umsu.de/trees/#~6y~6z%28~6x%28x=p%28y,z%29~5P%28x%29%29~4P%28p%28y,z%29%29%29

[Fritz Feldhase]

On Tuesday, August 23, 2022 at 9:06:33 PM UTC+2, Dan Christensen wrote:
> On Tuesday, August 23, 2022 at 2:45:55 PM UTC-4, Fritz Feldhase wrote:
> >
> > Oh, we don't say (x_1, x_2) =/= (y_1, y_2) for certain x_1, x_2, y_1, y_2 e IR in the context of IR^2? Are you serious?
> >
> We can, instead, say the pt(x_1, x_2) =/= pt(y_1,y_2), etc.

Yeah, we might say that, with

pt(x, y) := (x, y) .

But that "approach" would be quite strange.

Yeah, in undergraduate texts we might see things like p(x, y) which actually denotes a point p with p = (x, y).

But "pt(x, y)" doesn't make much sense. I guess you mean something like

tuple(x_1, ..., x_n) := (x_1, ..., x_n).

But, as you can see, we already use "(...)" to define /tuple/ here.

Well, I see, we might "define" /tuple/ recursively:

tuple(x) = x
tuple(x_1, ... x_n+1) = tuple(tuple(x_1, ..., x_n), x_n+1).

> > So we don't claim that e_1 =/= e_2 with e_1 := (1, 0) and e_2 := (0, 1)?
> >
> The pt function would have be a bijection. pt(a,b)=pt(c,d) <=> a=c & b=d

ordered_pair(x, y) := (x, y).

Then ordered_pair(a, b) = ordered_pair(c, d) <=> a = c & b = d.

As desired. :-P

It's just that in math we usually write an ordered pair (with first component a and second component b) as "(a, b)" or "<a, b>".

> > Ever heard of n-tupels? Or vectors?
> >
> Why would something like the above pt function not work for vectors?

Sure "tuple()" [as "defined" above] would work. But again, it's just that in math we usually write a vector (with first component x_1, second component v_2, ..., and n-the component x_n) as "(x_1, ... x_n)" (without "..." of course, if not "abbreviated").

> > No sets of n-tupels (or vectors) in math?
> >
> The Cartesian Product Axiom is used to construct sets of ordered pairs.

Great. But no way to refer to them "directly"? I mean using the usual notation <., .> or (., .)?

Well, ok, if there'sno way to make that possible in DC Proof...

Funny side note: You alrady HAVE that notaton "implicitly" in DC Proof - otherwise "ordered_pair(a, b)" would not refer (exactly) to (a, b) (or <a. b>).

> > "Mathematicians usually write tuples by listing the elements within parentheses "( )" and separated by commas; for example, (2, 7, 4, 1, 7) denotes a 5-tuple. [...] The term tuple can often occur when discussing other mathematical objects, such as vectors."
> >
> > Source: https://en.wikipedia.org/wiki/Tuple
> >
> > Holy shit!
> >
> > _____________________________________________
> >
> > Yes, it's true that mathematicans often write
> >
> > F(x, y)
> >
> > instead of
> >
> > F((x, y))
> Or F(pt(x,y))?
> >
> > but that's just a convention for convenience.
> >
> > In a formal system it SHOULD be possible to write F((x, y)).
> >
> Not necessarily AFAICT.

NOTHING (of this kind) is "necessary", you silly prick!

From a mathematical/logical point of view, one might consider F(x) a unary set operation, and G(x, y) a binary set operation. So there's a (logical) difference between F(z) where z = (x, y) and G(x, y), even if F((x, y)) = G(x, y) for all x, y.

For example, if we use G(x, y) (x, y, e IR) we may, say, define

G(x, y) := x^2 + y^2.

On the other hand, if we use F(z) (with x e IR x IR) instead, we will have to use some additional "machinery" for achieving" the same":

F(z) := pi_1(z)^2 + pi_2(z)^2.

Then we actually would have

F(<x, y>) := pi_1(<x, y>)^2 + pi_2(<x, y>)^2 = x^2 + y^2 for all x,y e IR.

Hence, in this case, F(<x, y>) = G(x, y) for all x, y e IR.

Again:

> > How about writing/using "<x, y>" instead of "(x, y)" to avoid problems with parsing of expressions?
> >
> Why not pt(x,y)?

Since it just seem to be a TECHNICAL problem of DC Proof, why not use, say, _(x, y) as a workaround?

Or ... '(x, y)?

[Fritz Feldhase]

On Tuesday, August 23, 2022 at 9:48:48 PM UTC+2, Mostowski Collapse wrote:

> Thats also a valid sententence you cannot currently prove in
> DC Proof. But Wolfgang Schwartz tree tool can prove it:
>
> ∀y∀z(∀x(x = p(y,z) → Px) ↔ Pp(y,z)) is valid.

Yeah, would be nice if DC Proof could prove, say,

∀f∀Y∀Z∀T(function(f, YxZ, T) -> ∀y∀z(y e Y & z e Z -> ∀x(x = '(y,z) → f(x) = f('(y,z)))))

if Dan could use '(y, z) to denote the ordered pair of y and z (with y as first component and z as second component).

[Dan Christensen]

[snip abuse]

> Where is the equality?
>
> ALL(y):ALL(z):[EXIST(x):[x = (y,z) <-------------- !!!! equality !!!!
> & P(x)] <=> P((y,z))]
>

> One can even not enter an expression x = (y,z) [snip abuse]

Instead, we can write x = pt(y,z) where pt(a,b)=pt(c,d) <=> a=c and b=d.

What's wrong with that? Yes, it differs from the text books, but it is a minor point.

[Fritz Feldhase]

On Tuesday, August 23, 2022 at 11:50:28 PM UTC+2, Dan Christensen wrote:
> On Tuesday, August 23, 2022 at 3:38:35 PM UTC-4, Mostowski Collapse wrote:

> > One can even not enter an expression x = (y,z)

It seems to me that this is indeed a certain weekness of DC Proof.

> Instead, we can write x = pt(y,z) where pt(a,b)=pt(c,d) <=> a=c and b=d.
>
> What's wrong with that? Yes, it differs from the text books, but it is a minor point.

Agree. But "pt" seems to refer to "point", that's not always "intended".

So something "neutral" would be better. Say, '(x, y) if possible (reminds me to LISP somehow, btw.)

On the other hand, you really might EXTEND DC Proof, such that <x, y> is recognized as (a name for an) an "ordered pair" (i. e. THE ordered pair with x as first component and y as second component).

How hard can that be?

Of course, in this case, it would be necessary, do add some additional operators (which work on ordered pairs), say "_1" and "_2" such that

AxAy(<x, y> = <<x, y>_1, <x, y>_2>).

Moreover

<x, y> = <z, t> <-> x = z & y = t

should be ensured by DC Proof.

================================================

Hint: In the context of "standard math", say set theory, all these notions can be DEFINED. Standard math allows for (quite different) DEFINED NOTIONS.

For example:

(x, y) := {{x}, {x, y}}

or

f[X] := {f(x) : x e X}

etc.

It's clear that it's not that easy to allow for a comparable flexibility in the context of a formal system.

_______________________________

MY IDEA how TO DEAL with these problems .. would be to PREPARE some "libraries" for DC Proof with "predefined" notions which are the main notions in that context. Say, a "function library" with (the definitions) for, say,

function(f)
function(f, X, Y)
dom(f)
img(f)
cod(f)
surjective(f)
etc.

I guess these library would itself have to be based on the "set theory" library. This way you could define "mathematical functions" in the context of set theory (which is the prefered way in math, I'd say).

So DC Proof would only provide the LOGICAL FRAMEWORK (inclusive "identity theory") but everything else would have to be "added" (by "loading" a library).

This way "math" in DC Proof would have a certain hierarchical structure. So what?

I mean, if you want to use "ordered pairs" in math you have to accept them as "undefined notions" (as well as the projections _1 and _2) OR you will have to DEFINE them somehow. The usualy way is to define them in the context of (some) set theory. Hence the "hierarchical structure". Same with RELATIONS and FUNCTIONS, etc. etc.

It seems to me that you would like to avoid that "hierarchical structure". (By, say, considering "functions" as primitives etc.)

[Dan Christensen]

On Tuesday, August 23, 2022 at 6:26:44 PM UTC-4, Fritz Feldhase wrote:
> On Tuesday, August 23, 2022 at 11:50:28 PM UTC+2, Dan Christensen wrote:
> > On Tuesday, August 23, 2022 at 3:38:35 PM UTC-4, Mostowski Collapse wrote:
>
> > > One can even not enter an expression x = (y,z)

> It seems to me that this is indeed a certain weakness of DC Proof.

[snip]

One thing at a time...

Maybe a silly question, but why we would it ever be necessary to formally equate a single object to an ordered list of two or more objects. What important insights would be missed if we never allowed such constructs?

Dan

[Mostowski Collapse]

The insight that Bourbaki is less clumsy? Because you can equate:

f = (g,a,b)

Now I cannot define Surjective Bourbaki style, because of your
two nonsense bugs. Bug 1:

Surjective((g,a,b)) <=> ...

gets scrambled into this here:

Surjective(g,a,b) <=> ...

Bug 2: I cannot write this here, to avoid the scrambling:

Surjective(f) <=> EXIST(g):EXIST(a):EXIST(b):[f = (g,a,b) ...]

Two bugs in one row, Bug 1 and Bug 2, as soon as one
wants to do some Bourbaki mathematics. The insight is here,

18 years and still nothing works in DC Proof.

[Mostowski Collapse]

So what is the joke behind his comment here:

Dan Christensen schrieb am Mittwoch, 17. August 2022 um 20:27:51 UTC+2:
> I have tried various definitions of a surjectivity abbreviation including
your suggestion to restrict its application using the Function(f,x,y) signature,
but found it needlessly cumbersome.
https://groups.google.com/g/sci.logic/c/QSfRj2g1ur8/m/fFHeqEU7AQAJ

The sad truth is he tried, and there were bugs.

Thats what happened in DC Broken Mess.

[Fritz Feldhase]

On Wednesday, August 24, 2022 at 1:41:30 AM UTC+2, Dan Christensen wrote:
> On Tuesday, August 23, 2022 at 6:26:44 PM UTC-4, Fritz Feldhase wrote:
> > On Tuesday, August 23, 2022 at 11:50:28 PM UTC+2, Dan Christensen wrote:
> > > On Tuesday, August 23, 2022 at 3:38:35 PM UTC-4, Mostowski Collapse wrote:
> > > >
> > > > One can even not enter an expression x = (y,z)
> > > >
> > It seems to me that this is indeed a certain weakness of DC Proof.
> >
> [snip]
>
> One thing at a time...

Fair enough.

> Maybe a silly question,

but maybe not :-)

> but why would it ever be necessary to formally equate a single object to an ordered list of two or more objects. What important insights would be missed if we never allowed such constructs?

Hmmm... Not sure I got the meaning of your question, but... we can have a set of ordered pairs, say, {<1, a>, <2, b>}, right? This set contains 2 ordered pairs. Without ordered pairs _as objects_ we could not define such a set.

Now such sets allow to define RELATIONS as sets of ordered pairs and FUNCTIONS as certain sets of ordered pairs. etc. etc.

These things were first formulated/discovered by C. S. Peirce. Later adopted by others (for example by Russell and Whitehead in their PM)... It seems that this is a rather reasonable approach.

In any case, these days it's just the usual/mainstream approach concerning relations and functions.

[Dan Christensen]

On Tuesday, August 23, 2022 at 9:14:19 PM UTC-4, Fritz Feldhase wrote:
> On Wednesday, August 24, 2022 at 1:41:30 AM UTC+2, Dan Christensen wrote:
> > On Tuesday, August 23, 2022 at 6:26:44 PM UTC-4, Fritz Feldhase wrote:
> > > On Tuesday, August 23, 2022 at 11:50:28 PM UTC+2, Dan Christensen wrote:
> > > > On Tuesday, August 23, 2022 at 3:38:35 PM UTC-4, Mostowski Collapse wrote:
> > > > >
> > > > > One can even not enter an expression x = (y,z)
> > > > >
> > > It seems to me that this is indeed a certain weakness of DC Proof.
> > >
> > [snip]
> >
> > One thing at a time...
> Fair enough.
>
> > Maybe a silly question,
>
> but maybe not :-)
>
> > but why would it ever be necessary to formally equate a single object to an ordered list of two or more objects. What important insights would be missed if we never allowed such constructs?
>
> Hmmm... Not sure I got the meaning of your question, but... we can have a set of ordered pairs, say, {<1, a>, <2, b>}, right? This set contains 2 ordered pairs. Without ordered pairs _as objects_ we could not define such a set.
>

I'm not questioning ordered n-tuples. In DC Proof, order n-tuples are used only as elements of sets, e.g. (x,y) in A. They are just an optional part of the set-element notation. Nothing else.

I want to know why expressions like z=(y,z) are thought to be logically necessary. What if anything makes them indispensable?

Dan

[Dan Christensen]

See my reply just now to your identical posting at sci.math

On Tuesday, August 23, 2022 at 8:34:08 PM UTC-4, Mostowski Collapse wrote:
> So what is the joke behind his comment here:
>

[snip]

Pour Jan Burse still pouting...

[Mostowski Collapse]

Oh boy, did you really ask about use cases for pairs as first
class citizens when you wrote this?

Dan Christensen schrieb am Mittwoch, 24. August 2022 um 01:41:30 UTC+2:
> Maybe a silly question, but why we would it ever be necessary to formally
> equate a single object to an ordered list of two or more objects. What
> important insights would be missed if we never allowed such constructs?

https://groups.google.com/g/sci.logic/c/xjV--M0JhXE/m/eGZIviRhBQAJ

Did you ever do these constructions:

1) Z from N, via equivalence class over NxN, we would have (2,5) ~ -3
Can you do that in DC Proof?

2) Q from Z, via equivalence class over Zx(N\{0}), we would have (3,6) ~1/2
Can you do that in DC Proof?

[Daniel Pehoushek]

about holes in general pointer theory
in john mccarthys general pointer language theory for functions
he had an interpreter bug spelled r p l a c a that was provably unsolvable
daniel2380++

[Dan Christensen]

SUMMARY

On Tuesday, August 23, 2022 at 2:18:01 PM UTC-4, Dan Christensen wrote:
> On Tuesday, August 23, 2022 at 1:02:22 PM UTC-4, Mostowski Collapse (Jan Burse) wrote:
>
> > How do you prove this valid theorem [in DC Proof 2.0]
> >
> > ALL(y):ALL(z):[EXIST(x):[x = (y,z) & P(x)] <=> P((y,z))]
> >
> > You cannot even enter it.
> >
>
> True. In DC Proof, the parser will eliminate what it sees as redundant brackets. "P((y,z))" as above will be automatically trimmed to "P(y,z)"

[snip]

More importantly, however, in DC Proof, ordered n-tuples are used only in the context of being an element of a set, e.g. (x,y) in z. I have never found it necessary to equate an ordered n-tuple with an ordinary free variable, e.g. (x,y) = z.

As has been pointed out by others here, the ordered-pair (x,y) is often used in textbooks to signify a point or vector the R^2 plane (itself a set of ordered pairs).

There is a simple workaround in DC Proof if, for example, you want to formalize the notion of a vector on R^2.

First, construct the set S = { {(a,b)} | (a,b) in R^2}. S is the set of all singletons of ordered pairs in R^2.

Then construct the bijective function V: R^2 --> S such that V(x,y) = {(x,y)}. "V(x,y)" can be read "the vector x, y".

Being bijective, we would have, as required, V(x,y) = V(a,b) iff x=a and y=b.

We could also define V(x,y) + V(a,b) = V(x+a, y+b) where +, depending on the context, could be either addition on R, or vector addition on R^2. Similarly, we could define scalar multiplication such that m*V(x,y) = V(m*x, m*y)

[Fritz Feldhase]

On Thursday, September 1, 2022 at 3:55:20 AM UTC+2, Dan Christensen wrote:
>
> I have never found it necessary <bla>

You are a crank, Dan.

Good luck. Bye.

[Dan Christensen]

On Wednesday, August 31, 2022 at 11:04:25 PM UTC-4, Fritz Feldhase wrote:
> On Thursday, September 1, 2022 at 3:55:20 AM UTC+2, Dan Christensen wrote:
> >
> > I have never found it necessary <bla>
>

[snip abuse]

Just giving DC Proof users a simple workaround to handle ordered pairs, e.g. how to formalize the notion of a vector on R^2.

We have the function V such that V(x,y)={(x,y)}. This function can be proven to exist and that it is bijective. From this simple construct, we have: V(x,y)=V(a,b) iff x=a and y=b, etc. We don't need (x,y)=(a,b) iff x=a and y=a=b. It works. Deal with it, Fritz.

Dan

[Mostowski Collapse]

Is this some kind of joke to use the
Peano Unit just to have pairs?

LoL

Dan Christensen schrieb:

[Mostowski Collapse]

What about pair equality? I am even afraid to
ask. Does pair equality exist in Dan O Matiks world?

Or do we have to wait for dcproof33.exe so
that it suddently has a pair equality menu item?

LoL

[Dan Christensen]

See my reply just now to your identical posting at sci.math

Dan

[Mostowski Collapse]

A PDF is downloadable here:

The Empty Set, the Singleton, and the Ordered Pair
Akihiro Kanamori - The Bulletin of Symbolic Logic
https://www.researchgate.net/publication/38327298

The Peano Unit or Unit Class, {a} for an individual a,
allows eliminating equality, since we have:

a = b <=> a e {b}

But its rather unusual to apply this trick, only to
get vectors, when the proof tool has already
equality, looks "needlessly cumbersome" to me.

Possibly the right use of "needlessly cumbersome"
now, since we have evidence:

1 Symbol _ = _: a = b

2 Symbols _e_ and {_}: a e {b}

Which one is more cumbersome?

[Mostowski Collapse]

cumbrous: ponderous elephants in a circus parade
https://www.merriam-webster.com/dictionary/cumbersome

LoL

[Fritz Feldhase]

On Thursday, September 1, 2022 at 4:47:25 PM UTC+2, Mostowski Collapse wrote:

> But its rather unusual to apply this trick, only to
> get vectors, when the proof tool has already
> equality, looks "needlessly cumbersome" to me.

Why not call it idiotic?

Hint: In the context of set theory we usually have

(x, y) := {{x}, {x, y}}.

Now Dan Crank proposes to use {{{x}, {x, y}}} instead of {{x}, {x, y}}, just because he rejects to use the term "(x, y)" in certain contexts like "f(<HERE>)" and "<HERE> = <HERE>".

Holy shit!

[Dan Christensen]

On Thursday, September 1, 2022 at 11:46:10 AM UTC-4, Fritz Feldhase wrote:
> On Thursday, September 1, 2022 at 4:47:25 PM UTC+2, Mostowski Collapse wrote:
>
> > But its rather unusual to apply this trick, only to
> > get vectors, when the proof tool has already
> > equality, looks "needlessly cumbersome" to me.

[snip abuse]

> Hint: In the context of set theory we usually have
>
> (x, y) := {{x}, {x, y}}.
>

Yeah, that would go over REALLY well is most math textbooks!!!

> Now [snip abuse] proposes to use {{{x}, {x, y}}} ....

I propose to use the by simple bijective function f(x,y) = {(x,y)} to formalize vectors and spatial coordinates in R^2. It works. Deal with it, Fritz.

[Jim Burns]

On 9/1/2022 4:55 PM, Dan Christensen wrote:
> On Thursday, September 1, 2022
> at 11:46:10 AM UTC-4, Fritz Feldhase wrote:

> [snip abuse]
>
>> Hint: In the context of set theory
>> we usually have
>> (x, y) := {{x}, {x, y}}.
>
> Yeah, that would go over REALLY well
> is most math textbooks!!!

...because...

∀x,∀y,∀u,∀v,
{{x},{x,y}} = {{u},{u,v}}
iff x = u & y = v

∀x,∀y,∃z = {{x},{x,y}}