蕴涵逻辑规则

Question

我需要一些帮助来制定 Latex 中的蕴涵规则。我最大的问题是盒子。

Answer 1

\boxed包的示例amsmath：

\documentclass{article}
\usepackage{amsmath}
\begin{document}
\[
    \frac{
      \boxed{
        \begin{array}{c}
          \phi\\
          \vdots\\
          \psi
        \end{array}
      }
    }{
      \phi \rightarrow \psi
    }
    \rightarrow
    - \mathbf{I}
\]
\end{document}

使用更好的中间线，删除 的额外水平边距array，并微调 的位置\vdots：

\documentclass{article}
\usepackage{amsmath}

\makeatletter
\newcommand*{\Frac}[2]{%
  % Even numbered box and register numbers smaller than 10 are
  % for local assignments.
  \begingroup
    % "Numerator" in box 0
    \sbox0{$#1\m@th$}%
    % "Denominator" in box 2
    \sbox2{$#2\m@th$}%
    % Maximum width in \dimen2
    \ifdim\wd0 > \wd2 %
      \dimen0=\wd0 %
    \else
      \dimen0=\wd2 %
    \fi
    % Add overshoot (5pt) of the line
    \advance\dimen0 by 10pt\relax
    % Vertical separation
    \dimen2=3pt\relax
    \setbox4=\vbox{%
      \hbox to \dimen0{\hfill\unhcopy0\hfill}%
      \kern\dimen2
      \hrule % default line thickness: 0.4pt
      \kern\dimen2
      \hbox to \dimen0{\hfill\unhcopy2\hfill}%
      \kern0pt\relax
    }%
    % Box for measuring height of math axis
    \sbox0{$\vcenter{}$}%
    % Set result with the line at the math axis
    \raise\dimexpr\ht0 - \ht2 - \dp2 - \dimen2 - .2pt\relax\copy4 %
  \endgroup
}
\makeatother

\begin{document}
\[
    \Frac{
      \boxed{
        \begin{array}{@{}c@{}}
          \phi\\[-2pt]
          \vdots\\
          \psi
        \end{array}
      }
    }{
      \phi \rightarrow \psi
    }
    \rightarrow
    - \mathbf{I}
\]
\end{document}