>>142
>構成的集合論では、ディアコネスクの定理は、選択公理が排中律を暗示していることを示しています

参考引用
https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
Diaconescu's theorem

In mathematical logic, Diaconescu's theorem, or the Goodman–Myhill theorem, states that the full axiom of choice is sufficient to derive the law of the excluded middle or restricted forms of it.

The theorem was discovered in 1975 by Radu Diaconescu[1] and later by Goodman and Myhill.[2] Already in 1967, Errett Bishop posed the theorem as an exercise (Problem 2 on page 58 in Foundations of constructive analysis[3]).
Proof
略
Other frameworks
In constructive type theory, or in Heyting arithmetic extended with finite types, there is typically no separation principle at all - subsets of a type are given different treatments. A form of the axiom of choice is a theorem, yet excluded middle is not.