First of all I would have thought of a proposition at least as the class of all sub-objects with domain $\phi$, and this would still be weaker than the logician's notion of proposition. But let's accept this weak notion of proposition that nlab is giving. If someone wants to make a comment about it, more than welcome.
What troubles me the most is that there are possibly many monomorphisms $\phi\hookrightarrow A$ ---terms of type $A$ with a free variable of type $\phi$ with the usual quotient for the definition of sub-object that under this interpretation becomes alpha equivalence.
What do these terms add to the interpretation of what the proposition ends up being?
For instance, what's the difference between the two "propositions" $f(x) : [x:\phi] \hookrightarrow A$ and $g(x) : [x:\phi] \hookrightarrow A$, for $f$ and $g$ different function symbols.
I'm just starting to learn about this so I might be getting some stuff wrong.
Thanks in advance!
Usually we define subobjects of $A$ not as monomorphisms $\phi \hookrightarrow A$, but as equivalence classes of such monomorphisms. Intuitively we should identify two monomorphisms with the same image in $A$.
Precisely, say that $(\phi : X \to A) \leq (\psi : Y \to A)$ if and only if there is an arrow $f : X \to Y$ so that $\phi = \psi f$. Intuitively this says that the image of $\phi$ is contained in the image of $\psi$. Then we quotient the category of monos into $A$ by the equivalence relation where $\phi \sim \psi$ if and only if $\phi \leq \psi$ and $\psi \leq \phi$.
This solves your problem (2).
I don't fully understand your issue with (1). In $\mathsf{Set}$ we can identify subsets of $A$ with predicates on $A$. Namely we identify $P \subseteq A$ with the predicate $\mathbb{1}_P$ where $\mathbb{1}_P(a) = \begin{cases} \top & a \in P \\ \bot & a \not \in P \end{cases}$. Conversely, given a predicate $\phi(x)$ on $A$, we identify it with the subset $\{ a \mid \phi(a) \} \subseteq A$.
Generalizing to the world of categories, we don't have a way to get our hands on "subsets", only arrows. But we know that the subsets of $A$ are exactly the images of monomorphisms into $A$. After all, for any $P \subseteq A$, the inclusion $P \hookrightarrow A$ is a mono whose image is $P$. Conversely, for any mono $f : X \to A$, its image (which we can identify with $X$, up to isomorphism) is a subset of $A$.
This is what motivates the definition of subobject as monomorphisms into $A$. As you've correctly noticed, though, we overcount quite a bit when we do this (since we only really care about the image in $A$, not the mono itself). This is why we quotient by the equivalence relation outlined above.
(This is a slight fib -- it turns out we do often care about the monos themselves, especially when doing actual calculations. But I don't think this answer is a good place to get into such subtleties)
I hope this helps ^_^