Hacker News Reader

Comment by pa7x1 | Hacker News Reader

It's both. The axioms are invented, the corpus of theorems is discovered. As once the axioms are chosen the provable theorems are already fixed.

But the axioms are a choice, and we can pick different ones. The common choice of axioms is utilitarian, they lead to interesting math that helps us describe the universe.

View on HN

I would agree the axioms are chosen, but what’s the connection between choosing something and inventing it?

Choosing to study molecular biology doesn’t mean cells are a human invention.

That the universe chose axioms is indeed the mystery.

Proving a theorem given a set of axioms is a search problem. Given a set of axioms you can apply rules of inference to generate the graph of all provable theorems. Proving a theorem is about finding a path from the axioms to the vertex which is your theorem.

But you can make the same case for axioms - that they are not invented but discovered through a process of search in the space of axioms.

I'm not sure I see why the axioms were not also discovered though? Choice between irreducible assumptions does not seem to make them any more 'invented'.

Without entering into an endless debate about semantics and metaphysics I would simply say that if you want to use the word discovered for the axioms then you must acknowledge that the theorems are not the same kind of discovered.

What about natural numbers?

I've read that Godel's result and diagonalization procedure shows that they exist (not invented).

Are the theories beyond axiom fundamentally different if axioms are changed, though? And if not, aren't then axioms merely props or placeholders for invariants?

Yes they are different - example: https://en.m.wikipedia.org/wiki/Parallel_postulate

Reply on news.ycombinator.com