Infinitely long formulas Formulas in predicate logic cannot be infinitely long, or so I have been told.
But I don't understand how this can be the case.
For we can disjoin $A \lor A \lor A \lor...$ indefinitely.
Isn't this an infinitely long formula?
Is the idea that formulas can only be countably infinite, and that even with such a long formula it is only countably infinite? 
How would one prove that formulas in predicate logic can only be such?

Edit
Answers along the lines of "formulas are defined to be of finite length" I find unsatisfying, for the following reason: the rule for forming disjunctions doesn't say that we can't go on to form $A \lor A \lor...$. If it did a disjunction would be defined as something which can only be of length $n$ for some $n$. So I fail to see how Asaf's answer answers my question.

I think the import of the answer is that it is a precondition of something being a formula in standard predicate logic that it be of finite length. Then when recursive rules are stated, it is simply a precondition that they can't go on expanding forever $A \lor A...$. 
But this raises the question, could one instead simply state that they can't go on forever for each recursive rule?
One would have then
"If $θ$ and $ψ$ are formulas of $ℒ1K=$, then so is $(θ\land ψ)$, so long as the length of $(θ\land ψ)$ is less than $n$, for some $n \in \mathbb{N}$" 
 A: It's not that you can't, it's just that the standard definition of predicate logic requires formulas (and proofs) to have finite length.
There are infinitary logics where you can have infinite conjunctions and disjunctions, or infinitely many quantifiers. And that all works out fine. But once you move from the "finite realm", set theory starts playing a much more significant role. Which makes things far more complicated (for example, the compactness and completeness theorems no longer hold in general).
A: In a comment to Asaf you write,

Take the inductive definition of formula-hood in plato.stanford.edu/entries/logic-classical. Where does it state or imply that a formula may only be finite? Nowhere seemingly. Or it must be implicit in something that I am not seeing.

Finiteness is implicit there - in the precise meaning of "inductive definition!"
The inductive definition basically says, "The set $Form$ is the smallest set containing [stuff] and closed under [operations]." (Another way this is phrased is in three clauses, with the last being "and nothing is in $Form$ if it is not required to be by the previous clauses, but this is less precise.) A formula is then an element of $Form$. 
The point is that since these operations and starting formulas are finitary, we never get infinitely long expressions in $Form$. Specifically, what you need to convince yourself of is:

The class of finitely long formulas satisfies the closure properties in the definition.

This exactly says that nothing else is a formula.  And the fact that this closure holds is because the "basic operations" of formula-forming are finitary.

It might help to consider a simpler inductive definition first: $\mathbb{N}$ is the smallest set containing $0$ and closed under $a\mapsto a+1$. Now there's nothing in this definition explicitly excluding $\pi$ from being a natural number ... except for that word "smallest." This is the essence of inductive definability.
A: Just because you can indefinitely disjunct yet another term to your ever-growing disjunction does not mean that you ever reach an infinitely long disjunction, just as much as you never get to an infinite number just by adding $1$ to an ever-growing number.
Indeed, by induction over the recursive ddefinition of expressions you can easily prove that every statement has to be of finite length:
Base: every atomic statement like $A$ or $B$ is of finite length
Step: if $\varphi$ and $\psi$ are of finite length, then $\varphi \lor \psi$ is of finite length as well (and same for the other operators)
A: Let's assume your "infinite disjunction", $A\lor A\lor A\lor \cdots$, is right associated so we have $A\lor (A \lor \cdots)$. As you state (e.g. quoting https://plato.stanford.edu/entries/logic-classical/): For formulas $\varphi$ and $\psi$, we can form the formula $\varphi\lor\psi$. To prove that $A\lor(A\lor\cdots)$ is a formula we need to show that it is of the form of $\varphi\lor\psi$ for formulas $\varphi$ and $\psi$. Clearly, we can set $\varphi=A$, and $A$ is an (atomic) formula. We then have to show that $\psi=A\lor\cdots$ is a formula. We can again immediately show that the left hand side is a(n atomic) formula but the right hand side is $\cdots$ which is certainly not a formula. Oh, but you meant $\cdots$ to mean "indefinitely disjoining $A$". Well, okay, then you just will never get to the point where you can definitively state that $A\lor\cdots$ is a formula and thus that we're allowed to call $A\lor(A\lor\cdots)$ a formula. That is, we never get to a point where we can show that there actually is a formula corresponding to $\psi=A\lor\cdots$.
This is the informal (and also philosophical) argument that formulas (and many other inductively defined structures) are finite. There are two distinct ways of formalizing this that are equivalent in typical foundations but separate in weaker foundations. First, we can define the set of formulas to be the smallest set that's closed under the given formation rules. In this case, the set of all finite formulas is certainly included and is closed under the formation rules. Even if our meta-theory allowed sets that contained infinite objects formed by the rules, any set that was closed under the rules and contained those infinite objects would be larger (i.e. a superset of) the set that only contained the finite objects. (This is the purpose of rule 8, "That's all folks", from the aforementioned link.) A second approach to formalization is akin to the approach in your edit. You define a notion of "simpler" formulas, say formulas with depth less than $n$ for some given natural $n$, and you define formulas by stages. You say formulas of depth $n$ are formulas built from formulas of at most depth $m<n$. You then can define the set of all formulas as the union of formulas of depth $n$ for all $n\in\mathbb N$. (We can easily avoid set-theoretic talk at all, e.g. formula this in PRA if we want.
A: No, a formula is defined inductively, that is, via some finite sequence of the rules allowed by your language. It's sort of like the idea that a natural number can't be infinitely long -- even if you can always tack on another digit to the beginning to get another natural number, if you go on forever, you will end up with something that is not a natural number. In this case, if you take $A \lor A \lor A \lor \dots$, the result will not be considered a formula in your language. But if you change the underlying language, you can take something like $\bigvee_{k \in \mathbb{N}} A$, to be a formula, which seems to intuitively be what you want.
