Proposed inference rule of First Order Logic

Question

I am asked to consider this as a proposed inference rule of FOL: ~P(a) . . . . ~∀xP(x)

I am having trouble interpreting the proposed rule as one that "will always" produce correct inferences? As in,could this be added to the existing inference rules in Fitch without producing some mistaken inferences?

I want to assume that it won't be the case because ~P(a) isn't the same logic of what is being followed but am unsure.

Answer 1

I assume that the exercise asks you to consider the proposed rule:

from $\lnot Pa$, derive $\lnot \forall x \ Px$

and check if it is "correct" (or sound), i.e. truth-preserving: from a true premise it never derives a false conclusion.

Consider an interpretation with domain $D$.

If the premise $\lnot Pa$ is true in $D$, this means that there is an object in $D$, call it $a^D$, such that $P$ does not hold of it.

This means that it is not true that $P$ holds of every object in the domain $D$ of the interpretation (because it does not hold of at least $a^D$), i.e. that $\forall x \ Px$ is false in it.

---

Recall that: $\lnot \forall x$ is equivalent to: $\exists x \lnot$.

Answer 2

Hint: If you are allowed rules for existential generalization, quantifier switch and removal of double negation, then you can derive the theorem:

$\forall a:[\neg P(a) \implies \neg \forall x:P(x)]$

So, there would be no need for your proposed rule.