Hacker News Reader

Comment by rogpeppe1 | Hacker News Reader

This was a fun puzzle, but I came to a roadblock here too.

I have to confess I'm confused by what I believe might be the "local hypothesis block" mentioned above. The confusion is somewhat greater because the blocks don't seem to have any attached name or description, so it's not clear what they're meant to be doing.

Up until task 5 in session 2, all the solutions are pretty trivial. But I can't work out what sort of wiring that block implies (for the record, the task is "given (A->B, B->C), prove (A->C)").

It's really not clear to me what the "notch" at the top of that block implies, or how it might be used.

I think there should be at least one "hand-holding" solution for the first use of each block type. Even the papers linked to don't describe the intended semantics of each block.

Any hints here?

View on HN

OK, replying to myself for future reference. I found the answer here: https://youtu.be/0GeJdTTzaDo (incidentally, that series of videos seems to have solutions for most of these problems).

The answer is that the left and right side of the notch holds local equivalents to the global "given X, prove Y" connectors. You can use the left side of the notch as an input, and you can connect that up through the global blocks to prove the hypothesis.

That was non-obvious! Also, the technique of connecting the output first and making connections to nothing to see what the implied proposition is was very useful - I should have thought of that.

There are two other block types with notches.

One is for a proof by cases; it accepts a disjunction ("or") as input, gives you a local branch for each disjoined option, and hopes you'll show that each branch individually proves P. Then the block globally proves P. This one was intuitive to me.

One is for instantiating variables from existential quantifiers. If you send ∃x.P(x) into that block's global input, you will get P(c), where c is a constant, coming out of that block's local output. You're supposed to prove an expression that does not involve c, send that to local input, and get it back out of global output.

As far as I can tell, this is done for reasons of convenient implementation. Mathematically, the notch shouldn't be there at all -- you should just be able to hook up ∃x.P(x) to global input, and get P(c) on global output. But I think the tool author wants to think of c as being a variable which is scoped inside the ∃-instantiation block and can't exist outside it.

Reply on news.ycombinator.com