Did Brouwer describe Hilbert's formal theories as a 'game'? Maybe he did, but I think it was Weyl's mention of a 'game' that Hilbert was most saliently responding to.

I agree with you that Hilbert asked the great questions (or stated the great challenges). Hilbert was like the "master of ceremonies" of a great direction in mathematics and the philosophy of mathematics. But I am inspired by all the contributions, including the constructivists, intuitionists and predicativists toward the development of this deep and rich enquiry.

Without unique readability we wouldn't even have true in one reading and not in another. Without unique readability we wouldn't even have the recursive definition of 'true in the model'.

parses into two different syntax trees, then it almost always has two different interpretations. — alcontali

Unique readability affords definition by recursion, and definition by recursion affords the method of models, which provides that every statement has exactly one meaning per a given model.

Proving unique readability is necessary for proving the definition by recursion theorems. Each formal system will have its own proofs of unique readability.

Meanwhile, mathematics is usually written in a combination of formal and informal notation along with natural language. This is not ordinarily problematic, since it is usually clear enough how one would formulate such semi-formal writings into pristine formalization (permitting proof of unique readability) if one wanted to do that.

the formalist philosophy admits that on the whole a good mathematical theory is meaningless (has nothing to do with the real world) and useless (no direct application possible). — alcontali

There are different variants of formalism. Only a quite extreme variant holds that mathematics is meaningless, let alone that it is useless.

There are no actual infinitesimals in calculus. — Dfpolis

Right, standard analysis does not admit infinitesimals. However, calculus can be formulated in non-standard analysis or in internal set theory, as those approaches do formalize the notion of infinitesimals.

The problem with Hilbert's "language game" is again connotational — alcontali

Yes, it is not a problem in itself to refer to 'games'. If is fair enough to say that Hilbert took mathematics, in a certain regard, as concerned with symbol games. But it is egregiously incorrect - blatantly against the clear evidence of Hilbert's writings - to claim that Hilbert took mathematics to be merely a matter of symbol games.

I did not claim to address, let alone undermine, your thesis. I set straight certain of the mathematical subjects you mentioned. That is not pedantic. In some cases, your comments were incorrect, and in other cases, your comments were unclear, ambiguous, or confused so that they deserve response even if those responses are not onto themselves corrections. It was my fault not to distinguish between those cases. But in followup at this juncture, it would be unwieldy to always separate those cases, so not each of my responses should be taken necessarily as disputing you.

(1) In your first post you wrote, "the movement characterized by Hilbert's program, which sees mathematical truths as reducible to logical truths", and in a later post you stated that Hilbert viewed mathematics as logic.

But those are incorrect onto themselves, and they are incorrect even as you claim now that you meant only to refer to the position that mathematics only needs to be consistent. Moreover it cannot be discerned from what you originally posted that you did not mean, as you actually wrote, that Hilbert saw "mathematical truths as reducible to logical truths" but instead meant to refer to the very different position that "mathematics need only be logically self-consistent".

Moreover, I should add, while adequacy of consistency is, in a certain key aspect, an important part of Hilbert's view, he does not take mathematics to be merely a matter of consistency.

And your second comment about mathematics as logic (known as 'logicism'*) was in your context of the incompleteness theorem. Perhaps it can be argued that the incompleteness theorem refutes logicism, but that is not really related to Hilbert. The damage the incompleteness theorem does to Hilbert's concept is a different subject: The incompleteness theorem shows that the hope for a finitary consistency proof cannot be realized, but this does not, in itself, entirely refute the adequacy or role of consistency. (* Elsewhere you refer to 'logicalism'. I have never read that term before, so I take it that you mean 'logicism'.)

(2) You wrote:

"One can always add a determinate and previously unprovable truth, or its equivalent (if one knows what it is and not merely that it is) to an axiom system and then "deduce" it. Still, the number of propositions we (all humans) can know is necessarily limited. So any knowable set of axioms is finite. No matter how large that finite set may be, there will be truths that cannot be deduced from it. Also, no computable procedure for generating new axioms will exhaust the possible axioms in a finite time. So, an exhaustive axiom set is unknowable. So there are truths we will never be able to deduce."

There's a lot to sort through:

(2a) For any given system, we always know, by finitary construction, the specific Godel sentence. So I don't see the point of saying "if one knows what it is".

(2b) I don't know your point in putting the word 'deduce' in (scare) quotes. Any axiom, of course, is deducible from itself.

(2c) When writers in mathematical logic or in the theory of computability talk about such things as derivability, of course, this means derivability in principle, not limited to any given finite lifespan of human beings. And, of course, computable procedures are also not limited by finite "time" (such as a recursive enumeration that "runs" infinitely).

So to point out that

in finite time, in anthropomorphic terms or even in terms of physical computations running finitely long, there will always be unknown theorems

does not require invoking the incompleteness theorem.For the point you want to make, mentioning the incompleteness theorem is gratuitous. And the point you want to make is your defense of your original claim:

"There are truths that cannot be deduced from any knowable set of axioms".

I should have addressed the qualification 'knowable' last time. There is a difference between known and knowable.

Perhaps* at any given finite point, there are axiom sets that are not known, but that doesn't entail that they are never to be known (that they are unknowable). (In this context, by 'axioms' we mean recursive, consistent, arithmetically adequate axioms.) (* One might look into whether there is a finite description of the class of systems, as indexed by the ordinals, so that, in a sense, we do know the set (I'd have to brush up on that question).)

Quantifiers help:

There are truths that cannot be deduced from any knowable set of axioms. (False.)

From any particular set of axioms, there are truths that cannot be deduced. (True.)

You wrote:

"I am saying we cannot generate actual axiomatic sets sufficient to deduce all truths in a finite time -- for any finite set of axioms will leave some truths undeducable."

(2d) Axiom sets don't have to be finite to be recursive.

(2e) Again, we don't need the incompleteness theorem to tell us that the entire set of arithmetical truths (or any infinite set of statements) cannot be derived in finite time. Your point can be made even stronger: The incompleteness theorem yields that for any (recursive, consistent, arithmetically adequate) set of axioms, there are truths not provable from those axioms (provable period, not just in finite time). But your point doesn't change that your original statement "there are truths that cannot be deduced from any knowable set of axioms" is incorrect, or at best misleading pending explication of 'knowable' not just 'known', and anyway, that does not concern the incompleteness theorem.

(3) You wrote:

"Godel's work means that we cannot prove the consistency of a set of axioms"

As I mentioned, that is flat out incorrect. Thankfully, you have not disputed my correction.

(4) On Cantor and the continuum, you have conceded. Thank you. But I would like to answer your question:

"do you think that an explanation based on the concept of power sets is more comprehensible to a general philosophic audience"

I don't know what is more comprehensible to any given audience. I only mentioned that the power set proof is, in a sense, more basic and simpler. Proving by reference to the real numbers requires getting into the subject of representation by denumerable sequences (and in what base notation).

(5) I wrote, "If a consequence of C is falsified, then C is falsified" and you replied "Isn't that exactly what I said?" Maybe it was what you meant; I don't know because it was not clear to me what you meant.

(6) You wrote, "If [Hilbert] was right, then the mathematical statements used by the natural science have to be instantiated in nature, and so are true in the sense of correspondence theory. That effectively vitiates formalism."

Instrumentalism does not commit one to requiring that a mathematical statement onto itself must correspond to a corresponding statement about the natural world.

math is not logic. That was Hilbert's view — Dfpolis

That was not Hilbert's view. It seems you are confusing Hilbert with Russell.

Godel's work shows more: it shows that there are truths that cannot be deduced from any knowable set of axioms. — Dfpolis

That is terribly incorrect. Godel's result is that, for any S that is a certain relevant kind of axiom system, there are true statements that cannot be deduced in S. However there are other systems, even of the relevant kind, in which the statement can be deduced. Then, in a followup:

In any lifetime, or finite number of lifetimes, we can only go through a finite number of axiom sets. So, there are true axioms we cannot deduce. — Dfpolis

No, again, that is terribly incorrect. There is no axiom such that there is no system in which the axiom can be deduced. And it is not needed to refer to Godel to point out that we can only look at finitely many systems.

David Hilbert's "program" (concept of math) was destroyed by Kurt Gödel. — Dfpolis

It is reasonable to argue that certain central aspects of Hilbert's program were shown by Godel to not be achievable. But that doesn't destroy Hilbert's concept entirely.

Godel's work means that we cannot prove the consistency of a set of axioms — Dfpolis

No, that is terribly incorrect. Godel's result is that for any S that is a certain kind of axiom system, the consistency of S cannot be deduced in S. But the consistency of S might be deducible by certain other systems.

We come to the notion of Aleph-1 (uncountable) infinity by proving that the numbers we assign to the points of continuous extents cannot be counted. — Dfpolis

'aleph_1' is not synonymous with 'uncountable'. aleph_1 is the least uncountable cardinal. And showing that there are uncountable sets does not rely on proving the uncountability of the continuum, but comes even more simply from proving that the power set of any set has more members than the set, so if there is an infiinite set then there is an uncountable set. And, just to be clear, Cantor didn't prove that the cardinality of the continuum is aleph_1. The proposition that the cardinality of the continuum is alelph_1 is the continuum hypothesis, famously not proven by Cantor.

Perhaps I'm wrong on C being unfalsifiable. Perhaps some consequent of C can be falsified. — Dfpolis

If a consequence of C is falsified, then C is falsified.

It has been claimed that formalists, such as David Hilbert (1862–1943), hold that mathematics is only a language and a series of games. — alcontali

Hilbert didn't say that mathematics is only a language game. He regarded certain aspects of mathematics as a kind of language game. But he explicitly said that certain parts of mathematics are meaningful, and even that the ideal mathematics that he regarded as literally meaningless is still instrumental and crucial for the mathematics of the sciences.