 As an example, the Dedekind-infinity of the domain may be considered. A set \(S\) is Dedekind-infinite precisely when there exists an injective function from \(S\) to its proper subset. Let \(\phi_{inf}\) be the following sentence of  \(\mathbf{IFL}\):[37]