I've only really seen constructivism talked about by people who actually have a strong math background. Because it is hard to speak out against, say, the classical notions of existence that say that there are more real numbers than rational ones unless you actually understand why the classical proofs don't work constructively. And not just as, "We don't allow that proof."

To make that concrete, let's use computable analysis as a foundation for constructivism. In short, we represent Cauchy sequences as computer programs about which we can prove things in our favorite axiom system. You can build up a version of real analysis from that. It is easy to attempt Cantor's diagonal argument. You'll get a concrete program. But it will only represent a real number in our system if our axiom system can prove that every program it proves works, works as proven. This immediately brings up consistency. And so Gödel proves that showing this program represents a computable number in our system would imply our axioms to be inconsistent. (Bad axioms! Bad axioms!) And therefore Cantor's proof fails to produce a number in our system.

Of course classically we would say that if the axioms are consistent, then the program will compute a Cauchy sequence. And so it really does represent a real number even though we couldn't verify it. But whether we accept this alternate argument is a question of philosophy, not logic.

Therefore the truth of Banach-Tarski has nothing to do with any statement you can readily make about the integers, which would include any statement that you can make about anything that can be done on a Turing machine.

Incidentally the whole debate about constructivism is much more subtle than you likely appreciate. For instance it is trivial to prove that almost all real numbers that exist, cannot be written down. (Proof, I can easily write out a countably infinite set of statements that could define real numbers. So the set of real numbers that can be written down is countable. But there are an uncountable number of real numbers, so almost all cannot be written down.) In what sense do said real numbers actually exist?

If our axioms say that numbers must exist, which have in a very real sense no actual existence, then are those axioms capturing what we want to mean by "exist"?

If you say it does not, then you're a constructivist who hasn't thought carefully enough yet. If you say it does make sense, then you've been brainwashed by decades of standard mathematical presentations into accepting a definition of "existence" that makes no sense to the average lay person. :-P

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?

The world of ZFC doesn't feel very constrained by the actual universe, is all.

And if you don't like ZFC, you can pick another set of axioms entirely- there are several alternatives.

How's this different to a set of facts as you say, like one unit + one unit is two units? It's not. I'm not sure of this, but I'd say you could construct a set of axioms based on those facts that is compatible with the ZFC axiom set.

So, why choose ZFC? Because it's simple to define (how'd you formally define what is a unit, and what does the + operation mean?) and because it's more or less consistent with our world. We can extrapolate the things we find while doing mathematics to the real world. And, sometimes, we can discover things of the real world based on findings on things that don't exist. Complex numbers, for example: they don't exist, but they're really useful to define and explain electrical experiments [3].

We approach all of mathematics like this because its easier to study everything within the same system. And it's important that we keep a consistent underlying system so we can be sure that everything we discover based on the set of axioms and rules we've defined is true in a mathematical sense; and then those discoveries could describe our world. Wouldn't we have a consistent system, we could end up with contradictions. If we extracted mathematical concepts from the real world, we wouldn't be sure if a discovery we make from those concepts can be applied to the real world.

TL;DR: Our set of axioms describes properly the real world, is simple and consistent enough and that enables us to infer new ideas that can be applicable to the real world too.

[1] http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_th... [2] http://en.wikipedia.org/wiki/Axiom_schema_of_specification [3] http://en.wikipedia.org/wiki/Complex_number#Electromagnetism...

I don't think Russel's paradox is a problem with ZFC set theory. Building sets out of "the set of everything" is not used, and even people are careful to specify when the axiom of choice is being used.

> Building math on saying "this exists" without actually building towards what it is, is a bit of a "sin".

It's actually not. The idea is that you prove only what you actually need for the next step. A nice example is again in the field of differential equations. Ultimately people are interested in a solution, but to get that solution you need an approximation method, and to get an approximation method you need to know when does it work and how fast does it work, and to know that you need to know when a solution can be found and what properties does it have.

Constructivism is something that in theory might sound interesting, but forcing all mathematics to fit that model only servers to make certain proofs of true and useful statements far more complicated or even impossible.

But respectfully, ZFC came about because of logical paradoxes that couldn't be accepted as consistent.

You can create a new number system and derive all kinds of consequences but the truth is, most mathematicians care more entirely about prime number theory on the naturals that are entirely based on counting.

Most of modern math is based on the natural numbers. You can't remove all intuition. The thread that holds our love for math is also the same one that tells us we are exploring consequences that tell us a dearth about our universe.

I said that as soon as you fix some axioms (such as those of classical FOL), the conclusions are irrefutable. This is where mathematics begins. The question where those axioms come from or whether they are "true" are philosophical. The two disciplines are related, but separate.

Lots of mathematicians have different "foundational" beliefs from each other; some have studied or deeply thought about the philosophy, others may just speak to their intuition. However, this doesn't change the fact that they all come to the same conclusions from the same premises. E.g. a constructivist wouldn't be able to claim that a classical proof is "wrong", only that it's non-constructive and therefore unacceptable for some (philosophical or practical) reason; in fact non-constructive proofs can be seen as constructive proofs of some meaningless strings (e.g. the constructivist will maybe dispute the fact that there are discontinuous functions, but they will certainly accept the existence of a first-order derivation of the string representing "not all functions are continuous" from the axioms of set theory), the constructivist would just dispute that there is any meaning to these strings...

It's only incompleteness if the CH is true or false at the semantic level, "outside" of the logic system under discussion.

But the CH may be neither true or false, semantically, if the meaning of "existence of a set whose cardinality is strictly between that of the integers and the real numbers" strictly depends on the axioms and logic used to define sets and real numbers.

Can you give relevant pointers? I'm curious because while I do know a couple of arguments for the inconsistency of ZFC, none of these are related to the Banach–Tarski paradox or similar nonintuitive results.

Also I'd like to stress that ZFC and ZF are exactly as consistent: If ZF is consistent, then so is ZFC (and vice versa). This meta-result is proven in a very weak finitary logical meta-system ("PRA"), hence can be trusted even if one is wary of set-theoretic infinities. The keyword is "Gödel's constructible hierarchy".

In this line, there are even more astonishing meta-theorems, all provable in PRA:

* From any ZFC-proof of a purely number-theoretical statement (a statement which refers only to natural numbers), any usage of the axiom of choice can be mechanically eliminated. That is, any ZFC-proof of such a result can be transformed into a ZF-proof.

* From any ZFC-proof of a statement of the form "for all numbers n, there exists a number m such that ...", where in "..." no more quantifiers ("for all", "there exist") appear, any usage of the law of excluded middle ("any statement is either true or not") can be mechanically eliminated. That is, any such ZFC-proof can be transformed into a proof in IZF ("Intuitionistic Zermelo–Fraenkel"). The keyword is "double negation translation".

These meta-theorems indicate that the axiom of choice and the law of excluded middle can be regarded as "mathematical phantoms". Just as the complex numbers work wonders for us but can be compiled away to pairs of real numbers, these set-theoretic principles promise to work wonders for us and their usage can be compiled away if we wish so.

As a sibling comment mentioned, most mathematicians have a sense of truth that is not bound to any axiom system.

I don’t think it’s contradictory to work in ZFC whilst simultaneously having a non-axiomatic notion of mathematical truth.

I would hazard a guess that most (all?) working research mathematicians would accept the truth of the Gödel sentence for their preferred axiom system (and deductive calculus), be it ZF/ZFC or TG or something else entirely, so I cannot accept the claim that they see the “standard” notion of truth as being relative to all models of some axiom system.

You might think this is just nit-picking, but if it’s fine (in the sense that this is still “standard”) to add an arbitrarily large set of Pi_1 formulae to ZFC from repetitions of Gödel 1, then I don’t think we can say that ZFC is the standard basis of mathematical truth because this cannot be justified in ZFC; there must be some other (standard) notion of mathematical truth used to justify this.

But you can also assume ZF plus the negation of the axiom of choice, and get a system that is consistent if and only if ZF is consistent. It's not clear (to me, at least) that this other system will let you build the real numbers.

I just want to point out, because the HN crowd seems to generally not be mathematical Platonists, that this entire article is implicitly assuming a Platonist philosophical foundation. This may cause confusion for lay readers who are not mathematical Platonists.

In other words the article assumes that mathematical objects have an objective existence: they either exist or they do not. Hence every single logical axiom has a truth value. You do not get to arbitrarily choose what logical axioms you want. If you do, you can end up choosing the "wrong one." Therefore it is an important question to understand whether the Continuum Hypothesis is true or not, even if it's independent of ZFC (and hence requires ultimately philosophical rather than mathematical arguments).

If you aren't a Platonist and instead view logical axioms as having no inherent truth value, but rather foundations that you can pick and choose from as necessary (where in one case you may choose to use an axiom and in another you may choose its negation), then all that might sound very strange to you. In that case, you should mentally substitute every instance of "true" or "false" in the article with "agrees or disagrees with the meta model used to examine the semantics of a logical theory." In particular, whenever we talk about a formal treatment of the semantics (i.e. model) of a theory, whether that be something like ZFC or a programming language, we must always make those statements relative to a meta-model.

For example if we talk about the formal semantics of a language like C, we must first posit a meta-model which already contains notions of things like "integer" and "natural number" which can be used to give meaning to statements such as "performed an operation n times." If you're not a Platonist then you probably believe that there are multiple possible meta-models you could use.