Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: principle of omniscience

Bottom of Page

1 to 16 of 16

  1.  
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeAug 28th 2014

    I added a couple of comments about topos models to principle of omniscience.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeAug 28th 2014

    trivia:

    “Errett” is with two “t”, right? At least we do have Errett Bishop. I changed it in the entry, but check.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeAug 28th 2014

    Wikipedia agrees; thanks.

    • CommentRowNumber4.
    • CommentAuthorspitters
    • CommentTimeAug 28th 2014

    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.

    • CommentRowNumber5.
    • CommentAuthormartinescardo
    • CommentTimeFeb 28th 2020

    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.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2020

    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”.

  7. added section about the principles of omniscience in homotopy type theory and its truncated vs untruncated versions.

    Anonymous

    diff, v20, current

    • CommentRowNumber8.
    • CommentAuthorandrew
    • CommentTimeJan 3rd 2023

    typo

    diff, v23, current

    • CommentRowNumber9.
    • CommentAuthorncfavier
    • CommentTimeDec 4th 2023

    Added WLPO, which was mentioned later down the page but not defined.

    diff, v24, current

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 18th 2024

    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?

  11. Andrew Swan on the CT Zulip says that the reals having decidable equality is actually “analytic WLPO” rather than “analytic LPO”.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJan 18th 2024

    Ah, yes, I agree!

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 18th 2024

    Decidable equality of the reals is the analytic WLPO.

    diff, v27, current

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeJan 25th 2024

    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.

  15. There is a discussion on the Category Theory zulipchat about the bullet point which says

    • Every modulated Cantor real number has a radix expansion in any base (e.g., a decimal expansion or binary expansion) iff LLPO ℕ\mathrm{LLPO}_\mathbb{N} holds; every Dedekind real number has a radix expansion iff the analytic LLPO holds. At least in the presence of countable choice (which also implies that modulated Cantor reals and Dedekind reals agree), this is equivalent to the claim that the rings of radix expansions in any two bases are isomorphic. See Daniel Mehkeri's answer to Feldman (2010).

    https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-questions/topic/Radix.20expansions.20in.20constructive.20mathematics

    and the conclusions on there are that

    1. 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.

    2. 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

    diff, v37, current

  16. The LLPO makes an appearance in section 7.2 of

    Anonymouse

    diff, v46, current

1 to 16 of 16

  1.