Infinitely long proofs Take a proof to be a sequence (I'm working in Hilbert style system for simplicity). I have heard of infinitely long proofs. 
When we speak of infinitely long proofs, are we talking about proofs indexed by $\mathbb N$, or some other ordinal? Or perhaps uncountably long proofs? 
What kind of use can you think of for such proofs (especially proofs indexed by something larger than $\mathbb N$)?
EDIT: If we regard computations as derivations in some formal system, then an endless loop could be an example of an infinitely long derivation? But I think that's not an example of a derivation that needs to be indexed by something bigger than $\mathbb N$.
 A: For starters, you could prove Peano's Fifth Axiom, a.k.a. the Axiom of Induction.
A: It's actually vastly easier to view proofs as trees in this context, so I'll do that.
Generally, an "infinitely long proof" is more accurately a well-founded infinitely-branching tree (or something morally equivalent) - the idea being that we're working in some infinitary logic (or some logic of similar nature) where the basic deductive steps might involve infinitely many hypotheses. "Well-founded" means that the tree has no infinite paths, that is, no infinite regress: a node is "justified" by its immediate successors, with the root being the conclusion of the proof.
Now the point is that there is a notion associated to a well-founded tree which serves as a decent proxy for proof length - namely, the rank of the tree. Given a well-founded tree $T$, there is a unique function $\nu$ from the nodes of $T$ to the ordinals such that for each node $\alpha$ we have $$\nu(\alpha)=\sup\{\nu(\beta)+1: \alpha\prec \beta\}$$ (we take the supremum of the emptyset to be $0$, which means that $\nu(\alpha)=0$ for every terminal node $\alpha$). When we speak of the "length" of a proof in an infinitary system, this is what we (usually) mean. There are well-founded trees of arbitrary ordinal rank - while we generally are interested in at-most-countably-branching trees, which always have rank $<\omega_1$, we're not a priori limited to such.
As for their application, they show up in the study of infinitary logic in several ways (and Barwise's book has a good section on them) but they're also used to study classical first-order logic by replacing a complicated finitary system by an infinitary system which nonetheless has some better features; this happens with reasonable frequency in ordinal analysis, see e.g. here).
