First Isomorphism Theorem for Monoids?

Proposition $2$ is certainly true as soon as the operation on $G/H$ is well-defined, i.e. as soon as it doesn't depend on the choice of representatives $a$ and $b$ for the cosets $aH$ and $bH$. This is the case if $H$ is a "normal submonoid" as in your Definition 2, and can be shown more or less like in groups.

But it is not true that $aN=N$ is equivalent to $a\in N$ if $N$ is a submonoid: for example if you take the monoid of natural numbers with operation given by multiplication, then $N=\{0,1\}$ is a submonoid, and $0\in N$; but $0N=\{0\}\neq N$.

As I mentionned in a comment, the true problem is that the kernel of a homomorphism can be trivial without the homomorphism being injective. For example consider the homomorphism $$\varphi : (\Bbb N,\cdot ,1)\to (\Bbb N,\cdot ,1): x\mapsto 0 \text{ iff } x\neq 1;$$only $1$ is sent to $1$, so the kernel is trivial; but it is not injective, since every natural other than $1$ is mapped to $0$. Thus the quotient monoid (if it is well-defined) should be isomorphic to $\Bbb N$, while the image of $\varphi$ is the submonoid $N$ defined above. The problem with monoids is that unlike in groups, you can't take inverses, so the kernel doesn't give you enough information.

There is however a form of isomorphism theorem that holds; instead of quotienting by a subobject, you need to quotient by the equivalence relation defined by $$x\sim y\Leftrightarrow \varphi(x)=\varphi(y).$$ Then you can define an operation on the equivalence classes by putting $\overline{x}\cdot \overline{y}=\overline{x\cdot y}$, and show that $\varphi$ factorise through the quotient; and this factorisation will be injective because of the choice of the relation.

As Arnaud D. already pointed out, your approach is too naive to work properly, but you can consider the kernel congruence associated to $\varphi$. This approach works for many types of algebras, including monoids. See First Isomorphism Theorem for more details.

Defining the kernel of an homomorphism of monoids is another story and it took a long time to obtain an appropriate definition. The main problem with your definition 3, which has been frequently used, is that it does not contain enough information.

The difference between monoids and groups can be outlined as follows. Let $\pi: H \to G$ be a surjective group morphism and let $K = \pi^{-1}(1)$. Then $\pi(x_1) = \pi(x_2)$ iff $x_1x_2^{-1} \in K$. Let now $\pi: M \to G$ be a surjective monoid morphism and let $K = \pi^{-1}(1)$. Even if $K$ is given, it does not help to decide whether $\pi(x_1) = \pi(x_2)$, a major difference!

In order to avoid this problem, one needs to consider more general algebras than monoids, namely categories. I will just explain the case of a surjective monoid morphism $\pi$ from a monoid $M$ to a group $G$ (the general case, where $G$ is a monoid, is slightly more difficult to handle).

Definition. The kernel category $Ker(\pi)$ of $\pi$ has $G$ as its object set and for all $u,v \in G$ $$ Mor(u, v) = \{ (u, m, v) \in G \times M \times G \mid u\pi(m) = v \} $$ Note that $Mor(u, u)$ is a monoid equal to $\pi^{-1}(1)$ and that $G$ acts naturally (on the left) on $Ker(\pi)$.

I will not give here any detail on this theory, but I would like to give its spirit. In group theory, if $\pi: H \to G$ is a surjective group morphism and $K$ is the kernel of $\pi$, the synthesis problem consists in constructing $H$ given $G$ and $K$. This is in general a very difficult problem and there is a huge literature on this topic. In the same way, if $\pi: M \to G$ is a surjective monoid morphism, one would like to get information on $M$, given $G$ and $Ker(\pi)$. The results obtained in monoid theory are much weaker than the corresponding results for groups, but are nevertheless nontrivial to obtain.

For more information on this topic see these slides and the following references:

[1] S. Margolis, J.-É. Pin, Inverse semigroups and extensions of groups by semilattices, J. of Algebra 110 (1987), 277-297.

[2] J. Rhodes, B. Steinberg, The $q$-theory of finite semigroups. Springer Monographs in Mathematics. Springer, New York, 2009. xxii+666 pp. ISBN: 978-0-387-09780-0

[3] B. Steinberg, B. Tilson, Categories as algebra. II. Internat. J. Algebra Comput. 13 (2003), no. 6, 627--703.

[4] Tilson, Bret. Categories as algebra: an essential ingredient in the theory of monoids. J. Pure Appl. Algebra 48 (1987), no. 1-2, 83--198.