A la, Penrose, if one believes in mathematical Platonism and such, then there seems to be a final system that could account for all proofs in it, no? — Posty McPostface

‎Gödel was in fact a Platonist. He believed in mathematical truth. His incompleteness theorems show the limits of formal systems in finding that truth.

It seems intuitively obvious if you consider QM in infinite Hilbert Space or anything in infinite Hilbert Space. — Posty McPostface

Not sure what that means. Hilbert space is easily modeled within standard set theory. Infinite dimensional spaces aren't very mysterious. The set of all polynomials has basis {1, x, x^2, x^3, ...} That's an infinite dimensional space that's accessible to the understanding of a high school student. Hilbert space in general is just a function space; that is, a collection of functions with pointwise addition and scalar multiplication. There is no mathematical mystery to Hilbert space.

There is no mathematical mystery to Hilbert space. — fishfry

Yes, I understand that much. But, having objects that can only exist in infinite Hilbert space isn't a mystery to you? Like, say, the very unprovable mathematical truths according to Godel?

Yes, I understand that much. But, having objects that can only exist in infinite Hilbert space isn't a mystery to you? — Posty McPostface

No, why? Perhaps you can explain your point of view to me. I didn't study much physics but I've studied functional analysis. Hilbert spaces aren't very mysterious at all. In fact when I learned that the mysterious bra-ket notation is nothing more than a linear functional acting on a vector, I felt enlightened, as if perhaps QM isn't that far beyond me. If you can explain to me what you're thinking I'm sure I'd learn something. Maybe there's a mystery I'm not appreciating.

No, why? Perhaps you can explain your point of view to me. I didn't study much physics but I've studied functional analysis. Hilbert spaces aren't very mysterious at all. In fact when I learned that the mysterious bra-ket notation is nothing more than a linear functional acting on a vector, I felt enlightened, as if perhaps QM isn't that far beyond me. If you can explain to me what you're thinking I'm sure I'd learn something. Maybe there's a mystery I'm not appreciating. — fishfry

Well, I just edited that post to include Godelian unprovable truths that can exist in such a 'logical space' of sorts. I'm not entirely sure they exist in the domain of infinite Hilbert space. I may be wrong; but, reading some works by Max Tegmark was enlightening to say the least, to present the notion that there are different domains of where mathematical truths can exist but are still unprovable in lower domains of (what I call) state space's or 'logical space'.

So it does not rule out the possibility that one might be able to prove 'everything' in a language with an uncountably infinite alphabet. — andrewk

Maybe not prove everything perfectly?
Say we have a language which says that this statement "currently points to being true".
In the sense a language where you lose accuracy and precision a little, but it points to everything being true or not.

I think such a language can exist.

One of these days I'll read Tegmark. I only know about his mathematical universe hypothesis and can't really respond to the point you are making about domains of mathematical truth.

The way I understand all this is by example. Say we take Zermelo-Fraenkel set theory, or ZF. We know that the Axiom of Choice (AC) is formally independent of ZF. So we can then adjoin Choice to ZF and study the resulting system (called ZFC) or we can adjoin the negation of ZF and study that resulting system.

A Platonist is someone who thinks that "out there" in the Platonic world there are sets, and that in that world of sets, Choice is either true or else it's false. There's a definite answer. Formalists think neither system is true, we're just describing different conceptions of what sets might be.

Viewed that way, I think this is all much less mysterious than it's sometimes made to seem. It's more of a syntactic problem. Sufficiently complex formal systems will always have well-formed statements that can neither be proved nor disproved by the system. There's less than meets the eye. It's not any kind of cosmic mystery. It's just a limitation of formal symbolic systems.

A Platonist is someone who thinks that "out there" in the Platonic world there are sets, and that in that world of sets, Choice is either true or else it's false. There's a definite answer. — fishfry

But the world is every changing. How do they account for that?
What if Choice being true or Choice being false shifted in value. That could very well be true as well.

In that case you would only be able to say that "Choice so far points to True".

But the world is every changing. How do they account for that? — guptanishank

Not being a Platonist, I couldn't say. I can't imagine that there are mathematical sets that actually exist anywhere except as abstract ideas that behave whichever way the axioms say they do. That's just my personal sense of things. I don't think there's any actual truth about sets beyond trivial observations about finite collections.

Yeah, I meant how do the platonists who do think this way, think about it?

Yeah, I meant how do the platonists who do think this way, think about it? — guptanishank

I don't know enough to say. As I mentioned, Gödel was a Platonist and he was pretty smart. There's a lot I don't know about Platonism.

This conversation made me look up this article https://plato.stanford.edu/entries/platonism-mathematics/ . I'll give it a read when I get a chance.

Gödel was a Platonist — fishfry

I did not know that about Godel.

I did not know that about Godel. — guptanishank

These conversations always make me look things up.

This is from his SEP entry.

In his philosophical work Gödel formulated and defended mathematical Platonism, the view that mathematics is a descriptive science, or alternatively the view that the concept of mathematical truth is objective. On the basis of that viewpoint he laid the foundation for the program of conceptual analysis within set theory (see below). He adhered to Hilbert's “original rationalistic conception” in mathematics (as he called it); and he was prophetic in anticipating and emphasizing the importance of large cardinals in set theory before their importance became clear.

Later in the article in section 3.2, "‎Gödel's Realism," they quote this passage from his writings. These are Gödel's own words.

Classes and concepts may, however, also be conceived as real objects, namely classes as “pluralities of things,” or as structures consisting of a plurality of things and concepts as the properties and relations of things existing independently of our definitions and constructions.

It seems to me that the assumption of such objects is quite as legitimate as the assumption of physical bodies and there is quite as much reason to believe in their existence. They are in the same sense necessary to obtain a satisfactory system of mathematics as physical bodies are necessary for a satisfactory theory of our sense perceptions and in both cases it is impossible to interpret the propositions one wants to assert about these entities as propositions about the “data,” i.e., in the latter case the actually occurring sense perceptions.

That's a pretty good description of Platonism. I'm struck by his comment that these objective structures are "necessary to obtain a satisfactory system of mathematics ..." That's a fantastic claim. That the existence of abstract entities is actually necessary to the enterprise of math. You can't dismiss them as a mere formalism.

There's a lot more in that SEP article about all this and more.

To me, ‎Gödel's Platonism is a clue to the meaning of incompleteness. He's not saying that we can't know mathematical truth. He's saying that formal systems are too weak to know mathematical truth. But like they used to say on the X-Files, The truth is out there.

The next question is, if formal systems can't get at the truth, what can? I don't know anything about what philosophers think about that.

Informal systems?

The next question is, if formal systems can't get at the truth, what can? I don't know anything about what philosophers think about that. — fishfry

Wouldn't it have to be something like intuition? Or perhaps, on the other hand, new formalizations that are truer to intuition?

For me the finite and the computational are just nakedly "real" or "true." They are more persuasive than the philosophy that might try to ground them. You'll probably agree that it's the infinite that gives us trouble. Tentatively this trouble seems to involve the gap between a fuzzy, linguistic concept and a mechanizable concept. There are limits to mechanization (halting problem, for instance), and yet mechanization is as Platonic as it gets?

Wouldn't it have to be something like intuition? Or perhaps, on the other hand, new formalizations that are truer to intuition? — t0m

Yes, the work of modern set theory has consisted largely in trying out new axioms that might solve the Continuum hypothesis. I suppose you could say that this is the vision of Gödel. To find better axioms that are natural in the sense of being intuitively right.

As one example, Gödel proposed a model of set theory called L. [Technical definition not important]. In this model, the Axiom of Choice and the Continuum hypothesis are both true. That proves that these statements are at the very least consistent with ZF [Zermelo-Fraenkel set theory].

Now you might think this would be enough. We'd say, we have a model of set theory and AC and CH are both true, so let's all work in L forever and be happy.

However!! It turns out that Gödel himself did not believe that L was the entire universe of sets. We don't work in L, we work in a much more generous model of set theory.

If we call the entire universe of sets V, then the claim that L is the entire universe can be notated as V = L and nobody thinks it's true.

This is perhaps what Gödel is getting at. We can use pure symbolic manipulation to learn more about our axioms. But there is always an "intended" or "real" interpretation out there, and we are not content with a purely symbolic or formal interpretation.

The point is that modern set theory is the search for new axioms that are plausible and seem natural for the world of sets we have in our minds. In our intuition. Yes, it's ultimately driven by intuition. By our intuition about what the Platonic sets must be. Even if we're formalists in the end we must be part Platonist.

For me the finite and the computational are just nakedly "real" or "true." They are more persuasive than the philosophy that might try to ground them. You'll probably agree that it's the infinite that gives us trouble. — t0m

I would say that the infinite is what makes math interesting! Otherwise it's just combinatorics. Balls in bins. Finite sets are boring. Also you need infinity to come up with a satisfactory theory of the real numbers. Which themselves are a philosophical mystery.

It's true that once we allow infinite sets we have paradoxes and strange and counterintuitive results. But that's the fun part! Because when we're doing math, we should think like formalists. That means we just push the symbols and see how much we can prove and if we prove some crazy stuff, well that's fun too. It's a game played with symbols. We do it because it's fun and interesting.

I think that deep down, we're all Platonists. Math is telling us something about the world. But when we DO math, we are formalists. Push the symbols, don't worry too much about what it might mean.

Tentatively this trouble seems to involve the gap between a fuzzy, linguistic concept and a mechanizable concept. There are limits to mechanization (halting problem, for instance), and yet mechanization is as Platonic as it gets? — t0m

Yes. Something that I find interesting is that even though we have all these crazy theories about humongous infinite sets; all of our reasoning is finitistic. Proofs are finite strings. The axioms and theorems are finite strings. The rules of inference are described with finite strings. You could program a computer to check if a proof is valid. This is a huge area of active research these days, they're doing amazing things.

So all we're really doing is playing around with finite strings of symbols. We tell ourselves it's "about infinity," but it really isn't. We are only pretending to be able to deal with infinity. That's one way to look at things.

But recursion need not be finite. Surely that is possible.

But recursion need not be finite. Surely that is possible. — guptanishank

The strings of symbols that represent recursion are finite. The simplest example is the intuition of the natural numbers 1, 2, 3, ...

Those dots are finite. I used 9 symbols above, not counting spaces. 9. I "represented" infinity but ... what does that mean? It's clever of us humans to have worked out a system of symbols to discuss infinity. But the symbology is finite.

Gödel's theorems are about the properties of certain collections of finite strings of symbols. That's why you can do mathematical proofs on a computer. There's no infinity in the computer but we can use a computer to reason symbolically about infinite sets.

But a computational process, could go on forever? The symbols might be finite, but they are referring to something quite plausible.

But a computational process, could go on forever? The symbols might be finite, but they are referring to something quite plausible. — guptanishank

No, computations are required to finish after a finite number of steps. That's part of Turing's definition of computation and it's fundamental to computer science. It's just as proof in math is required to consist of a finite number of steps.

Even then, as a realist I can argue, that if I were to travel along a circle, I could go on forever. So infinity in nature or reality is not so unfathomable.

The point is that modern set theory is the search for new axioms that are plausible and seem natural for the world of sets we have in our minds. In our intuition. Yes, it's ultimately driven by intuition. By our intuition about what the Platonic sets must be. Even if we're formalists in the end we must be part Platonist. — fishfry

I agree with there's a Platonist or intuitionist motive involved. I suppose I experience it in terms of a virtue intersubjective reality. I don't know or even care much how sets or numbers may exist apart from human cognition. It's the aesthetic experience of exact imagination that does it for me. So indeed I'm not just writing symbols down at the end of a proof. The theorem is a revealed truth about a potentially shared world.

I would say that the infinite is what makes math interesting! Otherwise it's just combinatorics. Balls in bins. Finite sets are boring. Also you need infinity to come up with a satisfactory theory of the real numbers. Which themselves are a philosophical mystery. — fishfry

You have a point, but you may be underselling the charms of the finite. I especially like Turing machines and other models of computation. This theorem really moved me: https://en.wikipedia.org/wiki/Cook–Levin_theorem Of course lots of models allow for infinite tape or memory, but in practice computation is utterly finite. I love the cold, perfect mechanization. It's an engineering-scultpure in a material that never rusts or bends ('imaginary titanium').

The reals are beautiful but troubling. "Almost all" of them are incomputable, utterly untouchable. They are elusive ideal entities. We stuff geometrical intuitions into a formal system that seems to work. Perhaps the passionate analysts are Platonist of the continuum and they just use the symbols as part of a "normal" discourse or to discipline their intuition. I've heard an analyst say that for analysts the world is continuous (metaphysically he meant).

Something that I find interesting is that even though we have all these crazy theories about humongous infinite sets; all of our reasoning is finitistic. Proofs are finite strings. The axioms and theorems are finite strings. The rules of inference are described with finite strings. You could program a computer to check if a proof is valid. This is a huge area of active research these days, they're doing amazing things.

So all we're really doing is playing around with finite strings of symbols. We tell ourselves it's "about infinity," but it really isn't. We are only pretending to be able to deal with infinity. That's one way to look at things. — fishfry

Yes, these "finite stings" are what especially interest me. But we do indeed handle them in terms of an intuition of the infinite. It reminds me of Heidegger. There's a framework that "opens" the meaning of the strings for us, but we can't put this dimly visible framework itself in a string. I liked Kleene's book on logic. I know what you mean about proofs being finite strings. Getting Turing machines to search through the countable set of all strings for proofs is a pretty great idea.

I'd say that not all of our reasoning is finitistic. On the other hand, the non-finitistic stuff is therefore problematic. It's a fuzziness that may be the condition of possibility for what is crystal clear.

One thing:
I think Math IS an incomplete language.

How do we know that the statement we are proving outside the axioms is the same statement as inside the axioms?
A statement is comprised of all the axioms above it. So in a way we are proving different statements to be true, even though they may look the same.
Any thoughts?

It seems very counter intuitive to me to use two different axiomatic systems for two different proofs of the same statement.
Could it not be that a statement is True under one axiomatic system and False under another then?

One thing:

How do we know that the statement we are proving outside the axioms is the same statement as inside the axioms? — guptanishank

I don't know what that means. Can you give an example?

A statement is comprised of all the axioms above it. — guptanishank

That doesn't correspond with my understanding of what a statement is. A statement in a formal system is simply a well-formed formula that may be true or false. For example "2 + 2 = 5" is a statement. "2 + 2 =" isn't.

So in a way we are proving different statements to be true, even though they may look the same.
Any thoughts? — guptanishank

Don't know what you mean. Example?

It seems very counter intuitive to me to use two different axiomatic systems for two different proofs of the same statement.
Could it not be that a statement is True under one axiomatic system and False under another then? — guptanishank

Of course. In Euclidean geometry there's exactly 1 line through a given point parallel to another given line. In non-Euclidean geometry there may be zero or many.

One thing:

How do we know that the statement we are proving outside the axioms is the same statement as inside the axioms?
— guptanishank

I don't know what that means. Can you give an example? — fishfry

Well, we discussed that if a statement is unprovable, then we go outside the ambit of the axiomatic system to establish a larger meta system which can prove or disprove that statement, in the above discussion.

A statement is comprised of all the axioms above it.
— guptanishank

That doesn't correspond with my understanding of what a statement is. A statement in a formal system is simply a well-formed formula that may be true or false. For example "2 + 2 = 5" is a statement. "2 + 2 =" isn't. — fishfry

Of course 2+2 = isn't a statement, but 2+2 = 4, comprises of all the axioms needed to define 2, +, = and 4

So in a way we are proving different statements to be true, even though they may look the same.
Any thoughts?
— guptanishank

Don't know what you mean. Example? — fishfry

Let's say under ZFC we could not prove 2+2 = 4, as true. Then to prove Godel's theorems we would still need to establish that statement as true or false eventually. The thing is that truth or falsehood of the statement will vary according to the axiomatic framework we consider.

The thing is that truth or falsehood of the statement will vary according to the axiomatic framework we consider. — guptanishank

The provability of a statement is a function of the axioms.

The truth of a given statement is a function of which model, or interpretation of the axioms we choose.

But now that you've clarified your ideas I still don't understand your question.

Provability and truth are two distinct notions?
How would you know if a statement is true without the proof?

What do you do with a statement unprovable within the axioms? Do you say that it is neither true nor false?

Provability and truth are two distinct notions? — guptanishank

Yes, different. Provability is a syntactic notion. Given some axioms and some inference rules, a given statement either has a proof or its negation has a proof or neither. There is no meaning attached to the symbols.

Truth is a semantic notion. Given an axiomatic system, we choose some interpretation of the symbols, and then we see if the statement is true or false under that interpretation.

Gödel's completeness theorem says that in first-order predicate logic, a statement is true in every model of the system if and only if it has a proof in that system.

How would you know if a statement is true without the proof? — guptanishank

You look at the model in question and see if it's true. If I tell you it's raining, you look outside and see if it's raining.

This distinction between truth and provability is at the heart of ‎Gödel's Platonism. Even though he can't prove the Continuum hypothesis within ZFC, he is certain that "out there" in the actual world of sets, CH has a definite truth value.

But if it is unknown it is alright? And what if it's truth value changed according to the axiom framework under consideration?

Truth is a semantic notion. Given an axiomatic system, we choose some interpretation of the symbols, and then we see if the statement is true or false under that interpretation. — fishfry

How do you "see" this without proving? Mathematical statements can be notoriously hard to "see" if true or false.

How do you "see" this without proving? Mathematical statements can be notoriously hard to "see" if true or false. — guptanishank

Now we're back to formalism versus Platonism. To a formalist, there is no truth, just provability. To a Platonist, there's truth and then there's what you can prove. We can't solve that here. It's enough to note that syntax and semantics are two different things.

A simple example is basic propositional logic. If I have propositions P and Q, then I can define an operator ^ (and) and say that P ^ Q is true just when P is true and Q is true. But that's just syntax. I haven't assigned any meaning to P and Q.

If I say that P is the proposition, "It's raining outside right at this moment," I can look outside and see if it's true or not. I agree with you that when it comes to math, the question of "how do we look outside?" is a tricky matter of philosophy.