De Morgan's Laws (Predicate Logic)/Denial of Universality/Formulation 2/Forward Implication

Theorem

Let $\forall$ and $\exists$ denote the universal quantifier and existential quantifier respectively.

Then:

$\vdash \neg \paren {\forall x: \map P x} \implies \paren{ \exists x: \neg \map P x }$

Proof

This proof is derived in the context of the following proof system: Hilbert Proof System Instance 1 for Predicate Logic.

By the tableau method:

$\vdash \neg \paren {\forall x: \map P x} \implies \paren{ \exists x: \neg \map P x }$
Line Pool Formula Rule Depends upon Notes
1 1 $\neg\neg \map P c \vdash \map P c$ Premise (None) Axiom 1: Propositional Tautology, $c$ arbitrary
2 $\forall x: \neg\neg \map P x \vdash \neg\neg \map P c$ Universal Instantiation
3 $\forall x: \neg\neg \map P x \vdash \map P c$ Theorem Introduction (None) from 1, 2, Provable Consequence of Theorems is Theorem
4 $\forall x: \neg\neg \map P x \vdash \forall x: \map P x$ Universal Generalisation 3
5 $\paren{ \forall x: \neg\neg \map P x } \implies \forall x: \map P x$ Theorem Introduction (None) from 4, Deduction Theorem for Hilbert Proof System for Predicate Logic
6 $\neg \paren{ \forall x: \map P x } \implies \neg \paren{ \forall x: \neg\neg \map P x }$ Theorem Introduction (None) from 5, Rule of Transposition
7 7 $\paren{ \forall x: \neg \neg \map P x } \iff \neg \paren{ \exists x: \neg \map P x }$ Premise (None) Axiom 6
8 $\neg \paren{ \exists x: \neg \map P x } \implies \paren{ \forall x: \neg \neg \map P x }$ Biconditional Elimination: $\iff \EE_2$ 7
9 $\neg \paren{ \forall x: \neg\neg \map P x } \implies \paren{ \exists x: \neg \map P x }$ Theorem Introduction (None) from 8, Rule of Transposition
10 $\neg \paren {\forall x: \map P x} \implies \paren{ \exists x: \neg \map P x }$ Theorem Introduction (None) from 6, 9, Hypothetical Syllogism

$\blacksquare$