Don't you mean "The proposition that all dogs must be animals is necessary, but analytic."? That seems to me to be an example of an analytic proposition. While the first one you mention is not.
---------- Post added 01-06-2010 at 06:27 PM ----------
An(p), means, p is analytic.
D1. An(p) =df <>p -> p.
D2. (p => q) =df (p -> q).
D3. (p <=> q) =df (p <-> q).
1. An(p) => (p <-> p).
2. An(p) => (p <-> <>p).
3. An(p) => (<>p <-> p).
4. An(p) <=> (<>p <=> p).
5. An(p) <=> (p <=> <>p).
6. An(p) <=> (<>p <=> p).
7. (An(p) & <>p) -> p, is a theorem.
These definitions and theorems show that some modal arguments are circular.
For example, Hartshorne (1962), claims proof of God's existence with the following argument.
G = God exists.
8. (An(G) & <>G) -> G.
(God exists is analytic. & God exists is possible.) implies, God exists is actual.
This argument which is an instance of 7, is valid and not sound.
But, if G is analytic then <>G <=> G, (by 5.)
That is, the argument becomes..
8a. (An(G) & G) -> G) which is a circular argument. The premise includes the conclusion.
Since (An(p) & <>~p) -> ~p, is also a theorem...
8b. (An(G) & <>~G) => ~G, is also valid and not sound.
ie. God exists is analytic & God does not exist is possible, implies God does not exist is actual.
Hartshorne's modal ontological argument proves nothing.
Careful not to confuse circular logic with begging the question. His argument begs the question but it is not circular. A circularly argument, you may recall, is one where the conclusion is a premise of the argument. Being a conjunct of a conjunction that is a premise is question begging and not circularity.
Your formulas are unclear. I'm guessing that "=>" means logical implication, and "->" means material implication, "<>" logically possible, "" logically necessary. I prefer to use proper symbols such as "⇒" and "→" (and "◊" and "□"). I already linked you earlier to a site where you can find them but you don't seem to want to use them.
Otherwise I agree with you.