Say you prove □S (where □S is defined by means of Gödel numbering). Do you believe then that there is a proof of S inside the system? Conversely, if you prove ¬□S, do you actually believe that there is no proof of S? Or do you think that having □S gives us no information about proof of S, because it is based on meta-theory which isn’t justified? I don’t think one can evade these questions by throwing away meaning. If there is a proof of S, there is a chance that someone finds it. If meta-theory justifications are worthless, one would expect someone eventually proving ¬□S and S for some particular S. I don’t think it is going to happen and would find it extremely surprising and interesting if it did. What about you?
Well, actually doing mathematics is an ‘application’ of the Platonic ideal mathematics; the perfect draughtsman’s copy does involve semantics simply because that’s how the brain works. So I would indeed be surprised to see ¬□S and S proved for some PA-statement S, but only because in my experience thus far it has been predictively accurate to apply second-order arithmetic to PA. Nonetheless, if it did happen, then it wouldn’t refute PA, nor would it refute second-order arithmetic (neither has inherent ‘truth-value’, so the concept of ‘refuting’ them is unsinnig). What it would refute is the informal application of second-order arithmetic to PA. Though note that it wouldn’t refute the third-order arithmetic which proves the statement “second-order arithmetic applies to PA”, because “PA” is not PA.
It is, in my opinion, important to distinguish between the formal system X (which is timeless, unchanging, and Platonically real), and our experiences of applying X. Such experiences, which may lead us to make predictions, are not informative about X, rather they are informative about the informal process of applying X. My experiences with arithmetic lead me to predict, informally, that applying second-order arithmetic to PA won’t lead to contradiction. That says nothing about either arithmetic itself.
It is, in my opinion, important to distinguish between the formal system X (which is timeless, unchanging, and Platonically real), and our experiences of applying X.
Why is it important? I have actually difficulties seeing the boundary. What other information we have about a formal system except experiences of its application?
This reply seems a bit too brief. When speaking about e.g. physics, it’s clear what’s the map (our models and theories) and what’s the territory (nature around us). There are two principal ways of obtaining knowledge: exploring the territory by conducting experiments and exploring the map by calculating implications of our theories. In reality experimental results are viewed indirectly through prism of the theory, but the distinction between experimentally established facts and theoretically derived propositions is still pretty clear.
I don’t see similar distinction for formal system. All we know about a formal system we know because we apply its rules and derive theorems. We can in fact analyse the system on the meta level, but you seem to be objecting to that. So, what practical importance lies in the map-territory distinction here? What actual mistakes I could commit because I forget to make the distinction?
Say you prove □S (where □S is defined by means of Gödel numbering). Do you believe then that there is a proof of S inside the system? Conversely, if you prove ¬□S, do you actually believe that there is no proof of S? Or do you think that having □S gives us no information about proof of S, because it is based on meta-theory which isn’t justified? I don’t think one can evade these questions by throwing away meaning. If there is a proof of S, there is a chance that someone finds it. If meta-theory justifications are worthless, one would expect someone eventually proving ¬□S and S for some particular S. I don’t think it is going to happen and would find it extremely surprising and interesting if it did. What about you?
Well, actually doing mathematics is an ‘application’ of the Platonic ideal mathematics; the perfect draughtsman’s copy does involve semantics simply because that’s how the brain works. So I would indeed be surprised to see ¬□S and S proved for some PA-statement S, but only because in my experience thus far it has been predictively accurate to apply second-order arithmetic to PA. Nonetheless, if it did happen, then it wouldn’t refute PA, nor would it refute second-order arithmetic (neither has inherent ‘truth-value’, so the concept of ‘refuting’ them is unsinnig). What it would refute is the informal application of second-order arithmetic to PA. Though note that it wouldn’t refute the third-order arithmetic which proves the statement “second-order arithmetic applies to PA”, because “PA” is not PA.
It is, in my opinion, important to distinguish between the formal system X (which is timeless, unchanging, and Platonically real), and our experiences of applying X. Such experiences, which may lead us to make predictions, are not informative about X, rather they are informative about the informal process of applying X. My experiences with arithmetic lead me to predict, informally, that applying second-order arithmetic to PA won’t lead to contradiction. That says nothing about either arithmetic itself.
Why is it important? I have actually difficulties seeing the boundary. What other information we have about a formal system except experiences of its application?
Map-territory. You’re not distinguishing formal system X from our knowledge of formal system X.
This reply seems a bit too brief. When speaking about e.g. physics, it’s clear what’s the map (our models and theories) and what’s the territory (nature around us). There are two principal ways of obtaining knowledge: exploring the territory by conducting experiments and exploring the map by calculating implications of our theories. In reality experimental results are viewed indirectly through prism of the theory, but the distinction between experimentally established facts and theoretically derived propositions is still pretty clear.
I don’t see similar distinction for formal system. All we know about a formal system we know because we apply its rules and derive theorems. We can in fact analyse the system on the meta level, but you seem to be objecting to that. So, what practical importance lies in the map-territory distinction here? What actual mistakes I could commit because I forget to make the distinction?