I am tasked with converting to CNF:
¬[∀x : P(x)] → [∃x : ¬P(x)]
There are two main concerns I have in my attempt at this problem: My negation distribution, and whether the Skolemization is necessary here.
1. Remove implications
Before I even did this step, I was tempted to distribute the negation in the original sentence, so I would get:
[¬∀x : ¬P(x)] → [∃x : ¬P(x)]
In addition to this not being consistent with the process of converting FOL to CNF, it wasn't consistent with this discussion on Negation distribution (I think this exemplifies my shaking confidence with some aspects of FOL).
In the end, I decided to just follow the steps directly, getting:
¬[¬∀x : ¬P(x)] ∨ [∃x : ¬P(x)]
2. Move ¬ Inwards
[∀x : ¬P(x)] ∨ [∃x : ¬P(x)]
3. Standardize Variables
[∀x : ¬P(x)] ∨ [∃y : ¬P(y)]
4. Skolemization
[∀x : ¬P(x)] ∨ [ ¬P(F(y))]
Is skolemization necessary here? Although the variable x is used twice, it's used by P(x) in both cases.
5. Drop universal quantifiers
¬P(x) ∨ ¬P(F(y))
Thanks in advance!