Resolving finite indeterminacy
Peter M. Schuster, Daniel Wessel · 2020
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.