Axiom of choice for infinite strictly descending chains of subsets. Let $X$ be an infinite set. Then there are infinite stictly decreasing chains of subsets of X. Does this fact require axiom of choice? If yes, what is the choice of function?
 A: We say that a set is Tarski-finite if every [non-empty] $\subseteq$-chain of subsets has a minimum and maximum elements. We say that a set is Dedekind-finite if it has no proper subset which is equipotent with it, and this turns out to be equivalent to the fact that there are no countably infinite subsets.
It is not hard to show that every finite set is Tarski-finite, and every Tarski-finite is Dedekind-finite. Simply because if $X$ is Dedekind-infinite it has a countably infinite set $\{x_n\mid n\in\mathbb N\}$ and we can take $X_k=\{x_n\mid n<k\}$ to be a chain without a maximal element.
Without the axiom of choice it is consistent that there are infinite Dedekind-finite sets. But not all Dedekind-finite sets have to be Tarski-finite sets. For example if there is a Dedekind-finite set of reals $D$ then the sets $D_r=\{x\in\mathbb R\mid r<x\}$ is an infinite decreasing chain of subsets.
However it is consistent that there are infinite Tarski-finite sets. For example an amorphous set is an infinite set which cannot be written as a disjoint union of two infinite sets. It is consistent that such amorphous set exists, and one can show that every amorphous is Tarski-finite.
But it is also consistent that there are infinite Dedekind-finite sets, but no infinite Tarski-finite sets. One provable property of Tarski-finite sets is that they cannot be linearly ordered (then we can construct a decreasing chain like with $D$ above). There are models in which there exists an infinite Dedekind-finite set, and every set can be linearly ordered (e.g. Cohen's first model). In such model, it follows, there are no infinite Tarski-finite sets.
So the answer is yes, we need the axiom of choice. But how much exactly is quite little, if all infinite sets are Dedekind-infinite then this should be true and this would already require less than countable choice; but as I wrote before, just for Tarski-infiniteness we require even less.
Furthermore note that if there is one decreasing chain then there are infinitely many (we can take subsets of the decreasing chain; or take some finite translation of all the sets in the chain). So either there are none, or there are infinitely many of them.
As for the actual function, the exact amount of choice does not reveal to you what is the function or the chain. Much like the axiom of choice is not constructive, so are weak choice principles are not constructive. If you add more assumptions, for example that the set is a set of real numbers, it's possible to actually define such chain, but this is not necessary.
The last part is a reasonable question, but I feel it is a wrong question to ask. Let me explain why. The axiom of choice guarantees the existence of choice functions, and from such functions we can define all sort of objects. We may define a well-ordering of our infinite set, or a well-ordering of its power set. We use choice functions to prove the existence of other objects, and from those objects we prove the existence of more objects, and so on. At some point the actual choice function becomes murky and we cannot really say what is the choice function, or what is the one necessary only for that sort of result.
We know that we may use the axiom of choice to prove that every infinite set is Dedekind-infinite, in which case the proof in the second paragraph easily shows how to generate a decreasing chain. Countable choice is sufficient for this. However if we can prove that every set is linearly ordered then we can also create decreasing chains of subsets, and it is consistent that every set can be linearly ordered but countable choice fails (and vice versa, actually).
So what is the choice of $f$? In the most general and simple answer, fix a choice function on $\mathcal P(X)\setminus\{\varnothing\}$ from which we may well-order $X$ and write it as $\{x_\alpha\mid\alpha<\kappa\}$, where $\kappa$ is some infinite ordinal. Then we can easily create many decreasing chains.
The important part about the axiom of choice is to know that it allows us to prove certain things exist; and we can use them. It is also important that a lot of the weak choice principles are not actually described in existence of choice functions, but rather in existence of some other objects (e.g. ultrafilters, linear orders, partitions, subsets, etc.) from which we can prove the existence of further objects.
A: Even without the Axiom of Choice, a set $X$ is Dedekind infinite iff there exists an injective map $f\colon\mathbb N\to X$.
For $n\in\mathbb N$, let $A_n=\{f(k)\mid k\ge n\}$. This is an infinite strictly decreasing chain.
However for infinite without Dedekind, you may need at least countable choice (to find $f$).
