Questionnaire-2024/natural_deduction_propositional_logic/0043_sol.tex

From a given formula $\varphi \lor \psi$, we want to proof some other formula $\chi$.
We only know that $\varphi$ \emph{or} $\psi$ holds. It could be that both of them are true,
but it could also be that only $\psi$ is true, or only $\varphi$ is true.
Sine we don't know which sub-formula is true, we have to give two separate proofs:
\begin{itemize}
    \item First box: We assume $\varphi$ is true and need to find a proof for $\chi$.
    \item Second box: We assume $\psi$ is true and need to find a proof for $\chi$.
\end{itemize}
Only if we can prove $\chi$ in the first and in the second box, then we can conclude that $\chi$ holds also outside of the box.

The $\ore$ rules says that we can only derive $\chi$ from $ \varphi \lor \psi$ if we can derive $\chi$
from the assumption $ \varphi$ as well as from the assumption $\psi$.
Formally the rule is written as:
\begin{center}
  \begin{prooftree}
    \AxiomC{\begin{tabular}{l}
      \vspace*{0.95ex}\\
      \vspace*{0.95ex}\\
      $ \varphi \lor \psi $\\
    \end{tabular}}
    \AxiomC{\begin{tabular}{|l|}
      \hline
      $ \varphi $ ass.\\
      \hspace*{0.2em}$ \vdots $\\
      $ \chi  $\\
      \hline
    \end{tabular}}
    \AxiomC{\begin{tabular}{|l|}
      \hline
      $ \psi $ ass.\\
      \hspace*{0.2em}$ \vdots $\\
      $ \chi  $\\
      \hline
    \end{tabular}}
    \RightLabel{$ \ore$}
    \TrinaryInfC{$ \chi $}
  \end{prooftree}
\end{center}