A Direct Proof of the Equivalence between Brouwer's Fan Theorem and König's Lemma with a Uniqueness Hypothesis

Простая страница элемента
dc.creatorSchwichtenberg,Helmut
dc.date2005
dc.date.accessioned2024-02-06T12:54:04Z
dc.date.available2024-02-06T12:54:04Z
dc.descriptionFrom results of Ishihara it is known that the weak (that is, binary) form of König's lemma (WKL) implies Brouwer's fan theorem (Fan). Moreover, Berger and Ishihara [MLQ 2005] have shown that a weakened form WKL! of WKL, where as an additional hypothesis it is required that in an effective sense infinite paths are unique, is equivalent to Fan. The proof that WKL! implies Fan is done explicitely. The other direction (Fan implies WKL!) is far less directly proved; the emphasis is rather to provide a fair number of equivalents to Fan, and to do the proofs economically by giving a circle of implications. Here we give a direct construction. Moreover, we go one step further and formalize the equivalence proof (in the Minlog proof assistant). Since the statements of both Fan and WKL! have computational content, we can automatically extract terms from the two proofs. It turns out that these terms express in a rather perspicuous way the informal constructions.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-011-12-2086
dc.identifierhttps://lib.jucs.org/article/28536/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/8908
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 11(12): 2086-2095
dc.subjectBrouwer's fan theorem
dc.subjectKönig's lemma
dc.titleA Direct Proof of the Equivalence between Brouwer's Fan Theorem and König's Lemma with a Uniqueness Hypothesis
dc.typeResearch Article
Файлы
Коллекции
Публикации в журналах НИЯУ МИФИ