I know that if $P$ is a projective module, then there exists a free module $F$ such that $F\cong P\oplus K$ for some module $K$.
If $P$ is also finitely generated, it may be a direct summand of an infinitely generated free module, but are we guaranteed the existence of at least one finitely generated free module $F$ satisfying the statement above? If so, how do we know such an $F$ exists?
On
As a counterpoint to the approach of "reprove the theorem with a free module of finite rank," we can also see if it can be recovered from $F$ directly.
Lemma: Let $\kappa$ be an infinite cardinal used to index summands of the free module $F=\bigoplus_{i\leq\kappa}R_i$. If $N\subseteq F$ is a f.g. submodule, then $N\subseteq \bigoplus_{i\leq n}R_i$ for some natural number $n$.
Proof: Obviously each member of a finite generating set for $N$ lies in such an initial segment of $F$. Take the maximum length required by each generator: this suffices for $n$. Since all generators are trapped in this finite initial segment, the span ($=N$) is contained in the finite initial segment.Proposition: If for any modules $N,F,F'$ we have $N\subseteq F'\subseteq F$ and $N$ is a summand in $F$, then $N$ is also a summand in $F'$.
Proof: Let $N\oplus C=F$. Then $F'=F'\cap F=F'\cap(N+ C)=N+(F'\cap C)$. (This depends on the assumption $N\subseteq F'$. It is not necessarily true otherwise.) Obviously $N+(F'\cap C)\subseteq N\cap C=\{0\}$, so the sum $F'=N\oplus (F'\cap C)$ is direct.
Of course to apply it to your situation, you are letting $F'$ be the finite initial segment found in the first lemma.
Yes, this is immediate from the proof that such a free module exists. The proof is to take a free module $F$ with a surjection $F\to P$, and use projectivity to conclude that that this surjection splits. All this argument uses is that $F$ is some free module with a surjection to $P$. If $P$ is finitely generated, there exists such an $F$ that is finitely generated (just take the free module on any finite set of generators of $P$).