/sci/ - Science & Math

>>9645959
The standard set theory axiom that enables you to prove equality of sets is

∀x,y. ( ∀z. (z∈x ⇔ z∈y) ⇒ x=y )

i.e. two sets x and y are equal if any set x that is in one is also in the other. I.e. if x and y have the same elements.
In logic you say things about "=", e.g. x=y => y=x, and not how you can generally prove equality of two terms in a theory. Such axioms are instead to be taken as axioms of the theory (not of the logic).
Generally adopting the Leibniz principle which involves "any P" forces you to have infinite axioms or choose a higher order logic.
However, not that since set theories (e.g. Fraenkels) merely fix axioms to use "is element of" and all statements come down to sentences involving this notion, the axiom I wrote above is also a kind of specialized instantiation of the Leibniz axiom.

Notions of equalities like in Martin-Löf type theory are also related to that, except the rules there (some super induction rules about how to prove equality) are more involved.

>>9645967
Let's say something people in other fields could know about too. Might be a bad restriction, though. Let's come from the other side: What motivates you for the generalization quest?

>>9645971
You guys discussion is a bit moot. In any case, you can put R and R^3 in bijection, but of course if you model triples as some kind of contrainer, and you got a model for 0 as number in R, then the zero vector (0,0,0) in R^3 can't be equal to 0 (in that model) as then you had the expression for 0 nested in itself. That's not a formal argument, but I suppose you can formalize this. For set theories which break with that, however, see e.g.
https://en.wikipedia.org/wiki/Non-well-founded_set_theory
There are many ways to play those things.

>>9399407
https://www.instagram.com/dubnitskiy_david/

[math] \int_0^t {\mathrm d} \sqrt{s} = \sqrt{t} [/math]

>>9175155
Okay, write [6] instead of [3]x[2].

That doesn't solve the bulk of the problem.
The question is how to take the pair (i,j) in NxN and surjectively map it into the key value list
[3] -> N x [6]