I'm enjoying this series, but can't shake the feeling that what you are showing is not the difficulties for constructivist mathematics per se, but the difficulties of conceiving it as "just" classical mathematics minus the law of the excluded middle.

Let’s say we flip the assumption around and start with the decidable finite cases as the "normal" ones. Then it is the introduction of undecidability and infinity that blurs things and invalidates the law of the excluded middle, and requires more care to avoid paradoxes and fallacies.

With this approach, we end up with a mathematics where the constructive portions look a lot more like our naive intuitions and experience of numbers, and the “stones” become those of classical mathematics.

I realize this might seem heretical to pure mathematicians trained in the last century or so ;-), but it is essentially orthodox in theoretical computer science, for example.

This is a wonderful series. Thanks for posting it!

The proofs so far seem all to rely on a "denotational" equality between propositions. It seems trivial that p or not p with such a coarse equality, since you can always just test whether p = T.

(Maybe I don't understand what you mean by an arbitrary truth value p in Omega--is that different from a proposition?)

This "denotational" equality seems inherently nonconstructive to me. What do we get if we use a finer equality? Is that meaningful in this setting?

I’m starting to doubt that sets are the proper abstraction to study. Wouldn’t lists be more appropriate?

If you do insist on using sets, I’d at least like to know what the word means to you. Is it something I can define in Agda, or do I need to postulate (⟨Set⟩ : Set) as well as all the ZFC axioms?

Reply to Jake (3): what do you mean by "test whether p = T"? It sounds like you expect equality to be somehow classical, i.e., two things are either definitely equal or definitely not-equal. In reality, the truth value p = T is p. Equality on the set of truth values Omega is the same thing as logical equivalence, i.e., p = q means (p => q) and (q => p). It's not like we get to choose different equalities on our sets. Equality is a primitive notion, and it makes perfect sense constructively.

Reply to Samuel (4): lists are too limited because not every mathematical object is a list, or the image of a list. I am doing constructive mathematics informally in the style of Bishop. But if you press me, I will say that I am using higher-order intuitionistic logic, i.e., the internal language of a topos. This would be a bit like an impredicative Agda in which Prop is a type. And by the way, ZFC implies classical logic (because the axiom of choice implies the law of excluded middle). There is IZF, intuitionistic Zermelo-Fraenkel, but I don't need that. Topos if fine, and most of the arguments can be rephrased in type theory, if you read "set" as "setoid" and Omega as Prop.

Andrej (5): no, I don't expect equality to be classical; I am coming at this with a syntactic prejudice, so whether some proposition p (to me, some syntax tree) is equal to T must be decided.

In the argument "if c(S) != 1 then S is not a singleton, therefore T != p and not p holds", I find it troubling that S not a singleton implies T != p. Can we not have a set S = {T, p} where we don't know whether T = p? Or, does it even make sense to call the set a singleton or not when we don't know whether T = p?

Jake (6): the details are as follows. Suppose S = {T, p}. The statement "S is a singleton" is equivalent to p. Indeed: if p holds then T = p and S = {T}, a singleton. Conversely, if S is a singleton then T = p, which means that p holds.

In other words, if you do not know whether p holds then you do not know whether S is a singleton, and vice versa. But if you know that S is not a singleton, then you know that p does not hold.

Maybe the right spin here is that the classical concept of cardinality is really not all that important. After all, it has rather poor properties when considered constructively, and I cannot think of very many things in math, other than those to do with cardinality itself, that rely on sets having definite sizes that are lined up linearly. It's just a weird, possibly irrelevant, and, in the infinite case, rather poorly defined notion (relying as it does on arbitrary functions) anyway.

Andrej (7): Thanks for the explication (and for editing my previous comment). In other words the existence of c implies that we know whether each S is a singleton or not, and therefore that p or not p.

[...] Read the original:  Mathematics and Computation » Constructive stone: cardinality of sets [...]

In the first proof you said: "Either c(S)=1 or c(S)≠1. ... This establishes p∨¬p."

IANAM (I am not a mathematician), but isn't this circular? You presuppose in the first sentence what you were trying to prove.

This is probably just a silly misunderstanding on my part, but anyway, I had to ask. :)</i>

Rok: there is no circularity. Here c is a function which maps into the natural numbers N. For the natural numbers we can prove by induction that forall n : NN, n = 1 or n != 1 (try it). So what you call "presupposition", namely that "either c(S) = 1 or c(S) != 1" is something that we can actually prove separately.

Ah, it really was a very silly remark. Thanks for the explanation. :)