>>13442423Subset of finite set necessarily being finite implies LEM.*
On the other hand, if you have choice then you have LEM and some subsets of finite sets become all finite.**
But this shouldn't be something you wonder about if you understand subsets/constructive logic, so I think you should read that up.
*Take any undecidable proposition P (or even unprovable in ZFC, like the continuum hypothesis suffices here).
Then the set
S := {u in {0} | (u is 0) and (P or not(P))}
is a subset of {0}. If you claim that that "x \mapsto x" is indeed a function from {0} to S, you claim that P or not(P) holds, which constructively means you can witness either other two given options.
**Take the subsets
X := {u in {0,1} | u=0 or (u=1 and P)}
Y := {u in {0,1} | u=1 or (u=0 and P)}
of {0,1}.
You know 0 is in X and 1 is in Y, but you nonetheless can't give me choice function f:{X,Y}->{01}.
If P is true then {(X,0), (Y,1)} is a choice function and if P is false then {X,Y}={X} and {(X,0)} is a choice function.
(Classically you say "well those are the options right? Right? And so some choice exists, even if I don't know what it is lel, I won't tell you any more details teehee")
