![Genzen 式证明树](https://linux22.com/image/417163/Genzen%20%E5%BC%8F%E8%AF%81%E6%98%8E%E6%A0%91.png)
我想生成以下证明树。这是我目前的尝试:
\def\ae\qquad\mathbf{\forall Elim}
\def\ai\qquad\mathbf{\forall Intro}
\def\be\qquad\mathbf{\leftrightarrow Elim}
\def\bi\qquad\mathbf{\leftrightarrow Intro}
\def\oe\qquad\mathbf{\lor Elim}
\def\oi\qquad\mathbf{\lor Intro}
\def\ne\qquad\mathbf{\neg Elim}
\def\ni\qquad\mathbf{\neg Intro}
\begin{equation}
\dfrac{
\dfrac{
\dfrac{
\dfrac{
\dfrac{\forall x(Pa \lor Rx)}{Pa \lor Rb}\ae
\dfrac{\dfrac{Pa}{Pa \lor \forall xRx \quad \lnot(Pa \lor \forall xRx)}}{Rb \qquad Rb}\ne
}{
Rb
}\oe
}{
\forall xRx
}\ai
}{
Pa \lor \forall xRx \quad \lnot(Pa \lor \forall xRx)
}\oi
}{
Pa \lor \forall xRx
}\ne
\end{equation}
是否有可能不延长树的这两段中的分数线?
因此,在第一种情况下,该行看起来如下:
也许,有更好的方法来解决这个问题。我将使用 MathJax。