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