Theory meeting, Sept. 12th

[Lyle Kopnicky]

We'll discuss Chapter 14, "Relations in Lean", 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.

September 12th, 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/gwtbcpyxmbqb/

[Lyle Kopnicky]

I’ve attached my solutions to the Chapter 14 exercises.

--
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.

[Matt Rice]

I've posted mine here,

https://gist.github.com/ratmice/9c3a745feb0912186d573aea7e6ecad3

fairly similar with different syntactic structure,
your solution exercise 1 part 2 is a little simpler where you avoided
eliminiating h2 twice,
by performing substitution on h2 directly, neat.

[Ed Snow]

My answers to the exercises are at:

https://gist.github.com/es30/899e3d81f6516d9cfb314d8a4e01703b

There is nothing new here over what you and Matt have already posted.

[Lyle Kopnicky]

And here's mine as a gist. Same code: https://gist.github.com/lylek/4e608751f1042db3343742e4ad5d5b43

[Lyle Kopnicky]

Great meeting! There weren't many exercises, but the time we spent comparing solutions was constructive.

I then showed some recent work I've done on my proof checker, with the rationale behind it. I discussed the issues surrounding scope in checking the conditions for the forall-introduction rule, and found a bug in my code int the process! I also asked the more philosophical question of how we know what the correct criteria are for applying rules. The rough answer is that too few criteria will allow rules to be applied when they shouldn't, violating soundness. And too many criteria will prevent the rule from being applied when it could be, violating completeness.

We also discussed whether variables, constants, or both should be allowed to be the term that is abstracted over to produce a quantification. That is, if we have  and conclude , is supposed to be a variable, a constant, or can it be either? Chiswell & Hodges say it can be either. But I don't see anything lost in the logic if we restrict it to only constants. Restricting it to constants allows us to maintain a neat property that variables are always bound. But, it also requires us to have enough constants in our language. If we only have, say, 0 as a constant, then any time we want to introduce a universal quantifier, we must first prove something about 0. And any time we do existential elimination, we must use 0 as the constant. But we can't do that if we have any other assumptions about 0, such as .

We can of course add arbitrary constants to the language to satisfy this need. It's interesting to note that the completeness proof for first-order logic relied on the idea of adding arbitrary constants. And it was argued there that adding constants doesn't change what you can prove. But if constants are the only thing that you can use as witnesses in existential elimination or universal introduction, then it does make a difference. Suddenly we can prove things that we couldn't before! Perhaps that points out a fault in my restriction.

You could make similar arguments about variables. What if you only have one variable in your language? Then there's no way you can express, say, a transitivity property, because that requires three variables. So, adding variables allows you to prove more things. I wonder whether it would be possible, in a language with only one or two variables, to create statements that are valid semantically, but can't be proven, due to the lack of sufficient variables?

To put it more succinctly: Are we sure in the completeness proof that we've properly handled the cases where the language has a very limited set of constants and/or variables?

Perhaps it's fine. Perhaps the fact that you can't express transitivity in a proof with only one or two variables means you can't express it semantically either, so there's no true statement that can't be proven.