Prove by Hilbert deduction: $\vdash _{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$

I'd really like your help proving:

$\vdash_{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$

Where $HFOL$ is the proof system which contains the Hilbert relevant axioms:

1. $A\rightarrow(B \rightarrow A)$
2. $(A\rightarrow(B\rightarrow C))\to((A\rightarrow B)\rightarrow(A\rightarrow C))$
3. $(A\rightarrow B)\rightarrow ((A\rightarrow\bar{B})\rightarrow \bar{A})$
4. $\bar{\bar{A}} \rightarrow A$

Plus the following two axioms:

$\forall x(B\to A)\to (\exists xB \to A)$

$\forall x(A \to B) \to (A \to \forall x B)$

Restricted to use only while $x$ is not a free variable in $A$.

And other two axioms: $\forall xA \to A \{ t/x \}$, $A\{t/x\} \to \exists xA$ where $t$ is free for assignment instead of $x$ in $A$.

Finally theres the $MP$ rule: From $A, A\to B$ we conclude $B$ and the Gen rule which from $A$ we conclude $\forall xA$.

I tried couple of different ways but didn't come with any smart result.

Any suggestions?

-
\$\neg\$ to get $\neg$ –  Git Gud May 25 '13 at 10:00
you don't have any rule talking about $\neg$. Is it a short-hand for something else ? Is $\neg \phi$ the same as $\bar \phi$ ? –  mercio May 27 '13 at 12:40
@mercio: yes, it is. –  Jozef May 27 '13 at 12:58

3 Answers

Jozef, forgive the clumsiness of my notation, since I'm not used to HFOL,I enjoyed the challenge. I also provided a second proof in Dijsktra's Style, since I found it an useful aid to my intuition, since you mentioned that you tried many things without luck. It may prove useful.

Proof in HFOL:

$\forall x(\neg (A\rightarrow \neg B))\vdash\neg (\forall xA\rightarrow \neg \forall xB)$

Knowing $(A\rightarrow B)\rightarrow ((A\rightarrow \neg B)\rightarrow \neg A)$, we could try:

$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash \neg (A\rightarrow \neg B), (A\rightarrow \neg B)$

I picked $\neg (A\rightarrow \neg B), (A\rightarrow \neg B)$ because we can get $\neg (A\rightarrow \neg B)$ it easily.

We get $\neg (A\rightarrow \neg B)$ from $\forall x(\neg (A\rightarrow \neg B))$ and $\forall xA\rightarrow A{t/x}$.

Now for the tricky part. $A\rightarrow \neg B$

$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash A\rightarrow \neg B$

Knowing the MP rule we could try:

$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB,A\vdash \neg B$

We get $\forall xA$ from $A$ and the Gen rule.

We get $\neg \forall xB$ from $\forall xA$, $\forall xA\rightarrow \neg \forall xB$ and the MP rule.

We get $\neg B$ from $\neg \forall xB$ and $\forall xA\rightarrow A\lbrace{ t/x\rbrace}$.

Done.

Now in Dijkstra's Style.

$\forall x(\neg (A \rightarrow \neg B))\rightarrow \neg (\forall xA \rightarrow \neg \forall xB)$

$=\lbrace p\rightarrow q = \neg p\vee q \rbrace$

$\forall x(\neg (\neg A \vee \neg B)) \rightarrow \neg (\neg \forall xA \vee \neg \forall xB)$

$=\lbrace de Morgan\rbrace$

$\forall x(A \wedge B)\rightarrow (\forall xA \wedge \forall xB)$

$=\lbrace Distributivity\,\, of \,\, \forall\,\, over\,\, \wedge \rbrace$

$(\forall xA \wedge \forall xB)\rightarrow (\forall xA \wedge \forall xB)$

Done.

Edit: To clarify why I found the second proof useful for aiding my intuition. As you can see this proof is considerately shorter. This is because the style allows more general laws (instead of a minimal set of axioms) and because it prefers rules that avoid case analysis. This means that it is far easier to prove something in this style.

Now, to me, the hardest step in my first proof was:

$\forall x(\neg (A\rightarrow \neg B)), \forall xA\rightarrow \neg \forall xB\vdash \neg (A\rightarrow \neg B), (A\rightarrow \neg B)$

I knew I had to apply $(A\rightarrow B)\rightarrow ((A\rightarrow \neg B)\rightarrow \neg A)$ But I had to decide, what formula to use as $B$.

Going back to my second proof, $\forall x(\neg (A \rightarrow \neg B))$ and $\neg (\forall xA \rightarrow \neg \forall xB)$ are equal. That meant that whatever I could prove with one, I could prove with the other.

So, when I notice I could prove $\neg (A \rightarrow \neg B)$ from $\forall x(\neg (A \rightarrow \neg B))$, I knew I could prove the opposite from $(\forall xA \rightarrow \neg \forall xB)$. This reduced the amount of things to try immensely.

-

Well, you can use the deduction theorem because ∀x(¬(A→¬B)) has no free variables. After using it you get: ∀x(¬(A→¬B))⊢HFOL¬(∀xA→¬(∀xB))

Now we will build a proof in HFOL:

1. ∀x(¬(A→¬B)) - by assumption.
2. ∀x(¬(A→¬B))→¬(A→¬B) - first axiom.
3. ¬(A→¬B) - MP on 1,2.
4. ¬(A→¬B)→A - because you can prove it on hpc.
5. A - MP on 3,4.
6. ∀xA - Gen on 5.
7. ¬(A→¬B)→B - because you can prove it on hpc.
8. B - MP on 3,7.
9. ∀xB - Gen on 8.
10. ¬(∀xA→¬(∀xB)) - because you can prove it on hpc.
-

Conventions 1.
1. We abbreviate the symbol $\vdash_\mbox{HFOL}$ by $\vdash$.
2. We abbreviate the term wff of HFOL by wff.
3. We denote a formal proof as a deduction, and a metaproof as a proof.
4. When giving abbreviated deductions, we refer to subdeductions by citing lemmata.

Since the Lemmata 1 and 2 are used in the proof of the Deduction Theorem, we will not presuppose the Deduction Theorem in their proofs.

Lemma 1. Let $A$ be a wff.
Then $\vdash A \rightarrow A$.

Proof. We will give a deduction.
$$\begin{array}{lll} 1. & (A \rightarrow ((A \rightarrow A) \rightarrow A)) \rightarrow & \\ & ((A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)) & \mbox{Axiom schema 2} \\ 2. & A \rightarrow ((A \rightarrow A) \rightarrow A) & \mbox{Axiom schema 1} \\ 3. & (A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A) & \mbox{MP: 2, 1} \\ 4. & A \rightarrow (A \rightarrow A) & \mbox{Axiom schema 1} \\ 5. & A \rightarrow A & \mbox{MP: 4, 3} \end{array}$$ Thus, we can conclude that $\vdash A \rightarrow A$.

Q.E.D.

Lemma 2. Let $A$, $B$, and $C$ be wffs.
Then $A \rightarrow B, B \rightarrow C \vdash A \rightarrow C$.

Proof. We will give a deduction.
$$\begin{array}{lll} 1. & A \rightarrow B & \mbox{Hyp} \\ 2. & B \rightarrow C & \mbox{Hyp} \\ 3. & (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) & \mbox{Axiom schema 2} \\ 4. & (B \rightarrow C) \rightarrow (A \rightarrow (B \rightarrow C)) & \mbox{Axiom schema 1} \\ 5. & A \rightarrow (B \rightarrow C) & \mbox{MP: 2, 4} \\ 6. & (A \rightarrow B) \rightarrow (A \rightarrow C) & \mbox{MP: 5, 3} \\ 7. & A \rightarrow C & \mbox{MP: 1, 6} \end{array}$$ Thus, we can conclude that $A \rightarrow B, B \rightarrow C \vdash A \rightarrow C$.

Q.E.D.

Definition 1 (Depends on). Let $B_1, \ldots, B_k$ be a deduction, and let $A$ and $C$ be wffs.

1. A subset $M$ of $\{ B_1, \ldots, B_k \}$ is called inductive if and only if the following three properties are satisfied:
• If $A$ is some hypothesis of the deduction $B_1, \ldots, B_k$, then $A \in M$.
• If for $1 \leq i \leq k$, $B_i$ is a direct consequence by MP of some wffs $B_p$ and $B_q$ with $1 \leq p < i$, $1 \leq q < i$, and $\{ B_p, B_q \} \cap M \neq \emptyset$, then $B_i \in M$.
• If for $1 \leq i \leq k$, $B_i$ is a direct consequence by Gen of some wff $B_p \in M$ with $1 \leq p < i$, then $B_i \in M$.
2. Let $D = \bigcap \{ M | \mbox{$M$is an inductive set} \}$.
3. The wff $C$ is said to depend on $A$ for $B_1, \ldots, B_k$ if and only if $C \in D$.

Remark. The set $D$ is well-defined since $\{ B_1, \ldots, B_k \}$ is an inductive set.

Proposition 1 (Deduction Theorem). Let $\Gamma$ be a set of wffs, and let $A$ and $B$ be wffs. Assume that in some deduction $B_1, \ldots, B_k$ showing that $\Gamma, A \vdash B$, no application of Gen to a wff that depends on $A$ for $B_1, \ldots, B_k$ has as its quantified variable a free variable of $A$. Then $\Gamma \vdash A \rightarrow B$.

Proof. See the constructive proof in the book [1]. It uses only properties of the book author's formal theory K that are also given by the formal theory HFOL.

Lemma 3. Let $A$ and $B$ be wffs.
Then $A \vdash (A \rightarrow B) \rightarrow B$.

Proof. Since $A, A \rightarrow B \vdash B$ by MP, we can apply the Deduction Theorem and conclude that $A \vdash (A \rightarrow B) \rightarrow B$.

Q.E.D.

Lemma 4. Let $A$ and $B$ be wffs. Then
1. $A, B \rightarrow \neg A \vdash \neg B$.
2. $\vdash (B \rightarrow \neg A) \rightarrow (A \rightarrow \neg B)$.
3. $A \vdash \neg \neg A$.
4. $\vdash A \rightarrow \neg \neg A$.
5. $\neg A, \neg B \rightarrow A \vdash B$.
6. $\vdash (\neg B \rightarrow A) \rightarrow (\neg A \rightarrow B)$.
7. $A, \neg A \vdash B$.
8. $\vdash \neg A \rightarrow (A \rightarrow B)$.

Proof. Ad 1. We will give a deduction.
$$\begin{array}{lll} 1. & A & \mbox{Hyp} \\ 2. & B \rightarrow \neg A & \mbox{Hyp} \\ 3. & A \rightarrow (B \rightarrow A) & \mbox{Axiom schema 1} \\ 4. & B \rightarrow A & \mbox{MP: 1, 3} \\ 5. & (B \rightarrow A) \rightarrow ((B \rightarrow \neg A) \rightarrow \neg B) & \mbox{Axiom schema 3} \\ 6. & (B \rightarrow \neg A) \rightarrow \neg B & \mbox{MP: 4, 5} \\ 7. & \neg B & \mbox{MP: 2, 6} \end{array}$$ Thus, we can conclude that $A, B \rightarrow \neg A \vdash \neg B$, as was required.

Ad 2. Applying two times the Deduction Theorem to Lemma 4.1, we can conclude that Lemma 4.2 holds, as was required.

Ad 3. We will give an abbreviated deduction.
$$\begin{array}{lll} 1. & A & \mbox{Hyp} \\ 2. & A \rightarrow (\neg A \rightarrow A) & \mbox{Axiom schema 1} \\ 3. & \neg A \rightarrow A & \mbox{MP: 1, 2} \\ 4. & \neg A \rightarrow \neg A & \mbox{Lemma 1} \\ 5. & (\neg A \rightarrow A) \rightarrow ((\neg A \rightarrow \neg A) \rightarrow \neg \neg A) & \mbox{Axiom schema 3} \\ 6. & (\neg A \rightarrow \neg A) \rightarrow \neg \neg A & \mbox{MP: 3, 5} \\ 7. & \neg \neg A & \mbox{MP: 4, 6} \end{array}$$ Thus, we can conclude that $A \vdash \neg \neg A$, as was required.

Ad 4. Applying the Deduction Theorem to Lemma 4.3, we can conclude that $\vdash A \rightarrow \neg \neg A$, as was required.

Ad 5. We will give an abbreviated deduction.
$$\begin{array}{lll} 1. & \neg A & \mbox{Hyp} \\ 2. & \neg B \rightarrow A & \mbox{Hyp} \\ 3. & A \rightarrow \neg \neg A & \mbox{Lemma 4.4} \\ 4. & \neg B \rightarrow \neg \neg A & \mbox{Lemma 2: 2, 3} \\ 5. & \neg \neg B & \mbox{Lemma 4.1: 1, 4} \\ 6. & \neg \neg B \rightarrow B & \mbox{Axiom schema 4} \\ 7. & B & \mbox{MP: 5, 6} \end{array}$$ Thus, we can conclude that $\neg A, \neg B \rightarrow A \vdash B$, as was required.

Ad 6. Applying two times the Deduction Theorem to Lemma 4.5, we can conclude that $\vdash (\neg B \rightarrow A) \rightarrow (\neg A \rightarrow B)$, as was required.

Ad 7. We will give an abbreviated deduction.
$$\begin{array}{lll} 1. & A & \mbox{Hyp} \\ 2. & \neg A & \mbox{Hyp} \\ 3. & \neg A \rightarrow (\neg B \rightarrow \neg A) & \mbox{Axiom schema 1} \\ 4. & \neg B \rightarrow \neg A & \mbox{MP: 2, 3} \\ 5. & \neg \neg B & \mbox{Lemma 4.1: 1, 4} \\ 6. & \neg \neg B \rightarrow B & \mbox{Axiom schema 4} \\ 7. & B & \mbox{MP: 5, 6} \end{array}$$ Thus, we can conclude that $A, \neg A \vdash B$, as was required.

Ad 8. Applying two times the Deduction Theorem to Lemma 4.7, we can conclude that Lemma 4.8 holds.

Q.E.D.

Lemma 5. Let $A$ and $B$ be wffs. Then
1. $A, B \vdash \neg (A \rightarrow \neg B)$.
2. $\neg (A \rightarrow \neg B) \vdash A$.
3. $\neg (A \rightarrow \neg B) \vdash B$.

Proof. Ad 1. We will give an abbreviated deduction.
$$\begin{array}{lll} 1. & A & \mbox{Hyp} \\ 2. & B & \mbox{Hyp} \\ 3. & (A \rightarrow \neg B) \rightarrow \neg B & \mbox{Lemma 3: 1} \\ 4. & ((A \rightarrow \neg B) \rightarrow \neg B) \rightarrow (B \rightarrow \neg (A \rightarrow \neg B)) & \mbox{Lemma 4.2} \\ 5. & B \rightarrow \neg (A \rightarrow \neg B) & \mbox{MP: 3, 4} \\ 6. & \neg (A \rightarrow \neg B) & \mbox{MP: 2, 5} \end{array}$$ Thus, we can conclude that $A, B \vdash \neg (A \rightarrow \neg B)$, as was required.

Ad 2. We will give an abbreviated deduction.
$$\begin{array}{lll} 1. & \neg (A \rightarrow \neg B) & \mbox{Hyp} \\ 2. & \neg A \rightarrow (A \rightarrow \neg B) & \mbox{Lemma 4.8} \\ 3. & (\neg A \rightarrow (A \rightarrow \neg B)) \rightarrow (\neg (A \rightarrow \neg B) \rightarrow A) & \mbox{Lemma 4.6} \\ 4. & \neg (A \rightarrow \neg B) \rightarrow A & \mbox{MP: 2, 3} \\ 5. & A & \mbox{MP: 1, 4} \end{array}$$ Thus, we can conclude that $\neg (A \rightarrow \neg B) \vdash A$, as was required.

Ad 3. We will give an abbreviated deduction.
$$\begin{array}{lll} 1. & \neg (A \rightarrow \neg B) & \mbox{Hyp} \\ 2. & \neg B \rightarrow (A \rightarrow \neg B) & \mbox{Axiom schema 1} \\ 3. & (\neg B \rightarrow (A \rightarrow \neg B)) \rightarrow (\neg (A \rightarrow \neg B) \rightarrow B) & \mbox{Lemma 4.6} \\ 4. & \neg (A \rightarrow \neg B) \rightarrow B & \mbox{MP: 2, 3} \\ 5. & B & \mbox{MP: 1, 4} \end{array}$$ Thus, we can conclude that $\neg (A \rightarrow \neg B) \vdash B$.

Q.E.D.

Proposition 2 (Main Proposition). Let $A$ and $B$ be wffs, and let $x$ be an individual variable. Then
1. $\forall x \neg (A \rightarrow \neg B) \vdash \neg (\forall x A \rightarrow \neg \forall x B)$.
2. $\vdash \forall x \neg (A \rightarrow \neg B) \rightarrow \neg (\forall x A \rightarrow \neg \forall x B)$.

Proof. Ad 1. We will give an abbreviated deduction.
$$\begin{array}{lll} 1. & \forall x \neg (A \rightarrow \neg B) & \mbox{Hyp} \\ 2. & \forall x \neg (A \rightarrow \neg B) \rightarrow \neg (A \rightarrow \neg B) & \mbox{Axiom schema 7} \\ 3. & \neg (A \rightarrow \neg B) & \mbox{MP: 1, 2} \\ 4. & A & \mbox{Lemma 5.2: 3} \\ 5. & \forall x A & \mbox{Gen: 4} \\ 6. & B & \mbox{Lemma 5.3: 3} \\ 7. & \forall x B & \mbox{Gen: 6} \\ 8. & \neg (\forall x A \rightarrow \neg \forall x B) & \mbox{Lemma 5.1: 5, 7} \end{array}$$ Thus, we can conclude that Proposition 2.1 holds, as was required.

Ad 2. Since we apply Gen in the abbreviated deduction of of the proof of Proposition 2.1 only with the individual variable $x$ as quantified variable and $x$ is not a free variable in $\forall x \neg (A \rightarrow \neg B)$, we can apply the Deduction Theorem to Proposition 2.1, and conclude that $$\vdash \forall x \neg (A \rightarrow \neg B) \rightarrow \neg (\forall x A \rightarrow \neg \forall x B).$$

Q.E.D.

References

[1]: Mendelson, Elliott. Introduction to mathematical logic. 3rd ed. (c) 1987 by Wadsworth. ISBN 0-534-06624-0.

-
Well done ! Please note that (see Mendelson) Axiom schema 4 ($\vdash \lnot \lnot B \rightarrow B$) is redundant. It can be derived from Axiom schema 1 and Axiom schema 3 with your Lemma 2 and an additional Lemma : $A \rightarrow (C \rightarrow B), C \vdash A \rightarrow B$, easily provable with the Deduction Theorem. –  Mauro ALLEGRANZA May 19 at 15:59