1

Okay, I'm trying to prove the constructive dilemma:

\{p\lor q, p\to r, q\to r\} \vdash r

And I was attempting a proof tree for it in ebproofs and it is giving me some problems.

My code looks like this:

\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\end{prooftree}

Up to this point it turns out fine. But when I add this:

\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\Hypo{\neg r} \Hypo{p\to q} \Infer{2}[MT]{\neg q}
\end{prooftree}

I know this is an unfinished proof, but I get a problem here when I try to run the code. Apparently it's a "malformed proof tree".

MT = modus tollens here.

1

Well, never mind. I figured out the problem. Turns out, ebproofs can't seem to run partial proofs. Basically, completing the proof removed the problem I had.

\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\Hypo{\neg r} \Hypo{p\to q} \Infer{2}[MT]{\neg q}
\Infer{2}[F]{\bot}
\end{prooftree}

So there's that...

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.