logic - 如何在精益中证明 r → (∃ x : α, r)

Question

我试图证明逻辑语句r → (∃ x : α, r)，其中r是 a Prop（命题或语句）并且α是 a Type。通过本书的练习，我已经证明了精益中的一些事情，但我被困在这一点上。

我真的不确定我什至不明白为什么这是真的。由于不存在任何类型，无人居住不会α使这是一个错误的陈述吗？xα

我最好的“尝试”是 1）希望精益的阐述者能满足我的需要，

theorem t5_2: r → (∃ x : α, r) :=
  assume rx: r,
    ⟨_, rx⟩

但它不能推断出一些 type α，这是有道理的。2）我还认为这可能是一个非建设性的证明，所以我正在考虑做一个反证法。然而，我在纸上得到的最远距离是

  ¬ (∃ x : α, r) → (∀ x : α, ¬ r) → ??

我不确定如何在精益中执行第一个含义，即使我这样做了，我仍然需要一个xof 类型α来消除∀.

任何提示将不胜感激。

score 1 · Accepted Answer

这种说法一般来说是不正确的。α可能是empty：

example : ¬ ∀ (α : Type) (r : Prop), r → (∃ x : α, r) :=
begin
  intro h,
  cases h empty _ true.intro with w,
  cases w
end

如果您假设，您可以证明原始陈述[inhabited α]

example (α : Type) [inhabited α] (r : Prop) : r → (∃ x : α, r) :=
λ h, ⟨inhabited.default α, h⟩

1 回答 1