以下是我想要实现的目标
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
。以下修补主证明命令\fitchprf
,以便规则在证明期间为 0pt。表格中规则的常规宽度在最后恢复。
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}]
}
}\\
}
生产