"The Unreasonable Effectiveness of Mathematics in the Natural Sciences" by Eugene Wigner https://www.dartmouth.edu/~matc/MathDrama/reading/Wigner.htm...
> The first point is that mathematical concepts turn up in entirely unexpected connections. Moreover, they often permit an unexpectedly close and accurate description of the phenomena in these connections. Secondly, just because of this circumstance, and because we do not understand the reasons of their usefulness, we cannot know whether a theory formulated in terms of mathematical concepts is uniquely appropriate. We are in a position similar to that of a man who was provided with a bunch of keys and who, having to open several doors in succession, always hit on the right key on the first or second trial. He became skeptical concerning the uniqueness of the coordination between keys and doors.
> Most of what will be said on these questions will not be new; it has probably occurred to most scientists in one form or another. My principal aim is to illuminate it from several sides. The first point is that the enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and that there is no rational explanation for it. Second, it is just this uncanny usefulness of mathematical concepts that raises the question of the uniqueness of our physical theories.
(The article happens to mention the Brouwer-Hilbert controversy but only in a footnote).
Most importantly, the leap that if a medium can be used to create accurate representations, it must contain inherent, unquestioning truth about that represented phenomena, is just hogwash. Michelangelo could sculpt masterful representations of the human form, but the beauty and accuracy of the representation are the products of a skilled master, not the inherent humanness of marble.
It's not just the medium _can_ be used to create accurate representations, by a skilled master. It's that mathematical concepts created with no regard for the natural world but purely on their formal elegance, turn out, years later, to be an elegant way to describe and predict natural phenomena.
I don't think it "proves" anything, it's just... mysterious. The mystery doesn't go away if we insist that math is just an arbitrary human invented formal system. There's no a priori reason it should work to describe and predict the natural world at all, is there?
We could invent other arbitrary formal systems based on completely different axioms and rules that _weren't_ useful to describe and predict the natural world at all, could't we? I think?
I don't know where this characterization of "proof" comes from. It is merely an essay, and not intended as anything other than one. When I read it years ago, I did not get the sense that Wigner was asserting inherent mathematical truth.
>It focuses on cherry-picked phenomena that are easily represented by simple math, but ignores those where math struggles or appears to be inherently incapable.
Does he assert anywhere that any phenomenon will yield easily to mathematics? I don't think so. I think his point is that there's no good reason that even the phenomena that are well explained by mathematics should yield so easily to it. It's not "All of nature is surprisingly mathematical." It's "I see no good reason that a lot of phenomena is mathematical."
I'm too lazy to reread the essay, so I may be remembering it wrong.
Any particular "arbitrary formalized language of symbols" is validated by experiment, either explicitly or implicitly. Humanity/ culture keeps the string games that works and jettison the ones that don't; it is a slow, collaborative process. We have worked out a pretty good "arbitrary formalized language of symbols", but not because we derived these string games or intuited them, but rather because we test them daily.
To be a formalist doesn't imply that a person under-appreciates the mysterious power of mathematics, just that they don't believe in an underlying psuedo-Kantian "truth".
Also, as I understand it, advanced physics is necessarily done formally only, since our intuition is so ridiculous at the atomic scale and all the equations like Schrodingers are only postulated, then verified empirically.
Also, it is snarky and under-informed, but I think of this debate as Hilbert (Hilbert!) and Some Guy.
Interestingly, your latter point is exactly formalism (the "formal" part is referring to the formalized language), i.e. Hilbert's position. Formalism basically asserts that mathematics is a fancy string manipulation game.
> The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.
This is usually called "physics".
Of course, the proofs are first constructed in the context of meaning, but the entire process seems to be a struggle to context-switch between the realms of meaning and symbology, which do not necessarily mirror one another.
But Godel has somehow proved that symbols cannot always provide both a consistent and complete system of meaning.
Gödel seems very much related to this, but I'm still lost.
On the other hand, unprovable statements never make it to the "but can be explained" stage: either the formal system is consistent, and these expressions by definition cannot have an answer, or they can be answered but the formal system is demonstrably inconsistent.
The formal system also needs to be a little more precise than "significantly expressive": it needs to allow for self-referential expressions. In effect, it must be possible to create an expression that can be mapped to the natural language sentence "This statement has no proof in this formal system".
While in natural language puzzles that might be a fun paradox to try to figure out, where the challenge is to determine whether, given the rules of the context, the answer is actually "true" or "false", when it comes to Godel sentences for formal systems there is never a paradox. Either they are undecidable, or the formal system is inconsistent. And we don't get an "out" by saying "but in reality, the answer is ..." because the whole point of formal systems is to be self-contained. There is nothing "outside" of them that we can use to make claims about expressions within that formal system. We only get the axioms of the formal system itself.
The above is a complete misrepresentation of Gödel’s second incompleteness theorem.
The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means.
Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8].
All of these languages are designed to be consistent. Of course, implementation bugs do happen[9].
If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11].
[1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co...
[2] Gödel’s second incompleteness theorem, https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...
[3] Dependent type, https://en.wikipedia.org/wiki/Dependent_type
[4] Total functional programming, https://en.wikipedia.org/wiki/Total_functional_programming
[5] Agda programming language, http://agda.readthedocs.io
[6] Coq proof assistant, http://coq.inria.fr
[7] Idris programming language, http://www.idris-lang.org
[8] Lean theorem prover, http://leanprover.github.io
[9] The rise and fall of @proofmarket, https://twitter.com/i/moments/921153475836305408
[10] Friedman, D.P., Christiansen, D.T. (2018) ‘The Little Typer’, https://mitpress.mit.edu/books/little-typer
[11] Turner, D. (2004) ‘Total Functional Programming’, http://www.jucs.org/jucs_10_7/total_functional_programming
To be even more precise, the system or theory T proves that there is no number n which provides a proof of contradiction for the axioms of T.
So its the axioms of the systems which all formal systems assume and hold to be true. Basically its impossible to prove that axioms are true with the same system.
In short, no formal system can define its own consistency because in order for its axioms to be true, the system must be inconsistent.
If you understand mathematics and logic as merely a formalized language of symbols then you can judge those systems on certain qualities (complexity, clarity, expressiveness, etc.) but not "truth." The creation of a logical expression analogous to a natural phenomenon should instead use the methods of science hypotheses and testing.