Having now looked up the PH theorem, I don’t understand what you mean. Do you disagree with any of the following?
Computers can prove Paris-Harrington just as easily as humans can. They can also prove the strong Ramsey result that is the subject of PH as easily as humans can.
Both humans and computers are incapable of proving the Ramsey result within Peano arithmetic. Both are capable of proving it in some stronger formal systems.
Both humans and computers can “see that the Ramsey result is true” in the sense that they can verify that a certain string of symbols is a valid proof in a formal system. They are both equally capable of verifying that the Ramsey result (which concerns finite sets of integers) is true by experiment. Neither a human nor a computer can “see that the Ramsey result is true” in any stronger sense.
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.
Having now looked up the PH theorem, I don’t understand what you mean. Do you disagree with any of the following?
Computers can prove Paris-Harrington just as easily as humans can. They can also prove the strong Ramsey result that is the subject of PH as easily as humans can.
Both humans and computers are incapable of proving the Ramsey result within Peano arithmetic. Both are capable of proving it in some stronger formal systems.
Both humans and computers can “see that the Ramsey result is true” in the sense that they can verify that a certain string of symbols is a valid proof in a formal system. They are both equally capable of verifying that the Ramsey result (which concerns finite sets of integers) is true by experiment. Neither a human nor a computer can “see that the Ramsey result is true” in any stronger sense.
I agree with everything in your comment except the last sentence. Sorry for being cryptic, I think this still gets the point across :-)
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.
Shades of Penrosian nonsense.