Jetzt fünfzehn Prozent verfassungskonformer.

A short thought on the axiom of choice
Thu, 11 Aug 2016 16:14:34 GMT

It is a well-known fact that ZFC\vdash_i TND:

Assume we wanted to prove \neg Q \vee Q. We can then, by the schema of specification, define the sets A := \{x\in 2\mid x = 0\vee Q\} and B := \{x\in 2\mid x = 1\vee Q\}. We constructively know that both sets are non-empty: At least 0\in A and 1\in B. Therefore, \{A, B\} is a set of non-empty sets, and therefore, by the axiom of choice, there is a function g such that g(A)\in A and g(B)\in B, that is, we know that g(B)=0\vee g(B)=1 and g(A)=0\vee g(A)=1. Trivially, g(A)=1\rightarrow Q, hence, g(A)=0\vee Q. Similarly, g(B)=1\vee Q. Hence, g(A)\neq g(B)\vee Q. On the other hand, Q\rightarrow A=B=\{0,1\}, therefore also Q\rightarrow g(A)=g(B). Contraposition (which is constructive in this direction) yields g(A)\neq g(B)\rightarrow \neg Q. Hence, \neg Q\vee Q.

Now, in my opinion, the problem here is not the axiom of choice. Let us recall what the axiom of choice says: If we proved that every set in a collection has an element, then we can find an element for every such set. I find this principle very constructive: If we can prove that something exists, then we can find it. As long as we cannot prove the existence of things that we cannot find, the axiom of choice should not do any harm to constructivity, as far as I see – correct me if I am wrong.

Of course, if you can prove the existence of things that you cannot find, the axiom of choice might make the situation worse. And in my opinion, in the case of ZFC, in this proof, the schema of specification is the actual culprit. Whcih is why I wonder why even some "constructive" set theories have a similar axiom scheme. For some reason, the impression that "smaller" sets are always simpler than "larger" sets is prevalent, and from that perspective, separation is not a problem. I wonder where this comes from.

Even without any deeper knowledge of recursion theory or logic, it should be clear that while the set of natural numbers \mathbb{N} is rather simple, there are subsets which are more complicated. Of course, you can encode the halting problem into a subset of \mathbb{N}, but you don't have to go that far: Consider the set of prime numbers. It is intuitively more complicated than \mathbb{N}. (This somehow reminds me of the concept of entropy, considering the "amount of information" encoded in a set. Not sure whether there is a formal correspondence, though.)

An obvious limitation one could impose to comprehension-like schemes would be that the propositions used need to be provably decidable. This would break the above proof in the sense that Q would be decidable from the start. And it makes more sense in a constructive setting: If we assume that we can decide a set, the resulting set would still be decidable. Not sure whether there exists a constructive set theory with such an axiom, though.

Just my two cent. Feel free to enlighten me if I am wrong.