1. Formal Predicate Logic

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 $K_L$ is here.

So, we know that $((p \to q) \to (\neg q \to \neg p))$ is a tautology since:

$(p \to q) \iff (\neg p \vee q)$
$\iff (q \vee \neg p)$
$\iff (\neg \neg q \vee \neg p)$
$\iff (\neg q \to \neg p)$

Now, I guess the first step is to show that $\{ \forall x (A \to B), \neg(\forall x \neg B) \} \vdash_{K_L} \neg \forall x \neg A$.

1. $\forall x (A \to B)$ .....(Hyp)
2. $(\forall x (A \to B)) \to (\forall x (\neg B \to \neg A))$ .....(instance of tautology $((p \to q) \to (\neg q \to \neg p))$)
3. $(\forall x (\neg B \to \neg A))$ .....(1,2, Modus Ponen)
4. ...

I'm stuck at this point... How should I continue? Any help is appreciated.

2. Re: Formal Predicate Logic

A quick question: are you allowed to use the deduction theorem?

3. Re: Formal Predicate Logic

I should have looked at the example. If you can use the deduction theorem and generalization, it's pretty easy. Let me post a derivation in natural deduction. It is straightforward to convert it to a derivation in $K_L$.

4. Re: Formal Predicate Logic

Hello, demode!

$\text{Verify that }\,(p \to q) \to (\sim\!q\to\:\sim\!p)\,\text{ is a tautology.}$

$\begin{array}{cccccccccc}1. & (p \to q) \to (\sim\!q \to\: \sim\!p) && 1. & \text{Given} \\ 2. & (\sim\!p \vee q) \to (q\: \vee \sim\! p) && 2. & \text{Def. impl'n} \\ 3. & \sim(\sim\!p \vee q) \vee (q\: \vee \sim\!p) && 3. & \text{Def. Impl'n} \\ 4. & (p \:\wedge \sim\!q) \vee (q\: \vee \sim\!p) && 4. & \text{DeMorgan} \\ 5. & [(p\: \wedge \sim\!q) \vee q]\: \vee \sim\!p && 5. & \text{Assoc.} \\ 6. & [(p \vee q) \wedge (\sim\!q \vee q)]\: \vee \sim\!p && 6. & \text{Distr.} \\ 7. & [(p\vee q) \wedge T]\: \vee \sim\!p && 7. & s\: \vee\! \sim\!s \:=\:T \\ 8. & (p \vee q)\: \vee \sim\!p && 8. & s \wedge T \:=\:s \\ 9. & (p\: \vee \sim\!p) \vee q && 9. & \text{Comm, Assoc.} \\ 10. & T \vee q && 10. & s\: \vee\!\sim\!s \:=\:T \\ 11. & T && 11. & T \vee s \:=\:T \end{array}$

5. Re: Formal Predicate Logic

Originally Posted by emakarov
A quick question: are you allowed to use the deduction theorem?
I think we are required to follow the given example very closely. But yes we can use the Deduction Theorem. The deduction theorem for $K_L$ goes like this: for $\Sigma \cup \{A\} \vdash_{K_L} B$, the derivation of $B$ from $\Sigma \cup \{A\}$ does not use an application of generalization to a free variable of $A$. Then $\Sigma \vdash_{K_L} (A \to B)$.

6. Re: Formal Predicate Logic

Well, as my derivation shows, $\forall x\,(A\to B),\forall x\,\neg B\vdash\neg A(x)$. Then you use generalization on x. Note that x does not occur free in the assumptions, so you can apply the deduction theorem.

7. Re: Formal Predicate Logic

Originally Posted by emakarov
Well, as my derivation shows, $\forall x\,(A\to B),\forall x\,\neg B\vdash\neg A(x)$. Then you use generalization on x. Note that x does not occur free in the assumptions, so you can apply the deduction theorem.
I really appreciate your response. But I'm having some trouble following your derivation in post #3, could you please show it in the simple format (like the one in my post)?

8. Re: Formal Predicate Logic

1. $\forall x\,(A\to B)$ Hyp
2. $(\forall x\,(A\to B))\to(A\to B)$ K4
3. $A\to B$ 1, 2, MP
4. $(A\to B)\to(\neg B\to\neg A)$ instance of tautology
5. $\neg B\to\neg$ A 3, 4, MP
6. $\forall x\,\neg B$ Hyp
7. $(\forall x\,\neg B)\to\neg B$ K4
8. $\neg B$ 6, 7, MP
9. $\neg A$ 5, 8, MP
10. $\forall x\,\neg A$ 9, generalization applied to x
11. $(\forall x\,\neg B)\to\forall x\,\neg A$ 6, 10, deduction theorem
12. $(\forall x\,(A\to B))\to(\forall x\,\neg B)\to\forall x\,\neg A$ 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.

9. Re: Formal Predicate Logic

I'm also stuck on a very similar question where I'm required to deduce that $\{\forall x \neg (A \to B) \} \vdash_{K_L} \neg (\forall x A \to B)$. And I have already shown that $\{\forall x \neg (A \to B) \} \vdash_{K_L} \neg B$ and $\{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A$. [And I want to use an instance of the tautology $(p \to (\neg q \to \neg (p \to q)))$]. So we have

1. $\neg(A \to B)$ Hyp

2. $\neg B$ Hyp

3. $\forall x A$ Hyp

4. $A$ K4

5. $A \to (\neg B \to \neg (A \to B))$ Taut

Any ideas how to proceed? I even tried K5, but to no avail... I don't see a way to get the $\forall x$ part inside the bracket with next to A in ~(A -> B)...

10. Re: Formal Predicate Logic

Since $(\forall x\,A)\to\neg B\to\neg((\forall x\,A)\to B)$ is an instance of the tautology and you have shown $\{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A$ and $\{\forall x \neg (A \to B) \} \vdash_{K_L} \neg B$, then what's the problem? Just use MP twice. Or do you need to derive $\forall x\,(A\to B)$?

11. Re: Formal Predicate Logic

Originally Posted by emakarov
Since $(\forall x\,A)\to\neg B\to\neg((\forall x\,A)\to B)$ is an instance of the tautology and you have shown $\{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A$ and $\{\forall x \neg (A \to B) \} \vdash_{K_L} \neg B$, then what's the problem? Just use MP twice. Or do you need to derive $\forall x\,(A\to B)$?
Edit: I get it. Thank You!