Now the SEP shows that it's possible to derive Gödel's 2nd incompleteness theorem from this setup. However, what is its connection with Gödel's 1st incompleteness theorem? It seems unlikely that this is contained within Löb's theorem, as this answered a question by Henkin about sentences that assert their own provability, whereas Gödel investigated sentences that asserted their non-provability.
(2 years later) I stumbled across a very nice and clean answer, here goes:
First, let's suppose arithmetic is consistent. If it isn't, Gödel/Rosser is trivially valid since their result is of form "if PA is consistent, then ...".
Assume that you can prove F, or prove ¬F, for each formula F (contrary to Gödel/Rosser's theorem).
If you can prove a certain arbitrary but fixed formula F, then you can also prove Bew([F]), Bew being the standard provability predicate and  coding (meta)operator. If you can prove ¬F, then you can prove Bew([¬F]). Thus, regardless whether F is provable or ¬F is provable, you can prove (Bew([¬F]) or Bew([F])) for each formula F.
But by Solovay's completeness theorem for provability logic (system GL), formula (F or ¬F) should then be a theorem of GL. However, it isn't. Counterexample Kripke model: l[p] <- w -> r[¬p], model is transitive and converse well-founded, but w |=/= (p or ¬p).
edit: see my other answer (below or above this one).
The second theorem would actually be (ASCII art since we lack LaTeX here):
GL |- ~_|_ => GL |- _|_,
and not what SEP gives a proof of, which is:
GL |- ~_|_ -> _|_
which is actually a "formalized" version of the second incompleteness theorem (PA talking about itself, again). I don't think the first version given above makes any sense (the "actual" 2. I. T.), since we know
GL |-/- _|_ (that is, that GL is consistent)
So, my guess is that the best you could look for in GL is a formalized version of the first incompleteness theorem.
Perhaps this is a good place to start (the formula below is indeed a theorem, you can check that by trees or direct proof given in Boolos' The Logic of Provability):
GL |- (p <-> ~p) -> (p <-> ~_|_)
Which can be (roughly) translated as "If (it's provable that) P says that P is unprovable, then P is provable if and only if you can prove consistency".
If you assume: (p <-> ~p) then (p <-> ~_|_), and if p, then: ~_|_, then _|_, while if ~p, then ~~_|_, that is: _|_
GL |- ((p <-> ~p) && (p or ~p)) -> (_|_ or _|_)
Perhaps there is even a more direct way to represent the first theorem, I'm not sure. (This would have been a comment if I was allowed to post one. :) ).
According to this answer by Peter Smith:
As you say, you can get the second incompleteness theorem from the Hilbert-Bernays-Löb derivability conditions on the provability predicate (which are what are reflected in the modal "provability logic") together with the diagonalization lemma which tells us that there is a fixed point for 'not provable'. But you need the diagonalization lemma for the standard proof of the second theorem using the derivability conditions (no?).
And that diagonalization lemma, of course, will give you the first theorem almost immediately.
So, the answer is yes.