Comments (7)
My current assumption is that the existence of a choice function for any countable collection of inhabited sets requires more than countable choice. If I look at something like the definition of the Axiom of Countable Choice, ACω, in section 10.2 of [AczelRathjen] they only discuss an infinitely countable collection and the same is true of places like Lemma: 8.1.27 (a countably infinite collection of countable sets has a sequence of enumerations, given countable choice).
At least based on a browse through that work, it would seem like the question everyone is asking about is the union of a sequence of countable sets (that is, a countably infinite number of them), rather than the union of countably many countable sets.
from set.mm.
But we are looking for a choice function on
A
, and given an element ofA
, there might be multiple natural numbers whichF
maps to that element and no way to choose one of them that I noticed.
Luckily, the natural numbers come with a canonical choice function: choose the minimal one. Any inhabited subset of natural numbers should have a minimum element (constructively), you take the intersection of all the ordinals considered as sets.
from set.mm.
Any inhabited subset of natural numbers should have a minimum element (constructively),
You mean like https://us.metamath.org/ileuni/nnregexmid.html ?
from set.mm.
Any inhabited subset of natural numbers should have a minimum element (constructively),
You mean like https://us.metamath.org/ileuni/nnregexmid.html ?
A way to formalize Mario's original claim that you do not need the axiom of choice or any variant is to assume that the subset of natural numbers has decidable membership: "An inhabited decidable subset of natural numbers has a minimum element."
from set.mm.
A way to formalize Mario's original claim that you do not need the axiom of choice or any variant is to assume that the subset of natural numbers has decidable membership: "An inhabited decidable subset of natural numbers has a minimum element."
Oh, I think that works, using https://us.metamath.org/ileuni/ctssdc.html .
I've started in on this, and it is enough formalizing that it might take me a day or two to work this out, but at first glance it seems like it will work. Thanks for the suggestion.
Update: I don't think ctssdc helps the way I thought it would. Although the set s
from that theorem is decidable, the set which wasn't decidable was the set of indexes which map to a particular element of A
.
from set.mm.
Yes, the theorem I was thinking of assumes that the set has decidable membership. In this case, that amounts to a requirement that A
has decidable equality. If you don't have that, then I think you will not be able to prove the original claim. It might be better to have A
index a collection of sets instead of being a collection of sets, since there are some examples where the indexing set has decidable equality even if the sets themselves don't.
from set.mm.
See https://us.metamath.org/ileuni/cc3.html or https://us.metamath.org/ileuni/cc4.html for examples where the choice is on one set which is indexed by a second set, a countably infinite one. I'm going to consider cc3 and cc4 as sufficient solutions and close this issue, since they should make it possible to prove what you need to prove in this area.
from set.mm.
Related Issues (20)
- should iset.mm have both ax-bndl and ax-i12 ? HOT 2
- Appropriate names for +g and gsum HOT 1
- Appropriate name (and new symbol) for LSSum HOT 4
- Barycentric coordinates HOT 2
- Existence of a certain non-constant function implies the limited principle of omnisience HOT 10
- If not equal implies apart, Markov's principle follows HOT 2
- Updating mmset.html HOT 12
- Symbol and token for the class of semigroups HOT 9
- Update of the topological structure overview figure HOT 4
- Can a space filling curve exist in iset.mm? HOT 5
- The sine function is decreasing over [2,4] HOT 17
- Making SymGrp a structure restriction of EndoFMnd HOT 7
- Discourage indirect usage of ax-13? HOT 17
- Hypotheses with an "is a set" property using the universal class _V HOT 5
- Newbie here, I created a proof with mmj2. How do I add the proof to the database HOT 17
- </table> tags in AS's mathbox are outside <html> blocks HOT 3
- Interchanging factors in integrals and sums (Lemmas for AKS) HOT 4
- Contributor code RM is used twice HOT 1
- Feedback from a new user, improvement suggestions. HOT 23
- move polynomial section HOT 6
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from set.mm.