5 ms·

Thanks, that was very helpful. One question though: > there is absolutely no statement in first order logic that can explain what we mean by finite That seem

by lisper 2y ago

Thanks, that was very helpful. One question though: > there is absolutely no statement in first order logic that can explain what we mean by finite That seems implausible. All natural numbers are finite. I can easily express that in F.O.L.

btilly 2y ago
Well, you can define something meaning "finite" in first order logic. It just won't mean what we want it to mean. Take your example. "All natural numbers are finite." How do we define the natural numbers in first order logic? Let's use PA. Now take a nonstandard model of PA in which you can prove that PA is inconsistent. You will have a "proof" in that model that PA is inconsistent. That "proof" has a length. In that model, that "proof" will be of "finite" length. There is no contradiction here...but only because that "proof" is (from our point of view) infinitely long. So the proof can go wrong even though it goes wrong at no step. From my point of view, first order logic captures the idea of "finite" as well (or poorly) as classical mathematics captures the idea of "exists". And second order logic requires accepting the truth of unprovable things. But if you're willing to accept the truth of unprovable things, and the existence of non-constructible ones, we get the standard mathematics that mathematicians use without questioning too hard.
- lisper 2y ago
  > Now take a nonstandard model of PA in which you can prove that PA is inconsistent. Sorry, I lost you there. You don't prove things in models, you prove things in systems. Models are semantic things, proofs are syntactic things, so a "proof in a model" sounds like a category error to me.
  - Tainnor 2y ago
    Proofs are natural numbers via Gödel's encoding, or any other encoding scheme that you'd like (e.g. ASCII). The sentence "PA is inconsistent" can be stated in the language of PA and it means "there is a number that encodes a valid proof from the axioms of PA to a contradiction (e.g. 0 ≠ 0)". This sentence is either true in all models of PA (in which case PA would be inconsistent, which we don't think it is), or it is true in some models and false in others - it can't be false in all models because otherwise, by completeness, there'd be a proof of PA's consistency in PA which is what the second incompleteness theorem rules out. The reason why this is not a category error is because of the self-referentiality of strong enough systems of logic.
  - btilly 2y ago
    I guess I calibrated your understanding of formal logic to the wrong place. Let me try again. PA is a set of axioms satisfied by the natural numbers. As Gödel showed, all of first order logic can be encoded into the natural numbers. And questions like, "This is a proof of X" can be viewed as arithmetic statements. (We can actually go further, and encode all of computation into the natural numbers, and reason about computation using nothing more than PA.) Gödel famously went further. Suppose that X is an axiom system. Then Gödel's famous incompleteness theorem says: ((X => PA) + (X => Con(X))) => not Con(X) Let's take that apart. By (X => PA) I mean that from X we can find the existence of something that satisfies the Peano axioms. By (X => Con(X)) I mean that there is a proof from X that X is consistent. And from those facts, Gödel can construct a proof from X that X is not consistent. It is very important here to note. If we actually have a proof from X of Con(X), then Gödel actually gives us a proof from X of not Con(X). But, thanks to the Gödel numbering, (X => Con(X)) can also be interpreted as a statement about the natural numbers. As such, (X => Con(X)) is a potential axiom in first order logic. Of course all proofs that "really are proofs" correspond to actual finite numbers. So if there "isn't really" a proof of Con(X) from X, then any model of X + (X => Con(X)) will have the Gödel number of that proof not be a finite number. But that's OK because first order logic can't rule out nonstandard models. And nonstandard models of PA include infinite integers. So any model of X + (X => Con(X)) will have a "proof" of X + (X => Con(X)). We can decode as much of that "proof" as we like. But we can't decode the whole thing, and it "isn't really" a proof after all. Of course if we have that then Gödel's construction gives us a Gödel number for the proof of not Con(X). This is an absolutely general line of reasoning. Take any consistent set of first order axioms X which imply PA. If it is consistent, we don't create a contradiction by adding the axiom that there exists a Gödel number representing (X => Con(X)). Because this new set of axioms is consistent, there must exist (for some definition of existence) a model for it. That model for it will include a model of PA. That model of PA will include a Gödel number for a proof that isn't really a proof, meaning that it can't really a be finite integer. Therefore it must be an infinite integer. And therefore the set of first order axioms X cannot distinguish between what we want finite to mean, and something that is clearly not finite. Second order logic gets around this problem. But it does so by accepting that things can be true without there being any proof that it is true. This is one of the potential sticking points for someone with Constructivist tendencies.
Tainnor 2y ago
> 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 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.
- lisper 2y ago
  > 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.
  - Tainnor 2y ago
    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-mathematical-logic/ https://milneopentextbooks.org/a-friendly-introduction-to-ma...

by lisper 2y ago

btilly 2y ago

Well, you can define something meaning "finite" in first order logic. It just won't mean what we want it to mean. Take your example. "All natural numbers are finite." How do we define the natural numbers in first order logic? Let's use PA. Now take a nonstandard model of PA in which you can prove that PA is inconsistent. You will have a "proof" in that model that PA is inconsistent. That "proof" has a length. In that model, that "proof" will be of "finite" length. There is no contradiction here...but only because that "proof" is (from our point of view) infinitely long. So the proof can go wrong even though it goes wrong at no step. From my point of view, first order logic captures the idea of "finite" as well (or poorly) as classical mathematics captures the idea of "exists". And second order logic requires accepting the truth of unprovable things. But if you're willing to accept the truth of unprovable things, and the existence of non-constructible ones, we get the standard mathematics that mathematicians use without questioning too hard.

lisper 2y ago
> Now take a nonstandard model of PA in which you can prove that PA is inconsistent. Sorry, I lost you there. You don't prove things in models, you prove things in systems. Models are semantic things, proofs are syntactic things, so a "proof in a model" sounds like a category error to me.
- Tainnor 2y ago
  Proofs are natural numbers via Gödel's encoding, or any other encoding scheme that you'd like (e.g. ASCII). The sentence "PA is inconsistent" can be stated in the language of PA and it means "there is a number that encodes a valid proof from the axioms of PA to a contradiction (e.g. 0 ≠ 0)". This sentence is either true in all models of PA (in which case PA would be inconsistent, which we don't think it is), or it is true in some models and false in others - it can't be false in all models because otherwise, by completeness, there'd be a proof of PA's consistency in PA which is what the second incompleteness theorem rules out. The reason why this is not a category error is because of the self-referentiality of strong enough systems of logic.
- btilly 2y ago
  I guess I calibrated your understanding of formal logic to the wrong place. Let me try again. PA is a set of axioms satisfied by the natural numbers. As Gödel showed, all of first order logic can be encoded into the natural numbers. And questions like, "This is a proof of X" can be viewed as arithmetic statements. (We can actually go further, and encode all of computation into the natural numbers, and reason about computation using nothing more than PA.) Gödel famously went further. Suppose that X is an axiom system. Then Gödel's famous incompleteness theorem says: ((X => PA) + (X => Con(X))) => not Con(X) Let's take that apart. By (X => PA) I mean that from X we can find the existence of something that satisfies the Peano axioms. By (X => Con(X)) I mean that there is a proof from X that X is consistent. And from those facts, Gödel can construct a proof from X that X is not consistent. It is very important here to note. If we actually have a proof from X of Con(X), then Gödel actually gives us a proof from X of not Con(X). But, thanks to the Gödel numbering, (X => Con(X)) can also be interpreted as a statement about the natural numbers. As such, (X => Con(X)) is a potential axiom in first order logic. Of course all proofs that "really are proofs" correspond to actual finite numbers. So if there "isn't really" a proof of Con(X) from X, then any model of X + (X => Con(X)) will have the Gödel number of that proof not be a finite number. But that's OK because first order logic can't rule out nonstandard models. And nonstandard models of PA include infinite integers. So any model of X + (X => Con(X)) will have a "proof" of X + (X => Con(X)). We can decode as much of that "proof" as we like. But we can't decode the whole thing, and it "isn't really" a proof after all. Of course if we have that then Gödel's construction gives us a Gödel number for the proof of not Con(X). This is an absolutely general line of reasoning. Take any consistent set of first order axioms X which imply PA. If it is consistent, we don't create a contradiction by adding the axiom that there exists a Gödel number representing (X => Con(X)). Because this new set of axioms is consistent, there must exist (for some definition of existence) a model for it. That model for it will include a model of PA. That model of PA will include a Gödel number for a proof that isn't really a proof, meaning that it can't really a be finite integer. Therefore it must be an infinite integer. And therefore the set of first order axioms X cannot distinguish between what we want finite to mean, and something that is clearly not finite. Second order logic gets around this problem. But it does so by accepting that things can be true without there being any proof that it is true. This is one of the potential sticking points for someone with Constructivist tendencies.

Tainnor 2y ago

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

lisper 2y ago
> 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.
- Tainnor 2y ago
  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-mathematical-logic/ https://milneopentextbooks.org/a-friendly-introduction-to-ma...