@MihaHabič If $f$ and $g$ are permutations of $S$, then the assignment $h: X \mapsto S \setminus g[S \setminus f[X]]$ is an order isomorphism of the power set lattice of $S$. Is $h$ induced by a permutation of $S$?

Sorry, I read hastily and linked the adjective 'natural' to 'isotone injection' (rather than to 'instance'). I'll think about your question, I don't know the answer off the top of my head.

@JoelDavidHamkins I don't even know what 'natural isotone injection' means in this context. Is it something related to the independence of CH from ZFC? I'm not familiar with the details of any proof of Cohen's result.

@HighAsAKiteOnMath It wouldn't fit the thread, especially because I've eventually concluded that the mysterious proof alluded to in the OP is probably Nagell's proof. (I'll delete this comment in the future.)

In the commutative case (where the two definitions agree), $\mathfrak I_{\rm fin}(S)$ has been extensively studied by people in multiplicative ideal theory as an important special case of a (weak) ideal system. With that said, one could always define $\mathfrak I_{\rm fin}(S)$ as the subsemigroup of the ideal semigroup generated by the ideals that are finitely generated in the usual sense. In hindsight, I'm more or less convinced that this would be more natural than adopting the alternative definition of 'finitely generated ideal' suggested in the OP.