Натуральный вывод LaTeX

Question

Как написать доказательство, подобное показанному на изображении?

Я знаю, как писать все символы, но не знаю, как сделать прямоугольник и написать как таблицу. Я использовал эту веб-страницу:https://www.tablesgenerator.com/, но мне не нравится, как он отображает доказательства.

Answer 1

Вот решение с использованием tabularокружения. Для простоты кода самого доказательства я определил несколько новых команд. Во-первых, окружение prooftabular, которое начинается tabularс трех столбцов:

1. Первый автоматически отображает номер строки доказательства (вам не нужно ничего вписывать);
2. Второй автоматически находится в математическом режиме и, как предполагается, используется для шагов доказательства;
3. Третий вариант находится в текстовом режиме и, как предполагается, используется для обоснования шагов доказательства.

Эту среду можно было бы использовать отдельно для отображения доказательства. Однако, чтобы добавить поле с символами в углу, я определил три другие команды:

• \hlineproofboxдобавляет горизонтальные линии поля с \cline{2-2}.
• \proofboxedдобавляет вертикальные линии вокруг ячейки в поле. В качестве аргумента принимает содержимое соответствующей ячейки. Добавляет только вертикальные линии с \multicolumn{1}{|...|}{...}.
• \cornerдобавляет свой аргумент в верхнем индексе, в углу. Он должен быть помещен внутри первого \proofboxed{}.

Эти три команды не так уж полезны в том смысле, что их содержимое можно было бы разместить прямо в таблице. Я просто подумал, что код доказательства так читать легче.

В любом случае, вот полный пример с вашим доказательством.

\documentclass{article}
\usepackage{amsmath}
\usepackage{array}
\newcounter{proofrow}
\newenvironment{prooftabular}{%
    \let\oldarraystretch\arraystretch
    \renewcommand{\arraystretch}{1.5}
    \begin{tabular}{%
        @{\stepcounter{proofrow}\theproofrow}%
        p{1em}@{}>{\(}l<{\)}>{\quad}l%
    }
    }{%
    \end{tabular}
    \renewcommand{\arraystretch}{\oldarraystretch}
}
\newcommand{\hlineproofbox}{\cline{2-2}}
\newcommand{\proofboxed}[1]{\multicolumn{1}{|>{\(}l<{\)}@{\ }|}{#1}}
\newcommand{\corner}[1]{\qquad {}^{#1}}

\begin{document}
\[
\forall x, P_1^1(x) \implies P_2^1(x), \forall x . P_2^1(x) \implies P_3^1(x) \vdash \forall x . P_1^1(x) \implies P_3^1(x)
\]
\begin{prooftabular}
    & \forall x . P_1^1(x) \implies P_2^1(x)                        & Prem \\
    & \forall x . P_2^1(x) \implies P_3^1(x)                        & Prem \\
    \hlineproofbox
    & \proofboxed{P_1^1(n) \implies P_2^1(n) \corner{/ \forall n}}  & \(E \ \forall 1\) \\
    & \proofboxed{P_2^1(n) \implies P_3^1(n)}                       & \(E \ \forall 2\) \\
    & \proofboxed{P_1^1(n) \implies P_3^1(n)}                       & Teo \(\alpha \implies \beta, \beta \implies \gamma \vdash \alpha \implies \gamma\) \\
    \hlineproofbox
    & \forall x . P_1^1(x) \implies P_3^1(x)                        & \(\forall x . P_1^1(x) \implies P_2^1(x), \forall x . P_2^1(x) \implies P_3^1(x)\)
\end{prooftabular}
\end{document}

Answer 2

Если не возникнет проблем с написанием команд символов, то вы можете использовать empheqpackage, чтобы создать рамку вокруг некоторых уравнений (два для простоты), например:

И его код

\documentclass{article}
\usepackage{amsmath}
\usepackage{empheq}
\begin{document}
%
\begin{empheq}[box=\fbox]{align}
    E=mc^2 \\
    y=ax+b
\end{empheq}
%
\end{document}

И, конечно, вы можете добавить звездочку {align*}, чтобы убрать нумерацию уравнений.

Если вы хотите, чтобы уравнения нумеровались слева, вы можете использовать опцию [leqno]класса, articleнапример, такую:

с некоторыми уравнениями, пронумерованными, а другими нет (используйте \nonumber), тогда код может быть

\documentclass[leqno]{article}
\usepackage{amsmath}
\usepackage{empheq}
\begin{document}
%
\begin{empheq}[box=\fbox]{align}
    E=mc^2 \\
    y=ax+b \\
    y_2 = ax+b \nonumber
\end{empheq}
%
\end{document}

Ну, это не идеальный ответ. Это просто некоторые идеи, которые, я уверен, другие могут улучшить.