嘿，我来一步步拆解你这些关于Enderton这段内容的疑问，咱们从最基础的概念开始捋：

1. 这里的“logical axioms”是不是特指公理组1？ #

完全没错！Enderton这里讨论的“逻辑公理”就是公理组1的内容。因为其他公理组（比如量词相关的公理组2、等词相关的公理组3）根本不属于“重言式”范畴——重言式是纯命题逻辑层面的概念，只看命题联结词的真值表规则，而量词、等词是一阶逻辑独有的，它们的公理没法用命题逻辑的重言式来解释。所以这段讨论完全聚焦在公理组1上。

2. 公理组1是不是所有重言式的概括？ #

你说的太对了！Enderton定义的公理组1，就是所有重言式的“概括”（generalizations）——简单说就是：先拿命题逻辑里的任意重言式，把里面的命题符号换成一阶逻辑的任意合式公式（wff），还可以给公式里的自由变量加全称量词，得到的所有公式都属于公理组1。比如命题逻辑里的$P\to P$，替换成$\forall x R(x)\to\forall x R(x)$或者$\exists y S(x,y)\to\exists y S(x,y)$，这些都是公理组1的成员。

3. “精简公理组1到一组重言式”是什么意思？ #

说白了就是：不用把所有重言式的概括都直接当公理，而是只选**一小部分最基础的命题逻辑重言式（或者它们的一阶替换实例）作为核心公理，剩下的所有重言式概括，都可以通过肯定前件规则（modus ponens）**推导出来。

比如命题逻辑里，我们只需要选3条公理模式就够了：

• $A\to(B\to A)$
• $((A\to(B\to C))\to((A\to B)\to(A\to C)))$
• $(\neg A\to\neg B)\to(B\to A)$
  这三条是多项式时间可判定的（一眼就能看出是不是符合模式），而且通过肯定前件规则，能推导出所有命题逻辑重言式。把这个思路扩展到一阶逻辑，就是用这些模式的一阶替换实例（把命题符号换成任意一阶wff）作为精简后的公理组1基础。

4. 精简后的公理组1具体是哪组重言式？ #

核心是命题逻辑层面的极小完全公理模式集——就是那些能作为命题逻辑完全系统的重言式模式，比如刚才提到的三条经典希尔伯特式公理模式。对应的，在一阶逻辑里就是这些模式的一阶替换实例（把命题符号换成任意一阶wff）。

5. 是把一阶wff当成命题符号的重言式？还是把一阶原子公式当成命题符号的重言式？ #

其实更准确的是：我们先在纯命题逻辑层面选定极小公理模式（用命题符号表示），然后把这些模式里的命题符号替换成任意一阶逻辑的wff（不管是原子公式还是复合公式），得到的一阶公式就是精简后的公理。

不过这里要明确：一阶逻辑里的“重言式”，就是把整个一阶wff当成命题逻辑里的“命题符号”（不管它内部的量词、谓词结构），看整个公式是不是命题逻辑意义上的重言式。比如$(\forall x R(x)\to\exists y S(y))\leftrightarrow(\neg\forall x R(x)\lor\exists y S(y))$就是这样的重言式，因为它对应命题逻辑里的$(P\to Q)\leftrightarrow(\neg P\lor Q)$。

6. 为什么其他重言式能通过肯定前件推导出来？ #

这是因为命题逻辑的希尔伯特式公理系统是完全的——意思是，只要选对了那几条极小公理模式，加上肯定前件规则，就能推导出所有命题逻辑重言式。而一阶逻辑里的重言式概括，本质上就是命题重言式的一阶替换版本，所以用这些精简后的公理模式的一阶实例，加上肯定前件，就能推导出原来公理组1的所有内容。

举个简单例子：用那三条基础公理推导出$A\to A$（不管A是命题符号还是一阶wff）：

1. $A\to((A\to A)\to A)$ （第一条公理模式）
2. $(A\to((A\to A)\to A))\to((A\to(A\to A))\to(A\to A))$ （第二条公理模式）
3. $(A\to(A\to A))\to(A\to A)$ （肯定前件1和2）
4. $A\to(A\to A)$ （第一条公理模式）
5. $A\to A$ （肯定前件3和4）

所有其他重言式都能通过类似的步骤推导出来，扩展到一阶逻辑的替换实例也完全适用。

备注：内容来源于stack exchange，提问作者Tim