令$\operatorname{\mathscr{P}}(X) = \{Y \mid Y \subseteq X\}$表示$X$的幂集,集合$X$称为Dedekind有限集意谓每个$X \to X$的单射都是满射.
命题:若$\operatorname{\mathscr{P}}\operatorname{\mathscr{P}}(X)$是Dedekind有限集,则$\operatorname{\mathscr{P}}(X)$的任意非空子集有关于$\subseteq$的极小元.
我的问题:能否不使用自然数和无穷公理证明上述命题?
如果必须使用无穷公理感觉有些怪异,很难想象一个纯粹关于有限集的命题需要无穷公理,但是又找不到不用无穷公理的证明QAQ
如果必须使用无穷公理,那么还有哪些关于有限集的命题必须要无穷公理呢?
@geelaw 既然谈到了这个概念，显然不能自动假设选择公理成立，此时 Dedekind 有限的集合可以不是有限集，实际上“$S$ 是 Dedekind 有限”（包括有限和无限的情况）当且仅当“不存在 ${\mathbb N\to S}$ 的单射”，这说明 Dedekind 有限（的无限）集和 $\mathbb N$ 有密切的联系。
主要是 Dedekind无穷不需要$\mathbb{N}$来定义,让我产生了"有没有什么办法绕过它"的想法.常规的不用AC的证明是反设$X$无穷,令$f_n = \{Y \subseteq X \mid \operatorname{Card}(Y) = n\} \neq \varnothing$,则 $f \colon \mathbb{N} \to \operatorname{\mathscr{P}}\operatorname{\mathscr{P}}(X)$是单射,一个关于有限的结果用无穷公理证明感觉有些奇怪 /asnowwolf-amused
@geelaw 好像说反了？任何关于“任意有限集”的命题都必然需要 $\mathbb N$ 才能写下来，因为“$X$ 有限”的定义是“存在 ${y\in\mathbb N}$ 使存在 ${X\to y}$ 的双射”，应该问的问题是：哪些只和 Dedekind 有限集相关的命题必须用到 $\mathbb N$？
那不一定吧,比如Kuratowski有限集就不需要用自然数和$\mathbb{N}$定义,但是跟你的定义是等价的.而且感觉用到自然数也未必需要无穷公理,例如可以将$n \in \mathbb{N}$看作"$n$是有限序数"的缩写或许可以避免使用无穷公理?
似乎自然数可以作为有限序数$Fin(n)$指$k\leq n \implies k = 0\lor (\exists m)k = m+1$表述?
无穷公理只是说"存在(Kuratowski或者与之等价意义的)无穷集",不用自然数是指用等价的定义(例如Kuratowski)替代标准定义,因为关于有限集的证明也不一定非要证明各种等价定义的等价性才能证明,而我问的某种意义上就是"是否必须证明定义的等价性才能证明那个命题?"
@geelaw 🤔 但是“Kuratowski 有限等价于是自然数”这句话本身也需要“自然数”，删去无穷公理后，等价性本身无法表述？
他的意思是你一开始符号打错了，$A$ 和 $X$ 混淆。
后面$A$和$X$是我昏头了打错了当然$A=X$我改一下 /asnowwolf2-tear
geelaw OK 我觉得我有必要澄清一下之前的想法，我从某个时刻开始把问题考虑为：能否在 ${ZF-\infty}$（没有无穷公理的 ZF 集合论）里面证明题设命题？如果可以，说明证明不需要无穷公理，否则说明需要。
在 #3 的证明，起初我觉得不用无穷公理无法“说出来”，后来我觉得可以考虑把作出的 $f$ 作为类映射使用？
在跟映射密切相关的命题的证明里拿出类映射来，至少在ZF里是不是不太合乎周礼合适 /asnowwolf-worry
话说虽然同样都不在ZF/ZF-Inf内部，但是感觉这里$\omega/\mathbb N $和真类不太一样，而是更像ZF(C)里谈论大基数，毕竟真类是真的不适用一些集合公理会引发矛盾的，但归纳集只是像ZF里的大基数一样不知道是否存在.
不过ZF-Inf是不是属于ZF研究里倒数的（不可能有人减掉存在/空集公理或者外延公理研究ZF吧？），这套公理应该相当无聊吧.
@geelaw OK 我觉得我有必要澄清一下之前的想法，我从某个时刻开始把问题考虑为：能否在 ${ZF-\infty}$（没有无穷公理的 ZF 集合论）里面证明题设命题？如果可以，说明证明不需要无穷公理，否则说明需要。
在 #3 的证明，起初我觉得不用无穷公理无法“说出来”，后来我觉得可以考虑把作出的 $f$ 作为类映射使用？
在NBG里倒是可以考虑$\mathbb{N}$作为所有有限序数的类,无穷公理只是(等价地)断言$\mathbb{N}$是集合.虽然我也不是很执着要在ZF-inf里考虑,但是因为关于有限集的许多命题甚至不需要自然数就可以证明而且命题的叙述并不需要自然数,所以我希望不仅避免无穷公理而且避免任何自然数来证明,很显然常规证明是行不通的只是我不知道有没有别的办法.
@涂效灰 在跟映射密切相关的命题的证明里拿出类映射来，至少在ZF里是不是不太
合乎周礼合适 /asnowwolf-worry
话说虽然同样都不在ZF/ZF-Inf内部，但是感觉这里$\omega/\mathbb N $和真类不太一样，而是更像ZF(C)里谈论大基数，毕竟真类是真的不适用一些集合公理会引发矛盾的，但归纳集只是像ZF里的大基数一样不知道是否存在.不过ZF-Inf是不是属于ZF研究里倒数的（不可能有人减掉存在/空集公理或者外延公理研究ZF吧？），这套公理应该相当无聊吧.
怀疑是因为ZF-inf被研究得比较清楚了,只是我不知道 /asnowwolf2-tear
如果没有无穷公理，那我们既没法讨论一个不是“有限集”的集合是什么样的，也没法谈论“所有‘有限集’”.
@Hypatia 如果必须使用无穷公理感觉有些怪异,很难想象一个纯粹关于有限集的命题需要无穷公理,但是又找不到不用无穷公理的证明QAQ
其实这个命题并不是“纯粹关于有限集的命题”：我们不知道讨论对象是不是“有限集”.真正纯粹关于有限集的命题应该是像“有限集和有限集的并还是有限集”“有限集的幂集也是有限集”这样的命题.
我们很容易知道我们熟知的有限集必定是戴德金有限集（等价的）并且有$\subseteq $的极小元（所以如果默认讨论对象是有限集，那这个命题压根用不着讨论）.也因为这样，我们要证明这个命题要么间接证明，比如假设存在一个“无穷”$\subseteq-$链，这很难绕过“所有‘有限集’的集合”或者非有限集；要么绕过有限集，直接证明，但我很难想象怎么找出这样的$\subseteq $极小元.（如果是有限集可以通过操作有限次来找出来）
@Hypatia 怀疑是因为ZF-inf被研究得比较清楚了,只是我不知道 /asnowwolf2-tear
主要是……如果没有无穷公理，一本集合论书基本上就没什么东西可讲了。连冯琦都说过学集合论的基本上只处理不小于$\aleph_1$的问题 /asnowwolf2-poker-face
关于
@Hypatia 如果必须使用无穷公理,那么还有哪些关于有限集的命题必须要无穷公理呢?
我倒是想到一些独立于皮亚诺公设的数论问题（不能在逻辑上就使用超穷手段），比如古德斯坦定理 /asnowwolf-amused
有限集在没有无穷公理的时候貌似可以这么定义：若序数$\alpha$的任意非零元素都是后继序数，则称$\alpha$是有限序数。与某个有限序数等势的集合称为有限集。
另外，在ZF中将无穷公理换成它的否定的理论（也就是$\mathsf{ZF}-\mathsf{Inf}+\neg\mathsf{Inf}$）也是有研究的，又叫作$\mathsf{ZF}_{\mathsf{fin}}$，可以证明$\mathsf{ZF}_{\mathsf{fin}}$下面所有的非零序数都是后继序数，且选择公理成立。所以楼主的问题或许可以这么迂回地处理：利用排中律得到$\mathsf{Inf}\vee\neg\mathsf{Inf}$，然后分别对$\mathsf{Inf}$与$\neg\mathsf{Inf}$成立的情形给出证明。
@tyj518 有限集在没有无穷公理的时候貌似可以这么定义：若序数$\alpha$的任意非零元素都是后继序数，则称$\alpha$是有限序数。与某个有限序数等势的集合称为有限集。
另外，在ZF中将无穷公理换成它的否定的理论（也就是$\mathsf{ZF}-\mathsf{Inf}+\neg\mathsf{Inf}$）也是有研究的，又叫作$\mathsf{ZF}_{\mathsf{fin}}$，可以证明$\mathsf{ZF}_{\mathsf{fin}}$下面所有的非零序数都是后继序数，且选择公理成立。所以楼主的问题或许可以这么迂回地处理：利用排中律得到$\mathsf{Inf}\vee\neg\mathsf{Inf}$，然后分别对$\mathsf{Inf}$与$\neg\mathsf{Inf}$成立的情形给出证明。
我还是挺好奇的，$\mathsf{ZF}-\mathsf{Inf}+\neg\mathsf{Inf}$研究出了什么有意思的东西吗？
@涂效灰 如果没有无穷公理，那我们既没法讨论一个不是“有限集”的集合是什么样的，也没法谈论“所有‘有限集’”.
其实这个命题并不是“纯粹关于有限集的命题”：我们不知道讨论对象是不是“有限集”.真正纯粹关于有限集的命题应该是像“有限集和有限集的并还是有限集”“有限集的幂集也是有限集”这样的命题.
我们很容易知道我们熟知的有限集必定是戴德金有限集（等价的）并且有$\subseteq $的极小元（所以如果默认讨论对象是有限集，那这个命题压根用不着讨论）.也因为这样，我们要证明这个命题要么间接证明，比如假设存在一个“无穷”$\subseteq-$链，这很难绕过“所有‘有限集’的集合”或者非有限集；要么绕过有限集，直接证明，但我很难想象怎么找出这样的$\subseteq $极小元.（如果是有限集可以通过操作有限次来找出来）主要是……如果没有无穷公理，一本集合论书基本上就没什么东西可讲了。连冯琦都说过学集合论的基本上只处理不小于$\aleph_1$的问题 /asnowwolf2-poker-face
关于
我倒是想到一些独立于皮亚诺公设的数论问题（不能在逻辑上就使用超穷手段），比如古德斯坦定理 /asnowwolf-amused
关于“这不是`纯粹关于有限集的命题'”能具体讲讲吗?是指我们不能先验地认为$X$是有限集吗?
如果是这样的话却又可以不用$\mathsf{inf}$证明命题"若$\operatorname{\mathscr{P}}(X)$有限则$X$有限"而同样不能先验地认为$X$有限,如果认为这个命题也不是"纯粹关于有限集的命题"而这两个命题的(常规/熟知的)证明方法却表现出了明显的区别,那么如何界定"纯粹关于有限集的命题" /??
感觉二战前关于有限集的研究还是有一些的,可能专家们都比较关心没解决的问题吧(sigh)这也是我觉得"是不是前人已经研究过了只是我不知道的''的原因.
确实现在的问题就在于不知道有没有办法绕过标准自然数 /TT