See this SEP section.
“if what our brains can do is computable then there is no way we can do mathematics that avoids both inconsistency and incompleteness.”
This sentence illustrates the formalist essentialism that I’m criticizing. If we consider mathematics as a social activity, as Brouwer did, then the notion of completeness doesn’t come up in the first place, and it’s useless to worry about such a thing. This perspective, in part, influenced Gödel to make his discoveries in the first place.
Much of the point of Hilbert’s program (and the wider goal of formalism/logicism) was to prove mathematics in entirety consistent by providing a formal logic which could be considered mathematics itself. Without that, there’s no meaningful sense in which mathematics is actually founded on a formal logic. After all, that would mean that everything outside of your chosen logic wouldn’t be part of mathematics, which is obviously wrong. After incompleteness was established, this situation was shown to be terminal. I think calling the whole project untenable after the publication of Gödel’s incompleteness theorems is a fairly reasonable read of history.
“If what the universe does is computable then there is no way the whole community of mathematicianscan do mathematics that avoids both inconsistency and completeness. ”
I don’t think you understand what I’m getting at. It’s not that completeness shouldn’t be worried about, it’s that it doesn’t make sense if you aren’t already assuming that mathematics is a formal logic. If you worry about formal logic then you worry about completeness. If you don’t assume that mathematics is a formal logic, then worrying about mathematics does not lead one to consider completeness of mathematics in the first place. I’m saying that it does not make sense to talk about mathematics being complete or incomplete in the first place, since mathematics isn’t a formal logic. Yes, it’s impossible for the community of mathematicians to create a formal logic (of sufficient expressivness) which avoids inconsistency and incompleteness, but since mathematics isn’t a formal logic, that doesn’t matter.
“a formalist can still choose to work with different formal systems on different occasions, and regard both as part of mathematics.”
Implicit in that statement is the assumption that mathematics is not, at its core, a formal logic. Yes, it contains formal logics, but it isn’t one. I think you’re using a very weak (and very modern) definition of “foundation of mathematics”, being something capable of doing a significant chunk, but not all, of, mathematics. I think I’ve been clear in what I mean by “foundation of mathematics”, being something that should be capable of facilitating ALL of mathematics. My point is that such a thing doesn’t exist. If you disagree, feel free to argue against what I’m actually saying.
I do not take issue with the idea that one can do a significant chunk (perhaps most of in practice) mathematics using a formal logic. That logic would not then be mathematics, though. That’s all I asserted.
I’m getting the feeling that you didn’t read my post because you’re ascribing beliefs to me that I do not hold. I will quote myself;
“[...] many people seem to think that mathematics is, at some level, a formal logic, or at least that the activity of mathematics has to be founded on some formal logic[...]”
That is the statement you’re taking issue with, yes? Do you think that mathematics is, in fact, a formal logic? If not, then you agree with me. Do you think that mathematics has to be founded on a formal logic? If not, then you agree with me. What are you actually disagreeing with? Are you going to support the assertion that mathematics is a formal logic? Are you going to support the assertion that mathematics has to be founded on a formal logic?
“You might contemplate a strong version of formalism one of whose tenets is “all mathematical questions must be soluble by these means”
I don’t know what version of formalism you think I’m referring to, but my explicit reference to Hilbert should have clued you into the fact that I’m talking about Hilbertian formalism. I’d personally prefer it if you didn’t waste time arguing with a straw-man.