EDITAR

Question

Esto es lo que pretendo lograr

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

Esto es lo que obtuve:

Aquí está mi 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}

El problema:

¿Cómo hacer la sangría dentro de una prueba formal? No me importa si el texto de la derecha no está perfectamente alineado, pero me gustaría que la sangría sea correcta. La sangría producida por el código anterior es demasiado grande.

Como probablemente podrás ver, soy nuevo en LaTex. Se agradece cualquier sugerencia. También sería bueno si hubiera algún paquete para este tipo de cosas.

¡Gracias!

Editar

Una prueba formal completa sería 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

Puedes hacer algo como esto

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

En este caso, el entorno levelaumenta la sangría del elemento en la lista y la disminuye automáticamente. Puedes cambiar la longitud cambiando el 2emtamaño.

Answer 2

Puedes usar enumerateyenumitem

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

Tenga en cuenta que he utilizado \labelun \refmecanismo para las referencias. Para ajustar aún más las distancias, consulte el enumitemmanual del paquete (disponible en www.texdoc.net)

Answer 3

Creo que sería mejor utilizar un paquete diseñado para componer este tipo de pruebas. lplfitchprobablemente sea el más cercano. Dibuja reglas para marcar los alcances pero estas se pueden eliminar con la ayuda de etoolbox. Lo siguiente parchea el comando de prueba principal \fitchprfpara que las reglas tengan 0 puntos durante la prueba. El ancho normal de las reglas en tablas se restablece al final.

lplfitchTambién ofrece una gama de facilidades diseñadas para facilitar la composición tipográfica de dichas pruebas. Por ejemplo, define una variedad de símbolos lógicos con el espaciado adecuado. (Consulte el manual para obtener más detalles).

\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

Además, si esto es útil o no depende del sistema que esté utilizando, pero el paquete también proporciona justificaciones de varios tipos. Por ejemplo, continuando un poco la prueba:

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

produce