EDITAR

Question

Aqui está o que pretendo alcançar

1.r                             (Given)
2.(t ∧ r) → s                   (Given)
3.(p → t) → (q → ¬s)            (Given)
    4.t ∧ r                     (Assumption)

Aqui está o que consegui:

Aqui está meu código

\documentclass[11pt]{article}

\usepackage{amsmath,amsthm,amssymb}
\def\imp{\rightarrow}

\begin{document}

\section{formal proof}
\textbf{(a)}
\begin{proof}
    \begin{align*}
    &1. r& &&\text{(Given)}\\
    &2. (t \land r) \imp s&  &&\text{(Given)}\\
    &3. (p \imp t) \imp (q \imp \neg s)& &&\text{(Given)}\\
    &&4. t \land r& &&\text{(Assumption)}
    \end{align*}
\end{proof}

\end{document}

O problema:

Como fazer o recuo dentro de uma prova formal? Não me importo se o texto à direita não estiver alinhado perfeitamente, mas gostaria que o recuo estivesse correto. O recuo produzido pelo código acima é muito grande.

Como você provavelmente pode perceber, sou novo no LaTex. Qualquer sugestão será apreciada. Também seria bom se houvesse algum pacote para esse tipo de coisa.

Obrigado!

Editar

Uma prova formal completa seria algo como:

1.r                             (Given)
2.(t ∧ r) → s                   (Given)
3.(p → t) → (q → ¬s)            (Given)
    4.t ∧ r                     (Assumption)
    5.t                         (From 4)
    6.s                         (From 2, 4)
        7. (p → t)              (Assumption)
        8. p                    (From 5, 7)
        ...
    ...
...

Answer 1

Você pode fazer algo assim

\documentclass{article}

\usepackage{amsmath,amsthm,amssymb}
\def\imp{\rightarrow}

\newenvironment{level}%
{\addtolength{\itemindent}{2em}}%
{\addtolength{\itemindent}{-2em}}

\begin{document}

\section{formal proof}
\textbf{(a)}
\begin{proof}\leavevmode
    \begin{enumerate}
    \item $r$ \hfill(Given)
    \begin{level}
    \item $(t \land r) \imp s$ \hfill (Given)
    \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
      \begin{level}
        \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
        \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
      \end{level}
    \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
    \end{level}
    \item $t \land r$ \hfill (Assumption)
    \end{enumerate}
\end{proof}

\end{document}

Neste caso, o ambiente levelaumenta o recuo do item na lista e diminui automaticamente. Você pode alterar o comprimento alterando o 2emtamanho.

Answer 2

Você pode usar enumerateeenumitem

\documentclass[11pt]{article}

\usepackage{amsmath,amsthm,amssymb}
\def\imp{\rightarrow}

\usepackage{enumitem}

\begin{document}

\section{formal proof}
\textbf{(a)}
\begin{proof}\leavevmode
    \begin{enumerate}[ref=\arabic*]
    \item $r$ \hfill(Given)
    \item $(t \land r) \imp s$ \hfill (Given)\label{enum:second}
    \item $(p \imp t) \imp (q \imp \neg s)$ \hfill(Given)
    \begin{enumerate}[start=4,label=\arabic*.,ref=\arabic*]
    \item $t \land r$ \hfill (Assumption)\label{enum:fourth}
    \item $t$ \hfill         (From~\ref{enum:fourth})\label{enum:fifth}
    \item $s$ \hfill          (From~\ref{enum:second},~\ref{enum:fourth})
    \begin{enumerate}[start=7,label=\arabic*.,ref=\arabic*]
    \item $(p \imp t)$ \hfill   (Assumption)\label{enum:seventh}
     \item $p$  \hfill          (From~\ref{enum:fifth},~\ref{enum:seventh})
    \end{enumerate}
    \end{enumerate}
    \end{enumerate}
\end{proof}

\end{document}

Observe que usei \labelum \refmecanismo para referências. Para ajustar ainda mais as distâncias, consulte o enumitemmanual do pacote (disponível em www.texdoc.net)

Answer 3

Acho que seria melhor usar um pacote projetado para compor esse tipo de prova. lplfitchprovavelmente é o mais próximo. Desenha regras para marcar os escopos, mas estas podem ser eliminadas com a ajuda de etoolbox. O seguinte corrige o comando de prova principal \fitchprfpara que as regras tenham 0pt durante a prova. A largura regular das regras nas tabelas é restaurada no final.

lplfitchtambém oferece uma variedade de recursos projetados para facilitar a composição tipográfica de tais provas. Por exemplo, define uma gama de símbolos lógicos com espaçamento apropriado. (Consulte o manual para obter detalhes.)

\documentclass[11pt]{article}
\usepackage{mathtools,amsthm,amssymb}
\usepackage{lplfitch}
\usepackage{etoolbox}
\newlength\savearrayrulewidth
\setlength\savearrayrulewidth{\arrayrulewidth}
\pretocmd{\fitchprf}{\setlength{\arrayrulewidth}{0pt}}{\typeout{Great!}}{\typeout{Oh, no!}}
\apptocmd{\fitchprf}{\setlength{\arrayrulewidth}{\savearrayrulewidth}}{\typeout{Great!}}{\typeout{Oh, no!}}
\begin{document}

\fitchprf{%
  \pline[1]{r}[(Given)]\\
  \pline[2]{(t \land r) \lif s}[(Given)]\\
  \pline[3]{(p \lif t) \lif (q \lif \lnot s)}[(Given)]
}{%
  \subproof{%
    \pline[4]{t \land r}[(Assumption)]
  }{%
  }\\
}

\end{document}

EDITAR

Além disso, se isso é útil ou não, depende do sistema que você está usando, mas o pacote também fornece justificativas de vários tipos. Por exemplo, continuando um pouco a prova:

\fitchprf{%
  \pline[1]{r}[(Given)]\\
  \pline[2]{(t \land r) \lif s}[(Given)]\\
  \pline[3]{(p \lif t) \lif (q \lif \lnot s)}[(Given)]
}{%
  \subproof{%
    \pline[4]{t \land r}[(Assumption)]
  }{%
    \pline[5]{s}[\life{2}{4}]\\
    \pline[6]{t}[\lande{5}]\\
    \subproof{%
      \pline[7]{p \lif t}[(Assumption)]
    }{%
      \pline[8]{q \lif \lnot s}[\life{3}{7}]
    }
  }\\
}

produz