I have a question concerning convergence and divergence of sequences in terms of notations from propositional calculus.
Suppose we have the following statements $P(x)$, $Q(y)$, with $\forall x
\exists y [P(x) \implies Q(y)] \equiv \forall x
\exists y [\neg P(x) \lor Q(y)]$ (1)
If we want to negate (1), we would have the following:
$\neg(\forall x
\exists y) [P(x) \implies Q(y)] \equiv \neg(\forall x
\exists y) [\neg P(x) \lor Q(y)]\equiv \exists x \forall y [P(x) \land \neg Q(y)]$ (2)
Now suppose we let $P(N,\epsilon):=n>N$ and $Q(N,\epsilon):= \mid x_{n}- l\mid < \epsilon$, and the definition of convergence is usually given in the form of (1), we have:
$\forall \epsilon > 0
\exists N>0 \forall n\in \mathbb{N} [n > N \implies \mid x_{n}- l\mid < \epsilon] \equiv \forall \epsilon > 0
\exists N>0 \forall n\in \mathbb{N} [\neg (n > N) \lor \mid x_{n}- l\mid < \epsilon]\equiv \forall \epsilon > 0
\exists N>0 \forall n\in \mathbb{N} [n \leq N \lor \mid x_{n}- l\mid < \epsilon]$ (3)
If we want to negate (3) along the lines of (2) to give the definition of divergene, won't it go as follows:
$\exists \epsilon > 0
\forall N>0 \exists n\in \mathbb{N} [\neg (\neg(n > N)) \land \mid x_{n}- l\mid \geq \epsilon] \equiv \exists \epsilon > 0
\forall N>0 \exists n\in \mathbb{N} [n > N \land \mid x_{n}- l\mid \geq \epsilon]$
Am I correct in my translation to propositional calculus notation. Thank you in advance.