theorem-proving - 有限界量词的消除规则

Question

我有以下目标:

∀x ∈ {0,1,2,3,4,5}. P x

我想将这个目标分解为六个子目标 P 0、P 1、P 2、P 3、P 4 和 P 5。这可以通过 apply auto 轻松完成。但是 auto 用来执行此操作的相关规则是什么？我问是因为我的实际目标看起来更像这样:

∀x ∈ {0..<6}. P x

和 apply auto 并没有以同样的方式分解这个目标(它给了我

⋀x. 0 ≤ x ⟹ x < 6 ⟹ P x

代替)。

Answer 1

auto 使用的规则是ballI (bounded all introduction)。这会将 ∀x ∈ S. P x 转换为 x ∈ S ==> P x。

将 x ∈ {0,1,2,3,4,5} 转换为 6 个单独的子目标的问题是一个单独的问题。基本上，auto 将显式枚举转换为析取，然后将其拆分。