-1

I'm trying to solve this box-proof puzzle but I don't understand how to complete it as I need to somehow assume $A0$ or $\neg\neg B2$.

Solving a box proof in Jape

I've used a truth-table solver to confirm that this is a tautology so it must be solvable using box proofs:

$$(\neg\neg C\to C)\to ((\neg\neg D\to D)\to ((\neg\neg E\to E)\to (((A\to C)\to D)\to (((A\to C)\to C)\to D)\to (((B\to D)\to E)\to ((((B\to C)\to D)\to E)\to E)))))$$

Shaun
  • 44,997
Ozzy
  • 385

1 Answers1

0

You shouldn't understand how to complete this. I don't know what you did with the truth table or the write-up of this question.

The first three assumptions qualify as tautologies and also theorems in terms of "box proofs". So, they end up automatically true or provable. The last six assumptions are

  1. [(ao→bo)→b1]

  2. {[(ao→bo)→bo]→b1}

  3. [(a1→b1)→b2]

  4. {[(a1→b0)→b1]→b2}

  5. (a1→b0)

  6. (ao→bo)

Suppose b2 true, b1 true, a1 false, a0 false, and b0 false. Then the last 6 assumptions are true, but b0 is false. Consequently, you can't prove b0.

Doug Spoonwood
  • 11,211
  • The point was to solve it using box proofs, and yes I don't need to know how to complete this but I do want to know, thanks. – Ozzy Nov 26 '13 at 19:28
  • @Ozzy You can't solve this using box proofs. The argument isn't valid (all the assumptions can hold true and the conclusion got to before using any conditional introduction can hold false). A box proof can get written if and only if there exists that sort of valid argument. There is no such valid argument here, and consequently no one can solve it using such box proofs with sound rules of inference. – Doug Spoonwood Nov 26 '13 at 21:27
  • I was informed it was solvable using classical contradiction but otherwise I couldn't see how it could be solved either – Ozzy Nov 27 '13 at 21:58