# Is my proof of p→q⊢¬p∨qp\to q\vdash \lnot p\lor q correct?

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

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

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