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 definitions 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 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: choice operator

Bottom of Page

1 to 5 of 5

  1.  

  1. removing query box from page

    +– {: .query} Mike Shulman: Is there a formal statement in some formal system along the lines of “a non-extensional choice operator does not imply AC”?

    Toby: I don't know about a formal statement, but I can give you an example.

    Recall: In Per Martin-Löf's Intuitionistic Type Theory (and many other systems along similar lines), the basic notion axiomatised is not really that of a set (even though it might be called ’set’) but instead a preset (or ’type’). Often one hears that the axiom of choice does hold in these systems, which doesn't imply classical logic due to a lack of quotient (pre)sets. However, if we define a set to be a preset equipped with an equivalence predicate, then the axiom of choice fails (although we have COSHEP if presets come with an identity predicate).

    A lot of these systems (including Martin-Löf's) use ’propositions as types’, in which ∃x:AP(x) is represented as ∑x:AP(x), which comes equipped with an operation π:∑x:AP(x)→A. That is not going to get us our choice operator, but since a choice operator is constructively questionable anyway, then let's throw in excluded middle. This is known to not imply choice, but we do have, for every preset A, an element εA of A∨¬A, that is of A⊎∅A. It's not literally true that εA is of type A, of course, but that would be unreasonable in a structural theory; what we do have is a fixed εA such that, if A is inhabited, then εA=ιA(e) for some (necessarily unique) e of type A (where ιA is the natural inclusion A→A⊎∅A), which I think should be considered good enough. This is for presets (types), but every set has a type of elements, so that gets us our operator.

    How is this nonextensional? We do have εA=εB if A=B (which is a meaningful statement to Martin-Löf, albeit not a proposition exactly), but if A and B are given as subsets of some U, then we may well have A=B as subsets of U without A=B in the sense of identity of their underlying (pre)sets. In particular, if f:U→V is a surjection and A and B are the preimages of elements x and y of V, then x=Vy will not imply that εA=εB, and the proof of the axiom of choice does not go through. It will go through if x and y are identical, that is if x=y in the underlying preset of V, so again we do get choice for presets (again), but not for sets.

    I'm not certain that a nonextensional global choice operator won't imply excluded middle in some other way, but I don't see how it would. You'd want to do something with the idea that εA always exists but belongs to A if and only if A is inhabited, but I don't see how to parse it (just by assuming that it exists) to decide the question.

    Mike Shulman: That’s a very nice explanation/example, and it did help me to understand better what’s going on; thanks! (Did you mean to say “excluded middle” and not “AC” in your final paragraph?) What I would really like, though, is a statement like “the addition of a nonextensional global choice operator to ____ set theory is conservative” (i.e. doesn’t enable the proving of any new theorems that doen’t refer explicitly to the choice operator). Of course I am coming from this comment, wondering whether what you suggested really is a way to get a choice operator without implying the axiom of choice.

    Toby: Yeah, I really did mean to say ’excluded middle’; remembering that comment, I assume that the real question is whether the thing is OK for a constructivist. I just argued ITT+EM⊨CO, and I know the result ITT+EM¬⊨AC, so I conclude ITT+CO¬⊨AC; but I don't know ITT+CO¬⊨EM for certain. I certainly don't have ITT+CO conservative over ITT, nor with any other theory (other than those that already model CO, obviously).

    Mike Shulman: Where should I look for a proof that ITT+EM doesn’t imply AC?

    Toby: I'm not sure, it's part of my folk knowledge now. Probably Michael J. Beeson's Foundations of Constructive Mathematics is the best bet. I'll try to get a look in there myself next week; I can see that it's not exactly obvious, and perhaps my memory is wrong now that I think about it.

    Mike Shulman: I’m trying to prove the sort of statement I want over at SEAR+?.

    Toby: No, I can't get anything at all out of Beeson (or other references) about full AC (for types equipped with equivalence relations) in ITT.

    Harry Gindi: I have references for this discussion that should settle the issue at hand:

    Bell, J. L., 1993a. ’Hilbert’s epsilon-operator and classical logic’, Journal of Philosophical Logic, 22:1-18

    Bell, J. L., 1993b. ’Hilbert’s epsilon operator in intuitionistic type theories’, Mathematical Logic Quarterly 39:323-337

    Meyer Viol, W., 1995a. ’A proof-theoretic treatment of assignments’, Bulletin of the IGPL, 3:223-243

    Toby: Thanks, Harry! Now I just have to find these journals at the library. =–

    Anonymous

    diff, v26, current

  2. added section about the global choice operator in dependent type theory

    Anonymous

    diff, v27, current

  3. Added section on choice operators in category theory

    Anonymouse

    diff, v42, current

  4. Distinguished between internal and external choice operators for choice operators in category theory.

    Anonymouse

    diff, v44, current

  5. Added section on choice operators in allegories

    Anonymouse

    diff, v46, current

1 to 5 of 5

  1.