"欧米茄"真的在这里做什么？

Question

这个证明可以用一个完成omega:

  a : Z
  b : Z                                                                                               
  H : a > 1
  H0 : b > 1
  H1 : b = 1                                                                                          
  H2 : a mod b = 0
  ============================
   False

这是为什么？omega这里到底做了什么？而且既然H0又H1相互矛盾,难道不可能证明什么吗？此外,这可以证明没有omega？怎么样？

Answer 1

1-在这里,omega意识到H0并且H1是相互矛盾的,并用它们来证明False.它不应该是很难直接通过重写显示此H1成H0(导致1 > 1),然后涂抹一些引理那就说明a > b -> a <> b,导致1 <> 1,然后再应用到我们的目标,产生了新的目标1 = 1,这可以通过排出reflexivity.很难描述如何 omega详细地工作,因为它背后有一个复杂的算法,它可以处理大量类似的目标(粗略地讲,预算算术)

2-是的.H0并且H1可以用来证明任何东西,包括False.这有时被称为爆炸原理.但请注意,您只能在特定上下文中证明任何内容.换句话说,并不是因为你在一些证据背景中有一个矛盾,你可以证明其他任何东西.