search

nomeata / incredible

The Incredible Proof Machine
MIT License
358 stars 36 forks source link

Solutions? #96

Closed garyb closed 6 years ago

garyb commented 6 years ago

Is there a list of solutions anywhere? It'd be great to see how some of the proofs that require a smaller number of blocks than my efforts are done.

There's also two proofs that I'm completely flummoxed by despite having completed just about everything else up to session 7. I must have spent hours trying to figure them out, periodically trying since this launched :smile: ((A∨(A→⊥)→⊥)→⊥, ((A→B)→A)→A)

nomeata commented 6 years ago

No, I failed to collect a list of solutions. Whenever I bumped the number of blocks, someone showed me a screenshot, sometimes here on GitHub, you can source the github issues.

As a rule of thumb: Whenever it gets hard, you need to use the rule of the excluded middle (the TND block) in a clever way

garyb commented 6 years ago

Ok thanks, I'll have a poke around!

Yeah, that's the problem I'm having with (A∨(A→⊥)→⊥)→⊥ - it's the last task before TND is introduced, and without it I have no idea :wink:

nomeata commented 6 years ago

Oh, right, that one should be solvable without. Well, I’ll let you play with it some more :-) Remember that you can use the output of a block multiple times.

garyb commented 6 years ago

Thank you! I never would have figured it out without that hint. It's been a while since I tried these though, so maybe that was necessary to solve something else and I just forgot about it.