Isabelle中使用exI规则证明存在无理数时为何报错？

报错的核心原因并非sqrt函数的问题，而是使用exI存在量词引入规则时，未明确绑定占位符?x到具体实例。

当你执行proof (rule exI)时，Isabelle生成的子目标是?x ∉ ℚ，其中?x是未绑定的元变量。此时直接show "sqrt 2 ∉ ℚ"，Isabelle无法将该语句与带占位符的子目标匹配——它不知道要把?x替换成sqrt 2，因此判定你的语句无法细化当前目标，抛出错误。

解决方法 #

有三种常见的修正方式：

1. 显式指定exI的实例
   在调用exI时通过where或of参数绑定x的值：

theorem exists_irrational_number: "∃x. x ∉ ℚ"
proof (rule exI[where x="sqrt 2"])
  show "sqrt 2 ∉ ℚ" using sqrt_2_not_rat by simp
qed

2. 简化的单步证明
   直接用by组合规则与事实，省略结构化证明的冗余步骤：

theorem exists_irrational_number: "∃x. x ∉ ℚ"
  by (rule exI[of "sqrt 2"], rule sqrt_2_not_rat)

3. 依赖自动规则选择
   省略proof后的显式规则，Isabelle会自动为存在量词选择exI规则，并匹配你给出的实例：

theorem exists_irrational_number: "∃x. x ∉ ℚ"
proof
  show "sqrt 2 ∉ ℚ" using sqrt_2_not_rat by simp
qed

补充说明 #

sqrt 2 ∉ ℚ这个断言本身完全正确，sqrt_2_not_rat事实也能正常引用，问题仅出在exI规则的使用逻辑上——未完成元变量到具体实例的绑定。

内容的提问来源于stack exchange，提问作者Juni