A quick question: are you allowed to use the deduction theorem?
I need help with part (b) of the following question:
Attempt:
To solve this I'm trying to follow a similar worked example here. And the definition of the formal system is here.
So, we know that is a tautology since:
Now, I guess the first step is to show that .
1. .....(Hyp)
2. .....(instance of tautology )
3. .....(1,2, Modus Ponen)
4. ...
I'm stuck at this point... How should I continue? Any help is appreciated.
1. Hyp
2. K4
3. 1, 2, MP
4. instance of tautology
5. A 3, 4, MP
6. Hyp
7. K4
8. 6, 7, MP
9. 5, 8, MP
10. 9, generalization applied to x
11. 6, 10, deduction theorem
12. 1, 11, deduction theorem
In step 10, similar to part (c) of the example, generalization is a rule that must have been derived using K5. It applies to x, which is not free in either of the assumptions, so one can use the deduction theorem in steps 11 and 12.
I'm also stuck on a very similar question where I'm required to deduce that . And I have already shown that and . [And I want to use an instance of the tautology ]. So we have
1. Hyp
2. Hyp
3. Hyp
4. K4
5. Taut
Any ideas how to proceed? I even tried K5, but to no avail... I don't see a way to get the part inside the bracket with next to A in ~(A -> B)...