Can I attempt a translation/expansion for Sewing-Machine of why you disagree with the last sentence?
It seems that there’s an intuition among humans that the Ramsey result is true, in the sense that PA + PH captures our intuition of the integers more closely than PA + ~PH given the second order result. What you want is a computer to be able to make that sort of intuitive reasoning or to make it more precise. Is that more or less the point?
We can all agree that human intuition is grand but not magical, I hope? Here is my point of view: you are having difficulty teaching a computer to “make that sort of intuitive reasoning” because that sort of reasoning is not quite right.
“That sort of reasoning” is a good heuristic for discovering true facts about the world (for instance, discovering interesting sequences of symbols that constitute a formal proof of the Paris-Harrington theorem), and to that extent it surely can be taught to a computer. But it does not itself express a true fact about the world, and because of that you are limited in your ability to make it part of the premises on which a computer operates (such as the limitation discussed in the OP).
I’m really at a loss as to why such a thing should be intuitive. The additional condition seems to me to be highly unnatural; Ramsey’s theorem is a purely graph-theoretic result, and this strengthened version involves comparing the number of vertices used to numbers that the vertices happen to correspond to, a comparison we would ordinarily consider meaningless.
If I’m following cousin it, the idea doesn’t have anything really to do with the statement about Ramsey numbers. As I understand it, if in some system that is only slightly stronger than PA we can show some statement S of the form A x in N, P(x), then we should believe that the correct models of PA are those which have S being true. Or to put it a different way, we should think PA + S will do a better job telling us about reality than PA + ~S would. I’m not sure this can be formalized beyond that. Presumably if it he had a way to formalize this, cousin it wouldn’t have an issue with it.
Can I attempt a translation/expansion for Sewing-Machine of why you disagree with the last sentence?
It seems that there’s an intuition among humans that the Ramsey result is true, in the sense that PA + PH captures our intuition of the integers more closely than PA + ~PH given the second order result. What you want is a computer to be able to make that sort of intuitive reasoning or to make it more precise. Is that more or less the point?
We can all agree that human intuition is grand but not magical, I hope? Here is my point of view: you are having difficulty teaching a computer to “make that sort of intuitive reasoning” because that sort of reasoning is not quite right.
“That sort of reasoning” is a good heuristic for discovering true facts about the world (for instance, discovering interesting sequences of symbols that constitute a formal proof of the Paris-Harrington theorem), and to that extent it surely can be taught to a computer. But it does not itself express a true fact about the world, and because of that you are limited in your ability to make it part of the premises on which a computer operates (such as the limitation discussed in the OP).
So I’ve been thinking lately, anyway.
I’m really at a loss as to why such a thing should be intuitive. The additional condition seems to me to be highly unnatural; Ramsey’s theorem is a purely graph-theoretic result, and this strengthened version involves comparing the number of vertices used to numbers that the vertices happen to correspond to, a comparison we would ordinarily consider meaningless.
If I’m following cousin it, the idea doesn’t have anything really to do with the statement about Ramsey numbers. As I understand it, if in some system that is only slightly stronger than PA we can show some statement S of the form A x in N, P(x), then we should believe that the correct models of PA are those which have S being true. Or to put it a different way, we should think PA + S will do a better job telling us about reality than PA + ~S would. I’m not sure this can be formalized beyond that. Presumably if it he had a way to formalize this, cousin it wouldn’t have an issue with it.