Of course I couldn’t say “we’ve just verified that the brain/pencil/computer behaves according to the laws of proof-verification as defined in [some formalization of metamathematics]” after producing a proof of “2+2=4″. To be able to say that, I would need to produce many different proofs and ascertain that they are correct from an independent source.
The idea of my “objection” was that I have to trust the medium of verification that it behaves according to the laws of proof-verification as defined in some formalization of metamathematics in order to use it for proving the theorem. But the medium itself is always part of the physical world, and there is no fundamental difference between proving the theorem using apples and proving it by drawing squiggles on a paper.
But the medium itself is always part of the physical world, and there is no fundamental difference between proving the theorem using apples and proving it by drawing squiggles on a paper.
The second statement does not follow from the first.
There is a difference between empirically observing that combining two apples with two apples yields four apples, and observing a sequence of squiggles on paper that constitutes a formal proof that 2+2=4. Yes, I’ll grant you that the difference isn’t written on the atoms making up the apples or the paper; rather it’s a matter of semantics, i.e. how these observations are interpreted by human minds. (You could presumably write out a formal proof using apples too—and then it would be just as different from the observation about combining pairs of apples as the squiggles on paper are.)
There is only one “level” of reality, but our model of reality can be organized into distinct levels. In particular, we use some parts of the physical world to model others; and when we do so, we have to be careful to distinguish discourse about the model from discourse within the model (i.e not to “confuse the map and the territory”).
Of course I couldn’t say “we’ve just verified that the brain/pencil/computer behaves according to the laws of proof-verification as defined in [some formalization of metamathematics]” after producing a proof of “2+2=4″. To be able to say that, I would need to produce many different proofs and ascertain that they are correct from an independent source.
The idea of my “objection” was that I have to trust the medium of verification that it behaves according to the laws of proof-verification as defined in some formalization of metamathematics in order to use it for proving the theorem. But the medium itself is always part of the physical world, and there is no fundamental difference between proving the theorem using apples and proving it by drawing squiggles on a paper.
The second statement does not follow from the first.
There is a difference between empirically observing that combining two apples with two apples yields four apples, and observing a sequence of squiggles on paper that constitutes a formal proof that 2+2=4. Yes, I’ll grant you that the difference isn’t written on the atoms making up the apples or the paper; rather it’s a matter of semantics, i.e. how these observations are interpreted by human minds. (You could presumably write out a formal proof using apples too—and then it would be just as different from the observation about combining pairs of apples as the squiggles on paper are.)
There is only one “level” of reality, but our model of reality can be organized into distinct levels. In particular, we use some parts of the physical world to model others; and when we do so, we have to be careful to distinguish discourse about the model from discourse within the model (i.e not to “confuse the map and the territory”).