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 finite 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 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: excluded middle

Bottom of Page

1 to 15 of 15

  1.  
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2016

    I added to excluded middle a discussion of the constructive proof of double-negated LEM and how it is a sort of “continuation-passing” transform.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeMay 11th 2016
    • (edited May 11th 2016)

    We have a stub entry continuation-passing style. I have now made “continuation-passing” redirect to it, so that one more of your links points somewhere.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2016

    Thanks!

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 12th 2016

    My coding skills are so bad. It would be good to have one example at least at continuation-passing style, but I can’t read even that first simple pyth program at the wikipedia page.

    • CommentRowNumber5.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeMay 12th 2016
    • (edited May 12th 2016)

    The connection between the double-negation translation and the continuation-passing transform is indeed quite intriguing! Also note that, while there is only one transformation on propositions/types, there are actually a few variants of the transformation on proofs/terms, corresponding to the different kinds of the continuation-passing transform.

    David, the key idea is the following. Ordinarily, you call a subroutine/procedure/function and it returns to you some result:

    y = f(x).

    In contrast, if you employ continuation-passing style, then subroutines never return. Instead, when calling a subroutine, you pass an additional argument (a so-called continuation). This argument is itself a subroutine; it expects the result of the computation as its argument:

    f(x,(y↦⋯)). f(x, (y \mapsto \cdots)). f(x,λy.⋯). f(x, \lambda y. \cdots).

    The continuation-passing transform is a mechanical procedure which transforms a program written in direct style into the equivalent program written in continuation-passing style.

    I have some slides on this material; but they are directed at a general computer science audience. Therefore they explain intuitionistic logic, but not continuations.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMay 13th 2016

    These are nice slides of yours. I have now referenced them here.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 13th 2016

    Yes, great slides.

    I’m slowly getting there with continuation-passing. The naive factorial example here helped.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2019
    • (edited Jun 6th 2019)

    added publication data for

    • Colin McLarty, Elementary Categories, Elementary Toposes, Oxford University Press, 1996

    added also pointer to

    • {#Diaconescu75} Radu Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51:176-178 (1975) (doi:10.1090/S0002-9939-1975-0373893-X)

    • {#GoodmanMyhill78} N. D. Goodman J. Myhill, Choice Implies Excluded Middle, Zeitschrift fuer Mathematische Logik und Grundlagen der Mathematik 24:461 (1978)

    And then I added pointer to a stand-alone entry Diaconescu-Goodman-Myhill theorem, which I am splitting off so that we may disambiguate from Diaconscu’s theorem

    diff, v27, current

    • CommentRowNumber9.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJun 17th 2020

  10. added section on sharp excluded middle

    Anonymous

    diff, v28, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2022

    This addition would deserve to be equipped with a comment on why or when one would consider such a definition.

    Related discussion of ♯\sharp-modal types forming a Boolean subtopos is at Aufhebung (in the subsection here).

  12. added a section on other equivalent statements to the principle of excluded middle

    Quentin Adamson

    diff, v30, current

  13. adding the paper to the references section:

    Quentin Adamson

    diff, v30, current

  14. also added a section on excluded middle in material set theory explaining Shulman’s distinction between excluded middle for all logical formulae and excluded middle only for Δ 0\Delta_0-formulae.

    Quentin Adamson

    diff, v30, current

    • CommentRowNumber15.
    • CommentAuthorGuest
    • CommentTimeMar 26th 2023

    added a section about excluded middle in type theory

    diff, v31, current

1 to 15 of 15

  1.