嘿，我完全懂你读这本书时的卡壳感——这部分把日常否定的直觉和形式系统的符号挂钩，确实容易让人绕进去，我来帮你拆解清楚：

1. ¬φ是不是严格定义为(φ→⊥)？ #

你的判断其实非常准！在绝大多数自然演绎系统里，¬φ本质上就是(φ→⊥)的缩写，Chiswell和Hodges之所以没直接说“这是定义”，而是用“完全当作(φ→⊥)来处理”这种表述，主要是为了照顾初学者的直觉：先从日常语言里“φ不成立”的否定概念入手，再慢慢过渡到形式系统里用“蕴涵荒谬”来刻画否定的严格逻辑。

简单说，他们的委婉表述其实就是在告诉你：在后续的形式推导中，¬φ和(φ→⊥)是完全等价的，可以互换使用——你把¬φ看作(φ→⊥)的定义，完全没问题，这就是他们想传递的核心意思。

2. 为什么“假设¬φ”能推出“只有有限个质数”？ #

这里要区分形式系统的符号操作和日常数学论证的直观表述，二者的衔接是关键：

• 日常语言里的“假设φ不成立”（也就是书中说的“Assume not”），对应的就是φ的否定命题¬φ。在这个质数的例子里，φ是“存在无穷多个质数”，它的否定“不存在无穷多个质数”，在数学语境下直接等价于“只有有限个质数”——这是集合论中“有限”和“无穷”的基本对立定义：一个集合要么是无穷的，要么是有限的，没有中间状态。
• 回到你纠结的形式化问题：如果把¬φ看作(φ→⊥)，日常论证里的“假设¬φ”其实对应形式推导中引入假设(φ→⊥)，但数学实践不会这么生硬地写符号，而是直接用自然语言的否定表述——因为我们已经默认了“φ的否定”和“φ不成立”的直观对应，以及“无穷的否定是有限”这个数学前提。

而归谬法（RAA）的作用，就是把这种日常的反证思路转化为严格的形式推导：你先假设¬φ（或者说假设φ→⊥），然后从这个假设出发推出矛盾（⊥），最后就能得到φ成立。在质数的证明里，从“只有有限个质数”构造出矛盾（找到一个不在列表里的新质数），这部分在形式系统里就是从假设¬φ推导到⊥，再应用RAA得到φ的过程。

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