The Incredible Proof Machine | Hacker News Reader

The Incredible Proof Machine

incredible.nomeata.de

95 pointspotomak13 comments

There is a coursera course on formal logic which starts in 3 days and covers this kind of stuff: https://www.coursera.org/course/intrologic

They have a very nice proof editor: http://logica.stanford.edu/php/fitch.php And some other logic tools: http://logica.stanford.edu/php/index.php

This system is pretty neat though.

EDIT: I'm having trouble with this. I can not get Or Introduction or Or Elimination to work. I have no idea what it where the inputs are supposed to go or why it doesn't accept it as valid. I did figure out how to do assumption, but it wasn't immediately obvious and is kinda clunky.

Also https://news.ycombinator.com/item?id=10272231.

That's a lot of fun :). It's a bit frustrating though that once you've grabbed a logic operator from the panel left, it loses the annotations. For example, for function application, i'd forgotten if the top or the bottom hole was for the function... Maybe i should just work on my short-term memory...

EDIT: I'm not really sure what the point is of all the propositions they want you to prove using bottom? Yeah so your logic is inconsistent if you introduce bottom as a true proposition, big deal :/

The propositions all assume false, but don't prove it. In session 4 you've also got translations of things like contraposition, (not (not (not A))) -> (not A) (which is importantly different from double negation elimination since it holds constructively).

In session 5 you've got excluded middle, the other form of contraposition, double negation elimination which are apparently going to show how providing tertium na datur works to provide classical and not merely constructive logic.

Could somebody explain me, please, what is the annotation block and how do I use it?

It lets you make assumptions. Assumptions let you prove implications.

Say you have A->B->C and B. And you want to prove A->C.

Then you can assume A, and do a regular proof that proves C.

Then you use that other weird block, with the A, B, and implication sign on it. You connect the assumption you made to the "A", and the result, to the "B", and then it lets you prove "A->C".

Ok, so the input socket of this block is the fact that I assume. And what's the meaning of the input socket of this block?

Hm, the more I play with this block, the less I understand it. As far as I can see, the input of this block equals its output, and I can decide what's its input and output.

Think of it like type annotation in Haskell. It doesn't change things, but it lets you pin things down where you know them to make it easier to figure out the bits you don't know (and lets you resolve ambiguity).

Oh, maybe the block I talk about is not called "annotate block"? I talk about the block that from the very beginning of the game is in the "helper blocks" region and which has a pencil icon on it.

No the helper block is the assumption block. The input to the block connects to the first output of the implication block. The output is the assumption, i.e. whatever you typed into it. You can use that to prove more things. Then use the implication block to show that the assumption implies those things.

Can't seem to figure out how the reverse or block works unfortunately, just stuck on A | B -> B | A

Here are two ways to proof it: http://postimg.org/image/c4ghgyw8r/

Reply on news.ycombinator.com