Resolving finite indeterminacy

Dynamical methods were designed to eliminate the ideal objects abstract algebra abounds with. Typically granted by an incarnation of Zorn's Lemma, those ideal objects often serve for proving the semantic conservation of additional non-deterministic sequents, that is, with finite but not necessarily singleton succedents. Eliminating ideal objects dynamically was possible also because (finitary) coherent or geometric logic predominates in that area: the use of a non-deterministic axiom can be captured by a finite branching of the proof tree. Incidentally, a paradigmatic case has widely been neglected in dynamical algebra: Krull's Lemma for prime ideals. Digging deeper just about that case, which we have dealt with only recently (with Yengui), has now brought us to unearth the general phenomenon underlying dynamical algebra: Given a claim of computational nature that usually is proved by the semantic conservation of certain additional non-deterministic axioms, there is a finite labelled tree belonging to a suitable inductively generated class which tree encodes the desired computation. Our characterisation works in the fairly universal setting of a consequence relation enriched with non-deterministic axioms; uniformises many of the known instances of the dynamical method; generalises the proof-theoretic conservation criterion we have offered before (with Rinaldi); and last but not least links the syntactical with the semantic approach: every ideal object used for the customary proof of a concrete claim can be approximated by one of the corresponding tree's branches.