Skip to main content
added 3 characters in body
Source Link
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

Au contaire. Like all questions of this kind it depends on the wording.

Let $S$ be an inhabited set of inhabited sets, so we are givengiven $x_0\in X_0)\in S$$x_0\in X_0\in S$.

If we are also givengiven bijections $f_{X,Y}:X\cong Y$ for each pair $X,Y\in S$ then in particular we have $f_{X_0,Y}:X_0\cong Y$.

Therefore there iswe have a defined element $y=f_{X_0,Y}(x_0)\in Y$ for each $Y\in S$.

No Choice required, if the question is understood in this way.

Indeed, by substituting "inhabited" for "non-empty", Excluded Middle is also avoided.

Au contaire. Like all questions of this kind it depends on the wording.

Let $S$ be an inhabited set of inhabited sets, so we are given $x_0\in X_0)\in S$.

If we are also given bijections $f_{X,Y}:X\cong Y$ for each pair $X,Y\in S$ then in particular we have $f_{X_0,Y}:X_0\cong Y$.

Therefore there is a defined element $y=f_{X_0,Y}(x_0)\in Y$ for each $Y\in S$.

No Choice required if the question is understood in this way.

Indeed, by substituting "inhabited" for "non-empty", Excluded Middle is also avoided.

Au contaire. Like all questions of this kind it depends on the wording.

Let $S$ be an inhabited set of inhabited sets, so we are given $x_0\in X_0\in S$.

If we are also given bijections $f_{X,Y}:X\cong Y$ for each pair $X,Y\in S$ then in particular we have $f_{X_0,Y}:X_0\cong Y$.

Therefore we have a defined element $y=f_{X_0,Y}(x_0)\in Y$ for each $Y\in S$.

No Choice required, if the question is understood in this way.

Indeed, by substituting "inhabited" for "non-empty", Excluded Middle is also avoided.

Source Link
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

Au contaire. Like all questions of this kind it depends on the wording.

Let $S$ be an inhabited set of inhabited sets, so we are given $x_0\in X_0)\in S$.

If we are also given bijections $f_{X,Y}:X\cong Y$ for each pair $X,Y\in S$ then in particular we have $f_{X_0,Y}:X_0\cong Y$.

Therefore there is a defined element $y=f_{X_0,Y}(x_0)\in Y$ for each $Y\in S$.

No Choice required if the question is understood in this way.

Indeed, by substituting "inhabited" for "non-empty", Excluded Middle is also avoided.