Live data from Hacker News

Doing Mathematics Differently

inference-review.com

31–40 of 73 posts

Re: Doing Mathematics Differently

#31
post #4

This is the Chaitin of Kolmogorov-Solomonoff-Chaitin complexity, if the argument seems familiar. 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 su…

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 measu…

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

Re: Doing Mathematics Differently

#32
post #4

This is the Chaitin of Kolmogorov-Solomonoff-Chaitin complexity, if the argument seems familiar. 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 su…

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 measu…

[deleted]

Re: Doing Mathematics Differently

#33

Earlier quoted context omitted.

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)…

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

Re: Doing Mathematics Differently

#34

Counterpoint (from my blog): 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.

You're confusing the statement

"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

Re: Doing Mathematics Differently

#35
post #30

Earlier quoted context omitted.

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

No, I'm saying the meaning behind statements are different. On some architectures, an int is 16-bit, on others 32-bit. Anyway, this analogy was pushed too far a long time ago.

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.

Re: Doing Mathematics Differently

#36
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!

Re: Doing Mathematics Differently

#37
post #24

Earlier quoted context omitted.

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)…

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.

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.

Re: Doing Mathematics Differently

#38

Earlier quoted context omitted.

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.

Re: Doing Mathematics Differently

#39
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).

Re: Doing Mathematics Differently

#40
Just read this part:

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

Post reply on HN