嘿，这个问题戳中了直觉主义和经典逻辑核心差异的关键点，咱们一步步把它掰明白：

首先得搞清楚直觉主义逻辑里的“存在”和经典逻辑的“存在”根本不是一回事——这是整个问题的核心。经典逻辑里的“存在”是“非空即存在”，哪怕你找不到具体的例子；但直觉主义逻辑是构造性的，“∃x P(x)”这句话的意思是你能实实在在地构造出这个x，或者给出找到它的有效方法。

那作者说“选择公理在直觉主义里平凡”，指的是那个构造性的选择原理：如果对每个a∈A，集合B_a都是非空的（这里的非空在直觉主义里就是“能构造出B_a里的一个元素”），那必然存在一个选择函数f:A→∪B_a，让f(a)∈B_a对每个a都成立。说白了，这个命题根本不需要额外当公理——因为每个B_a都能拿出一个具体元素，把这些拿元素的方法拼起来就是选择函数了，完全是构造性推理的自然结果，可不就是“平凡”嘛。

那为什么经典逻辑里它成了“外星怪兽”？因为经典逻辑抛弃了构造性要求：B_a非空仅仅是“不存在所有B_a都为空的情况”，但你根本不用拿出具体的元素来。这时候的选择公理是非构造性的——它硬说存在这么个选择函数，但完全不要求你能构造出来。这个版本的选择公理强到能推出排中律（LEM），比如你可以用它证明“要么P成立，要么¬P成立”，这在直觉主义里是绝对不允许的，因为直觉主义不接受“非黑即白”的无构造性断言。

你看到的相关讨论里提到的“弱版本”，就是刚才说的这个构造性选择原理，它和经典逻辑里的“完整版选择公理”的核心区别就在这：

• 弱版本（直觉主义平凡款）：依赖构造性，每个B_a的“非空”都对应一个可实现的元素选取方法，所以选择函数天然存在，推不出排中律。
• 完整版（经典逻辑怪兽款）：不要求构造性，仅仅断言选择函数存在，不管能不能找到。这个版本在经典逻辑体系下可以直接推出排中律，因为它允许你在没有具体方法的情况下“凭空”选择元素。

顺带提一句，很多文献会刻意区分这两个概念：把直觉主义里这个平凡的构造性命题叫“选择原理”，把经典逻辑里那个非构造性的强公理叫“选择公理”，就是为了避免混淆——作者说的“直觉主义里选择公理平凡”，其实就是在这个区分下说的。

备注：内容来源于stack exchange，提问作者Lave Cave