Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

> That seems implausible. All natural numbers are finite. I can easily express that in F.O.L.

Just for the sake of clear terminology, I'll take "finite natural number" to mean that it's either 0 or formed by applying the successor function to zero finitely many times.

Here's an easy proof for why you can't prove that every number is finite in PA:

Take the theory PA' = PA + the infinitely many sentences "c > 0", "c > S 0", "c > S (S 0)", etc. (with a new constant c)

We can probably agree that the standard natural numbers aren't a model of PA' because there is no natural number greater than every other natural number.

However, the natural numbers are clearly a model of any finite subset of that theory. And here's where we use the compactness theorem (which is easily proven from completeness): https://en.m.wikipedia.org/wiki/Compactness_theorem

By compactness, PA' has a model. But that model can't be the standard model of arithmetic. Yet it is also a model of PA. Thus we have a model of PA in which infinite numbers exist - so we can't prove that all natural numbers are finite from PA.

To rule out such models - and therefore prove that every natural number is finite - you need the second-order induction axiom.



> To rule out such models - and therefore prove that every natural number is finite - you need the second-order induction axiom.

Sorry, I don't see why second-order induction is required. AFAICT all you need is a first-order induction axiom instantiated on the predicated FINITE.


I don't know why I wrote an entire proof outlining why first-order PA cannot rule out infinite numbers, if you just ignore it and insist on your misconception. The set of finite numbers is undefinable in the language of first-order PA, which is why first-order induction isn't enough.

Read a textbook, these are well-known facts. Here's a free one that is quite good, chapter 3 is relevant: https://milneopentextbooks.org/a-friendly-introduction-to-ma...




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: