How to prove this
$$\vdash\forall x (B\land C)\leftrightarrow(\forall x B\land\forall x C)$$?
Here is my failed attempt:(
First I have two options to prove it:
- To suppose $\vdash\forall x (B\land C)$ and to prove $(\forall x B\land\forall x C)$ and then to do the converse.
OR
- $\vdash[\forall x (B\land C)\to(\forall x B\land\forall x C)]\land [\forall x (B\land C)\leftrightarrow(\forall x B\land\forall x C)]$
But in 2. I won't be able to use the Deduction Theorem. So I chose 1.
And I also tried to do an analogy of the proof of this theorem $$\vdash\forall x(B\to C)\to(\forall x B\to\forall x C)...(*)$$
I tried to change the $\land$ by $\to$ to make the theorem look like (*):
By hypothesis $\vdash\forall x (B\land C)$, but it's equivalent to
$\forall x\lnot(B\to\lnot C)$. By A4, $\lnot(B\to\lnot C)$ and here a problem appears since I won't be able to apply modus ponens to obtain $C$ or $\lnot C$ like it was done in the proof of (*).
Note: I can only use the axioms, modus ponens and the Gen rule.
As correctly remarked by Bram28, $\mathscr{A} \land \mathscr{B}$ is nothing but a shorthand for $\lnot (\mathscr{A} \to \lnot \mathscr{B})$, since in your system $\mathsf{K}$ there are no axioms dealing with $\land$. Similarly for $\mathscr{A} \leftrightarrow \mathscr{B}$, seen as a shorthand for $(\mathscr{A} \to \mathscr{B}) \land (\mathscr{B} \to \mathscr{A})$. This means that you have to prove $$\lnot \big( (\forall x\lnot(B\to \lnot C)\to\lnot(\forall x B\to\lnot\forall xC)) \to \lnot(\lnot(\forall xB\to\lnot\forall x C)\to\forall x\lnot(B\to\lnot C)) \big)$$ in your system $\mathsf{K}$. Finding a direct derivation of such a formula seems to be a very hard task, and the derivation could be huge and unintelligible.
An alternative, but equivalent, approach is to take seriously the idea of $\mathscr{A} \land \mathscr{B}$ as a shorthand for $\lnot (\mathscr{A} \to \lnot \mathscr{B})$ and to reason about $\mathscr{A} \land \mathscr{B}$ (which is easier to handle) instead of $\lnot (\mathscr{A} \to \lnot \mathscr{B})$. Of course, in order to be entitled to do this, we first have to prove in the system $\mathsf{K}$ that $\mathscr{A} \land \mathscr{B}$ (i.e. $\lnot (\mathscr{A} \to \lnot \mathscr{B})$) fulfills some natural introduction and elimination rules; in other words, we have to prove that the following formulas are derivable in the system $\mathsf{K}$:
\begin{align*} (\land_\text{intro})\quad& \mathscr{A} \to (\mathscr{B} \to (\mathscr{A} \land \mathscr{B})) &\text{i.e.}\quad & \mathscr{A} \to (\mathscr{B} \to \lnot(\mathscr{A} \to \lnot \mathscr{B})) \\ (\land_\text{elim1})\quad& (\mathscr{A} \land \mathscr{B}) \to \mathscr{A} &\text{i.e.}\quad & \lnot(\mathscr{A} \to \lnot \mathscr{B}) \to \mathscr{A} \\ (\land_\text{elim2})\quad& (\mathscr{A} \land \mathscr{B}) \to \mathscr{B} &\text{i.e.}\quad & \lnot(\mathscr{A} \to \lnot \mathscr{B}) \to \mathscr{B} \end{align*}
Proof that $\land_\text{intro}$ is derivable in $\mathsf{K}$. First, as a preliminary step, the derivation below shows that $\lnot \lnot (\mathscr{A} \to \lnot \mathscr{B}), \, \mathscr{A} \vdash_\mathsf{K} \lnot \mathscr{B}$. Let $\mathscr{C} = \mathscr{A} \to \lnot \mathscr{B}$: \begin{align} 1. \ &(\lnot\mathscr{C} \to \lnot\lnot\mathscr{C}) \to ((\lnot\mathscr{C} \to \lnot\mathscr{C}) \to \mathscr{C}) &\text{(by axiom $A_3$)} \\ 2. \ &\lnot\lnot\mathscr{C} \to (\lnot \mathscr{C} \to \lnot\lnot \mathscr{C}) &\text{(by axiom $A_1$)} \\ 3. \ &\lnot\lnot\mathscr{C} &\text{(by hypothesis)} \\ 4. \ &\lnot \mathscr{C} \to \lnot\lnot\mathscr{C} &\text{(by $\mathsf{MP}$ with 2 and 3)} \\ 5. \ &(\lnot\mathscr{C} \to \lnot\mathscr{C}) \to \mathscr{C} &\text{(by $\mathsf{MP}$ with 1 and 4)} \\ 6. \ &\big(\lnot\mathscr{C} \to ((\lnot\mathscr{C} \to \lnot\mathscr{C}) \to \lnot\mathscr{C}) \big) \to \big( (\lnot\mathscr{C} \to (\lnot\mathscr{C} \to \lnot\mathscr{C})) \to (\lnot\mathscr{C} \to \lnot\mathscr{C}) \big) &\text{(by axiom $A_2$)} \\ 7. \ &\lnot\mathscr{C} \to ((\lnot\mathscr{C} \to \lnot\mathscr{C}) \to \lnot\mathscr{C}) &\text{(by axiom $A_1$)} \\ 8. \ &(\lnot\mathscr{C} \to (\lnot\mathscr{C} \to \lnot\mathscr{C})) \to (\lnot\mathscr{C} \to \lnot\mathscr{C}) &\text{(by $\mathsf{MP}$ with 6 and 7)} \\ 9. \ &\lnot\mathscr{C} \to (\lnot\mathscr{C} \to \lnot\mathscr{C}) &\text{(by axiom $A_1$)} \\ 10. \ &\lnot\mathscr{C} \to \lnot\mathscr{C} &\text{(by $\mathsf{MP}$ with 8 and 9)} \\ 11. \ &\mathscr{A} \to \lnot \mathscr{B} &\text{(by $\mathsf{MP}$ with 5 and 10)} \\ 12. \ &\mathscr{A} &\text{(by hypothesis)} \\ 13. \ &\lnot\mathscr{B} &\text{(by $\mathsf{MP}$ with 11 and 12)} \end{align} From the Deduction Theorem, it follows that $\mathscr{A} \vdash_\mathsf{K} \lnot\lnot (\mathscr{A} \to \lnot \mathscr{B}) \to \lnot \mathscr{B}$ [$*$]. Now we can use $[*]$ in the derivation below to prove that $\mathscr{A}, \,\mathscr{B} \vdash_\mathsf{K} \lnot(\mathscr{A} \to \lnot \mathscr{B})$. Recall that $\mathscr{C} = \mathscr{A} \to \lnot \mathscr{B}$. \begin{align} 1. \ &(\lnot\lnot\mathscr{C} \to \lnot \mathscr{B}) \to ((\lnot\lnot\mathscr{C} \to \mathscr{B}) \to \lnot \mathscr{C}) &\text{(by axiom $A_3$)} \\ 2. \ &\mathscr{A} &\text{(by hypothesis)} \\ 3. \ &\lnot\lnot \mathscr{C} \to \lnot \mathscr{B} &\text{(by $[*]$, from 2)} \\ 4. \ &(\lnot\lnot\mathscr{C} \to \mathscr{B}) \to \lnot \mathscr{C} &\text{(by $\mathsf{MP}$ with 1 and 3)} \\ 5. \ &\mathscr{B} \to (\lnot\lnot\mathscr{C} \to \mathscr{B}) &\text{(by axiom $A_1$)} \\ 6. \ &\mathscr{B} &\text{(by hypothesis)} \\ 7. \ &\lnot\lnot\mathscr{C} \to \mathscr{B} &\text{(by $\mathsf{MP}$ with 5 and 6)} \\ 8. \ &\lnot(\mathscr{A} \to \lnot\mathscr{B}) &\text{(by $\mathsf{MP}$ with 4 and 7)} \end{align} From the Deduction Theorem (applied twice), it follows that $\vdash_\mathsf{K} \mathscr{A} \to (\mathscr{B} \to \lnot (\mathscr{A} \to \lnot \mathscr{B}))$.
Proof that $\land_\text{elim1}$ is derivable in $\mathsf{K}$: similar to the point below, slightly more complicated. A good exercise for the reader.
Proof that $\land_\text{elim2}$ is derivable in $\mathsf{K}$. The derivation below shows that $\lnot(\mathscr{A} \to \lnot \mathscr{B}) \vdash_\mathsf{K} \mathscr{B}$. \begin{align} 1. \ &(\lnot\mathscr{B} \to \lnot(\mathscr{A} \to \lnot \mathscr{B})) \to \big((\lnot\mathscr{B} \to (\mathscr{A} \to \lnot \mathscr{B})) \to \mathscr{B}\big) &\text{(by axiom $A_3$)} \\ 2. \ &\lnot(\mathscr{A} \to \lnot \mathscr{B}) \to \big(\lnot \mathscr{B} \to \lnot (\mathscr{A} \to \lnot \mathscr{B}) \big) &\text{(by axiom $A_1$)} \\ 3. \ &\lnot(\mathscr{A} \to \lnot \mathscr{B}) &\text{(by hypothesis)} \\ 4. \ &\lnot \mathscr{B} \to \lnot (\mathscr{A} \to \lnot \mathscr{B}) &\text{(by $\mathsf{MP}$ with $2$ and $3$)} \\ 5. \ &(\lnot\mathscr{B} \to (\mathscr{A} \to \lnot \mathscr{B})) \to \mathscr{B} &\text{(by $\mathsf{MP}$ with $1$ and $4$)} \\ 6. \ &\lnot\mathscr{B} \to (\mathscr{A} \to \lnot \mathscr{B}) &\text{(by axiom $A_1$)} \\ 7. \ &\mathscr{B} &\text{(by $\mathsf{MP}$ with $1$ and $5$)} \end{align} From the Deduction Theorem, it follows that $\vdash_\mathsf{K} \lnot(\mathscr{A} \to \lnot \mathscr{B}) \to \mathscr{B}$.
The advantage of proving $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$ is that $\mathscr{A} \land \mathscr{B}$ is still nothing but $\lnot (\mathscr{A} \to \lnot \mathscr{B})$, but now when dealing with $\mathscr{A} \land \mathscr{B}$ you can directly use $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$ and "forget" about its syntactic definition as $\lnot (\mathscr{A} \to \lnot \mathscr{B})$: this definition still holds but is "hidden" in the derivations of $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$.
Using $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$, we can prove that $\forall x (B \land C) \vdash_\mathsf{K} \forall x B \land \forall x C$, i.e. $\forall x \, \lnot(B \to \lnot C) \vdash_\mathsf{K} \lnot(\forall x B \to \lnot \forall x C)$, as shown by the derivation below. \begin{align} 1. \ &\forall x (B \land C) \to (B \land C) &\text{(by axiom $A_4$)} \\ 2. \ &\forall x B \to (\forall x C \to (\forall x B \land \forall x C)) &\text{(by $\land_\text{intro}$)} \\ 3. \ &(B \land C) \to B &\text{(by $\land_\text{elim1}$)} \\ 4. \ &(B \land C) \to C &\text{(by $\land_\text{elim2}$)} \\ 5. \ &\forall x (B \land C) &\text{(by hypothesis)} \\ 6. \ &B \land C &\text{(by $\mathsf{MP}$ with 1 and 5)} \\ 7. \ &B &\text{(by $\mathsf{MP}$ with 3 and 6)} \\ 8. \ &\forall x B &\text{(by generalization of 7)} \\ 9. \ &\forall x C \to (\forall x B \land \forall x C) &\text{(by $\mathsf{MP}$ with 2 and 8)} \\ 10. \ &C &\text{(by $\mathsf{MP}$ with 4 and 6)} \\ 11. \ &\forall x C &\text{(by generalization of 10)} \\ 12. \ &\forall x B \land \forall x C &\text{(by $\mathsf{MP}$ with 9 and 11)} \end{align} From the Deduction Theorem, it follows that $\vdash_\mathsf{K} \forall x (B \land C) \to (\forall x B \land \forall x C)$ $[**]$.
Using $\land_\text{intro}$, $\land_\text{elim1}$ and $\land_\text{elim2}$, we can prove that $\forall x (B \land C) \vdash_\mathsf{K} \forall x B \land \forall x C$, i.e. $\forall x \, \lnot(B \to \lnot C) \vdash_\mathsf{K} \lnot(\forall x B \to \lnot \forall x C)$, as shown by the derivation below. \begin{align} 1. \ &(\forall x B \land \forall x C) \to \forall x B &\text{(by $\land_\text{elim1}$)} \\ 2. \ &(\forall x B \land \forall x C) \to \forall x C &\text{(by $\land_\text{elim2}$)} \\ 3. \ &B \to (C \to (B \land C)) &\text{(by $\land_\text{intro}$)} \\ 4. \ &\forall x B \land \forall x C &\text{(by hypothesis)} \\ 5. \ &\forall x B &\text{(by $\mathsf{MP}$ with 1 and 4)} \\ 6. \ &\forall x C &\text{(by $\mathsf{MP}$ with 2 and 4)} \\ 7. \ &\forall x B \to B &\text{(by axiom $A_4$)} \\ 8. \ &\forall x C \to C &\text{(by axiom $A_4$)} \\ 9. \ &B &\text{(by $\mathsf{MP}$ with 7 and 5)} \\ 10. \ &C &\text{(by $\mathsf{MP}$ with 8 and 6)} \\ 11. \ &C \to (B \land C) &\text{(by $\mathsf{MP}$ with 3 and 9)} \\ 12. \ &B \land C &\text{(by $\mathsf{MP}$ with 11 and 10)} \\ 13. \ &\forall x (B \land C) &\text{(by generalization of 12)} \end{align} From the Deduction Theorem, it follows that $\vdash_\mathsf{K} (\forall x B \land \forall x C) \to \forall x (B \land C)$ $[***]$.
Finally, using $[**]$, $[***]$ and $\land_\text{intro}$, we can prove that $\vdash_\mathsf{K} \big(∀x(B∧C)→(∀xB∧∀xC) \big) \land \big( (∀xB ∧ ∀xC) \to ∀x(B∧C) \big)$, i.e. $\vdash_\mathsf{K} (∀x(B∧C)↔(∀xB∧∀xC))$, as shown by the following derivation. Let $\mathscr{C} = ∀x(B∧C)→(∀xB∧∀xC)$ and $\mathscr{D} = (∀xB ∧ ∀xC) \to ∀x(B∧C)$. \begin{align} 1. \ &\mathscr{C} \to (\mathscr{D} \to (\mathscr{C} \land \mathscr{D})) &\text{(by $\land_\text{intro}$)} \\ 2. \ &\mathscr{C} &\text{(by $[**]$)} \\ 3. \ &\mathscr{D} \to (\mathscr{C} \land \mathscr{D}) &\text{(by $\mathsf{MP}$ with 1 and 2)} \\ 4. \ &\mathscr{D} &\text{(by $[***]$)} \\ 5. \ &\mathscr{C} \land \mathscr{D} &\text{(by $\mathsf{MP}$ with 3 and 4)} \end{align}