Thank you for demonstrating my last point.

I am sorry that we have not been able to resolve our differences.

Fooloso4 I am sorry that we have not been able to resolve our differences. — Dfpolis

Why? This is not a flippant question.

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.

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.

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

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. — GrandMinnow

In the section, formation rules, of the wiki page on first-order logic, you can see how they quickly gloss over a glaring issue in the current practice of mathematics:

The role of the parentheses in the definition is to ensure that any formula can only be obtained in one way by following the inductive definition (in other words, there is a unique parse tree for each formula). This property is known as unique readability of formulas.

The traditional Russell-Whitehead notation is not necessarily unambiguous.

That is probably normal, because the notation was originally introduced for human use and human consumption, in 1910-1913, during the publication of Principia Mathematica (PM).

PM obviously does not contain an EBNF specification for its notation, and is actually not even aware of the glaring problem of ambiguity in its notation. The BNF metalanguage was introduced only in 1959.

Just look at how the gloss over the following issue:

Each author's particular definition must be accompanied by a proof of unique readability.

In all practical terms, it means that the author is supposed to provide the EBNF grammar along with the generated parser tables in order to demonstrate the automaton associated with his grammar is conflict free. That is serious work.

Some people seem to be reinventing the wheel on this matter:

As a corollary, we see that the well-formed formulas of the classical propositional logic, written in Polish notation, are uniquely readable. The unique readability of wffs using parentheses and infix notation requires a different proof.

You can trivially prove that postfix Polish notation can be executed/verified by a stack machine, while infix first requires translation to postfix. Therefore, it does not require a different, but an additional proof, i.e. that all infix expressions can unambiguously be translated to postfix. Again, that can be achieved by demonstrating the the associated automaton is conflict free.

So, to come back to what you were saying about Hilbert, yes, there is a very important "language game" going on, indeed. Entire areas in mathematics do not pay enough attention to it, and still indulge in ambiguous notation that is not machine verifiable.

So, what about finally getting the "symbol games" right?

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.

Proving unique readability is necessary for proving the definition by recursion theorems. — GrandMinnow

Not only!

If your statement correctly parses into two different syntax trees, then it almost always has two different interpretations. Greek and Roman antiquity were already very well aware of this problem:

Ibis redibis nunquam per bella peribis

What exactly does that sentence mean? If your parsing strategy is greedy, it means exactly the opposite of what it means in a lazy parsing strategy:

greedy: you will go, you will never return, in (the) war you will perish
lazy: you will go, you will return, never in war will you perish

It materializes as a shift-reduce conflict in the associated automaton. It is a problem with the grammar itself, and actually not just with this particular sentence. The conflict merely reveals itself in this particular sentence, but it is grammar wide.

This is also the material of which the more advanced network intrusion attacks are made. We can generally not ignore that kind of problems because the overall cost must now globally already run in the trillions of dollars.

Meanwhile, mathematics is usually written in a combination of formal and informal notation along with natural language. — GrandMinnow

Informal commenting versus more strictly regulated language is obviously normal practice. Still, it makes sense to machine-verify the regulated scope, at the very least, for well-formedness. It does not take much effort, and I wonder why anybody should be encouraged to publish formulas that are not even well-formed? E.g. MathJax could do more basic validation. That requires the use of more formal scope delimiters. Of course, we do not need to push it to the point that the editor only accepts expressions that are provable from the theory at hand, or so. That would obviously go too far.

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. — GrandMinnow

That sounds very yagni ("You aren't gonna need it"). In principle, I agree with yagni, but sometimes it is not the right approach, while the really hard problem is to know when it matters and when it doesn't.

Missing Comma Costs Millions

The essence: Delivery drivers who work for Oakhurst Dairy, a Portland, Maine-based company, will be entitled to an estimated $13 million in overtime pay after winning a three-year legal dispute with their employer. An appeals judge ruled that lack of a comma made interpretation of the phrasing of an agreement vague.

The post-mortem of a successful network intrusion almost always reads like that, and leaves the following impression:

What? Really? You must be kidding me!

Especially in cryptography, a lot of mathematical language ends up being implemented pretty much verbatim in software, without even checking the logic again; because that was supposed to have been done in the mathematical work anyway. An ambiguous syntax tree for a mathematical expression could then lead to billions of dollars in losses.

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.

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. — GrandMinnow

You will find comments about unique readability, similar to mine at math.stackexchange.com . Unique readability plays a role in model theory, but it plays an even much bigger role outside of it.

Why is the unique readability of wff's important?

The bottom line is that a statement cannot have unambiguous meaning unless you have a precise unambiguous way of interpreting (reading) it. Even in natural language almost all sentences have unambiguous grammatical structure and more or less clear semantic interpretation, which is not an accident, because otherwise it would fail to be a viable means of communication!
...
You will quickly realize that formal systems for mathematical logic are miniscule in complexity compared to programming languages, but you will also see clearly the reason for the exacting precision in defining a formal system.
...
If we didn't have unique readability, then the language would be useless - we wouldn't be able to say that a sentence is "true" or "false". We could have a sentence that was true under one reading, but not under the other.

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

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'. — GrandMinnow

Yes, and mentioning the issue "unique readability" forcibly drags the entire, seemingly endless field of formal language and therefore related automata theory into the fray.

That means that the "language game" now pushes you right into the middle of the mathematics that govern computer science and in front of the issues that arise in programming languages.

Automata theory is not something that was abstracted away from reality. There are no automata in nature. You have to painstakingly build them, and you have to know how they work, and why they work, before you can even build them. Furthermore, through the problem of unique readability, they strike at the core of mathematics.

If you cross over from the realm of computability into pure mathematics, the term "language game" does not sound controversial at all. Brouwer's accusation that Hilbert was merely "playing language games", gives the impression that Brouwer was seriously missing the point. Hilbert, on the other hand, was asking all the right questions, during the end of the 19th century and the first half of the 20th century, long before the first computer was even built.

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.