I was thinking how I could interpret the epsilon-delta definition of limits so that it could be done using more symbols rather than natural language. I'm not sure if this formulation of the definition of adequate, but I will try to explain my thought-process. Is this formulation of the epsilon-delta definition of limits consistent with how most people use the definition? If not, what can I improve?
We are required to have $\epsilon >0$, so I include in such a way that it can be done for a primary subderivation. Then, we cannot just have by magic a $\delta$, so I make sure that it either derives from $\epsilon$ or at least derived in a 'proper' way. Then we have the part where I am most concerned: the quantified statement. So I try to make everything nice and tidy for the secondary subderivation, and I have a pair of mutually redundant statements, the second and third conjuncts in the antecedent, but include them anyways, because if someone wanted to derive them formally, I save them the effort. Then we have the expected part in the consequent.
I apologize if I sound like I have no idea what I'm doing, for that is mostly true. I acknowledge that conjuncts could be neatly organized in more brackets, to make it more formal but I decided against that.
For fun, let's workshop this a little. The following is a definition of a limit, including natural language:
If we truly want to make this self-contained, we probably should symbolically define what it means to be an open interval, and what it means to be a function between two sets.
A set $I$ is a non-empty bounded open interval if there exist $a, b \in \Bbb{R}$ such that $a < b$ and $x \in I \iff a < x < b$. As a daunting string of symbols, we mean $$(\exists a, b \in \Bbb{R})(a < b \land (\forall x \in \Bbb{R})(x \in I \iff a < x < b)).$$
A set $f$ is a function from $A$ to $B$ if it is a relation (i.e. $f \subseteq A \times B$) such that, for all $x \in A$, there exists a unique $y \in B$ such that $(a, b) \in f$ (we say $f(a) = b$ for short). In symbols, $f : I \setminus \{c\} \to \Bbb{R}$ is a function if $$(f \subseteq (I \setminus \{c\}) \times \Bbb{R}) \land (\forall x \in I \setminus \{c\})(\exists y \in \Bbb{R})(\forall y' \in \Bbb{R})((x, y) \in f \land ((x, y')\in f \implies y'=y)).$$
So, with this in mind, the way I'd express this purely symbolically is with the following nightmare of symbols:
\begin{align*} &(\forall c \in \Bbb{R})(\forall I \in \mathcal{P}(\Bbb{R}))(\forall f \subseteq (I \setminus \{c\}) \times\Bbb{R})(\forall L \in \Bbb{R}) \\ &\Bigg(\bigg((\exists a, b \in \Bbb{R})(a < b \land (\forall x \in \Bbb{R})(x \in I \iff a < x < b)) \land \, \\ &(\forall x \in I \setminus \{c\})(\exists y \in \Bbb{R})(\forall y' \in \Bbb{R})((x, y) \in f \land ((x, y')\in f \implies y'=y))\bigg) \\ &\implies\bigg(\lim_{x \to c} f(x) = L \iff (\forall \varepsilon > 0)(\exists \delta > 0)(\forall x \in I \setminus \{c\}) \\ &(|x - c| < \delta \implies |f(x) - f(c)| < \varepsilon)\bigg)\Bigg), \end{align*} where $\mathcal{P}(\Bbb{R})$ is how I'm notating the power set.
Note that things like the power set and the subset relation, despite being symbols, could also be broken down further too, e.g. $A \subseteq B$ is defined to be $x \in A \implies x \in B$.
(Note: it's probable that I've made an error somewhere, possibly just mismatched parentheses, possibly something more grave. If you spot it, feel free to edit this answer.
$^*$ Boundedness is only included to make the definition a little easier to write symbolically. The same definition would work for any open interval containing $c$ (or any set containing an open interval containing $c$, or any set which has $c$ as an accumulation point). Indeed, this is one of the downsides of being so precise: you lose some flexibility in the definition.