Dedução natural LaTeX

Question

Qual é a forma de escrever uma prova como a da imagem?

Sei escrever todos os símbolos, mas não sei fazer o retângulo e escrever como uma tabela. Usei esta página:https://www.tablesgenerator.com/, mas não gosto de como ele exibe as provas.

Answer 1

Aqui está uma solução usando um tabularambiente. Pela simplicidade do código da prova em si, defini alguns novos comandos. Primeiro, um ambiente prooftabularque começa tabularcom três colunas:

1. O primeiro exibe automaticamente o número da linha da prova (não é necessário escrever nada nele);
2. O segundo está automaticamente no modo matemático e é pensado para ser usado nas etapas da prova;
3. O terceiro está em modo texto e destina-se a ser utilizado para as justificativas dos passos da prova.

Este ambiente pode ser usado sozinho para exibir uma prova. Porém, para adicionar a caixa com os símbolos no canto, defini outros três comandos:

• \hlineproofboxadiciona as linhas horizontais da caixa com \cline{2-2}.
• \proofboxedadiciona as linhas verticais ao redor de uma célula na caixa. Toma como argumento o conteúdo da célula correspondente. Ele apenas adiciona as linhas verticais com um \multicolumn{1}{|...|}{...}.
• \corneradiciona seu argumento em sobrescrito, no canto. Deve ser colocado dentro do primeiro \proofboxed{}.

Esses três comandos não são tão úteis no sentido de que seu conteúdo poderia muito bem ter sido colocado diretamente na tabela. Só pensei que o código da prova fosse mais fácil de ler dessa forma.

De qualquer forma, aqui está um exemplo completo com sua prova.

\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

Supondo que não haja problemas ao escrever os comandos de símbolos, então você pode usar empheqpackage para fazer uma caixa em torno de algumas equações (duas para simplificar) como esta:

E seu código

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

E é claro que você pode adicionar um asterisco {align*}para remover a numeração das equações.

Se você quiser numerar as equações do lado esquerdo, você pode usar a opção [leqno]da articleclasse como esta

com algumas equações numeradas e outras não (use \nonumber), então o código pode 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}

Bem, essa não é a resposta perfeita. São apenas algumas ideias que tenho certeza que outras podem melhorar.