3 ms·

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, fo

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 :/

tel 11y ago
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.