私が達成したいことは次のとおりです
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
使用しenumerate
てenumitem
\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}]
}
}\\
}
生産する