Tarski's high school algebra problem | Hacker News Reader

Tarski's high school algebra problem

en.wikipedia.org

76 pointsColinWright18 comments

I remember being told about this when I was introduced to type isomorphisms. Sum types correspond to addition, product types correspond to multiplication and function types correspond to exponentiation.

In haskell types:

    * Either a b corresponds to a+b

    * (a,b) corresponds to a*b

    * a -> b corresponds to b^a

Update:

I forgot 0 and 1. I don't know what 0 would be in haskell. Think of 0 as a type that does not have a constructor. 1 is () (the unit type).

You can actually write an "empty" (ignoring ⊥) type:

    data Void

Apart from maintaining symmetry and keeping the type system elegant, this is also very useful when you want to use types as "tags", ensuring they cannot be instantiated.

A little disappointing that it all boiled down to the lack of a way to handle a negative coefficient, but fun problem nonetheless.

Perhaps so, but it interesting to observe that a lot of very, very smart people stared at those axioms for a long time without noticing that, and that the corresponding proof of that fact was non-trivial.

I find it amazing how simple axioms can be, and yet how they are such tricky and subtle beasts. Seemingly obvious axioms can stand for decades until massive, fundamental failures are found in them, and the replacement are only slightly less simple axioms that upon visual inspection reveal none of their heritage. Truly amazing little buggers.

I remember in a mathematical probability class, the professor writing down the three basic axioms. The first two are very simple...the third is just additivity:

  P(A1 U A2 U ...) = P(A1) + P(A2) + ...

for disjoint Ai's.

He explained the intent, and asked us if we thought the axiom was reasonable. He seemed very disappointed when everyone nodded and smiled that it seemed okay, unobjectionable, even obvious. He re-emphasized that this was an infinite union. He said something to the effect of, you seem too complacent about this one, because the union is allowed to be infinite, and you can play all kinds of games with that.

It was only later that some of us came across the huge literature that alters these axioms (some by weakening the additivity axiom above), to see what more general systems come out.

The third should be just additivity over countable sets of disjoint Ai's.

If you leave out countable, then I can make each Ai be a single real number. Under any continuous probability distribution, they have individual probability 0. Yet all together we want them to have probability 1.

Indeed. I used the ... notation rather than an abstract index to indicate a countable index set. If you expand out all the details, it's tedious. For instance, each Ai also has to be measurable.

Countable does not make a difference. If you pick a random integer, each has probability zero, but you will pick one of them.

Not a counterexample. There exists no continuous probability distribution over the integers, and therefore there is no way to "pick a random integer, each with probability zero".

No, it needs to be countable unions only.

And to your specific example: There is no probability measure on the integers that assigns zero probability to each integer.

Yep, that was a lapse of mind. I was thinking of divergent double sums vs divergent double integrals.

Remember that this is over the positive integers.

I think if you were interested enough to give it deeper thought, you would not be so disappointed.

Seems to me quite interesting that you need methods involving negative polynomial coefficients to prove statements that use only positive numbers.

Actually, it seems to be a concrete example for Gödel's incompleteness theorems: a very simple system can be used to make statements whose veracity can be proven only by using concepts outside the system.

Something similar: If you want to write down a formula for solving a cubic: ax^3+bx^2+cx+d = 0, for give a,b,c,d, you can't avoid using complex numbers. This is true even if you only care about cubics which have real solutions.

To clarify that last sentence, contrast it with the quadratic formula, which has no mention of the imaginary unit i. It's true that a quadratic with real coefficients might have only complex solutions, but you might just interpret that as having no solutions: once the formula tells you "take the square root of a negative", you know it has no real solutions.

Maybe this could be worked into something similar to the high school algebra problem, but with a list of axioms about real numbers.

That's what I thought too: no fixed set of axioms can prove all the possible true affirmations. There is always going to be one that is outside of their scope. That makes mathematics more interesting, almost like a living organism, full of surprises.

It's interesting that you need negative numbers in order to prove certain statements containing only positive numbers.

It's analogous to needing complex numbers to prove certain things about reals.

Isn't this just a special case of one of Godel's incompleteness theorems?

Roughly, the incompleteness theorems state that, in any sufficiently powerful, self-consistent, decidable mathematical axiom system, there are statements which are true, but cannot be proved. And "sufficiently powerful" means basically "including addition and multiplication." The high school axioms look like they're at least that powerful, so wouldn't it just be a direct application of Godel that such statements exist?

No, the question here is not "are there statements in _this axiom system_ that cannot be proved by this axiom system" (what incompleteness theorem says), but "are there statements about _the positive integers_ that cannot be proved by this axiom system". In other words, is this system of axioms equivalent to the axioms that define positive integers.

Reply on news.ycombinator.com