How to efficiently read a predicate logic formula (best practices)

Question

This no question about how to understand a predicate logic proposition in general, it's about fast understanding such a proposition.

E.g. as a simple example, the convergence definition for $(a_n)_{n\in \mathbb{N}}$ with $a_n\in M$ (for all $n\in \mathbb{N}$ ; $M$ ordered ; e.g. $M=\mathbb{R}$ ) is

$\exists a\in M \forall \epsilon \in M_{>0} \exists N\in \mathbb{N} \forall n\in \mathbb{N}\colon n\ge N \implies |a_n -a|<\varepsilon $

When you read something like that (unknown to you): What is your approach?

So far, mine is the following:

Part 1: The part, that does include the quantifier declations. (e.g. "$\exists a\in M \forall \epsilon \in M_{>0} \exists N\in \mathbb{N} \forall n\in \mathbb{N}$"

Part 2: The part, that does not include the quantifier declrations. (e.g. "$n\ge N \implies |a_n -a|<\varepsilon $")

a) Directly read the formula as it is:

1. Look very shortliy at part 1 to get a short impression of the quantifiers (mostly to see what variables are used).

2. Read part 2.

3. Look closely to the part 1 again and read it carfully from right to left. While doing that, i look from time to time to part 2 again, to see how the read variable is used in context of part 2.

b) Transform the formula:

If the formula appears to be too "chaotic" for me, i transform it to an equivalent predicate logic propositions which composes of a declaration part (part 1) and a coresponding part (part 2). After that i do a).

My questions now are:

1. What is your approach/procedure to read a (new to you) formula efficiently?

2. Do you occasionally transform the formula in a better readable formula? And if yes: How do you transform (e.g. do you also separate the declaration part of the other part; do you write the discure universum conditions alltogether in the declaration part [e.g. short $\forall n \in \mathbb{N}\ge N$])?

Answer 1

The best solution to the problem is not to create the problem. Write formulas in a readable way. You might have to rewrite it yourself.

1) Don't use the variable "a" to refer to 2 different things. Avoid using $n/N/\mathbb N$ to refer to different things. Sometimes a convention helps, something like upper case for sets (and maybe sequences), lower case for primitive values.

2) Don't try to shove everything into 1 formula. Give different names to different concepts.

$$\exists l \in M~ \forall \varepsilon \in M_{>0} ~\exists k \in \mathbb{N} ~\forall j \in \mathbb{N} ~\colon~ j \ge k \implies |a_j - l|<\varepsilon$$

Break it up:

Eventuality: $E(a, P) = \exists k \in \mathbb N ~ \forall j \in \mathbb N ~:~ j \ge k \implies P(a_j)$ : "Eventually every value in a sequence has property P"

Boundedness : $B(a, l) = \forall \varepsilon \in M_{>0} ~:~ E(a, a_j \mapsto |a_j - l| < \varepsilon)$ : "For every deviation $\varepsilon$, (eventually every value in a sequence has property) that it is within $\varepsilon$ of L".

Existance : $F(a) = \exists l ~:~ B(a, l)$ : "There exists a limit L such that (for every deviation $\varepsilon$, (eventually every value in a sequence has property) that it is within $\varepsilon$ of L)"

You probably will have to start with the first part of the formula that makes sense, and go from there. It could be inside out, or left to right, or right to left.