# Thread: Natural Deduction: Predicate Logic. Need help!

1. ## Natural Deduction: Predicate Logic. Need help!

I have a question about Natural Deduction for Predicate Logic.

|-- Ǝx. ~P(x) ---> ~∀x. P(x) [ ~ = not ]

How about do you solve this, as I'm really getting a headache in figuring it out. The reason is that it contains no premises and just the conclusion, but my lecturer said it is solvable.

Does Ƚ can be assumed as ~∀x. P(x) (from ȽE)?

2. ## Re: Natural Deduction: Predicate Logic. Need help!

Originally Posted by nash160
|-- Ǝx. ~P(x) ---> ~∀x. P(x)
Do you mean "(Ǝx. ~P(x)) ---> ~∀x. P(x)" or "Ǝx. (~P(x) ---> ~∀x. P(x))"? I personally like the convention where the scope of ∀ is as small as possible, so that "Ǝx ~P(x) ---> ~∀x P(x)" means "(Ǝx ~P(x)) ---> ~∀x P(x)," but when a quantifier is followed by a dot, then its scope extends as far as possible, so that "Ǝx. ~P(x) ---> ~∀x. P(x)" means "Ǝx (~P(x) ---> ~∀x P(x))."

Assuming you need (Ǝx ~P(x)) ---> ~∀x P(x), an informal proof is as follows. Assume Ǝx ~P(x) and break into into some x and a proof of ~P(x) using existential elimination. To prove ~∀x P(x), assume ∀x P(x). Instantiate it with x to get P(x). It gives a contradiction with ~P(x). Closing the assumption ∀x P(x), we get ~∀x P(x).

Do you need a Fitch-style or tree-like derivation?

Originally Posted by nash160
Does Ƚ can be assumed as ~∀x. P(x) (from ȽE)?
What do you mean by Ƚ and ȽE?

3. ## Re: Natural Deduction: Predicate Logic. Need help!

I meant it as " (Ǝx ~P(x)) ---> ~∀x P(x) ".

Does a tree-like derivation look something like,

Solve,

Code:
∀x.P(x), ∀x.Q(x) |-  ∀x.(P(x) ^ Q(x))
Code:
| ∀x P(x)                1.
| ∀x Q(x)                  2.
|--------
|     | [c]                3.
|     |----
|     | P(c)              4. ∀E: 1
|     | Q(c)                5.  ∀E:2
|     | P(c) ^ Q(c)        6. ^I: 4,5
|  ∀x(P(x) ^ Q(x))        7. ∀I: 3-6

By "Ƚ", I meant one of the negation rule "ȽE" where "Ƚ" can be used for assumption.

4. ## Re: Natural Deduction: Predicate Logic. Need help!

Originally Posted by nash160
Does a tree-like derivation look something like,

∀x.P(x), ∀x.Q(x) |- ∀x.(P(x) ^ Q(x))

| ∀x P(x) 1.
| ∀x Q(x) 2.
|--------
| | [c] 3.
| |----
| | P(c) 4. ∀E: 1
| | Q(c) 5. ∀E:2
| | P(c) ^ Q(c) 6. ^I: 4,5
| ∀x(P(x) ^ Q(x)) 7. ∀I: 3-6
This is a Fitch-style derivation. Tree-like derivations look like the one in this post.

Originally Posted by nash160
By "Ƚ", I meant one of the negation rule "ȽE" where "Ƚ" can be used for assumption.
I am still not sure what the crossed L has to do with natural deduction rules. To prove ~∀x. P(x), indeed, you assume ∀x. P(x) and arrive at contradiction. This is probably called negation introduction rule.

5. ## Re: Natural Deduction: Predicate Logic. Need help!

I just used that symbol because I can't find the symbol that fits it. Sorry for the confusion. The symbol I was looking for is an upside down T That's what I meant.

6. ## Re: Natural Deduction: Predicate Logic. Need help!

Originally Posted by nash160
I just used that symbol because I can't find the symbol that fits it. Sorry for the confusion. The symbol I was looking for is an upside down T That's what I meant.
$$\bot$$ gives $\displaystyle \bot$.

7. ## Re: Natural Deduction: Predicate Logic. Need help!

Originally Posted by Plato
$$\bot$$ gives $\displaystyle \bot$.
Thanks, will keep that in mind!

8. ## Re: Natural Deduction: Predicate Logic. Need help!

This was how I solved it, and I'm not sure if it's correct...

Code:
1.   |
2.   |--------
3.   |     | Ǝx.~P(x)
4.   |     |----
5.   |     |  |  [c]
6.   |     |  |  ~P(c)
7.   |     |  |------
8.   |     |  |  |  ∀x.P(x)
9.   |     |  |  |------
10.  |     |  |  |  P(c)                       ∀E: 9
11.  |     |  |  |  _L                         _LI: 6,10
12.  |     |  |  ~∀x.P(x)                   ~I: 8-11
13.  |     |  ~∀x.P(x)                      ƎE: 3,5-12
14.  |   (Ǝx.~P(x)) ---> ~∀x.P(x)     -->I:3-13
btw, _L is $\displaystyle \bot$. It appears as an image, so it messed up the indent..

9. ## Re: Natural Deduction: Predicate Logic. Need help!

Seems OK. This is not a remark about this derivation, but the rule deriving ⊥ from A and ~A should be called ~E. In some precise sense it is dual to ~I. In fact, if ~A is considered an abbreviation for A -> ⊥, then ~I becomes ->I and ~E becomes ->E. As for ⊥, it has an elimination rule but no introduction rule.

10. ## Re: Natural Deduction: Predicate Logic. Need help!

Cheers, so does it mean that my working is acceptable?

Oh btw, I was following the rules that my lecturer provided for us. Here's the screenshot

As an alternative to my answer above (I will post it soon) from using ⊥E, can it be safe to assume ⊥ = "~∀x.P(x)" ?

11. ## Re: Natural Deduction: Predicate Logic. Need help!

Originally Posted by nash160
Cheers, so does it mean that my working is acceptable?
I think it's fine. One thing is that I am not sure it is necessary to number lines that don't have formulas.

Originally Posted by nash160
Oh btw, I was following the rules that my lecturer provided for us.
Rule names is not a big deal.

Originally Posted by nash160
As an alternative to my answer above (I will post it soon) from using ⊥E, can it be safe to assume ⊥ = "~∀x.P(x)" ?
I am nor sure I understand "As an alternative to my answer... from using ⊥E." Did you use ⊥E? And of course ⊥ and ~∀x.P(x) are completely different formulas.