1
$\begingroup$

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:

  1. 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

  1. $\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.

enter image description here

enter image description here

$\endgroup$
  • $\begingroup$ How are $\land$ and $\leftrightarrow$ defined ... since the axioms only deal with $\neg$ and $\rightarrow$ $\endgroup$ – Bram28 Dec 23 '17 at 16:41
  • $\begingroup$ @Bram28 Can't I use them then? I thought I could use them. $\endgroup$ – user178403 Dec 23 '17 at 16:55
  • 1
    $\begingroup$ yes, you can use the axioms ... but the $\land$ and $\leftrightarrow $ need to be defined in terms of $\neg$ and $\rightarrow$ ... that is, they need to be seen as shorthand for statements that involve latter. Thus, for example, $\phi \land\psi $ could be seen as shorthand for $\neg (\phi \rightarrow\neg \psi)$. So ... we're any such definitions given to you? $\endgroup$ – Bram28 Dec 23 '17 at 17:47
  • $\begingroup$ @Bram28 yes $\dots$ $\endgroup$ – user178403 Dec 23 '17 at 18:08
  • $\begingroup$ Ok, cool. Then the first thing you need to do is to rewrite the theorem to be proven in terms of $\neg$ and $\rightarrow$ $\endgroup$ – Bram28 Dec 23 '17 at 18:13
2
$\begingroup$

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}

$\endgroup$
  • $\begingroup$ Thank you for the help kind person :) $\endgroup$ – user178403 Dec 25 '17 at 3:34
  • $\begingroup$ Are you using this equivalence $p\to q\iff \lnot q\to\lnot p$ to get $(**)$? $\endgroup$ – user178403 Dec 25 '17 at 3:35
  • $\begingroup$ @Michelle - No, I am not. I have just used your axioms, your rules (modus ponens and generalization) and Deduction Theorem. In general, the advantage of proving $∧_\text{intro}$, $∧_\text{elim1}$ and $∧_\text{elim2}$ is that $𝒜∧ℬ$ is still nothing but $¬(𝒜→¬ℬ)$, but now when dealing with $𝒜∧ℬ$ you can directly use $∧_\text{intro}$, $∧_\text{elim1}$ and $∧_\text{elim2}$ and "forget" about its syntactic definition as $¬(𝒜→¬ℬ)$: this definition still holds but is "hidden" in the derivations of $∧_\text{intro}$, $∧_\text{elim1}$ and $∧_\text{elim2}$. $\endgroup$ – Taroccoesbrocco Dec 25 '17 at 6:40
  • $\begingroup$ I see, thank you again. $\endgroup$ – user178403 Dec 25 '17 at 22:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.