Doesn’t this argument presume some sort of Platonism? If F is a formal system that fully captures the computational resources of our brains, then a Godel sentence for F, G, will be true in some models of the axioms of F and false in others. When you say that we have a meta-proof that G is true, you must mean that we have a meta-proof that G is true in the intended model. But how do we pick out the intended model? After all, our intentions are presumably also beholden to the computational limitations of our brains. How could we possibly distinguish between the different models of F in order to say “I’m talking about this model, not that one”?
If you’re a Platonist, perhaps you can get around this by positing that only one of the many models of F actually obtains, in the sense that only the numbers that appear in this model actually exist. So while we can’t pick out this model as the intended model from the inside, perhaps there’s some externalist story about how this model is picked out and other models (in which G is false) are not. Maybe there’s a quasi-causal connection between our brain and the numbers which makes it the case that our mathematical statements are about those numbers and not others. But Platonism, especially the sort of Platonism proposed here, is implausible.
Is there any other way to make sense of the claim that our mathematical claims are about a model in which G is true, even though there is no computational procedure by which we could pick out this model?
If we can model the standard natural numbers, then it seems we’re fine—the number godel-encoding a proof would actually correspond to a proof, we don’t need to worry further about models.
If we can’t pick out the standard natural numbers, we can’t say that any Godel sentences are true, even for very simple formal systems. All we can say is that they are unprovable from within that system.
I’ve never got a fully satisfactory answer to this. Basically the natural numbers are (informally) a minimal model of peano arithmetic—you can never have any model “smaller” than them.
And it may be possible to fomarlise this. Take the second order peano axioms. Their model is entirely dependent on the model of set theory.
Let M be a model of set theory. Then I wonder whether there can be models M’ and N of set theory, such that:
there exists a function mapping every set of M to set in M’ that preserves the set theoretic properties. This function is an object in N.
Then the (unique) model of the second order peano axioms in M’ must be contained inside the image of model in M. This allows us to give an inclusion relationship between second order peano models in different models of set theory. Then it might be that the standard natural numbers are the unique minimal element in this inclusion relationship. If that’s the case, then we can isolate them.
Then it might be that the standard natural numbers are the unique minimal element in this inclusion relationship.
Why would we care about the smallest model? Then, we’d end up doing weird things like rejecting the axiom of choice in order to end up with fewer sets. Set theorists often actually do the opposite.
Doesn’t this argument presume some sort of Platonism? If F is a formal system that fully captures the computational resources of our brains, then a Godel sentence for F, G, will be true in some models of the axioms of F and false in others. When you say that we have a meta-proof that G is true, you must mean that we have a meta-proof that G is true in the intended model. But how do we pick out the intended model? After all, our intentions are presumably also beholden to the computational limitations of our brains. How could we possibly distinguish between the different models of F in order to say “I’m talking about this model, not that one”?
If you’re a Platonist, perhaps you can get around this by positing that only one of the many models of F actually obtains, in the sense that only the numbers that appear in this model actually exist. So while we can’t pick out this model as the intended model from the inside, perhaps there’s some externalist story about how this model is picked out and other models (in which G is false) are not. Maybe there’s a quasi-causal connection between our brain and the numbers which makes it the case that our mathematical statements are about those numbers and not others. But Platonism, especially the sort of Platonism proposed here, is implausible.
Is there any other way to make sense of the claim that our mathematical claims are about a model in which G is true, even though there is no computational procedure by which we could pick out this model?
If we can model the standard natural numbers, then it seems we’re fine—the number godel-encoding a proof would actually correspond to a proof, we don’t need to worry further about models.
If we can’t pick out the standard natural numbers, we can’t say that any Godel sentences are true, even for very simple formal systems. All we can say is that they are unprovable from within that system.
If my brain is a Turing machine, doesn’t it pretty much follow that I can’t pick out the standard model? How would I do that?
I’ve never got a fully satisfactory answer to this. Basically the natural numbers are (informally) a minimal model of peano arithmetic—you can never have any model “smaller” than them.
And it may be possible to fomarlise this. Take the second order peano axioms. Their model is entirely dependent on the model of set theory.
Let M be a model of set theory. Then I wonder whether there can be models M’ and N of set theory, such that: there exists a function mapping every set of M to set in M’ that preserves the set theoretic properties. This function is an object in N.
Then the (unique) model of the second order peano axioms in M’ must be contained inside the image of model in M. This allows us to give an inclusion relationship between second order peano models in different models of set theory. Then it might be that the standard natural numbers are the unique minimal element in this inclusion relationship. If that’s the case, then we can isolate them.
Why would we care about the smallest model? Then, we’d end up doing weird things like rejecting the axiom of choice in order to end up with fewer sets. Set theorists often actually do the opposite.
Generally speaking, the model of Peano arithmetic will get smaller as the model of set theory gets larger.
And the point is not to prefer smaller or larger models; the point is to see if there is a unique definition of the natural numbers.