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 ?