A finite witness criterion for reflection

Assume agreement. A true existential in $D$ transfers to $C$, where its satisfaction provides $b\in C$ with ${\psi }^C(b,\bar{a})$. Since $\psi \in \mathrm{\Phi }$, agreement for the matrix transfers this to ${\psi }^D(b,\bar{a})$. This proves necessity.

Conversely assume the witness condition. Atomic equality and membership agree by restriction. Constructor induction (F1) gives agreement for negation and conjunction from agreement of their subformulas, since the Boolean truth tables are the same.

For an existential with parameters in $C$, a witness in $C$ for its truth in $C$ satisfies the matrix in $D$ by induction, so also witnesses truth in $D$. If it is true in $D$, the stipulated witness condition gives $b\in C$ satisfying the matrix in $D$, and induction transfers the matrix to $C$. Thus the existential agrees in both directions. Subformula closure licenses each invocation of induction. This proves sufficiency and the equivalence; the finite class version uses the same fixed list of relativizations.