contrapositive not proved? about natural_number_game

[kbuzzard]

I totally agree that it's not clear when to use by_cases. Classical logic has the completeness theorem but in constructive logic it seems to be an art to spot when you can prove something.

I don't see any reason why not to swap advanced proposition world levels 9 and 10.

Wasn't that proved in Level 8 of the previous world (Proposition world)?

[kbuzzard]

Thanks. I'm hoping to get back to this game within a few weeks and deal with all the comments which are appearing in completely random places and which I'm now trying to collect here.

Hopefully you don't mind I leave two more comments about advanced proposition world level 9 here:

1. As a reader it is not clear when to use by_cases, the tutorial says it's for lemmas like ¬ ¬ P → P, but it's not obvious whether (P → Q) → (¬ Q → ¬ P) belongs to this category or not. (I tried to teach someone to play the natural number game and I realized that I was beaten by the question raised by the student)

2. As a reader who happens to be a masochist, if someone tries to solve level 9 without depending on cc, he has to use exfalso which is introduced in the next level, but we assume the user has no knowledge of future levels. Does it make sense to swap level 9 and level 10, or is there something I missed here?

[robx]

As a reader who happens to be a masochist, if someone tries to solve level 9 without depending on cc, he has to use exfalso which is introduced in the next level, but we assume the user has no knowledge of future levels. Does it make sense to swap level 9 and level 10, or is there something I missed here?

Just to note that I just came here struggling with the same thing. Thinking I should be able to handle all four cases by hand, but then having no idea how to synthesize a proof for Q having both P and not P.

I should also note that one thing that held me back here is that seemingly relevant things we'd proved before were not available (not_if_imp_false and contrapositive, in particular).

EDIT: And yes, switching 9 and 10 around made things clear to me!

[kbuzzard]

Also brought up by Victor Ahlquist on the Zulip chat.

[kbuzzard]

All this should be fixed now.