Prove (de Morgan 1) $\vdash A\wedge B \equiv \neg (\neg A \vee \neg B)$

Question

Proof - starting from the right side: $$\neg (\neg A \vee \neg B)$$ $<=>\text{(axiom: introduction of }\neg \text{)}$ $$\neg A \vee \neg B \equiv \bot $$ $<=> (\text{Leib + }\vdash\neg A\vee B\equiv A\vee B\equiv B\text{; 'C-part' is } p\equiv \bot)$ $$\neg A \vee B \equiv \bot \equiv A \vee B\equiv B \equiv \bot$$

I'm not sure what the next step is... from reviewing other answers somehow $$(\neg A \vee B \equiv \bot \equiv A \vee B\equiv B \equiv \bot)\equiv (A\vee\neg B\equiv \neg B \equiv \bot)$$

Answer 1

As per your previous post, the proof uses to Equational logic, following George Tourlakis, Mathematical Logic (Wiley, 2008).

In order to prove Th.2.4.17 (De Morgan-1) : $\vdash A \land B \equiv \lnot (\lnot A \lor \lnot B)$ [page 72], we have to start form the premise :

1) $¬(¬A \lor ¬B)$

and we have to transform it, through equivalences, into the conclusion.

The first step uses the axiom defining $\lnot$ : $\lnot A \equiv (A \equiv \bot)$ to get :

2) $(¬A \lor ¬B) \equiv \bot$.

The next step uses the previously proved Coroll.2.4.12 : $\vdash \lnot A \lor B \equiv (A \lor B \equiv B)$ [page 70].

We need Leibniz's rule :

from $D_1 \equiv D_2$ and $C[p:=D_1]$ derive $C[p:=D_2]$, where $C$ is a formula and $C[p:=D_i]$ is obtained from $C$ replacing part $p$ with formula $D_i$.

This means to use the 2) as $C$ and $(¬A \lor ¬B)$ as $D_1$ and $(A \lor \lnot B \equiv \lnot B)$ as $D_2$ to get :

3) $(A \lor \lnot B \equiv \lnot B) \equiv \bot$

and thus, using the axiom for Assiociativity of $\equiv$ :

4) $A \lor \lnot B \equiv (\lnot B \equiv \bot)$.

Then using Leibniz again, the axiom for $\lnot$ and Th.2.4.4 (Double Negation, page 67), we get :

5) $A \lor \lnot B \equiv B$.

Now we use the Corollary again : $\vdash (\lnot A \lor B \equiv A \lor B) \equiv B$. We have to replace in 5) $B$ with $\lnot A \lor B \equiv A \lor B$ to get :

6) $A \lor \lnot B \equiv (\lnot A \lor B \equiv A \lor B)$

and thus :

7) $(A \lor \lnot B \equiv \lnot A \lor B) \equiv A \lor B$.

Here we need the following : $(A \lor \lnot B \equiv \lnot A \lor B) \equiv (A \equiv B)$ [I've not found it in the book : we may check it with truth table].

Using it and Simmetry of $\equiv$ we get :

8) $A \lor B \equiv (A \equiv B)$.

The last step uses the Golden Rule axiom : $A \land B \equiv (A \equiv B \equiv A \lor B)$ and we conclude with :

9) $A \land B$.

---

Note: here is a proof of the "missing corollary" : $\vdash (A \lor \lnot B \equiv \lnot A \lor B) \equiv (A \equiv B)$

1) $(A \lor \lnot B \equiv \lnot A \lor B)$

2) $\lnot A \lor B \equiv A \lor B \equiv B$ --- Coroll.2.4.12

3) $\lnot B \lor A \equiv A \lor B \equiv A$ --- idem

Thus, using Leibniz twice :

3) $(A \lor B \equiv B) \equiv (A \lor B \equiv A)$.

Rearranging it :

4) $(A \lor B \equiv A \lor B) \equiv (A \equiv B)$.

By Coroll.2.1.21 [page 59 : $(A \lor B \equiv A \lor B) \equiv \top$], we get :

5) $\top \equiv (A \equiv B)$

and thus, by Coroll.2.1.21 again [$\vdash A \equiv (A \equiv \top)$] :

6) $(A \equiv B)$.