Would a proof of P=NP have philosophical implications? If so, what?

Does it make sense to discuss “HumanP,” loosely defined as the class of decision problems solvable in polynomial time by human beings? Is “HumanP” meaningless because we can’t give human beings arbitrarily-long inputs, in contrast to idealized computers? Or does this problem simply underscore that the asymptotic limit isn’t what we “really” cared about in the first place, but is just a theoretically-convenient approximation?

What can be said about the relationship of “HumanP” to P and to NP (in either direction)? Do we need to distinguish different versions of “HumanP”, depending on what resources the human has available (e.g., paper and pencil, a classical computer, a quantum computer), or whether we’re considering subconscious processes or conscious processes only?

How would a chess program need to be designed so that it chose the right move in the “wall of pawns” position? How would a SAT-solver need to be designed so that it quickly determined the unsatisfiability of a propositional formula representing PHP_{n} (the Pigeonhole Principle with n pigeons)?

Is the problem with existing SAT-solvers merely that they’re missing relevant “abstract knowledge” (e.g., that the Pigeonhole Principle is true)? Or is the problem that, even if they had that knowledge, they wouldn’t know how to use it, or to recognize when it *should* be used? Or is the problem that they don’t have the capacity to generate such abstract knowledge themselves? Are these distinctions even meaningful?

Does it make sense to speak about the “largest known prime number”? By what criterion, if any, can we say that **p := 2**^{43,112,609} – 1 is a “known” prime, whereas **q := the first prime larger than p** is not?

Are the above questions all “pseudoproblems” that evaporate as soon as we fix the right formal definitions for notions such as *knowledge*? If so, then what *are* the right formal definitions? And what questions should we be asking instead?