Can any sense be made out of my vague feeling that some proofs in Ramsey theory are as close as you can get to non-constructive proofs without crossing the line? Is there any way to make this precise?
PS: OK, the short version of the elaboration of which I wrote in the comments below goes like this: In many areas of mathematics, if you want to prove that $X$ exists, you somehow figure out some plausible guess about which object $X$ is or where to find $X$, and then you work on figuring out how to rigorously prove that $X$ is it. In Ramsey theory, it seems as if you have a systematically eliminate every suspect one-by-one and until nothing else is left but $X$.
Alright, one concrete example: Shortly before posting this I had worked through this elementary exercise: In a set of $(n-1)m+1$ people, show that either there is a set of $m$ who are mutually unacquainted or there is one who knows at least $n$ others.
I came up with a description of an algorithm, as follows.
$(1)$ Initially let $A=\varnothing$. We will increment $A$ by adding a new member to it as many times as this algorithm occasions that addition. The members of the set $A$ will always be mutually unacquainted.
$(2)$ Does some member of $A$ know at least $n$ non-members of $A$? If so, STOP. We're done.
$(3)$ Otherwise, each member of $A$ knows at most $n-1$ non-members of $A$, so the total number of people known by members of $A$ is at most $(n-1)|A|\le(n-1)m<(n-1)m+1$. In that case, at least one non-member of $A$ is unknown to all members of $A$. Let the new value of $A$ be $A\cup\{\text{that one non-member of $A$}\}$.
$(4)$ If $|A|=m$ the STOP; we're done. Otherwise return to $(2)$ and go on from there.
Comment was too short.
My intuition is that a proof is constructive if it gives an algorithm which constructs some representation of the desired object (the algorithm here has a slightly broader meaning than the usual notion in computer science). However, that algorithm might be infeasible/intracable, i.e. the number of operations it requires may make it unusable even for small inputs (e.g. see this class).
In such case we know the algorithm exists, but it doesn't help us in constructing the object. Strangely we find ourselves in situation that is practically (whatever that would mean in this abstract setting) no better than one with non-constructive proof. I would say that this is very close to your boundary and Ramsey theory does involve numbers so huge that my imagination has problems handling them.
I'm not sure if this is more precise than your description, but nevertheless I hope it helps $\ddot\smile$