There is a coursera course on formal logic which starts in 3 days and covers this kind of stuff: <a href="https://www.coursera.org/course/intrologic" rel="nofollow">https://www.coursera.org/course/intrologic</a><p>They have a very nice proof editor: <a href="http://logica.stanford.edu/php/fitch.php" rel="nofollow">http://logica.stanford.edu/php/fitch.php</a> And some other logic tools: <a href="http://logica.stanford.edu/php/index.php" rel="nofollow">http://logica.stanford.edu/php/index.php</a><p>This system is pretty neat though.<p>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 <a href="https://news.ycombinator.com/item?id=10272231" rel="nofollow">https://news.ycombinator.com/item?id=10272231</a>.
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...<p>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 :/