Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added a couple of comments about topos models to principle of omniscience.
trivia:
“Errett” is with two “t”, right? At least we do have Errett Bishop. I changed it in the entry, but check.
Wikipedia agrees; thanks.
The comment:
There are various other results that are equivalent to or related to the principles of omniscience, which it might be handy to collect here. For the connection to writing real numbers as decimals (or in some other radix), see Daniel Mehkeri’s answer to Feldman (2010).
leads to the field of constructive reverse mathematics, i.e. calibrating theorems by their logical strength. However, this certainly deserves its own page. Apparently, it is also related to centipede mathematics.
The terminology “omniscience” is attributed to Bishop in this page. But I’ve just found out that A. Kolmogorov already used it in 1931. See page 5 of this English translation: http://homepages.inf.ed.ac.uk/jmckinna/kolmogorov-1932.pdf.
The only use I see in the linked Kolmogorov paper is an informal appearance in one sentence:
Should our readers not consider themselves omniscient, they will readily determine that [LEM] cannot occur on the list of problems they have solved.
This certainly anticipates Bishop’s use, but I don’t think it invalidates the claim that Bishop was the first to talk formally about “principles of omniscience”.
In a conversation with Madeline Birchfield on CT Zulip, I realized that prior to 2016, this page said that the “analytic LPO” is the statement that the reals have decidable equality, but in revision 16, Toby changed it to say that “analytic LPO” is the statement that the reals have decidable apartness, which is stronger unless combined with (analytic) Markov’s principle. I don’t see any comments about that change here or elsewhere. Toby, are you there and have an explanation for the change in terminology? I’m generally on board with apartness being a better way to make constructive statements, but I’m curious if you had a specific application or model in mind as motivation? Or if anyone else knows one?
Andrew Swan on the CT Zulip says that the reals having decidable equality is actually “analytic WLPO” rather than “analytic LPO”.
Ah, yes, I agree!
I'm here, although I don't see most comments, so it's only luck that I saw this one. But we all seem to be in agreement.
There is a discussion on the Category Theory zulipchat about the bullet point which says
and the conclusions on there are that
One needs to clearly separate the existence of a radix expansion from having a choice of a radix expansion; the latter implies WLPO while the former doesn’t.
It isn’t clear that without weak countable choice, LLPO holds iff for Cauchy real numbers there exist a radix expansion.
As a result, I have separated out the bullet point from the others into its own section titled “Related statements”, and split it into two separate bullet points.
Ian Anderson
The LLPO makes an appearance in section 7.2 of
Anonymouse
1 to 16 of 16