Deducción natural LaTeX

Question

¿Cuál es la forma de escribir una prueba como la de la imagen?

Sé escribir todos los símbolos, pero no sé hacer el rectángulo y escribir como una tabla. Utilicé esta página web:https://www.tablesgenerator.com/, pero no me gusta cómo muestra las pruebas.

Answer 1

Aquí hay una solución que utiliza un tabularentorno. Para simplificar el código de la prueba en sí, definí algunos comandos nuevos. Primero, un entorno prooftabularque comienza tabularcon tres columnas:

1. El primero muestra automáticamente el número de la fila de la prueba (no es necesario escribir nada en él);
2. El segundo está automáticamente en modo matemático y está pensado para usarse en los pasos de la demostración;
3. El tercero está en modo texto y está pensado para la justificación de los pasos de la prueba.

Este entorno podría usarse solo para mostrar una prueba. Sin embargo, para agregar el cuadro con los símbolos en la esquina, definí otros tres comandos:

• \hlineproofboxAgrega las líneas horizontales del cuadro con \cline{2-2}.
• \proofboxedagrega las líneas verticales alrededor de una celda en el cuadro. Toma como argumento el contenido de la celda correspondiente. Solo agrega las líneas verticales con un \multicolumn{1}{|...|}{...}.
• \corneragrega su argumento en superíndice, en la esquina. Debe colocarse dentro del primero \proofboxed{}.

Estos tres comandos no son tan útiles en el sentido de que su contenido también podría haberse colocado directamente en la tabla. Simplemente pensé que el código de la prueba era más fácil de leer de esta manera.

De todos modos, aquí tienes un ejemplo completo con tu prueba.

\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

Suponiendo que no haya problemas al escribir los comandos de símbolos, entonces puede usar empheqel paquete para crear un cuadro alrededor de algunas ecuaciones (dos para simplificar) como esta:

y su codigo

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

Y por supuesto puedes agregar un asterisco {align*}para eliminar la numeración de ecuaciones.

Si desea que las ecuaciones se numeren en el lado izquierdo, puede usar la opción [leqno]de la articleclase como esta

con algunas ecuaciones numeradas y otras no (use \nonumber), entonces el código puede ser

\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}

Bueno, esa no es la respuesta perfecta. Son solo algunas ideas que estoy seguro que otros pueden mejorar.