proving{$\neg(\forall x)\alpha \rightarrow \alpha$}$\models$$(\forall x)\alpha$

Question

prove {$\neg(\forall x)\alpha \rightarrow \alpha$}$\vdash\space(\forall x)\alpha$

Im not sure what is the convention, so to be clear I am talking about proving the formula from the seven axiom schemes:
$(A_1) \alpha \rightarrow(\beta \rightarrow \alpha)$
$(A_2) (\alpha \rightarrow(\beta \rightarrow \gamma))\rightarrow((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma)) $
$(A_3) (\neg\beta \rightarrow\neg\alpha)\rightarrow((\neg\beta \rightarrow \alpha)\rightarrow\beta)$
$(A_4) (\forall x)\alpha\rightarrow \alpha(t)$ where $x\in FV(\alpha)$ and $\alpha(t)$ is the subtition of $t$ to all appearances of $x$ in $\alpha$
$(A_5) (\forall x)(\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow(\forall x)\beta))$ when $x\not\in FV(\alpha)$
$(A_6) (\forall x)x=x$
$(A_7) x=y\rightarrow(\alpha\rightarrow\alpha<y>)$ where $y\in FV(\alpha)$ and $\alpha<y>$ is the subtition of $y$ to some appearances of $x$ in $\alpha$

and the deduction rules (not sure about the accepted term but I hope you will understand) are:
if $\alpha$ appeared in the proof then it is eligible to use $(\forall x)\alpha$ and
if $\alpha\rightarrow\beta$ and $\alpha $appeared in the proof then it is eligible to use $\beta$

sorry if I misused some of the terms and if it's not a burden I'd like to be corrected.

Answer 1

See Elliott Mendelson, Introduction to mathematical logic (4ed - 1997), page 69.

We need at least a third propositional axiom, like :

(A3) --- $(\lnot γ → \lnot β) → ((\lnot γ → β) → γ)$

to be able to prove all tautologies.

In addition, I assume two axioms for the predicate calculus (and two further axioms for equality : we do not need them here) :

(A4) --- $\forall x \alpha(x) \rightarrow \alpha (t)$, where $t$ is a term free for $x$ in $\alpha(x)$

(A5) --- $(∀x(\alpha → \beta) → (\alpha → ∀x \beta))$, where $x$ is not free in $\alpha$.

We need also inference rules :

• modus ponens

• generalization : form $\alpha$, $\forall x \alpha$ follows.

Proof

(1) $\lnot \forall x \alpha \rightarrow \alpha$ --- assumed

(2) $\lnot \alpha \rightarrow \forall x \alpha$ --- form (1) using the tautology : $(\lnot \varphi \rightarrow \psi) \rightarrow (\lnot \psi \rightarrow \varphi)$ and modus ponens

(3) $\forall x \alpha \rightarrow \alpha$ --- by axion (A4), with $x$ as $t$

(4) $\lnot \alpha \rightarrow \lnot \forall x \alpha$ --- from (3) as above

(5) $\alpha$ --- from axiom (A3) with (4) and (2), by mp twice

(6) $\forall x \alpha$ --- from (5) by generalization

Thus, form (1) and (6) :

$\lnot \forall x \alpha \rightarrow \alpha \vdash \forall x \alpha$.

---

Note

In order to conclude from the above formula, by soundness, that :

$\lnot \forall x \alpha \rightarrow \alpha \vDash \forall x \alpha$

we have to check if the fine details regarding the definitions of satisfaction and logical consequence are consistent with those in Mendelson's book.

---

Comment

To prove the tautology : $(\lnot \varphi \rightarrow \psi) \rightarrow (\lnot \psi \rightarrow \varphi)$ we need some extra-work.

See this post for the "basic tools" according to Mendelson's proof system :

$\vdash \varphi \rightarrow \varphi$, Deduction Theorem, Syllogism and Double Negation laws.

With these theorems available, it is easy to prove the above tautology.