尽管已插入 $，但缺少 $

Question 1

回答：

在这种情况下，\infer（从proof包 (package) 要求其参数为公式，因此其参数已用美元符号包围。您应该删除所添加的多余符号。
一般提示：始终将“缺少 $ 插入”解释为“TeX 在非数学模式下遇到了以下数学模式问题”，并首先尝试找出为什么TeX 未处于数学模式。（有时实际上是缺少美元符号，但在这种情况下，这是因为它刚刚退出数学模式，因为有“多余”的美元符号。）

关于 TeX 错误消息和调试的更多详细答案：

尽管错误消息乍一看很奇怪，但原则上从错误输出来看一切都是有意义的，特别是如果您添加\tracingall并知道要查找什么。

\documentclass{article}
\usepackage{amsmath} 
\usepackage{proof} 
\begin{document} 

\tracingall
\infer{$\forall x\in A. P(x)$}{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

上面的输入中，您\infer在括号中输入了两个内容：第一个是

{$\forall x\in A. P(x)$}

第二个是

{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

输出\tracingall显示\infer，经过足够多的步骤后，TeX 会尝试扩展一个内部命令，\@infer [#1]#2#3其中

#1<-\@empty 
#2<-$\forall x\in A. P(x)$
#3<-$\forall x\in A.(\forall y\in A.x\xrightarrow {+}y\implies P(y))\implies P(x)$

这比最终的错误信息稍微高一点，即：

! Missing $ inserted.
<inserted text> 
                $
<to be read again> 
                   \forall 
<argument> $\forall 
                    x\in A. P(x)$
\@infer [#1]#2#3->\relax \if@ReturnLeftOffset \else \@SavedLeftOffset =\@LeftOffset \fi \setbox \@LabelPart =\hbox {$#1$}\relax \setbox \@LowerPart =\hbox {$#2
                                                                                                                                                               $}\relax \global \@LeftOffset =0pt \setbox \@UpperPart =\vbox {\tabskip =0pt \halign {\relax...
l.7 \infer{$\forall x\in A. P(x)$}{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

?

这表明 this 的定义\@infer是：

\@infer [#1]#2#3->\relax \if@ReturnLeftOffset \else \@SavedLeftOffset =\@LeftOffset \fi \setbox \@LabelPart =\hbox {$#1$}\relax \setbox \@LowerPart =\hbox {$#2
                                                                                                                                                              $}\relax \global \@LeftOffset =0pt \setbox \@UpperPart =\vbox {\tabskip =0pt \halign {\relax...

（...上面最后一行末尾的表示定义尚未完成！）其中，在执行命令\hbox {$#2$}（#2遇到时将被替换）时，会发生什么：

首先，TeX 发现\hbox并进入受限水平模式。
然后它看到$（来自的定义\@infer）并进入数学模式（并做一些事情，比如更改字体系列和执行中的任何内容\everymath）。
然后它看到#2并替换其定义 $\forall x\in A. P(x)$ 。
因此当它看到第一个字符时$，它离开数学模式。
然后它看到\forall，此时有了定义\mathchar"238。
这个\forall（\mathchar"238）只能在数学模式下使用，因此 TeX 会$在读取它（进入数学模式）之前“有帮助地”插入一个符号，但只是暂时的：它还会“有帮助地”让你知道（在继续对$插入的符号采取行动之前）它将要做什么，以防你想改变将要发生的事情。

这解释了错误消息，该消息由一条消息和后跟表示输入堆栈的几行组成：

! Missing $ inserted.

^ 錯誤信息。

<inserted text> 
                $

^ 输入堆栈的第一级：TeX 即将读取$它插入的内容，并通知您。

<to be read again> 
                   \forall

^ 输入堆栈的第二级：\forallTeX 先前读取过并放回了（当它遇到错误时），接下来它将再次读取它（如果您允许的话）。

<argument> $\forall 
                    x\in A. P(x)$

^ 输入堆栈的第三级：在读取一个参数 $\forall x\in A. P(x)$ （这是一个宏的参数，将在下文中展示）时，TeX 已完成读取$\forall，但尚未读取x\in A. P(x)$。

\@infer [#1]#2#3->\relax \if@ReturnLeftOffset \else \@SavedLeftOffset =\@LeftOffset \fi \setbox \@LabelPart =\hbox {$#1$}\relax \setbox \@LowerPart =\hbox {$#2
                                                                                                                                                               $}\relax \global \@LeftOffset =0pt \setbox \@UpperPart =\vbox {\tabskip =0pt \halign {\relax...

^ 输入堆栈的第四级：TeX 在遇到参数时正在扩展的宏。请注意，在这里您可以看到它刚刚读取\hbox{$#2，这就是正在发生的事情的线索。

l.7 \infer{$\forall x\in A. P(x)$}{$\forall x\in A.(\forall y\in A.x\xrightarrow{+}y\implies P(y))\implies P(x)$}

^ 输入堆栈的第五级：TeX 读取的源文件的第 7 行。

^ 提示，询问您如何继续。如果您按 Enter，它将读取$然后（从堆栈的前三层开始），然后继续读取从开始的堆栈的第四层\forall（这将导致另一个错误）。x\in A. P(x)$$

顺便说一句，推测什么样的设计或用户惯例可以避免这种无用的（至少乍一看）错误消息，从而获得更愉快的用户体验，这很有趣（作为一种无聊的想象力练习）。我轻率的回答是不要使用太多宏。:) 但更严肃地说，也许某种方式让包指定宏的某个参数是否应该是公式，并首先检查这一点（在输入到 TeX 内部之前）会有所帮助。不确定 expl3 是否提供了这个。另一件可能有帮助的事情是某种形式的 TeX 正在做什么的交互式/慢动作显示（比\tracingall这更好的东西需要一些经验才能理解），这样你就可以看到 TeX 因为而进入了数学模式\infer，并且因为您的而离开了数学模式$，在遇到之前\forall。

Answer

回答：

在这种情况下，\infer（从proof包 (package) 要求其参数为公式，因此其参数已用美元符号包围。您应该删除所添加的多余符号。
一般提示：始终将“缺少 $ 插入”解释为“TeX 在非数学模式下遇到了以下数学模式问题”，并首先尝试找出为什么TeX 未处于数学模式。（有时实际上是缺少美元符号，但在这种情况下，这是因为它刚刚退出数学模式，因为有“多余”的美元符号。）