This question deals with the same topic as can be found here; Uniqueness of meets and joins in posets. However, I would like to show the result - that the join of two given elements is unique - using predicate logic, either through natural deduction or by semantic definitions (thus applying the soundness theorem to obtain the result). In order to so, it is necessary to axiomatize the definitions involved. A partial order is a set $A$ with a binary relation $\leq$ on it such that $\leq$ is reflexive, transitive and antisymmetric.
$$\phi_{1}=\forall x P(x,x)$$ $$\phi_{2}=\forall x \forall y \forall z (P(x,y) \to (P(y,z) \to P(x,z))$$ $$\phi_{3}= \forall x \forall y(P(x,y) \to(P(y,z) \to x\dot{=}y))$$
Now, what I want to do is to formalize the definition of join: If $\langle A; \leq;- \rangle$ is a partial order and $x,y,z \in A $ one say that $z$ is a join of x and y if for all $c \in A$ we have $z \leq c$ if and only if $x \leq c$ and $y \leq c$.
I have formalized it as follows: $$\psi=\exists zP(z,\hat{c}) \leftrightarrow \exists x \exists y(P(x,\hat{c}) \land P(y,\hat{c})$$
As I interpret it, the formalization reads: "There exists a $z$ such that $z \leq c$ if and only if $x \leq c$ and $y \leq c$. Note that $\hat{c}$ simply signals that $c$ is a constant, in fact arbitrary, and nothing else. However, I believe that this attempted formalization might be wrong, because when I seek to prove (derive) that $\{\phi_{1}, \phi_{2}, \phi_{3}\}\vdash \forall u \forall v ((\psi[u/z]\land \psi [v/z]) \to (u \dot{=} v))$, which ought to be the formalized version of the uniqueness of the join, I run in to trouble.
Your $\psi$ has only one free variable $\hat c$. Also $\psi$ is trivially true in this formulation (given $z$ with $P(z,\hat c)$, you can pick $x=y=z$ to obtain $P(x,\hat c)\land P(y,\hat c)$, for example; in fact from $\phi_1$ we immediately get $P(\hat c,\hat c )$ and hence $\exists zP(z,\hat c)$ etc.). Try to translate your formulation of "$z$ is a join of $x$ and $y$" again.