Here is my way of natural deduction but I don’t really know if it is an okay proof:

p→qp\to q, premise

¬(¬p∨q)\lnot(\lnot p\lor q), assumed

¬q\lnot q, assumed

¬(¬p), ∨e2,3\lnot (\lnot p), ~~\lor e_{2,3}

p, ¬¬e4p, ~~~~~~~~~~~\lnot\lnot e_4

q, →e1,5q, ~~~~~~~~~~\to{e_{1,5}}

⊥ ⊥i3,6\bot ~~~~~~~~~~~\bot i_{3,6}

q ¬i3,7q ~~~~~~~~~~~~~~~~~~~~~~~\lnot i_{3,7}

¬p∨q ∨i8\lnot p\lor q ~~~~~~~~~~~~~\lor{i_8}

⊥ ⊥i2,9\bot ~~~~~~~~~~~~~~~~~~~~~\bot i_{2,9}

¬p∨q ¬e2,10\lnot p\lor q ~~~~~~~~~~~~~~~~~~~~~~~~\lnot e_{2,10}

Thanks in advance, I am open for any criticism.

EDIT: line numbers are messed up, they are supposed to be 1 to 11.

=================

How you derive 4 from 2 and 3 ? ∨\lor-elim “acts on” p∨qp \lor q.

– Mauro ALLEGRANZA

yesterday

@MauroALLEGRANZA Since I assumed ¬q\lnot q on 3, qq in 2 does not have any purpose so I eliminated it, hence ¬(¬p)\lnot (\lnot p). Is it not possible?

– ecclesia

yesterday

I’m assuming that ∨\lore is Disjunction elimination.

– Mauro ALLEGRANZA

yesterday

@MauroALLEGRANZA Yes, that is correct.

– ecclesia

yesterday

In 3 you have to assume ¬p\lnot p and then derive ¬p∨q\lnot p \lor q by ∨\lori. This is used to contradict 2.

– Mauro ALLEGRANZA

yesterday

=================

=================