Proofs whose length depends on the input

This may be a question from proof theory, but I'm not sure, since I don't know any proof theory. What I will be asking about is what happens, if the length of a proof isn't fixed: I'm going to present a structure of a proof, were this happens:

Suppose I have $n$ objects $O_1,\ldots,O_n$ which are related to oneanother by some relation $R$ (which is independent of the ordering of these objects) and I want to prove that I can replace these $n$ objects by some other $n$ objects $O'_1,\ldots,O'_n$ which satisfy the same relation $R$ and that the proof is structured in the following way:

First I prove that I can replace the first of the original objects with the new object, such that the $O'_1,O_2,\ldots,O_n$ thus obtained also satisfy $R$.

Then I argue, that in the course of obtaining $O'_1,O_2,\ldots,O_n$ from $O_1,\ldots,O_n$ I only used the fact that they satisfy $R$ and didn't use any of the properties a singular $O_i$ has. Thus this permits me to copy the first proof, where I got the sequence $O'_1,O_2,\ldots,O_n$ of objects and to replace (rename) them in the following way: $O'_1 \rightarrow O_2$, $O_2 \rightarrow O_3$,$\ldots$ ,$O_n \rightarrow O'_1$, i.e. $O'_1,O_2,\ldots,O_n$ becomes $O_2,\ldots,O_n,O'_1$ . This would then replace the first object in this sequence with a new one, so that I get the sequence $O'_2,O_3,\ldots,O_n,O'_1$.

Then I say say that "we repeat this process another $n-2$ times" to get $O'_n,O'_1,\ldots,O_{n-1}$ satisfying $R$, rearrange it to $O'_1,O_2,\ldots,O'_n$ and were done.

The problem I have with this proof is, that it's length depends on $n$, since at each step, at which I get myself a new object $O'_i$, I append a portion of text to the proof so far written down, which explains, how I get this new object in the sequence. This seems problematic to me, since I'm used to proofs having a fixed length - but the fact that the protion of text I'm appending to my proof is obtained in a totally mechanical/algorithmic way from the previous parts of text (only rename some symbols), is somewhat reassuring to me.

So I ask this: 1) Are proof like these allowed ? 2) If yes, what would happen if the proof wouldn't expand in a mechanical/algorithmic way, were only symbols have to be replaced before appending the new part of the proof (as explained above) ? (Whatever that would mean - this second question is more of a thought experiment.) 3) Is there a way to make this a fixed-length proof ?

-
There’s no problem: this is just a finite induction. – Brian M. Scott Dec 3 '12 at 22:43
Even to state the result involves a hidden induction, since the result refers to the symbols $O_1,...,O_n$. – coffeemath Dec 4 '12 at 2:15

You've uncovered the difference between a theorem and a theorem scheme. What you have here is a scheme with infinitely many theorems and infinitely many proofs, parametrized by the positive integer $n$. This does not guarantee that there is a single proof that covers all cases. Your argument uses external induction on $n$ to show that there is a proof for each positive integer $n$. The induction is called "external" because it is done in the meta-theory rather than in the theory itself. The theory you are working in might not even have positive integers and, even if it does, it might not be able to formalize this induction internally.

One often ignores the subtle difference between external and internal induction in everyday mathematics, but the difference becomes important in formal settings and such results can be very confounding. The Reflection Theorem in set theory is a prime example of this. This scheme says that for every formula $\phi(v_1,\dots,v_k)$ in the language of set theory the following is provable in ZFC:

For all sets $x_1,\dots,x_k$ if $\phi(x_1,\dots,x_k)$ is true then there is an ordinal $\alpha$ such that $x_1,\dots,x_k \in V_\alpha$ and $V_\alpha \vDash \phi(x_1,\dots,x_k)$.

Note that this is one theorem for each formula $\phi(v_1,\dots,v_k)$. One cannot prove in ZFC that:

For every formula $\phi(v_1,\dots,v_k)$ all sets $x_1,\dots,x_k$ if $\phi(x_1,\dots,x_k)$ is true then there is an ordinal $\alpha$ such that $x_1,\dots,x_k \in V_\alpha$ and $V_\alpha \vDash \phi(x_1,\dots,x_k)$.

Indeed, if this were true then every finite list of axioms of ZFC would be satisfiable and therefore, by the Compactness Theorem, ZFC would be satisfiable (and hence consistent). But we know that ZFC cannot prove its own consistency by Gödel's Incompleteness Theorem, so the reflection scheme cannot be internalized in ZFC even if ZFC can internalize most common uses of induction.

-
Excellent! This type of detailed and carefully put together answer is the reason I love math.SE! (And hate it, when people - with their imprecise manner - try to convince me that my question is trivial) – temo Dec 7 '12 at 18:06