Motivated by recent applications of proof theory in probability, we introduce a novel computational interpretation of probabilistic $$\exists \forall $$ -formulas, called dependent learnability. This encompasses several important notions of quantitative stochastic convergence, where it represents a generalized version of the property – widely studied in probability and ergodic theory – that a sequence of random variables has bounded fluctuations. We study both deterministic and stochastic variants of this notion and relate these to other computational interpretations of $$\exists \forall $$ -formulas from the literature. In particular, we prove dependent learnability to be primitive recursively equivalent to the influential notion of metastability, which in conjunction with results from applied proof theory highlights that dependently learnable rates can be extracted from large classes of nonconstructive proofs of $$\exists \forall $$ -formulas. Furthermore, we present a primitive recursive algorithm for joining two (and thus finitely many) dependently learnable rates, which in particular proves to be considerably more mathematically intuitive than the corresponding functional for joining rates of metastability. Finally, we discuss our results in the light of game semantics.

Abstract We discuss the logical principle of extensionality for set-valued operators and its relation to mathematical notions of continuity for these operators in the context of systems of finite types as used in proof mining. Concretely, we initially exhibit an issue that arises with treating full extensionality in the context of the prevalent intensional approach to set-valued operators in such systems. Motivated by these issues, we discuss a range of useful fragments of this full extensionality statement where these issues are avoided and discuss their interrelations. Further, we study the continuity principles associated with these fragments of extensionality and show how they can be introduced in the logical systems via a collection of axioms that do not contribute to the growth of extractable bounds from proofs. In particular, we place an emphasis on a variant of extensionality and continuity formulated using the Hausdorff-metric and, in the course of our discussion, we in particular employ a tame treatment of suprema over bounded sets developed by the author in previous work to provide the first proof-theoretically tame treatment of the Hausdorff metric in systems geared for proof mining. To illustrate the applicability of these treatments for the extraction of quantitative information from proofs, we provide an application of proof mining to the Mann iteration of set-valued mappings which are nonexpansive w.r.t. the Hausdorff metric and extract highly uniform and effective quantitative information on the convergence of that method.

Abstract We study propositional and first-order Gödel logics over infinitary languages, which are motivated semantically by corresponding interpretations into the unit interval $[0,1]$. We provide infinitary Hilbert-style calculi for the particular (propositional and first-order) cases with con-/disjunctions of countable length and prove corresponding completeness theorems by extending the usual Lindenbaum–Tarski construction to the infinitary case for a respective algebraic semantics via complete linear Heyting algebras. We provide infinitary hypersequent calculi and prove corresponding cut-elimination theorems in the Schütte–Tait style. Initial observations are made regarding truth-value sets other than $[0,1]$.