Pairing functions

[rzach]

We have an informal explanation of the pairing function in
https://github.com/OpenLogicProject/OpenLogic/blob/master/content/sets-functions-relations/size-of-sets/enumerability.tex
but it will be useful (and of interest) to have one or two explicit pairing functions. Add a section on that.

[marcusrossberg]

Might that fit in here?

https://github.com/OpenLogicProject/OpenLogic/blob/master/content/sets-functions-relations/sets/pairs-and-products.tex

I could have a go at that. Are we thinking Weiner-Kuratowski and perhaps an arithmetical one?

[rzach]

I was thinking the arithmetical ones, ie how to compute the place in the zig-zag enumeration from the coordinates. But constructing ordered pairs is a good idea too. Should probably each be their own sections. (And maybe it's own issue?)

[marcusrossberg]

Oh, right. Of course. Sorry.
Yes, both would be good, I think.

[rzach]

Kuratowski pair: #134

[rzach]

Hey @marcusrossberg are you still planning to do this?

[marcusrossberg]

Hi @rzach,

I looked over the whole thing and I am no longer convinced we need this---esp. since it's briefly mentioned in

https://github.com/OpenLogicProject/OpenLogic/blob/master/content/first-order-logic/models-theories/set-theory.tex

Thoughts?

If there's a desire to add it, I'm happy to do it.

[rzach]

But the arithmetical pairing function(s) aren't... see #108 (comment)

But if you weren't planning to write that, just the set theoretic definition of pairs, then no worries. I'll get to it at some point.

[marcusrossberg]

D'oh! I can't believe I mixed this up twice in the same thread...

I sent a pull request. Is that roughly what you had in mind?

[marcusrossberg]

#180

(I probably didn't do the pull request right again, but I'm sure you can sort it out, @rzach.)

[rzach]

Well, this has been fixed for a while. Thanks again though.
ff202ca