5 ms·

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

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

lisper 2y ago
Thanks for taking the time to explain this. I thought I understood this stuff, but apparently I'm still missing something. I obviously need to ponder it some more, because I still don't understand why second-order induction succeeds where first-order induction fails. We are only dealing with one predicate here, FINITE. So why should it make a difference if induction on FINITE is a first-order instantiation of an axiom schema, or an instantiation of a second-order axiom? Proving that all natural numbers are finite still boils down to induction on FINITE, no?
- Tainnor 2y ago
  What is "FINITE"?
  - lisper 2y ago
    Well, that is a good question. It’s a concept I’ve always just taken for granted. How do you define it? I don’t know.
    - Tainnor 2y ago
      So the problem with logic and in particular model theory is that you always have to assume some sort of logic for the world where your models live in (a meta-logic) - otherwise you can't talk about anything. If you take e.g. ZFC for granted in the world of your models, then you can talk about "the" natural numbers, where every number is finite, as a model of PA. And you can also define non-standard models of PA which include infinite numbers. If you use some other foundation, you can probably also define these models in some way. Now whether these constructions mean anything to you, or capture your intuition about "finiteness" is another thing entirely... The problem is that from within the theory you cannot distinguish between these different models. There's no way of defining a predicate "finite" in first-order PA that agrees with the notion of "finite" that you've established in your meta-logic. And in general, it's worse than that. As long as your first-order theory allows for any infinite model, there exist models of that theory of any infinite cardinality (this is the Löwenheim-Skolem theorem). So, in general, first-order logic cannot pin down structures uniquely. (Again, this is assuming ZFC in the world of our models.) This btw also leads to the "Skolem paradox" which states that there are countable models of (first-order) ZFC, even though ZFC says that there exist uncountable sets. But this is only a "paradox" until you realise that "countable" and "uncountable" don't mean the same thing within the model as they do outside of the model.

by btilly 2y ago

lisper 2y ago

Thanks for taking the time to explain this. I thought I understood this stuff, but apparently I'm still missing something. I obviously need to ponder it some more, because I still don't understand why second-order induction succeeds where first-order induction fails. We are only dealing with one predicate here, FINITE. So why should it make a difference if induction on FINITE is a first-order instantiation of an axiom schema, or an instantiation of a second-order axiom? Proving that all natural numbers are finite still boils down to induction on FINITE, no?

Tainnor 2y ago
What is "FINITE"?
- lisper 2y ago
  Well, that is a good question. It’s a concept I’ve always just taken for granted. How do you define it? I don’t know.
  - Tainnor 2y ago
    So the problem with logic and in particular model theory is that you always have to assume some sort of logic for the world where your models live in (a meta-logic) - otherwise you can't talk about anything. If you take e.g. ZFC for granted in the world of your models, then you can talk about "the" natural numbers, where every number is finite, as a model of PA. And you can also define non-standard models of PA which include infinite numbers. If you use some other foundation, you can probably also define these models in some way. Now whether these constructions mean anything to you, or capture your intuition about "finiteness" is another thing entirely... The problem is that from within the theory you cannot distinguish between these different models. There's no way of defining a predicate "finite" in first-order PA that agrees with the notion of "finite" that you've established in your meta-logic. And in general, it's worse than that. As long as your first-order theory allows for any infinite model, there exist models of that theory of any infinite cardinality (this is the Löwenheim-Skolem theorem). So, in general, first-order logic cannot pin down structures uniquely. (Again, this is assuming ZFC in the world of our models.) This btw also leads to the "Skolem paradox" which states that there are countable models of (first-order) ZFC, even though ZFC says that there exist uncountable sets. But this is only a "paradox" until you realise that "countable" and "uncountable" don't mean the same thing within the model as they do outside of the model.