That does not mean, however, that “2+2=4” is “independent of the physical world”. The dependence simply occurs at a different logical level: the level where the instruments of formal verification (brains, computers, pencils, papers) are considered to be physical objects.
It doesn’t seem to me that the levels can be easily separated. Even if you verify that “2+2=4” using your brain, pencil or computer, I can always object that you have not verified the proposition itself, but that the system of brain, pencil or the specific computer program behaves according to the laws of integer addition as defined in ZFC set theory. Now the computer program was probably written to simulate the said laws of integer addition, while the apples were added before mathematics was formalised, but that’s a remark of merely historical interest.
Even if you verify that “2+2=4” using your brain, pencil or computer, I can always object that you have not verified the proposition itself, but that the system of brain, pencil or the specific computer program behaves according to the laws of integer addition as defined in ZFC set theory.
Actually, no: if you wanted to make an “objection” like this, you’d have to pass to the next level up. You’d have to say something like “we’ve just verified that the brain/pencil/computer behaves according to the laws of proof-verification as defined in [some formalization of metamathematics]”. This is not the same—and, crucially, is not incompatible with also having verified “2+2=4”. The two notions of verification are different: verifying “2+2 = 4″ has to do specifically with producing a proof, while verifying that “X behaves according to laws Y” involves empirically observing X in general, in a way that directly depends on what Y is.
(To help illustrate the distinction, note for example that to verify that “2+2 =4”, you only need to produce a single proof, in a single medium; whereas verifying that “X behaves according to Y” would usually require observing a multitude of instances.)
So this “objection” wouldn’t support the first view, which holds that “2+2=4″ is verified in the latter way, by observing apples (etc.), and denies the necessity of a formal proof intervening for verification to take place. (To the holder of the first view, a formal proof would just be a kind of instrument for predicting the behavior of apples and the like, and is not necessary to the meaning of the proposition.)
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”).
Corrected, thanks.
It doesn’t seem to me that the levels can be easily separated. Even if you verify that “2+2=4” using your brain, pencil or computer, I can always object that you have not verified the proposition itself, but that the system of brain, pencil or the specific computer program behaves according to the laws of integer addition as defined in ZFC set theory. Now the computer program was probably written to simulate the said laws of integer addition, while the apples were added before mathematics was formalised, but that’s a remark of merely historical interest.
Actually, no: if you wanted to make an “objection” like this, you’d have to pass to the next level up. You’d have to say something like “we’ve just verified that the brain/pencil/computer behaves according to the laws of proof-verification as defined in [some formalization of metamathematics]”. This is not the same—and, crucially, is not incompatible with also having verified “2+2=4”. The two notions of verification are different: verifying “2+2 = 4″ has to do specifically with producing a proof, while verifying that “X behaves according to laws Y” involves empirically observing X in general, in a way that directly depends on what Y is.
(To help illustrate the distinction, note for example that to verify that “2+2 =4”, you only need to produce a single proof, in a single medium; whereas verifying that “X behaves according to Y” would usually require observing a multitude of instances.)
So this “objection” wouldn’t support the first view, which holds that “2+2=4″ is verified in the latter way, by observing apples (etc.), and denies the necessity of a formal proof intervening for verification to take place. (To the holder of the first view, a formal proof would just be a kind of instrument for predicting the behavior of apples and the like, and is not necessary to the meaning of the proposition.)
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”).