# Formal Predicate Logic

• Oct 4th 2011, 08:35 PM
demode
Formal Predicate Logic
I need help with part (b) of the following question:

http://img208.imageshack.us/img208/7784/53878038.jpg

Attempt:

To solve this I'm trying to follow a similar worked example here. And the definition of the formal system $\displaystyle K_L$ is here.

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

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

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

1. $\displaystyle \forall x (A \to B)$ .....(Hyp)
2. $\displaystyle (\forall x (A \to B)) \to (\forall x (\neg B \to \neg A))$ .....(instance of tautology $\displaystyle ((p \to q) \to (\neg q \to \neg p))$)
3. $\displaystyle (\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.
• Oct 6th 2011, 07:59 AM
emakarov
Re: Formal Predicate Logic
A quick question: are you allowed to use the deduction theorem?
• Oct 6th 2011, 01:37 PM
emakarov
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 $\displaystyle K_L$.

• Oct 6th 2011, 04:36 PM
Soroban
Re: Formal Predicate Logic
Hello, demode!

Quote:

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

$\displaystyle \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}$

• Oct 8th 2011, 12:43 PM
demode
Re: Formal Predicate Logic
Quote:

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 $\displaystyle K_L$ goes like this: for $\displaystyle \Sigma \cup \{A\} \vdash_{K_L} B$, the derivation of $\displaystyle B$ from $\displaystyle \Sigma \cup \{A\}$ does not use an application of generalization to a free variable of $\displaystyle A$. Then $\displaystyle \Sigma \vdash_{K_L} (A \to B)$.
• Oct 8th 2011, 12:54 PM
emakarov
Re: Formal Predicate Logic
Well, as my derivation shows, $\displaystyle \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.
• Oct 8th 2011, 09:56 PM
demode
Re: Formal Predicate Logic
Quote:

Originally Posted by emakarov
Well, as my derivation shows, $\displaystyle \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)?
• Oct 9th 2011, 06:58 AM
emakarov
Re: Formal Predicate Logic
1. $\displaystyle \forall x\,(A\to B)$ Hyp
2. $\displaystyle (\forall x\,(A\to B))\to(A\to B)$ K4
3. $\displaystyle A\to B$ 1, 2, MP
4. $\displaystyle (A\to B)\to(\neg B\to\neg A)$ instance of tautology
5. $\displaystyle \neg B\to\neg$ A 3, 4, MP
6. $\displaystyle \forall x\,\neg B$ Hyp
7. $\displaystyle (\forall x\,\neg B)\to\neg B$ K4
8. $\displaystyle \neg B$ 6, 7, MP
9. $\displaystyle \neg A$ 5, 8, MP
10. $\displaystyle \forall x\,\neg A$ 9, generalization applied to x
11. $\displaystyle (\forall x\,\neg B)\to\forall x\,\neg A$ 6, 10, deduction theorem
12. $\displaystyle (\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.
• Oct 13th 2011, 03:51 AM
demode
Re: Formal Predicate Logic
I'm also stuck on a very similar question where I'm required to deduce that $\displaystyle \{\forall x \neg (A \to B) \} \vdash_{K_L} \neg (\forall x A \to B)$. And I have already shown that $\displaystyle \{\forall x \neg (A \to B) \} \vdash_{K_L} \neg B$ and $\displaystyle \{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A$. [And I want to use an instance of the tautology $\displaystyle (p \to (\neg q \to \neg (p \to q)))$]. So we have

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

2. $\displaystyle \neg B$ Hyp

3. $\displaystyle \forall x A$ Hyp

4. $\displaystyle A$ K4

5. $\displaystyle 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 $\displaystyle \forall x$ part inside the bracket with next to A in ~(A -> B)...
• Oct 13th 2011, 05:02 AM
emakarov
Re: Formal Predicate Logic
Since $\displaystyle (\forall x\,A)\to\neg B\to\neg((\forall x\,A)\to B)$ is an instance of the tautology and you have shown $\displaystyle \{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A$ and $\displaystyle \{\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 $\displaystyle \forall x\,(A\to B)$?
• Oct 13th 2011, 10:36 AM
demode
Re: Formal Predicate Logic
Quote:

Originally Posted by emakarov
Since $\displaystyle (\forall x\,A)\to\neg B\to\neg((\forall x\,A)\to B)$ is an instance of the tautology and you have shown $\displaystyle \{\forall x \neg (A \to B) \} \vdash_{K_L} \forall x A$ and $\displaystyle \{\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 $\displaystyle \forall x\,(A\to B)$?

Edit: I get it. Thank You!