Talk: Peter Schuster (Verona)
Resolving Finite Indeterminacy. A Definitive Constructive Universal Prime Ideal Theorem
Joint work with Daniel Wessel
Dynamical proofs were designed to eliminate the ideal objects abstract algebra abounds with. Typically those ideal objects are granted by an incarnation of Zorn's Lemma and help to prove the semantic conservation of additional non-deterministic sequents, that is, with finite but not necessarily singleton succedents. This elimination was possible because algebra is predominated by coherent or first-order geometric theories, for which Barr's Theorem ensures constructivity in principle. In fact, every invocation of a non-deterministic axiom can be captured by a finite branching of the proof tree, and coherent logic lends naturally itself to automated theorem proving.
Incidentally, a paradigmatic case of using ideal objects had widely been neglected in dynamical algebra until recently: Krull's Lemma for prime ideals. This lack indeed emerged only from Kemper and Yengui's novel characterisation of the valuative dimension. Digging deeper just about that case, which we next settled in collaboration with Yengui, we then managed to unearth the underlying general phenomenon: For every concrete 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 the fairly universal setting of a consequence relation enriched with non-deterministic axioms; uniformises most if not all of the known instances of the dynamical method; generalises the proof-theoretic conservation criterion that we have offered with Rinaldi; complements the avenue to Krull's Lemma via proof mining we have initiated with Powell and Wiesnet; and last but not least offers a link between the syntactical and 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.