Somewhat related, a physics talk by Susskind about some interesting links between the inside of a black hole and (quantum) computational complexity. The complexity part starts at 20:00. He works with Scott Aaronson on this.
If you read a formal definition of Chaitin-Kolmogorov, you can find that the concept are essentially normalized by recursive function theory. By using the Church-Turing thesis, you can see that any program in any language can be simulated up to a constant length-multiple by an abstract Turing machine (speed isn't considered in these definitions so architecture doesn't matter much). Chaintin-Kolmogorov basically considers the log of the length of programs and then thus takes it's values as being plus or minus a constant for a given measure.
I'm sorry to say this, but your second post also doesn't really address the issue and continues to misunderstand the purpose and definitions of Kolgomorov complexity.
The fact that for any specific string S you can find a language L such that the Kolgomorov complexity K(L, S) is 0, is not that interesting.
1. For any specific L, you can only play this trick (hardcoding a target string) for a finite number of strings. That means for essentially all strings (all but a small finite number) the trick is irrelevant.
2. There is no free lunch: The trick you use to bring down the Kolgomorov complexity K(L, S) down to 0 increases the complexity of L. This can be taken into account, see "conditional Kolgomorov complexity".
The book "An Introduction to Kolmogorov Complexity and Its Applications" by Li and Vitányi explains this, and much more in great detail, and is highly recommended.
You measure it in the same way, using the idea of shortest decription w.r.t. a fixed universal language. You than show that this is absolute up to a constant. Any results produced that way such as the incompressibility of most strings is independent of such constants, hence the the choice of universal language doesn't matter.
"The Kolgomorov complexity of all strings is zero"
with
"For every string there exists a definition of Kolmogorov complexity in which that string has complexity 0"
The first (which you claim as a Theorem) presumes an already fixed definition of complexity, and is therefore false,
while the second is what you proof, and which is not interesting.
Here's how I would fix the definition of Kolmogorov Complexity:
I had long suspicions that Chaitin was a Leibnitzian, but there you go. I like thinking about the Principle of Sufficient Reason, too, but I have long suspected the phenomenon of causality can be more simply explained by positive feedback effects _only_. (http://howonlee.github.io/2016/01/21/Poking-20At-20Causation...)
The thing is that any computable complexity measure allows one to algorithmically produce an infinite which seems to have a complexity which goes to infinite as it get longer but since it is the product of a finite length computer program has finite complexity.
On the other hand, you can prove that for "nearly all" finite sequences of symbols, the algorithmic complexity is within a constant of naive statistical measures.
How is that done? My naive approach would be "always pick the next symbol that most increases complexity" but that doesn't seem guaranteed to diverge and could easily be trapped in local Maxima...
Anyone fascinated by the (non-)intelligibility of the world might like one of Chomsky's many talks on the subject. Such as https://chomsky.info/20060301/
> In fact, if you look at the history of science seriously, in the seventeenth century there was a major challenge to the existing scientific approach. I mean, it was assumed by Galileo and Descartes and classical scientists that the world would be intelligible to us, that all we had to do was think about it and it would be intelligible.
> Newton disproved them. He showed that the world is not intelligible to us. Newton demonstrated that there are no machines, that there’s nothing mechanical in the sense in which it was assumed that the world was mechanical. He didn’t believe it — in fact he felt his work was an absurdity — but he proved it, and he spent the rest of his life trying to disprove it. And other scientists did later on. I mean, it’s often said that Newton got rid of the ghost in the machine, but it’s quite the opposite. Newton exorcised the machine. He left the ghost.
> And by the time that sank in, which was quite some time, it just changed the conception of science. Instead of trying to show that the world is intelligible to us, we recognized that it’s not intelligible to us. But we just say, ‘Well, you know, unfortunately that’s the way it works. I can’t understand it but that’s the way it works.’ And then the aim of science is reduced from trying to show that the world is intelligible to us, which it is not, to trying to show that there are theories of the world which are intelligible to us. That’s what science is: It’s the study of intelligible theories which give an explanation of some aspect of reality.
"Gödel incompleteness is even unpopular among logicians. They are ambivalent. On the one hand, Gödel is the most famous logician ever. But, on the other hand, the incompleteness theorem says that logic is a failure."
I suspect Gödel himself didn't like the incompleteness for similar being very much an idealist who even created (but didn't) publish a modal-logic proof of the existence of God.
The thing is that if one takes a formalist position, that mathematics is a game played by pencil and paper (or computers) then the completeness and incompleteness theorems mean that foundational questions are simply done. oppositely, the position that foundations-people now have to take is that even though you create a universe compatible with any true-but-unprovable position (like the continuum hypothesis or its negation), some of these true-but-unprovable hypotheses are more plausible, aesthetically appealing or something and these hypotheses should be the one considered "true" in some ideal reality (I'm trying to crudely paraphrase Raymund Smullyan here).
What's the point of inserting untranslated French text into an English article?
Is it supposed to just be window-dressing? Is it supposed to promote the (outdated and highly dubious) notion that all educated people speak French? Is it just for the author to show off? Whatever the reason, it's a highly obnoxious practice and it doesn't improve the article.
I could get by with German, but that's beside the point: the essay is written for an English-speaking audience, so it's stupid to insert extended passages of foreign text without providing translation.
Obviously nobody is forcing you to read it. Perhaps it's written for an English speaking audience that doesn't mind skipping over some French here and there.
I found that slightly annoying as well, since elsewhere on the site they translate from French.
For mathematicians of a certain age knowing how to read French, English, and German is pretty common since often mathematics papers were only available in one language. So, my guess is that because of when the author was educated this is just normal for him.
This is a good article, and an important topic, but it mischaracterizes the discipline of mathematics:
> the principle that mathematical truth is black or white and provides absolute certainty.
> Pure mathematicians like to think that they have absolute truth
Formal mathematics has no concept of absolute truth; this is left for philosophy. It's just concerned with axioms and theorems (and their proofs). Whether an axiom reflects reality or not is out of scope, which is the whole point of their invention. As a philosopher you're welcome to debate them, and as a pragmatist you're welcome to choose them (and be compelled to accept their consequent theorems).
> Because it is easy for mathematicians to ignore Gödel’s proof. What lurks in their heart of hearts is a commitment to absolute truth, and a universal formal axiomatic theory for all of mathematics.
In one sense it's disheartening that we cannot prove or disprove every proposition in every axiomatic system. This is an unreasonable expectation as Gödel proved, but it doesn't invalidate the theorems we have proven and disproven. It also doesn't invalidate all of the programs we have written, even though there are non-terminating programs and uncomputable numbers.
You are being philosophic asserting that there would be a reality to reflect, in a rather colorful language, while axioms are real enough to not need to pull a strawman from beyond them.
This reminds me of my Calc professor. When I asked about applying a theory. I asked, "So, when applying this, these values would indicate the expression is true?" He said, we don't concern ourselves with truth in Mathematics.
> The axioms don't have to be true. You can still talk about their implications in absolute terms.
No, you can't. Two mathematicians using different rules of inference (say, those of classical vs. intuitionistic logic) will arrive at different theorems, even if they begin from the same axioms.
> "Assuming a=0 implies a=0" is absolutely true.
Assuming that “a = 0” and implication are both expressible in our formal system, it would indeed be very weird (though not a priori impossible) if “a = 0” didn't imply “a = 0”. But I have no problem imagining a formal system where “a = 0” isn't expressible (e.g., because equality is inexpressible), or implication isn't expressible (e.g., geometric logic), or implication has strange properties to someone only familiar with the classical and/or intuitionistic interpretation of “implication” (e.g., linear logic).
You can't have the same axioms with different rules of inference. The rules of inference are axioms.
By the axioms being the same, you mean the ink-shapes making up the symbols on a piece of paper being the same.
Not the actual meaning behind them.
Edit: Since you added more content to this reply later on, let me respond. In this case I was talking about specifically a formal system where a=0 makes sense and is expressible, but to keep it short and concise I didn't choose to write out all the details. So the rebuttal is moot.
Axioms and rules of inference are fundamentally different:
(0) An axiom is an internal statement to a mathematical theory that is assumed to be true. That is, inside of a mathematical theory, you don't need to prove that its axioms hold. However, if you want to construct a model of a mathematical theory, you need to prove externally that the axioms hold. In return, you get the theory's theorems (suitably interpreted) for free.
(1) A rule of inference exists in an external metatheory, where the original mathematical theory we were studying is treated as a syntactic object (also known as object language), in very much the same way a compiler treats the program being compiled as a (possibly annotated) syntax tree. A rule of inference defines a class of valid syntactic transformations, but doesn't concern itself with the impact of these transformations have on the meaning of the phases in the object language.
It is perfectly sensible to consider the effect of changing the rules of inference, on an axiomatic system.
If you have different rules, you have a different object and the meaning of the axiom is different. Even if it is written using the same symbols.
To continue the compiler analogy..
Just because the ASCII sequence "int c=0;" means different things in C and Java, doesn't imply "int c=0;" is meaningless when specifically talking about only C.
The problem with your analogy is that C and Java have completely different abstract syntaxes. A better analogy would be taking the syntax of an existing programming language, and completely changing its meaning. For instance, consider the effect of making Racket use lazy evaluation (Lazy Racket), or making Haskell use strict evaluation (the upcoming -XStrict pragma). Strict and lazy languages validate different sets of equational laws (and hence compiler optimizations!), neither of which is a subset of the other, so this is perhaps a more interesting example than switching between intuitionistic and classical logic.
What you're saying is more or less equivalent to “two C implementations targeting different [architectures / operating systems / whatever] are actually implementations of two different programming languages”.
Ah, lovely! You just arrived exactly where I was trying to get.
> I'm saying the meaning behind statements are different.
Yes, exactly! And, just like a single C program can have two different meanings under two different implementations, the same axiomatic system can have two different meanings when deducing its consequences (proving theorems) using different rules of inference.
Not necessarily. It's very possible for one system to embed inside the other. In this case you can often talk about exactly the same axiom/theorem/whatever within different inferential systems.
An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic. That said, we can use flattening to embed classical logic inside of intuitionistic logic and then recover a whole family of propositions of which AC is one and also see why it has a difficult time holding in IPL.
This seems to be a technical objection that dodges the meat of the parent's comment. In what sense is it true that a given theorem follows from a given set of axioms and a given choice of inference rules?
A “theorem” is by definition a statement in a mathematical theory that has a proof. In what sense is this true? Well, that depends on what “true” means in your model... :-p
I agree with parent comment. At the heart of your disagreement is that you seem to use definition from logic of what axioms are, while your opponents use "definitions" from metamathematics.
Umm. I've been of the understanding that we never change the inference rules, Can you point to some branch of mathematics that involves a change of inference rules?
At my level of understanding, it seems a reasonable characterization of intuitionistic logic to say that it operates with a more restricted set of inference rules. It was the parent who made the stronger claim about differences here, and they speak a bit more to the topic in nearby comments.
Umm. I've been of the understanding that we never change the inference rules, Can you point to some branch of mathematics that involves a change of inference rules?
Axioms and rules of inference are fundamentally different:
Things are not that simple, because you can often convert axioms to rules of inference or vice versa, without changing the set of derivable consequences.
As an example, consider pure first-order logic (FOL). As one extreme, you can present FOL with just one rule of inference (Modus Ponens), see for example [1]. The other extreme is Gentzen's sequent calculus [2] which has only one axiom (A |- A), everything else being a rule of inference. Most presentations of FOL are between these extremes.
[1] A mathematical introduction to logic, by H. Enderton
[2] Untersuchungen über das logische Schliessen I, by G. Gentzen
There is a difference, but it's not clear quite what it is.
For example, it becomes progressively harder to get nice
(with cut elimination and finite rule schemata) sequent calculi
for richer axiomatic systems. For example I have not come across a
nice (in the above sense) sequent style formalisation of ZFC set
theory. Have you?
> Things are not that simple, because you can often convert axioms to rules of inference or vice versa, without changing the set of derivable consequences.
Yes, but the derivations themselves will change.
> As an example, consider pure first-order logic (FOL). As one extreme, you can present FOL with just one rule of inference (Modus Ponens), see for example [1]. The other extreme is Gentzen's sequent calculus [2] which has only one axiom (A |- A), everything else being a rule of inference. Most presentations of FOL are between these extremes.
Yep. I'm aware of the phenomenon that a single mathematical object of type T (say, infinity-categories) may admit multiple presentations by objects of type T' (say, model categories). But, just because two objects of type T' present the same object of type T (e.g., two Quillen-equivalent categories), it doesn't mean that they are equal in all respects (e.g., the category of simplicial sets is much nicer than the category of topological spaces).
"Axioms are better thought of as universally accepted truths"
Not really universally accepted. You just have to specify which set of axioms you are using. Different problems may call for different axioms. Like if you want to prove theorems about the security of some computer system, you'll define a set of axioms that allow proving interesting results for that purpose. If you want to prove theorems about sets, you'll want to specify what set axioms you are using. You may even try to specify interesting minimal sets of axioms that make your theorem true. There is no reason to use the same axioms for everything, or to assume they are True in some teological sense.
Acioms are only viewed as true because they are defined as such.
It's obvious when applying math to real world. If you're talking about objects on Earth surface, for example, at first Euclid's geometry will get you good results, because objects you're working with can be assumed to fulfill it's axioms. However, when your scale gets bigger, you'll have apply a more complicated geometry apparatus.
Easiest analogy about axioms is interface in software engineering: you don't care what the object really is, but as long as it shows certain properties, you can prove theorems about it. Which will be true for any objects with these properties, and as true as exactly these properties are fulfilled by the real life object.
This is not correct. There is no such thing as absolute truth. Something can only be true within a set of previously agreed constraints and rules. For example, I can simply imagine a scenario where a=0 implies a=0 is considered to be false, because I define it to be so.
Although I know you meant that jokingly, presumably the op's statement is only true within the parameters of a world where "there is no such thing as absolute truth", therefore, the statement isn't absolutely true, it's just true within the confines of his own (subjective) world view. The actual world, may, in fact, have absolute truth.
As it was mentioned earlier we can’t think about “absolute truth" in terms of math because math is appliance science. It is like a language. The root science is physics and only it owns “absolute truth", the real axioms and implication rules.
> Formal mathematics has no concept of absolute truth ...
Well, it does. If you drag the propositional calculus into the fray, "true" is arbitrarily but probably most elegantly defined as following:
true(x) = x or not x
False is defined like this:
false(x) = x and not x
These definitions are pretty much arbitrary. The lambda calculus does this:
true(a,b)=a
false(a,b)=b
It also works absolutely fine.
> It's just concerned with axioms and theorems (and their proofs)
In the general case, theorems are indeed "provable" or "unprovable" (not "true" or "false").
However, if a theorem has exclusively been derived from propositional calculus, it can also be "true".
Gödel's incompleteness is exactly about statements that are "true but unprovable". In terms of propositional calculus, the theorem is "true" but since you can show that the theorem can never be derived from the axioms, it is also "unprovable".
Well, it does not. Mathematics is a symbolic system invented by humans, but that system tells you nothing about the state of the world.
Used correctly, it can be used to describe the world, but it can also be used to describe phenomena that have not been physically observed. E.g., currently accepted theories allow for existence of wormholes, but we do not know whether the actual physical laws of the universe ("absolute truth") do.
So, no, there is no "absolute truth" in mathematics. There are only valid derivations, but taking them as the "absolute truth" is like mistaking the pointing finger for the moon.
Yes there are absolute truths. 2+2 will not equal 5 in any universe. The laws of physics could be radically different, but I have 2 apples, and you give me two more, I will not suddenly have 5 apples.
Math can tell you an awful lot about the state of the world. That's why it's useful.
Have you followed Gödel's proof in detail? I know Fields medalists who like to speculate about Gödel, but haven't read Russell and Whiteheads Principia Mathematica (PM). Gödel's system is PM, but PM is quite an impossible read. Most of this discussed has been discussed over 30 years between 1900-1930. By the way Turing also builds on PM in his on computable numbers paper. PM is like a compiler before there were compilers. Today it would look more like metamath.org or https://github.com/vladimirias/Foundations
> Formal mathematics has no concept of absolute truth; this is left for philosophy.
No, it is called logic which is the intersection of both. And most mathematicians haven't done any logic whatsoever. They avoid it, because it means you actually have to think about things. You have to think about why greek symbols have special meanings. And as computer scientists/hackers know, computer code is an alternative medium.
I remember when I asked a math professor about the "=" sign and how things can be equal at all, since if they are either the same (A=A is trivial), it is trivial, or if they are different they are not the same (A=B is false). About 10 years later I discovered this is why physics has the notion of symmetries, which is a statement of the form A - B = 0. Two things are equal iff their transformation leads to the origin. But I should have known this all along, because in computer programs "=" can stand for various kinds of operations. It is just that the language of mathematics in general is so inaccurate that one gets lost on the way.
I'm a bit dubious about your sweeping generalisation that "most mathematicians haven't don't any logic".
I also agree with GP that logic also does not deal with absolute truth. Proofs in formal logic may be applied to models, but they only provide truths modulo the assumptions made in those models.
As for your remark on equivalence. Your original description is one of syntactic identity, a sort of free equivalence. But any relation that is reflexive, transitive and symmetric can be considered an equivalence (indeed, there are infinitely many equivalence relations over the integers). Also note that this is not the same as how "=" is used in computer programs where for the most part it is asymmetric (a=b is rarely semantically equivalent to b=a).
This is the crankiest comment I've seen on HN in a while. You "know Fields medalists"? Right.
You think that Pricipia Mathematica is the source of all truth in mathematics? Wrong. Most mathematicians working on foundational questions start out by learning Zermelo-Fraenkel set theory, which is well-understood, and avoids several difficulties that Russel had. While few people have read PM, it remains important because it goes through the hard task showing that high-level mathematics (calculus, &c.) can have rigorous, first-principle proofs.
"PM is like a compiler before there were compilers." What?
"I asked a math professor about the '=' sign and how things can be equal at all (...)" OMGWTFNO. I've seen comments like this before. Typically, it creates debate around a non-issue by sowing confusion and never nailing down precisely what we are talking about (hence the need for formal methods—it helps us call bullshit on comments like this).
"Two things are equal iff their transformation leads to the origin. [A - B = 0]". Wrong. There are equality relations that do not require the existence of a zero or the concept of addition or subtraction.
Omega is an amazing number. We know it has a digit in its binary expansion that is 0 or 1, yet it is impossible to formulate why. It is impossible to come up with a train of thought that explains it. There is no explanation that can be written down on a piece of paper.
So we are left with the weird conclusion:
1. It has the value it has for no reason.
2. It has the value it has for a reason that is impossible to formulate.
Nah, Omega is just defined as a number which contains countably infinite bits of algorithmic information. Since algorithmic information is equivalent to thermodynamic information (and likewise relates to quantum information if you head in that direction...), the whole "you can't calculate Omega" thing is really just a way of saying, "You can't have an infinite-precision physical measurement encoded into a finite physical system."
Chaitin makes far too much metaphysics of his work.
I don't really understand the insight with Chaitin's number. It's unknowable, but so are a lot of things. The halting problem already says that there are programs which we can't know if they will halt or not. And before that, Godel showed there are simple logical sentences which are true and unprovable.
The author keeps talking about going through all possible proofs built from the axioms, as if that's a thing that obviously could be done. However, if your system is complicated enough to allow arbitrarily large combinations of axioms in your proofs, then I don't understand how you can expect enumeration of all proofs to be a finite process. Any statement that says "enumerate all possible proofs" followed by "and then do X" is meaningless, because you will never reach the "do X" step!
An example of how this is useful: If it were provable that a program does not halt, an enumeration of all proofs would find the proof that the program does not halt. (If a program does halt, it is necessarily provable that it does so, for obvious reasons.)
Thus either,
- We can solve the halting problem, or
- There exists something that is true but not provable.
Thus the uncomputability of the halting problem implied Goedel's incompleteness theorem. Proving the other direction can be done by similar techniques.
In a sense mathematics already is experimental, because we already have, although not formally defined, class of things where we simply don't know their status of being true or false - hypotheses.
I am currently thinking how to make an automated mathematician based on lambda calculus, which would have its own notion of "beauty", and based on this it would try to select interesting definitions. It seems such a system needs to have a notion of experiment.
Since computations are proofs, theorems are basically computations that we know the result of already, i.e. which have already been done (all with respect to some axiomatic system, given by types).
Such system also needs notion of "economy", which lets it allocate computational resources effectively. So it needs to be able to evaluate things only partially, to avoid infinite loops etc.
This naturally leads to experimental approach, where you don't only know true or false, but there is a wide spectrum of what you know about certain statement (lambda expression).
> So we have a measure of the complexity of a formal mathematical theory A, and in theory A you cannot prove that any program is elegant that is larger in size than A’s complexity. That is what the paradoxical program P proves.
And thought: hmm. Sounds like, what was it called again? Checks Wikipedia, article on Kolmogorov Complexity. Oh yeah, Chaitin's Incompleteness Theorem. I wonder if it's mentioned in the article. CTRL-F - "Chaitin"
72 comments
[ 3.0 ms ] story [ 44.3 ms ] threadhttps://www.youtube.com/watch?v=IuY4RMehdP8
http://forwardscattering.org/post/7
http://forwardscattering.org/post/14
In summary i don't think AIT offers an absolute measure of complexity, due to having to choose the abstract machine.
Not to say the ideas aren't interesting, and that this isn't a nice article, from one of the main figures in the field.
If you read a formal definition of Chaitin-Kolmogorov, you can find that the concept are essentially normalized by recursive function theory. By using the Church-Turing thesis, you can see that any program in any language can be simulated up to a constant length-multiple by an abstract Turing machine (speed isn't considered in these definitions so architecture doesn't matter much). Chaintin-Kolmogorov basically considers the log of the length of programs and then thus takes it's values as being plus or minus a constant for a given measure.
The fact that for any specific string S you can find a language L such that the Kolgomorov complexity K(L, S) is 0, is not that interesting.
1. For any specific L, you can only play this trick (hardcoding a target string) for a finite number of strings. That means for essentially all strings (all but a small finite number) the trick is irrelevant.
2. There is no free lunch: The trick you use to bring down the Kolgomorov complexity K(L, S) down to 0 increases the complexity of L. This can be taken into account, see "conditional Kolgomorov complexity".
The book "An Introduction to Kolmogorov Complexity and Its Applications" by Li and Vitányi explains this, and much more in great detail, and is highly recommended.
"The Kolgomorov complexity of all strings is zero"
with
"For every string there exists a definition of Kolmogorov complexity in which that string has complexity 0"
The first (which you claim as a Theorem) presumes an already fixed definition of complexity, and is therefore false, while the second is what you proof, and which is not interesting.
Here's how I would fix the definition of Kolmogorov Complexity:
https://en.wikipedia.org/wiki/Binary_lambda_calculus
I like Grassberger-Crutchfield-Young (http://www.scholarpedia.org/article/Complexity, look for Statistical complexity) complexity, because it can actually be measured.
I had long suspicions that Chaitin was a Leibnitzian, but there you go. I like thinking about the Principle of Sufficient Reason, too, but I have long suspected the phenomenon of causality can be more simply explained by positive feedback effects _only_. (http://howonlee.github.io/2016/01/21/Poking-20At-20Causation...)
On the other hand, you can prove that for "nearly all" finite sequences of symbols, the algorithmic complexity is within a constant of naive statistical measures.
> In fact, if you look at the history of science seriously, in the seventeenth century there was a major challenge to the existing scientific approach. I mean, it was assumed by Galileo and Descartes and classical scientists that the world would be intelligible to us, that all we had to do was think about it and it would be intelligible.
> Newton disproved them. He showed that the world is not intelligible to us. Newton demonstrated that there are no machines, that there’s nothing mechanical in the sense in which it was assumed that the world was mechanical. He didn’t believe it — in fact he felt his work was an absurdity — but he proved it, and he spent the rest of his life trying to disprove it. And other scientists did later on. I mean, it’s often said that Newton got rid of the ghost in the machine, but it’s quite the opposite. Newton exorcised the machine. He left the ghost.
> And by the time that sank in, which was quite some time, it just changed the conception of science. Instead of trying to show that the world is intelligible to us, we recognized that it’s not intelligible to us. But we just say, ‘Well, you know, unfortunately that’s the way it works. I can’t understand it but that’s the way it works.’ And then the aim of science is reduced from trying to show that the world is intelligible to us, which it is not, to trying to show that there are theories of the world which are intelligible to us. That’s what science is: It’s the study of intelligible theories which give an explanation of some aspect of reality.
I suspect Gödel himself didn't like the incompleteness for similar being very much an idealist who even created (but didn't) publish a modal-logic proof of the existence of God.
The thing is that if one takes a formalist position, that mathematics is a game played by pencil and paper (or computers) then the completeness and incompleteness theorems mean that foundational questions are simply done. oppositely, the position that foundations-people now have to take is that even though you create a universe compatible with any true-but-unprovable position (like the continuum hypothesis or its negation), some of these true-but-unprovable hypotheses are more plausible, aesthetically appealing or something and these hypotheses should be the one considered "true" in some ideal reality (I'm trying to crudely paraphrase Raymund Smullyan here).
Is it supposed to just be window-dressing? Is it supposed to promote the (outdated and highly dubious) notion that all educated people speak French? Is it just for the author to show off? Whatever the reason, it's a highly obnoxious practice and it doesn't improve the article.
Would you have preferred Latin or German ? Leibniz used them too.
I could get by with German, but that's beside the point: the essay is written for an English-speaking audience, so it's stupid to insert extended passages of foreign text without providing translation.
You shouldn't jump to assuming malice when someone's aesthetic tastes differ from your own.
By the way, the quote means (my own translation):
> God chose the one which was the most perfect; that is, the one which whose hypotheses were the simplest, and whose phenomena were the richest.
> But when a rule is very intricate, that which follows it seems irregular.
For mathematicians of a certain age knowing how to read French, English, and German is pretty common since often mathematics papers were only available in one language. So, my guess is that because of when the author was educated this is just normal for him.
> the principle that mathematical truth is black or white and provides absolute certainty.
> Pure mathematicians like to think that they have absolute truth
Formal mathematics has no concept of absolute truth; this is left for philosophy. It's just concerned with axioms and theorems (and their proofs). Whether an axiom reflects reality or not is out of scope, which is the whole point of their invention. As a philosopher you're welcome to debate them, and as a pragmatist you're welcome to choose them (and be compelled to accept their consequent theorems).
> Because it is easy for mathematicians to ignore Gödel’s proof. What lurks in their heart of hearts is a commitment to absolute truth, and a universal formal axiomatic theory for all of mathematics.
In one sense it's disheartening that we cannot prove or disprove every proposition in every axiomatic system. This is an unreasonable expectation as Gödel proved, but it doesn't invalidate the theorems we have proven and disproven. It also doesn't invalidate all of the programs we have written, even though there are non-terminating programs and uncomputable numbers.
That's like an absolute truth in formal mathematics then, I suppose.
This is false. The axioms don't have to be true. You can still talk about their implications in absolute terms.
"Assuming a=0 implies a=0" is absolutely true. Regardless of whether a actually is 0.
No, you can't. Two mathematicians using different rules of inference (say, those of classical vs. intuitionistic logic) will arrive at different theorems, even if they begin from the same axioms.
> "Assuming a=0 implies a=0" is absolutely true.
Assuming that “a = 0” and implication are both expressible in our formal system, it would indeed be very weird (though not a priori impossible) if “a = 0” didn't imply “a = 0”. But I have no problem imagining a formal system where “a = 0” isn't expressible (e.g., because equality is inexpressible), or implication isn't expressible (e.g., geometric logic), or implication has strange properties to someone only familiar with the classical and/or intuitionistic interpretation of “implication” (e.g., linear logic).
By the axioms being the same, you mean the ink-shapes making up the symbols on a piece of paper being the same.
Not the actual meaning behind them.
Edit: Since you added more content to this reply later on, let me respond. In this case I was talking about specifically a formal system where a=0 makes sense and is expressible, but to keep it short and concise I didn't choose to write out all the details. So the rebuttal is moot.
(0) An axiom is an internal statement to a mathematical theory that is assumed to be true. That is, inside of a mathematical theory, you don't need to prove that its axioms hold. However, if you want to construct a model of a mathematical theory, you need to prove externally that the axioms hold. In return, you get the theory's theorems (suitably interpreted) for free.
(1) A rule of inference exists in an external metatheory, where the original mathematical theory we were studying is treated as a syntactic object (also known as object language), in very much the same way a compiler treats the program being compiled as a (possibly annotated) syntax tree. A rule of inference defines a class of valid syntactic transformations, but doesn't concern itself with the impact of these transformations have on the meaning of the phases in the object language.
It is perfectly sensible to consider the effect of changing the rules of inference, on an axiomatic system.
To continue the compiler analogy..
Just because the ASCII sequence "int c=0;" means different things in C and Java, doesn't imply "int c=0;" is meaningless when specifically talking about only C.
Anyway, this analogy was pushed too far a long time ago.
> I'm saying the meaning behind statements are different.
Yes, exactly! And, just like a single C program can have two different meanings under two different implementations, the same axiomatic system can have two different meanings when deducing its consequences (proving theorems) using different rules of inference.
An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic. That said, we can use flattening to embed classical logic inside of intuitionistic logic and then recover a whole family of propositions of which AC is one and also see why it has a difficult time holding in IPL.
Naïvely encoded in Martin-Löf type theory, that is.
As an example, consider pure first-order logic (FOL). As one extreme, you can present FOL with just one rule of inference (Modus Ponens), see for example [1]. The other extreme is Gentzen's sequent calculus [2] which has only one axiom (A |- A), everything else being a rule of inference. Most presentations of FOL are between these extremes.
[1] A mathematical introduction to logic, by H. Enderton
[2] Untersuchungen über das logische Schliessen I, by G. Gentzen
There is a difference, but it's not clear quite what it is.
For example, it becomes progressively harder to get nice (with cut elimination and finite rule schemata) sequent calculi for richer axiomatic systems. For example I have not come across a nice (in the above sense) sequent style formalisation of ZFC set theory. Have you?
Yes, but the derivations themselves will change.
> As an example, consider pure first-order logic (FOL). As one extreme, you can present FOL with just one rule of inference (Modus Ponens), see for example [1]. The other extreme is Gentzen's sequent calculus [2] which has only one axiom (A |- A), everything else being a rule of inference. Most presentations of FOL are between these extremes.
Yep. I'm aware of the phenomenon that a single mathematical object of type T (say, infinity-categories) may admit multiple presentations by objects of type T' (say, model categories). But, just because two objects of type T' present the same object of type T (e.g., two Quillen-equivalent categories), it doesn't mean that they are equal in all respects (e.g., the category of simplicial sets is much nicer than the category of topological spaces).
No, not at all. Axioms are better thought of as universally accepted truths which everything else depends on. https://en.wikipedia.org/wiki/Logical_atomism
It's obvious when applying math to real world. If you're talking about objects on Earth surface, for example, at first Euclid's geometry will get you good results, because objects you're working with can be assumed to fulfill it's axioms. However, when your scale gets bigger, you'll have apply a more complicated geometry apparatus.
Easiest analogy about axioms is interface in software engineering: you don't care what the object really is, but as long as it shows certain properties, you can prove theorems about it. Which will be true for any objects with these properties, and as true as exactly these properties are fulfilled by the real life object.
This is not correct. There is no such thing as absolute truth. Something can only be true within a set of previously agreed constraints and rules. For example, I can simply imagine a scenario where a=0 implies a=0 is considered to be false, because I define it to be so.
Isn't that an absolute truth?
Well, it does. If you drag the propositional calculus into the fray, "true" is arbitrarily but probably most elegantly defined as following:
true(x) = x or not x
False is defined like this:
false(x) = x and not x
These definitions are pretty much arbitrary. The lambda calculus does this:
true(a,b)=a
false(a,b)=b
It also works absolutely fine.
> It's just concerned with axioms and theorems (and their proofs)
In the general case, theorems are indeed "provable" or "unprovable" (not "true" or "false").
However, if a theorem has exclusively been derived from propositional calculus, it can also be "true".
Gödel's incompleteness is exactly about statements that are "true but unprovable". In terms of propositional calculus, the theorem is "true" but since you can show that the theorem can never be derived from the axioms, it is also "unprovable".
Used correctly, it can be used to describe the world, but it can also be used to describe phenomena that have not been physically observed. E.g., currently accepted theories allow for existence of wormholes, but we do not know whether the actual physical laws of the universe ("absolute truth") do.
So, no, there is no "absolute truth" in mathematics. There are only valid derivations, but taking them as the "absolute truth" is like mistaking the pointing finger for the moon.
Math can tell you an awful lot about the state of the world. That's why it's useful.
> Formal mathematics has no concept of absolute truth; this is left for philosophy.
No, it is called logic which is the intersection of both. And most mathematicians haven't done any logic whatsoever. They avoid it, because it means you actually have to think about things. You have to think about why greek symbols have special meanings. And as computer scientists/hackers know, computer code is an alternative medium.
I remember when I asked a math professor about the "=" sign and how things can be equal at all, since if they are either the same (A=A is trivial), it is trivial, or if they are different they are not the same (A=B is false). About 10 years later I discovered this is why physics has the notion of symmetries, which is a statement of the form A - B = 0. Two things are equal iff their transformation leads to the origin. But I should have known this all along, because in computer programs "=" can stand for various kinds of operations. It is just that the language of mathematics in general is so inaccurate that one gets lost on the way.
I also agree with GP that logic also does not deal with absolute truth. Proofs in formal logic may be applied to models, but they only provide truths modulo the assumptions made in those models.
As for your remark on equivalence. Your original description is one of syntactic identity, a sort of free equivalence. But any relation that is reflexive, transitive and symmetric can be considered an equivalence (indeed, there are infinitely many equivalence relations over the integers). Also note that this is not the same as how "=" is used in computer programs where for the most part it is asymmetric (a=b is rarely semantically equivalent to b=a).
You think that Pricipia Mathematica is the source of all truth in mathematics? Wrong. Most mathematicians working on foundational questions start out by learning Zermelo-Fraenkel set theory, which is well-understood, and avoids several difficulties that Russel had. While few people have read PM, it remains important because it goes through the hard task showing that high-level mathematics (calculus, &c.) can have rigorous, first-principle proofs.
"PM is like a compiler before there were compilers." What?
"I asked a math professor about the '=' sign and how things can be equal at all (...)" OMGWTFNO. I've seen comments like this before. Typically, it creates debate around a non-issue by sowing confusion and never nailing down precisely what we are talking about (hence the need for formal methods—it helps us call bullshit on comments like this).
"Two things are equal iff their transformation leads to the origin. [A - B = 0]". Wrong. There are equality relations that do not require the existence of a zero or the concept of addition or subtraction.
So we are left with the weird conclusion:
1. It has the value it has for no reason.
2. It has the value it has for a reason that is impossible to formulate.
Chaitin makes far too much metaphysics of his work.
An example of how this is useful: If it were provable that a program does not halt, an enumeration of all proofs would find the proof that the program does not halt. (If a program does halt, it is necessarily provable that it does so, for obvious reasons.)
Thus either,
- We can solve the halting problem, or - There exists something that is true but not provable.
Thus the uncomputability of the halting problem implied Goedel's incompleteness theorem. Proving the other direction can be done by similar techniques.
I am currently thinking how to make an automated mathematician based on lambda calculus, which would have its own notion of "beauty", and based on this it would try to select interesting definitions. It seems such a system needs to have a notion of experiment.
Since computations are proofs, theorems are basically computations that we know the result of already, i.e. which have already been done (all with respect to some axiomatic system, given by types).
Such system also needs notion of "economy", which lets it allocate computational resources effectively. So it needs to be able to evaluate things only partially, to avoid infinite loops etc.
This naturally leads to experimental approach, where you don't only know true or false, but there is a wide spectrum of what you know about certain statement (lambda expression).
> So we have a measure of the complexity of a formal mathematical theory A, and in theory A you cannot prove that any program is elegant that is larger in size than A’s complexity. That is what the paradoxical program P proves.
And thought: hmm. Sounds like, what was it called again? Checks Wikipedia, article on Kolmogorov Complexity. Oh yeah, Chaitin's Incompleteness Theorem. I wonder if it's mentioned in the article. CTRL-F - "Chaitin"
...the writer of this article is Gregory Chaitin.