Hacker News Reader

Comment by thaumasiotes | Hacker News Reader

I was really confused about "local hypotheses" for a minute there. In session 2, you get two blocks for working with implications.

One is a modus ponens block -- given the two inputs (X -> Y) and (X), it produces the output (Y).

The other is a block for positing assumptions ("local hypotheses"). In the block selection menu, it has an ordinary output of (X -> Y). It has a notch in the top with an output of (X) on the left and an input of (Y) on the right.

The function of this block, as shown by the ordinary output, is to prove statements of the form (X -> Y). For this purpose, it gives you a free output of X, but every path you send that X through must eventually either be abandoned or come back to the matching Y input in its notch.

The X will magically become the variable you need when connected to the appropriate input of a modus ponens block.

View on HN

i was confused by the "local hypothesis" block as well until i realized it's just `lambda x: ...` :)

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?

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