編集

編集

私が達成したいことは次のとおりです

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

私が得たものは次のとおりです:

ここに画像の説明を入力してください

これが私のコードです

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

問題:

正式な証明の中でインデントを行うにはどうすればよいでしょうか。右側のテキストが完全に揃っていなくてもかまいませんが、インデントは正しく設定したいと思います。上記のコードによって生成されたインデントは大きすぎます。

おそらくお分かりかと思いますが、私は LaTex 初心者です。何かアドバイスがあればありがたいです。また、このようなことのためのパッケージがあれば嬉しいです。

ありがとう!

編集

完全な形式的な証明は次のようになります。

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)
        ...
    ...
...

答え1

こんなこともできます

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

この場合、環境はlevelリスト上の項目のインデントを自動的に増やしたり減らしたりします。サイズを変更することで長さを変更できます2em

ここに画像の説明を入力してください

答え2

使用しenumerateenumitem

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

ここに画像の説明を入力してください

\label参照にはメカニズムを使用していることに注意してください\ref。距離をさらに調整するには、enumitemパッケージのマニュアルを参照してください (www.texdoc.net で入手可能)。

答え3

この種の証明をタイプセットするために設計されたパッケージを使用するのが最善だと思います。lplfitchがおそらく最も近いでしょう。 はスコープをマークするためにルールを描画しますが、 の助けを借りてこれらを削除することができますetoolbox。 次のコードは、証明の期間中ルールが 0pt になるようにメインの証明コマンド\fitchprfを修正します。 表形式のルールの通常の幅は最後に復元されます。

lplfitchまた、このような証明の組版を容易にするためのさまざまな機能も提供しています。たとえば、適切な間隔で論理記号の範囲を定義します。(詳細についてはマニュアルを参照してください。)

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

ルールのないフィッチスタイルの証明

編集

また、これが役に立つかどうかは使用しているシステムによって異なりますが、パッケージはさまざまな種類の正当化も提供します。たとえば、証明を少し続けます。

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

生産する

根拠のある証明

関連情報