I am surprised that the following theorem requires axiom of choice:
Theorem: For any real number x, there is a sequence x̂ : ℕ → ℚ converging to x.
It seems to me that it has a constructive proof with computable x̂, it goes like this:
To calculate x̂(n):
Start with a = 1, repeat a = a * 2 while |x| > a. This will end in a finite number of steps.
Start with the segment [-a, a]. On each step split it in half and pick the half that contains x (if x is exactly in the middle, pick the left half). Repeat this exactly n times. The last splitting point is x̂(n).
Here we have an algorithm that calculates x̂(n) in a finite number of steps for any particular x and n, so x̂ is computable.
What is happening, I think, is that the other side is not expressed when the person is talking to you. It is also possible that the person cannot properly verbalise the other side. Neither means that the other side doesn’t actually exist.
A typical mistake that psychotherapists are taught to avoid early on is to imagine that they are seeing the whole person when a client is passionately telling them how they can’t be with their spouse, how they can’t bear their job, etc. A conflict can’t exist if there is only one side to it.
And of course, being in such a conflict (or empathising with it) can be frustrating and unattractive.