I am trying to symbolize the following definition of a Cauchy Sequence with the syntax of predicate logic. Can someone please take a look and tell me if I am symbolizing the definition correctly according to the syntax of predicate logic?
Definition: "The sequence $\{a_n\}$ is a Cauchy Sequence if for all $\epsilon > 0$, there exists a number $Z$ such that $m,n > Z \implies |a_m -a_n| < \epsilon$."
I came up with the following symbolization key:
UD: The set of all sequences, terms of sequences and real numbers.
$Sx$: x is a sequence
$Tx,y$: x is a real number term of y
$Nx$: x is a natural number
$Rx$: x is a real number
$Gx,y$: x is greater than y
$Lx,y$: x is less than y
$A_x$: |x|
$Cx$: x is a Cauchy Sequence
$0$: $0$ as a constant
Using the key above, here is my attempt at symbolizing it into predicate logic syntax:
$(\forall s)(\forall a)(\forall n)(\forall m)[((Ss \wedge Ta,s) \wedge (Nn \wedge Nm) ) \wedge ((\forall \epsilon)(\exists z)[((G\epsilon,0 \wedge Rz) \wedge (Gmz \wedge Gnz)) \implies LA_{a_m-a_n}, \epsilon]) \Leftrightarrow Cs]$
Would my symbolized sentence be a correct interpretation of the definition of a Cauchy Sequence?