Chain Bounding, the leanest proof of Zorn's lemma, and an illustration of computerized proof formalization
Incatasciato, G. L., & Terraf, P. S. (2024). Chain Bounding, the Leanest Proof of Zorn’s Lemma, and an Illustration of Computerized Proof Formalization. arXiv preprint arXiv:2404.11638v2.
雖然鏈式邊界引理提供了一種簡潔而優雅的佐恩引理證明方法,但確實存在不依赖于它的更直观的證明方法。 其中一種常見方法是利用良序定理。
良序定理斷言,任何集合都可以被良序化,即賦予一個使得每個非空子集都有最小元素的排序。利用良序定理證明佐恩引理的思路如下:
假設偏序集 P 滿足佐恩引理的條件,即每個鏈都有上界。
利用良序定理,將 P 良序化。
從 P 的最小元素開始,構造一個遞增鏈,每次選擇鏈的上界中最小的那個元素加入鏈中。
由於 P 良序化,這個構造過程必然會在某個元素停止,否則就會構造出一個比 P 的良序更大的良序,矛盾。
這個停止的元素就是 P 的一個極大元素。
這種證明方法更加直觀,因为它直接構造了佐恩引理所需的極大元素。 然而,它依赖于良序定理,而良序定理本身就等價於選擇公理。 因此,从某种意义上说,这两种证明方法在逻辑上是等价的。