I'm still new to logic and proving so bare with me, I'll try to keep it short. I wanna write this proof entirely in symbolic form for practice reasons.
Two main questions right now: Are both the actual proof and the alternative proof correct? And for the second alternative proof did I really have to rewrite the symbolism to include an exclusive disjunction for its statement, or could I have just used the original statement but still have exclusive disjunctions in the proof and yet be valid?
\emph{Declarative statement}: Between any two different rationals there is another rational.
Symbolic form: \begin{gather*} \forall k_0, k_1 \in \mathbb{Q}, \exists x \in \mathbb{Q} \enspace \vert \enspace [k_0 > k_1] \wedge [k_0 > x > k_1] \end{gather*}
Which reads as "For all rational numbers (k_0) and (k_1), where (k_0) is greater than (k_1) and x is between the two rationals (k_0) and (k_1)
\emph{Less redundancy and overall better proof}
Proof: \begin{align*} \forall k_0, k_1 \in \mathbb{Q}, [\frac{k_0}{2} + \frac{k_1}{2}] > (2\frac{k_1}{2}) \Rightarrow \frac{k_0 + k_1}{2} > k_1 \Rightarrow [\exists x \in \mathbb{Q} \enspace \vert \enspace (\frac{(k_0 + k_1)}{2} = x)] \Rightarrow k_0 > x > k_1 \Rightarrow \enspace \text{Thus,} \enspace x \enspace \text{is a rational that lays between \(k_0\) and \(k_1\)}. \end{align*}
Inner proof of claim that x is a rational: x is a rational since if (k_0 = \frac{m}{n}) and (k_1 = \frac{p}{q}), then (\frac{k_0 + k_1}{2} = \frac{m(q)+p(n)}{2\cdot nq})
Rewriting the symbolic form for an alternative proof (not needed):
Symbolic form: \begin{gather*} \forall k_0, k_1 \in \mathbb{Q}, \exists x \in \mathbb{Q} \enspace \vert \enspace [k_0 > k_1 \oplus k_1 > k_0] \wedge [k_0 > x > k_1 \oplus k_1 > x > k_0] \end{gather*}
\emph{Alternative (longer proof, same proof kind of but with exclusive disjunctions for practiec)}
\begin{align*} \forall k_0, k_1 \in \mathbb{Q}, [(\frac{k_0}{2} > \frac{k_1}{2}) \oplus (\frac{k_1}{2} > \frac{k_0}{2}) \wedge (k_0 \neq k_1)] \Rightarrow [\frac{k_0}{2} > \frac{k_1}{2}] \oplus [\frac{k_1}{2} > \frac{k_0}{2}] \Rightarrow [\frac{k_0}{2} + \frac{k_1}{2}] > (2\frac{k_0}{2}) \oplus (2\frac{k_1}{2}) \Rightarrow \frac{k_0 + k_1}{2} > k_0 \oplus k_1 \Rightarrow [\exists x \in \mathbb{Q} \enspace \vert \enspace (\frac{(k_0 + k_1)}{2} = x)] \Rightarrow [k_0 > x > k_1] \oplus [k_1 > x > k_0] \Rightarrow \enspace \text{Thus,} \enspace x \enspace \text{is a rational that lays between \(k_0\) and \(k_1\)}. \end{align*}
Inner proof of claim that x is a rational: x is a rational since if (k_0 = \frac{m}{n}) and (k_1 = \frac{p}{q}), then (\frac{k_0 + k_1}{2} = \frac{m(q)+p(n)}{2\cdot nq})