4 ms·
The Incredible Proof Machine
- dang 11y agoAlso https://news.ycombinator.com/item?id=10272231 https://news.ycombinator.com/item?id=10272231.
- toothbrush 11y agoThat'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 :/
- tel 11y agoThe 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.
- Houshalter 11y agoThere is a coursera course on formal logic which starts in 3 days and covers this kind of stuff: https://www.coursera.org/course/intrologic https://www.coursera.org/course/intrologic They have a very nice proof editor: http://logica.stanford.edu/php/fitch.php http://logica.stanford.edu/php/fitch.php And some other logic tools: http://logica.stanford.edu/php/index.php 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.
- deleted 11y ago[deleted]
- zyzor 11y agoCould somebody explain me, please, what is the annotation block and how do I use it?
- Houshalter 11y agoIt 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".
- zyzor 11y agoOk, 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?
- zyzor 11y agoHm, 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.
- dllthomas 11y agoThink 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).
- zyzor 11y agoOh, 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.
- Houshalter 11y ago
- Strikingwolf 11y agoCan't seem to figure out how the reverse or block works unfortunately, just stuck on A | B -> B | A
- zyzor 11y agoHere are two ways to proof it: http://postimg.org/image/c4ghgyw8r/ http://postimg.org/image/c4ghgyw8r/