given $\neg p$ and $p\vee q$ how to use fitch system to prove $q$?

Question

as the title says: given $\neg p$ and $p\vee q$ how to use fitch system to prove $q$?

It seems like a simple thing but I can't figure out how to do it.

EDIT: I understand this is a valid rule of inference, but when I am trying to use "or elimination" in http://intrologic.stanford.edu/applications/herbrand.html after inserting the mentioned assumptions, it doesn't work. So perhaps I am using it wrong?

EDIT2: There seem to be a difference in the way Stanford university perceives the "or elimination" rule of inference and the way others perceive it, If I understand it correctly. I am trying to use the Stanford system and it doesn't seem to allow simply inferring q. I guess this question requires understanding the Stanford version of the Fitch system. See: http://intrologic.stanford.edu/academy/word.php?word=or_elimination

EDIT3: I've been required to add some context, so here it is: I've found the following logic puzzle on the internet: https://brilliant.org/practice/logic-puzzles/. Solving the puzzle is very easy, but I wanted to see if I can use first-order logic in order to prove the solution. So I formalized it like so: Since Kevin is the oldest, he is older than Nicolas and Joseph:

$o(k,n)\wedge o(k,j)$

Since Joseph is not the youngest he is either older then Kevin or older then Nicolas:

$o(j,k)\vee o(j,n)$

I also added these two axioms:

$\forall x\forall y(o(x,y)\Rightarrow\neg o(y,x))$

$\forall x\forall y(\neg o(x,y)\Rightarrow o(y,x))$

(for simplicity, let's assume everyone is older then themselves). I was able to infer $\neg o(j,k)$ and I knew that somehow this together with $o(j,k)\vee o(j,n)$ proves $o(j,n)$ but I didn't know how to get there using the Stanford University Fitch system that I used.

Answer 1

As you have seen, details depend on the proof system.

The proof needs Disjunction-elimination:

(i) assume $q$ and derive $q → q$ by $→$-intro.

(ii) assume $p$, and using the contradiction with $\lnot p$, derive $q$ and from it $p → q$, by →-intro again.

Answer 2

it is the Stanford University version of the Fitch system. I am beginning to understand it is different from other versions of Fitch system

Indeed, it lacks a contradiction symbol, has no implementation of "ex falso quodlibet", a slightly different implementations of "negation introduction" and "or elimination", its "negation elimination" is what is usually called "double negation elimination", and the quantifier rules have some quirks.

This should work on the system.

$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{~~1.~\neg p\hspace{12ex}\textsf{Premise}\\~~2.~p\vee q\hspace{10ex}\textsf{Premise}}{\fitch{~~3.~p\hspace{11ex}\textsf{Assumption}}{\fitch{~~4.~\neg q\hspace{7ex}\textsf{Assumption}}{~~5.~p\hspace{8ex}\textsf{Reiteration 3}}\\~~6.~\neg q\to p\hspace{4ex}\textsf{Implication Introduction 4-5}\\\fitch{~~7.~\neg q\hspace{7ex}\textsf{Assumption}}{~~8.~\neg p\hspace{7ex}\textsf{Reiteration 1}}\\~~9.~\neg q\to \neg p\hspace{3ex}\textsf{Implication Introduction 7-8}\\10.~\neg\neg q\hspace{8ex}\textsf{Negation Introduction 6,9}\\11.~q\hspace{11ex}\textsf{Negation Elimination 10}}\\12.~p\to q\hspace{8ex}\textsf{Implication Introduction 3-11}\\\fitch{13.~q\hspace{11ex}\textsf{Assumption}}{}\\14.~q\to q\hspace{8ex}\textsf{Implication Introduction 13-13}\\15.~q\hspace{13ex}\textsf{Or Elimination 2,12,14}}$