Moreover, I had the idea that Intuitionistic logic is advocated to curb with non-constructive proofs over non-finite sets rather than the simple case you mentioned.
And that attitude combined with a long chain of reasoning will wind up with you accepting that the following are entirely sensible statements.
"I accept that there exist real numbers which cannot ever be specified."
"I accept that there exists a reasonable computer science problem for which there exists a polynomial time algorithm but for which I cannot ever prove any algorithm correct."
If you do accept them as reasonable, it is worth carefully considering what the word "exists" actually means to you, and how someone else might think it should mean something different. IF you come to the conclusion that it should mean something different than what is implied by those statements, then you should take another look at constructivism. :-)
But we are now talking about the existence of something that cannot be specified or written down in any useful way, shape, or form. What does it actually mean to say that this exists? We've demonstrated that no direct evidence of existence can ever be found. This is pretty much the opposite of what a lot of people would actually want "existence" to mean.
From a classical point of view what is wrong is your notion of existence. But it is perfectly reasonable to instead conclude that it is classical mathematics which has gone off the rails and they are now using words like "existence" in a nonsensical way.
Both points of view are perfectly defensible. In fact it was proven by Goedel that any inconsistency in one leads to an inconsistency in the other. Therefore neither is actually able to claim to have a better grounding in logical consistency than the other. Historically the debate was that classical mathematics is more convenient to work with, while constructivism actually means something more reasonable.
But once the set paradoxes faded, and with no difference in consistency, the simplicity of classical mathematics won.
There are also cases of interest beyond constructivism: what if a number is non-constructible but can be approximated? Saying it doesn't exist doesn't sound particularly useful.
Not much. The philosophy of math is not noted for being particularly useful. :-)
That said, historically constructivism arose during a period when math was having trouble creating solid foundations. Today we can talk about "the reasonable existing logics". But a century ago you couldn't. Attempts to create such a thing had repeatedly resulted in paradoxes, and an inability to find solid foundations had caused repeated mathematical crises for a century.
In that light, it was reasonable to doubt lines of reasoning that proved the existence of things in infinite sets but provided no way to actually find them. This smelled too much of the kinds of things that had lead to paradox.
Hence the appeal of a philosophy that insisted that things are only known to exist when we have constructions for them. Proofs are only valid when they follow lines of reasoning that can, at least in principle, actually be followed in finite time.
These days this is mostly a historical footnote. But an important one.
There are also cases of interest beyond constructivism: what if a number is non-constructible but can be approximated?
Um, actually a constructivist would say that that number exists.
To understand, you have to ask what a real number is. One definition of a real number is a Cauchy sequence of rational numbers. Which is to say an infinite series of rational numbers that converges. Constructivists make this more precise. Rather than talking about an infinite series of rational numbers, they talk about a algorithm that generates a series of rational numbers. Rather than saying "for every epsilon greater than 0 there exists an N..." they insist that there is an algorithm which can take in epsilon and spit out N. Combining these two, from a valid specification of a real number, you can generate an algorithm that given an epsilon > 0 can generate a rational number within epsilon of the real number. And an algorithm that does that can easily be turned into a Cauchy sequence.
Thus to a constructivist, being able to approximate a number arbitrarily well is perfectly fine as a definition of said number. Things get odd in that you can have two different constructions of real numbers but you don't always know whether they are specifying the same number. But you quickly get used to this.
Saying it doesn't exist doesn't sound particularly useful.
Let me turn that around.
What is the use of asserting the existence of things that you cannot construct? What are you going to do with something that you cannot find in an infinite haystack? A thing that may be impossible to find, even in principle?
Expanding further, that's an issue I've had with definitions of computability also. Certain problems like the halting problem are extremely interesting but their non-computability sort of turns them dead. Approximating them even to a finite degree and studying them profoundly seems very worthwhile, from a practical and theoretical standpoint.
To a constructivist, sqrt(2) is a perfectly reasonable number. I can write down an algorithm to approximate it to any desired degree. I can describe its properties. I can find ways in which it arises naturally. I can compare it to rational numbers. It is quite reasonable to talk about its existence.
What constructivists object to are pure existence proofs. Take the numbers that I was describing. A classical proof of their existence would be to demonstrate that the set of such numbers has measure greater than 0. Therefore they both exist, and there are lots of them. But now we're stuck. What can we say that is sensible about them?
There are lots of them! There are some over here. There are some over there. How about some that start off with 1.2345678910111213...? Nope, we can compress the start of that one too easily. How about some that start off with 3.14159265359...? Nope, we can compress the start of that one too easily. How about ones that start off with 0.45399480855940464218372115598800974602442341777409214271555307732203389646276632569332825355032120233072728272048609801012859425779656167823065863748297...? Hrm, kind of hard to tell, we'd need to enumerate the output of a ton of programs and we might not be able to figure out whether some of them halt so if there are, we can't find out. But there are lots of them! Promise!
This is a fairly strong example demonstrating how existence to a classical mathematician does not agree with what a constructivist means.
I agree that it doesn't seem to make sense in that case. However, there are practical use for constructive proofs, for instance, program extraction. Consider a proposition such that "for all list L, there is a list L' such that L' is sorted and L' is a permutation of L". From a constructive proof of that proposition, you can extract a sorting algorithm. This works basically because the constructive proof has to exhibit a witness. That's the kind of things you can do with the Coq proof assistant.
"you may not be able to prove that Anne is married or prove that Anne is unmarried, but can't you prove by that Anne is either married or unmarried, by the definition of marriege?"
You can't prove it in constructive logic. You can always add an axiom of the form "for all x, x is married or x is not married". However, if you do that, your proof won't be constructive anymore (unless you provide a decision procedure together with your axiom).
Dog was the first thing that came to my head that would have a proper noun(Name) that wasn't a person. Didn't see a reason to change it? Interestingly though, I do prefer cats.