Question regarding translating English into first-order logic Someone asked this question: "A language $L$ that is regular will have
the following property: there will be some number $N$ (that depends on $L$) such that if $s$ is a string in $L$ (a $string$ is a sequence of characters) whose length is at least $N$ then $s$ can be written as $xyz$ where $y$ is not the empty string and $xy^iz$ is in the language $L$ for every nonnegative integer $i$."
Translating English into First Order Logic
My question how would one even translate that into first order logic? The user started writing out his attempted approach. But I couldn't quite follow it so I was wondering how one could even write such statements in first order logic. I looked into pumping lemma as one of the comments suggested but it didn't help me much. It got me slightly more confused.
P.S. I'm sorry if I broke any rules in stating this question. I'm new to the site.
 A: Why do we ever bother to translate bits of mathematical English into the symbolism of first-order logic?
Primarily because the quantifier-variable plus connectives representation of statements is wonderfully clear and non-ambiguous about logical structure. Careless or sloppy vernacular talk may fail to distinguish between the propositions represented by $P \lor (Q \land R)$ and $(P \lor Q) \land R$ [Recall the ambiguous invitation: "Bring your partner or come alone and have a good time!"]. Logical notation forces us to distinguish, as it also forces us to distinguish $\forall x \neg Px$ and $\neg\forall xPx$ [compare the ambiguous "Everyone has not yet arrived"], and to distinguish $\forall x\exists yRxy$ and $\exists y\forall xRxy$, and so on and so forth. 
So the key thing in rendering statements of mathematical English into the notation of first-order logic is to do enough to make logical structure perspicuous (in particular do enough to reveal the scope of various logical operators, i.e. to reveal just which bits of the proposition they govern). In this case, the statement after the colon has something like this sort of logical shape
$$\exists n\forall s[l(s)\geq n \to \exists x\exists y\exists z(s =  x^{\cap}y^{\cap}z \land y \neq 0 \land \forall i\,x^{\cap}y^i{}^{\cap}z \in L )]$$
if we take the quantifiers to be implicitly appropriately sorted so $s, x, y, z$ run over $L$-strings, and $n$ and $i$ over non-negative numbers (and where ${}^{\cap}$ is concatenation). The further finer details (e.g. whether you choose to explicitly type the variables by writing e.g. $\forall x \in L$ where $L$ is the set of $L$-strings) won't matter -- in most contexts -- so much as revealing the overall quantificational structure and scope dependencies.
I hope this helps ...
