My goal is mostly to collect my understanding of mathematics into some coherent collection that people can read. Mostly, I just want to expose people to an alternative way of thinking, as I've seen people from this community say things that rely on a narrow view of foundations. My plan for the series is not to be especially philosophical. The first post consists only of things which I think are obvious. As far as I can tell, the main reason people thought it might have been controversial is that they didn't understand what I was getting at in the first place.

The content of this post is actually the meat of my series. I don't think the philosophical discussion has much practical significance beyond settling one's mind. I'm far more interested in doing mathematics than talking about the doing of mathematics.

I will eventually write a post pertaining to truth-maker semantics, and I'll revisit some of the content from my first post then, but I wouldn't consider the content of the first post central, or even all that necessary, for the series.

"1 What is "formalism"? "

"I think it isn't, because positions like F1 and F2 involve such assumptions and aren't made untenable by the incompleteness theorems "

I think it's ironic that you're arguing with me over the meaning of a word, considering the content of my essay. I stated at the begining of my essay what I meant by "formalism". If you don't think that word should be used that way, that's fine, but I'm not interested in arguing about the meaning of a word. By pretending that I'm arguing against any and all forms of what may be called formalism, you are replacing what I actually said with something else. That's not a substantive disagreement with any position I actually endorsed.

"F1: The idea that we should pick some single formal system [...] "

In my original quote I said "has" for a very specific reason. "Should" is a matter of opinion. I don't think it's unreasonable to choose a safe window from which to study the universe of mathematics, but one shouldn't speak as if that window is the universe itself.

"I don't think "many people seem to think [...]"

When someone states something of the form "mathematics turns out to be incomplete" they are ascribing properties of a formal logic to mathematics. When someone states that mathematics is an activity involving, on occasion, a decision "to switch to a different formal foundation", they are ascribing properties of an activity which do not hold for formal logics. This is the central contradiction I'm fixating on. When I say "many people seem to think" I don't mean that many people explicitly endorse, but rather that many people implicitly think of mathematics as a formal system. Saying "mathematics is incomplete" is a form of synecdoche, saying "mathematics" but meaning only a part of it. Failure to realize that this is being done leads people to say silly things.

" F2: The idea that mathematics is the study of formal systems "

"making that choice isn't mathematics "

A field of study can't be incomplete in the way a formal logic can. Saying "mathematics is incomplete" is incompatible with the view that mathematics is a field of study, and yet I've seen many people endorse such a view. If you say that mathematics is the study of formal systems, I'd say that's wrong, but that's not relevant to any of my earlier points.

I think this might actually be the main point of disagreement. Making that choice involves mathematical reasoning and intuition which is certainly part of mathematics, not least because it's part of what mathematicians, in particular, actually do. Excluding such things from being mathematics is arbitrary and artificial. If you're going to make such a designation, then it seems the ultimate goal is to make mathematics mean "the study of formal systems", but I have no interest in talking about such a thing. This is, again, arguing over a definition.

Incidentally, I stated that the position which was untenable after Gödel's Incompleteness Theorems is the assumption, implicit in the statement "mathematics is incomplete", that mathematics is a formal logic. However, that doesn't appear as either your F0, F1, or F2.

I've found this discussion to largely be a waste of time. I won't be responding beyond this point.

No. I'm not advocating for some sort of finitism, nor was Brouwer. In fact, I didn't actually mention computability, that's just something gjm brought up. It's irrelevant to my point. Mathematics is a social activity in the same way politics is a social activity. As in, it's an activity which is social, or at least predicated on some sort of society. Saying that mathematics is incomplete is as meaningful as saying that politics is incomplete in the same way a formal logic might be. It just doesn't make sense.

Note that the intuitions which justify the usage of a particular axiom is not part of an axiom system, but those intuitions would still be part of mathematics. That's largely the intuitionist critique of "old" formalism. It was also used as a critique of logical positivism by Gödel.

"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.

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.