Logic: Proving a Negated Disjunction is a Conjunction of Negations

Question

~ = Not

V = Disjunction

& = Conjunction

A and B are stand ins for more complex formula but I know how to derive the whole derivation if I just had their negations. So I know that ~(A V B) = ~A & ~B, but I don't know how to prove that. Proofs I see online basically say "Assume A, or Assume B" but I'm doing work on a logic lab that doesn't let me just assume them in a negated disjunction. My logic lab also doesn't just let me use DeM. I also don't have (~A & ~B) as a goal, so I cant just negate that with negation elimination. I have another formula that can create the Falsum if I can derive ~A & ~B.

Assume: ~(A V B)

Goal: Falsum

Original Goal:(A V B)

Answer 1

$\lnot (a \lor b) \equiv \lnot(\lnot a \implies b) \equiv \lnot a\land \lnot b$. You can always show it via an arb. truth table, too.

Answer 2

The only way I can see to do this without making assumptions is to use a Hilbert system that contains axioms for disjunction and conjunction. Here’s how I’d do it:

1. ~A->(~B->(~A&~B)) (& Intro)

2. A->(AvB) (v Intro Left)

3. B->(AvB) (v Intro Right)

4. ~(AvB)->~A (2, Transposition)

5. ~(AvB)->~B (3, Transposition)

6. (~(AvB)->(~B->(~A&~B)))->

   ((~(AvB)->~B)->(~(AvB)->(~A&~B))) (axiom 2)

7. ~(AvB)->(~B->(~A&~B)) (1,4 HS)

8. (~(AvB)->~B)->(~(AvB)->(~A&~B)) (6,7 MP)

9. ~(AvB)->(~A&~B) (5,8 MP)