I'm studying generalized inductive definitions and I got the following question; here, I use the "rule" definition of a g.i.d., instead of the monotone operator approach. So let $\Phi$ be a set of rules and suppose $\Phi$ is deterministic, i.e. if $(X, a), (X', a) \in \Phi$, then $X = X'$. Suppose further that $\Phi$ is finitary, i.e. if $(X, a) \in \Phi$, then $X$ is finite (this is not really necessary, but it will simplify things, including the definition of proof). Let $I(\Phi)$ be the least set closed under $\Phi$. Define a notion of $\Phi$-proof of $b$ as follows:
A sequence $a_1, \dots, a_n$ is a $\Phi$-proof of $b$ if: (i) $a_n = b$; (ii) for each $m \leq n$, there is $X \subseteq \{a_i \; | \; i < m\}$ such that $(X, a_m) \in \Phi$.
Feferman and Sieg ("Inductive Definitions and Subsystems of Analysis", p. 22) then claim the following: $\Phi$ is deterministic iff for each $b \in I(\Phi)$ there is a unique $\Phi$-proof. Let aside the existence claim, which I can take it for granted. My question is, given this definition of $\Phi$-proof, is this correct? It seems to me that we could have a deterministic $\Phi$, but still be able to concoct different $\Phi$-proofs for a given $b \in \Phi$ by inserting superfluous elements in a given $\Phi$-proof. For instance, suppose that there are two elements $a, b \in I(\Phi)$ such that $(\varnothing, a), (\varnothing, b) \in \Phi$. In that case, we would have at least two different $\Phi$-proofs for each of them, for instance $a$ and $b, a$ would be two different proofs for $a$.
In fact, this seems to be a general problem. If $a_1, \dots, a_n$ and $b_1, \dots, b_n$ are $\Phi$-proofs, then $a_1, \dots, a_n, b_1, \dots, b_n$ is also a $\Phi$-proof of $b_n$. So it seems that we can always produce different $\Phi$-proofs by concatenating $\Phi$-proofs.
Note that this is not exactly a problem for Feferman and Sieg, since they use a different notion of $\Phi$-proof based on well-founded trees, and I'm rather confident that the above problem does not arise for that notion. The notion of $\Phi$-proof defined above is Aczel's in his "An Introduction to Inductive Definitions" (cf. p. 742). So my question is: am I correct in arguing that the above equivalence fails if we work with Aczel's definition?
Related to this: If we introduce a further definition saying that a $\Phi$-proof of $b$ is minimal iff it is of minimal length (obviously, $b$ may have several minimal $\Phi$-proofs), I think it's possible to derive the implication: $\Phi$ deterministic $\rightarrow$ unique minimal $\Phi$-proof. But then the converse fails, I believe. Can anyone confirm this?
You are right that the equivalence fails under Aczel's definition: as you point out, you can insert irrelevant steps into one of Aczel's proofs. You may also be able to permute the order of the steps. If you put $$\Phi = \{(\emptyset, a), (\{b\}, a)\}$$ then $\Phi$ is not deterministic, but minimal $\Phi$-proofs are all unique (the second rule for constructing $a$ is unusable, but violates the definition of determinism).