Talk:Kleene–Brouwer order

Uses, references

The Kleene-Brouwer order is not only of interest in descriptive set theory. It carries the names of Kleene and Brouwer (and also, sometimes, if I remember correctly, Kolmogorov) and yet the only reference is to Moschovakis. Ideally, both Kleene and Brouwer should be cited, but I do not know where a reference for Brouwer can be found. Kleene gives a classical proof of the well-foundedness theorem that the article says is so important (in Introduction to Metamathematics?). The Kleene-Brouwer order can be defined over trees over any set $X$ which carries a partial order (the order does not have to be total).

I once had a professional interest in this order as I was trying to give a constructive proof of well-foundedness, using the well-ordering principle for the set $X$ and the well-ordering principle for the tree over $X$. I conjecture that this is equivalent to the fan theorem when the set $X$ is N but I never understood this well enough to attempt a proof.

I'm happy to be corrected on any of the above; and I'd dearly love to find someone who understands it enough to correctly formulate and prove the conjecture above.

btw, I'm pretty new to Wikipedia...

Fairflow (talk) 17:12, 17 October 2010 (UTC)

Well, I think the question is, what would you cite Kleene and Brouwer as saying, that Moschovakis doesn't say? We don't generally strain to use sources just because they're closer to the historical origins of something. However, if there's an important point that's left out, but that you can find in Kleene or Brouwer, then by all means add it and cite them. --Trovatore (talk) 04:46, 18 October 2010 (UTC)

Indeed. I added the Moschovakis reference awhile ago because the article had no citations or references and it was the best resource I had on hand that defined the KB ordering. Not to mention it's a pretty nice and canonical descriptive set theory text that people could go to if they wanted to look more into the topic. If you know a better reference, then by all means add it, but for the content currently on the article, Moschovakis is fine. Thanks for fixing the definition by the way. Wgunther (talk) 17:46, 18 October 2010 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Kleene–Brouwer order. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://archive.is/20130414182741/http://eudml.org/doc/57945 to http://eudml.org/doc/57945

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 13:30, 11 December 2017 (UTC)

Constructive meaning of the the K-B order

My previous question about references to the K-B order and its constructive meaning was not exactly to the point. What I would like to know, and I hope that at least one of the writers/editors of this page knows already, is if the equivalence of the K-B-ordered tree giving rise to a well-ordering and the well-foundedness of the tree (as stated in the article itself) is (a) proved in the Moschovakis reference (ref. 1) and if so (b) if the proof is constructive. Sadly I do not have access to the book. I'd really appreciate if someone who knows could assist me. It might seem obvious, and it is trivial to prove classically. But if it's easy to sketch a constructive proof then I believe that would strengthen the article. Thanks! Fairflow (talk) 16:20, 21 October 2021 (UTC)

My experience is that there is no real agreement about what constitutes a "constructive" proof in set theory, especially when you get past the countable. Intuitively, the standard proof is pretty constructive, but I sort of doubt there's a way to avoid excluded middle. But I as well would be interested to know. --Trovatore (talk) 16:56, 21 October 2021 (UTC)

I've no idea how much of descriptive set theory can be developed in IZF (for example) or how much depends on the K-B ordering but this would seem to be a pretty basic result and a sensible candidate for an IZF proof. (If only I'd asked Peter Aczel when I met him at a conference when I was a new PhD student! My supervisor didn't have an answer for me.) --Fairflow (talk) 22:36, 21 October 2021 (UTC)

(I could answer your question (a) given time — the book is just a few feet to my right. But it'll have to wait till I'm off the clock.) --Trovatore (talk) 17:22, 21 October 2021 (UTC)

That would be fantastic if you get the chance! The proof I know goes as follows: suppose there is an infinite descending sequence in the K-B order on X. Consider the sequence of first elements of that sequence; since X is well-founded this must eventually reach a fixed point. This creates the first element of a new sequence. Continuing in this way we create an ever-lengthening (hence descending) sequence in the tree based on X, so the tree is not well-founded either. We've proved the contrapositive of the stated theorem, but that isn't the constructive argument I am looking for. --Fairflow (talk) 22:20, 21 October 2021 (UTC)