5 ms·

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 f

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

by btilly 2y ago

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.