Im reading logic books using the Hilbert-Ackerman system. When reading on predicate logic I find some equivalences such as the following:
$from:(\exists x) Px$
We get:
$\neg(\forall x)(\neg Px)$
Some books use them as definitions others just say they are equivalent. My question is: What is the correct way to proof this equivalence, are they axioms on the system or is there any way to deduct this rule?
On
In some systems they are axioms, in others they are consequences of the rules of inference. Either way, in a complete logic system, anything validated by the semantics should be something derivable by the syntax, and in a sound system, anything derivable by the syntax should be validated by the semantics.
The semantics of classical logic asserts: There is something which satisfies $P$, iff and only if, it cannot be that everything does not satisfy $P$.
Let $\Omega$ be the set of values in the universe of discussion.
Existence is a disjunctive claim about a predicate for these values. It states that the predicate is true for one value or another.
That is, $(\exists x{\in}\Omega)~P(x)$ is equivalent to $\bigvee\limits_{x\in\Omega} P(x)$.
Universality is a conjunctive claim; that the predicate is true for every value there may be.
That is, $(\forall x{\in}\Omega)~\neg P(x)$ is equivalent to $\bigwedge\limits_{x\in\Omega} \neg P(x)$.
The rest is just deMorgan's rules and mathematical induction (and a little handwaving about when the set is uncountable).
My question is: What is the correct way to proof this equivalence, are they axioms on the system or is there any way to deduct this rule?
Well, if you accept the Gentzen-style rules of inference for quantifiers introduction and elimination, you may derivate the equivalence:
$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{}{\fitch{~~1.~\exists x~P(x)\qquad\textsf{Assumption}}{\fitch{~~2.~\forall x~\neg P(x)\qquad\textsf{Assumption}}{\fitch{~~3.~[c]~P(c)\qquad\textsf{Assumption}}{~~4.~\neg P(c)\qquad\forall~\textsf{Elimination (2)}\\~~5.~\bot\qquad\neg~\textsf{Elimination (3,4)}}\\~~6.~\bot\qquad\exists~ \textsf{Elimination (1,3-5)}}\\~~7.~\neg\forall x~ \neg P(x)\qquad\neg~\textsf{Introduction (2-6)}}\\~~8.~\exists x~P(x)\to\neg \forall x~\neg P(x)\qquad\to\textsf{Introduction (1-7)}\\\fitch{~~9.~\neg\forall x~\neg P(x)\qquad\textsf{Assumption}}{\fitch{10.~\neg\exists x~P(x)\qquad\textsf{Assumption}}{\fitch{11.~[a]\qquad\qquad\textsf{Assumption}}{\fitch{12.~P(a)\qquad\textsf{Assumption}}{13.~\exists x~P(a)\qquad\exists~\textsf{Introduction (12)}\\14.~\bot\qquad\qquad\neg~\textsf{Elimination (13)}}\\15.~\neg P(a)\qquad\neg~\textsf{Introduction (12-14)}}\\16.~\forall x~P(x)\qquad\forall~\textsf{Introduction (11-15)}\\17.~\bot\qquad\qquad\neg~\textsf{Elimination (16,9)}}\\18.~\neg\neg \exists x~P(x)\quad\neg~\textsf{Introduction (10-17)}\\19.~\exists x~P(x)\qquad\qquad\neg\neg~\textsf{Elimination (18)}}\\20.~\neg\forall x~\neg P(x)\to\exists x~P(x)\quad\to~\textsf{Introduction (9-19)}\\21.~\exists x~P(x)\leftrightarrow \neg \forall x~\neg P(x)\qquad\leftrightarrow~\textsf{Introduction (8,20)}}$$
In some logic systems $\forall x$ is defined as $\neg \exists x \neg$, and in some systems, you can derive these kinds of equivalences from more basic inference principles regarding the $\forall $ and $\exists$, but most systems have a clear foral semantics for these two logical operators, so that an equivalence like $\neg \forall x P(x) \Leftrightarrow \exists x \neg P(x)$ can be proven using their formal semantics:
For any interpretation $I$ with domain $D$:
$I \vDash \neg \forall x P(x)$ iff (semantics $\neg$)
not $I \vDash \forall x P(x)$ iff (semantics $\forall$)
not for all objects $d \in D$: $I[d/c] \vDash P(c)$ iff (pure logic)
for some object $d \in D$: not $I[d/c] \vDash P(c)$ iff (semantics $\neg$)
for some object $d \in D$: $I[d/c] \vDash \neg P(c)$ iff (semantics $\exists$)
$I \vDash \exists x \neg P(x)$
Here, $I[d/c] $ is the interpretation that extends interpretation $I$ by interpreting a new constant symbol $c$ as object $d$
Since we have that for any interpretation $I$: $I \vDash \neg \forall x P(x)$ iff $I \vDash \exists x \neg P(x)$ we have that $\neg \forall x P(x) \Leftrightarrow \exists x \neg P(x)$
Notice though how in the 'pure logic' step we basically do the same logic as that we are trying to prove, which is that if not everything has some property, then there is something that does not have that property, and vice versa. And that more informal way of looking at it may well be the most understandable way to explain why $\neg \forall x P(x) \Leftrightarrow \exists \neg P(x)$. But as the above shows, there is a purely formal/mathematical way of proving the equivalence.