logic - 如何在精益中证明 r → (∃ x : α, r)
问题描述
我试图证明逻辑语句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) → ??
我不确定如何在精益中执行第一个含义,即使我这样做了,我仍然需要一个x
of 类型α
来消除∀
.
任何提示将不胜感激。
解决方案
这种说法一般来说是不正确的。α
可能是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⟩
推荐阅读
- java - 当我在命令提示符下运行 javac 时没有任何反应
- vert.x - 使用 Vert.x 进行批处理
- javascript - 有没有办法修复 react 项目中的 browserslist 和 glob-parent 漏洞?
- html - 填充 100% 的视口,忽略父级的侧边距但尊重垂直滚动条
- html - 如何自动创建分页符?
- angular - @firebase/firestore:Firestore (7.24.0):无法访问 Cloud Firestore 后端。后端在 10 秒内没有响应 - Angular 12
- rust - 如何调试一些 Rust 代码以找出“if”语句不运行的原因?
- r - R 中的分箱生理时间序列数据:计算每个箱中花费的持续时间
- pki - 我如何知道新的公共 CA 何时发布?
- python - IntelliJ想法解决python venv依赖