如何证明`Ø(A?ØA)`

Question

section\nopen classical\nexample : \xc2\xac (A \xe2\x86\x94 \xc2\xac A) :=\nhave hn : (A \xe2\x88\xa8 \xc2\xac A), from sorry,\n  assume h : (A \xe2\x86\x94 \xc2\xac A),\n  show false, from or.elim hn\n    (assume h1 : A, h.mp h1 h1)\n    (assume h2 : \xc2\xac A, h2 (h.mpr h2))\nend\n

\n

我正在阅读 Jeremy Avigad 的《逻辑与证明》一书来学习精益。问题是我只能用by_contradiction战术来应对排中法则。有人可以帮我吗？

\n

Answer 1

提示：证明这A \xe2\x86\x92 \xc2\xac A意味着\xc2\xac A.

\n

解决方案：

\n

\n

\n
1. A \xe2\x86\x92 \xc2\xac A相当于A \xe2\x86\x92 (A \xe2\x86\x92 False)（根据定义）\n
2. ...这相当于A \xe2\x86\x92 False(收缩)\n
3. ...这是\xc2\xac A\n

\n

\n

\n

有了这个：\n\n

\n
1. 假设A \xe2\x86\x94 \xc2\xac A\n
2. 将其弱化为A \xe2\x86\x92 \xc2\xac A\n
3. 根据上面的见解，这意味着\xc2\xac A\n
4. 将其反馈给 (1) 以获得A\n
5. 和\xc2\xac A都是A正确的。矛盾。\n

\n

\n

最终代码：

\n

\n

example : \xc2\xac (A \xe2\x86\x94 \xc2\xac A) :=\n  fun h =>\n    have : \xc2\xac A := fun a => h.mp a a\n    have : A   := h.mpr \xe2\x80\xb9\xc2\xac A\xe2\x80\xba\n    by contradiction

\n

\n

作弊：

\n

\n

当然，在现实世界的项目中，这不是家庭作业问题，我们只是使用库版本：\n\n

example : \xc2\xac (A \xe2\x86\x94 \xc2\xac A) := by exact?  -- Try this: exact iff_not_self

\n

\n