Help with Formal Proof using introduction and elimination rules

121 Views Asked by At

I need help with a proof where the premise is $\lnot A \land \lnot B$ and the goal is $\lnot (A \lor B)$. We are allowed to use the introduction and elimination of the following operators: $\lnot$,$\land$,$\lor$,$=$, and $\bot$. I am having some trouble with figuring out a way to use a getting the goal from the separated steps $\lnot A$ and $\lnot B$.

Thanks in advance.

1

There are 1 best solutions below

8
On

See the image below (coming from a book). $\rm\vdash (\lnot A\land\lnot B)\to\lnot(A\lor B)$

$$\rm \dfrac{\lower{1ex}{[A\lor B]^3}~~\dfrac{\lower{1.5ex}{[A]^4}~~\dfrac{[\lnot A\land\lnot B]^1}{\lnot A}{\small\land e}}{\bot}{\small\lnot e}~~\dfrac{\lower{1.5ex}{[B]^5}~~\dfrac{[\lnot A\land\lnot B]^2}{\lnot B}{\small\land e}}{\bot}{\small\lnot e}}{\dfrac{\dfrac{\bot}{\lnot(A\lor B)}{\lnot i^{3}}}{(\lnot A\land\lnot B)\to\lnot(A\lor B)}{\small{\to}i^{1,2}}}{\lor e^{4,5}} $$