Theory meeting, Feb. 13th

[Lyle Kopnicky]

We'll discuss Chapter 21, "The Real Numbers", of Logic and Proof (https://leanprover.github.io/logic_and_proof). Please try to work the exercises beforehand. At the meeting anyone will be able to present and contribute to the discussion.

Wednesday, February 13th, 2018, 6:30-8:30pm

Location:
Collective Agency

3050 SE Division, Suite 245 · Portland, OR

We'll be in the second floor conference room, not in the Collective Agency suite. It's just off the lobby area in the middle of the second floor. Elevator access is available.


RSVP at: https://www.meetup.com/Portland-Functional-Programming-Study-Group/events/gwtbcpyzdbrb/

[Lyle Kopnicky]

A very interesting meeting! We talked about the more difficult exercises, such as #4 and #8.

Exercise 4 is about defining multiplication on the integers, using the quotient construction from the chapter, and then proving that it respects the equivalence relation. We were able to define multiplication, but had a hard time proving that it respected the equivalence relation. Mainly it turned into a lot of algebraic terms without much of an idea as to how to manipulate them to prove the desired result.

Though someone pointed out that if we required normalization before doing the multiplication, proving that it respected the equivalence relation would be trivial. I agree, but I still want to solve it using the definition without normalization, because it feels more like the way that addition was defined in the chapter. I'll keep at it for next time.

Exercise 8 is about showing that the sum of two Dedekind cuts is a Dedekind cut. So, similar to Exercise 4, but for addition on a representation of the reals, instead of multiplication on a representation of the integers. We got a bit stuck proving that, too.

Well, I've done some more thinking and reading since then, and I have it figured out. It turns out that the way they defined it in the book, there's an edge case where it's broken! Try adding a representation of an irrational number and its negative, and the result you get will not be a Dedekind cut, because 0 will not appear in either the left or right set of the sum. You can fix this by making a special case, but, it's awkward. It turns out to work better to forget about having two sets, and just define a Dedekind cut by the left set. I'll write up more in my solution.

- Lyle

--
You received this message because you are subscribed to the Google Groups "pdxfunc" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pdxfunc+u...@googlegroups.com.
To post to this group, send email to pdx...@googlegroups.com.
Visit this group at https://groups.google.com/group/pdxfunc.
For more options, visit https://groups.google.com/d/optout.

[Ed Snow]

On Wednesday, February 20, 2019 at 10:43:39 PM UTC-8, Lyle Kopnicky wrote:

Well, I've done some more thinking and reading since then, and I have it figured out. It turns out that the way they defined it in the book, there's an edge case where it's broken! Try adding a representation of an irrational number and its negative, and the result you get will not be a Dedekind cut, because 0 will not appear in either the left or right set of the sum. You can fix this by making a special case, but, it's awkward. It turns out to work better to forget about having two sets, and just define a Dedekind cut by the left set. I'll write up more in my solution.

Yeah, I can see now that you are right. Concentrating on the A (left) set does simplify life considerably. Meanwhile, I have a solution to problem #4 (attached).

- Ed

[Lyle Kopnicky]

That’s brilliant, Ed! I like your multi-colored diagram showing the relationships between the factors!

I’ve also solved #4, but I got stumped on my own and found an external source. The solution involves setting up an equation with a trick I wouldn’t have thought of. Your solution feels more intuitive.

--