Prove without the completeness theorem that for every formula $A$ and variables $x,y,z$, it holds that $$\lnot\forall x\lnot A\left\{ x/z\right\} \vdash_{HC}\lnot\forall y\lnot A\left\{ y/z\right\} $$
The axioms we are given for
- Ax1 $A\to\left(B\to A\right)$
- Ax2 $\left(A\to\left(B\to C\right)\right)\to\left(\left(A\to B\right)\to\left(A\to C\right)\right)$
- Ax3 $\left(\lnot B\to\lnot A\right)\to\left(\left(\lnot B\to A\right)\to B\right)$
- Ax4 $\left(\forall xA\left(x\right)\right)\to A\left\{ t/x\right\}$ for a term $t$.
- Ax5 $\left(\forall x\left(A\to B\right)\right)\to\left(A\to\forall xB\right)$, where x is not free in A.
With two inference rules:
- MP Derive $B$ from $A$ and $A\to B$
- Gen Derive $\forall xA$ from $A$
We have also proven the Deduction, Dichotomey and Compactness theorems.
My issue is that I don't see much intuition behind the axioms, lacking any experience with these sort of proofs and as such have no idea even how to start. The fourth axiom looks the most relevant, so I assume I should first substitute and then generalize somehow, but then how do I deal with the negation signs?
Hint
1) $\forall y \ \lnot A[y/z]$ --- premise
2) $\lnot A[x/z]$ --- from 1) and Ax4 and MP
3) $\forall x \lnot A[x/z]$ --- from 2) by Gen
4) $\vdash \forall y \ \lnot A[y/z] \to \forall x \lnot A[x/z]$ --- from 1) and 3) by Ded Th
Note : contraposition is the tautology: $(A \to B) \to (\lnot B \to \lnot A)$.
The proof system is that of Mendelson's textbook: you can find it as Lemma 1.11 e), page 31.
Comment: how can we avoid the Ded Th ?.
Assume that $x$ is not free in $\forall y \ \lnot A[y/z]$.
By Ax4: $\vdash \forall y \ \lnot A[y/z] \to \lnot A[x/z]$ and by Gen: $\vdash \forall x \ (\forall y \ \lnot A[y/z] \to \lnot A[x/z])$.
By Ax5: $\vdash \forall y \ \lnot A[y/z] \to \forall x \ \lnot A[x/z]$; then contrapose to get: $\vdash \lnot \forall x \ \lnot A[x/z] \to \lnot \forall y \ \lnot A[y/z]$.