Here is a quote from Spivak's Calculus:
If $\lim\limits_{x \to a} f(x)$ exists and is $\neq f(a)$, then $f$ is
said to have a removable discontinuity.
It appeared in a problem, not in the main text. It seems to be a definition. I believe it can also be written as a biconditional:
$$\exists \lim\limits_{x \to a} f(x) \neq f(a) \iff\ f \text{ has a removable discontinuity at } a\tag{1}$$
In another problem, we are asked to prove that a particular function never has a removable discontinuity.
My proof assumed the antecedent $\exists \lim\limits_{x \to a} f(x) \neq f(a)$, and used a proof by cases to show that a contradiction is obtained in all cases. Thus, I concluded that the negation of the antecedent is true, and hence that the negation of the consequent is true.
In other words, I concluded that:
$$\lnot (\exists \lim\limits_{x \to a} f(x) \neq f(a))\tag{2}$$
Therefore
$$\lnot (f \text{ has a removable discontinuity at } a)\tag{3}$$
Negating the entire antecedent is good enough for me to conclude that "for all $a$ f never has a removable discontinuity at $a$".
However, my question is about what exactly the negated antecedent is in terms of first-order logic. What is $(2)$, in very precise terms, ie in a way that is correct in a formal first-order logic sense?
The antecedent of $(1)$ itself doesn't seem precise. Should it be
$$(\exists \lim\limits_{x \to a} f(x)) \land (\lim\limits_{x \to a} f(x) \neq f(a))$$
But then when we negate this we get
$$(\nexists \lim\limits_{x \to a} f(x)) \lor (\lim\limits_{x \to a} f(x) = f(a))$$
Seems like the two conjuncts are linked in a way that makes the disjunction feel funny.
Best Answer
The negation of $f$ having a removable discontinuity at $a$ is that either $f$ does not have a limit at $a$ or $f$ is continuous at $a$. The so-called "link" you speak of is that these conditions are mutually exclusive.