-
Proof mining and probability theory
Authors:
Morenikeji Neri,
Nicholas Pischke
Abstract:
We extend the theoretical framework of proof mining by establishing general logical metatheorems that allow for the extraction of the computational content of theorems with prima facie "non-computational" proofs from probability theory, thereby unlocking a major branch of mathematics as a new area of application for these methods. Concretely, we devise proof-theoretically tame logical systems that…
▽ More
We extend the theoretical framework of proof mining by establishing general logical metatheorems that allow for the extraction of the computational content of theorems with prima facie "non-computational" proofs from probability theory, thereby unlocking a major branch of mathematics as a new area of application for these methods. Concretely, we devise proof-theoretically tame logical systems that, for one, allow for the formalization of proofs involving algebras of sets together with probability contents as well as associated Lebesgue integrals on them and which, for another, are amenable to proof-theoretic metatheorems in the style of proof mining that guarantee the extractability of effective and tame bounds from larges classes of ineffective existence proofs in probability theory. Moreover, these extractable bounds are guaranteed to be highly uniform in the sense that they will be independent of all parameters relating to the underlying probability space, particularly regarding events or measures of them. As such, these results, in particular, provide the first logical explanation for the success and the observed uniformities of the previous ad hoc case studies of proof mining in these areas and further illustrate their extent. Beyond these systems, we provide extensions for the proof-theoretically tame treatment of $σ$-algebras and associated probability measures using an intensional approach to infinite unions. Lastly, we establish a general proof-theoretic transfer principle that allows for the lift of quantitative information on a relationship between different modes of convergence for sequences of real numbers to sequences of random variables.
△ Less
Submitted 1 March, 2024;
originally announced March 2024.
-
Generalized Fejér monotone sequences and their finitary content
Authors:
Nicholas Pischke
Abstract:
We provide quantitative and abstract strong convergence results for sequences from a compact metric space satisfying a certain form of generalized Fejér monotonicity where (1) the metric can be replaced by a much more general type of function measuring distances (including, in particular, certain Bregman distances), (2) these distance functions are allowed to vary along the iteration and (3) full…
▽ More
We provide quantitative and abstract strong convergence results for sequences from a compact metric space satisfying a certain form of generalized Fejér monotonicity where (1) the metric can be replaced by a much more general type of function measuring distances (including, in particular, certain Bregman distances), (2) these distance functions are allowed to vary along the iteration and (3) full Fejér monotonicity is relaxed to a certain partial variant. To that end, the paper provides explicit and effective rates of metastability and even rates of convergence for such sequences, the latter under a regularity assumption that generalizes the notion of metric regularity introduced by Kohlenbach, López-Acedo and Nicolae, itself an abstract generalization of many regularity notions from the literature of nonlinear analysis.
In the second part of the paper, we apply the abstract quantitative results established in the first part to two algorithms: one algorithm for approximating zeros of maximally monotone and maximally $ρ$-comonotone operators in Hilbert spaces (in the sense of Combettes and Pennanen as well as Bauschke, Moursi and Wang) that incorporates inertia terms every other term and another algorithm for approximating zeros of monotone operators in Banach spaces (in the sense of Browder) that is only Fejér monotone w.r.t. a certain Bregman distance.
△ Less
Submitted 4 December, 2023;
originally announced December 2023.
-
In silico high-resolution whole lung model to predict the locally delivered dose of inhaled drugs
Authors:
Maximilian J. Grill,
Jonas Biehler,
Karl-Robert Wichmann,
David Rudlstorfer,
Maximilian Rixner,
Marie Brei,
Jakob Richter,
Joshua Bügel,
Nina Pischke,
Wolfgang A. Wall,
Kei W. Müller
Abstract:
The big crux with drug delivery to human lungs is that the delivered dose at the local site of action is unpredictable and very difficult to measure, even a posteriori. It is highly subject-specific as it depends on lung morphology, disease, breathing, and aerosol characteristics. Given these challenges, computational approaches have shown potential, but have so far failed due to fundamental metho…
▽ More
The big crux with drug delivery to human lungs is that the delivered dose at the local site of action is unpredictable and very difficult to measure, even a posteriori. It is highly subject-specific as it depends on lung morphology, disease, breathing, and aerosol characteristics. Given these challenges, computational approaches have shown potential, but have so far failed due to fundamental methodical limitations. We present and validate a novel in silico model that enables the subject-specific prediction of local aerosol deposition throughout the entire lung. Its unprecedented spatiotemporal resolution allows to track each aerosol particle anytime during the breathing cycle, anywhere in the complete system of conducting airways and the alveolar region. Predictions are shown to be in excellent agreement with in vivo SPECT/CT data for a healthy human cohort. We further showcase the model's capabilities to represent strong heterogeneities in diseased lungs by studying an IPF patient. Finally, high computational efficiency and automated model generation and calibration ensure readiness to be applied at scale. We envision our method not only to improve inhalation therapies by informing and accelerating all stages of (pre-)clinical drug and device development, but also as a more-than-equivalent alternative to nuclear imaging of the lungs.
△ Less
Submitted 11 July, 2023; v1 submitted 7 July, 2023;
originally announced July 2023.
-
Rates of convergence for the asymptotic behavior of second-order Cauchy problems
Authors:
Nicholas Pischke
Abstract:
We provide a quantitative version of a result due to Poffald and Reich on the asymptotic behavior of solutions of a second-order Cauchy problem generated by an accretive operator in the form of a rate of convergence. This quantitative result is then used to generalize a result of Xu on the asymptotic behavior of almost-orbits of the solution semigroup of a first-order Cauchy problem to this second…
▽ More
We provide a quantitative version of a result due to Poffald and Reich on the asymptotic behavior of solutions of a second-order Cauchy problem generated by an accretive operator in the form of a rate of convergence. This quantitative result is then used to generalize a result of Xu on the asymptotic behavior of almost-orbits of the solution semigroup of a first-order Cauchy problem to this second-order case.
△ Less
Submitted 17 April, 2023;
originally announced April 2023.
-
A proof-theoretic metatheorem for nonlinear semigroups generated by an accretive operator and applications
Authors:
Nicholas Pischke
Abstract:
We further develop the theoretical framework of proof mining, a program in mathematical logic that seeks to quantify and extract computational information from prima facie `non-computational' proofs from the mainstream literature. To that end, we establish logical metatheorems that allow for the treatment of proofs involving nonlinear semigroups generated by an accretive operator, structures which…
▽ More
We further develop the theoretical framework of proof mining, a program in mathematical logic that seeks to quantify and extract computational information from prima facie `non-computational' proofs from the mainstream literature. To that end, we establish logical metatheorems that allow for the treatment of proofs involving nonlinear semigroups generated by an accretive operator, structures which in particular arise in the study of the solutions and asymptotic behavior of partial differential equations. In that way, the here established metatheorems facilitate a theoretical basis for the application of methods from the proof mining program to the wide variety of mathematical results established in the context of that theory since the 1960's. We in particular illustrate the applicability of the new systems and their metatheorems introduced here by providing two case studies on two central results due to Reich and Plant, respectively, on the asymptotic behavior of said semigroups and the resolvents of their generators where we derive rates of convergence for the limits involved which are, moreover, polynomial in all data.
△ Less
Submitted 4 April, 2023;
originally announced April 2023.
-
On computational properties of Cauchy problems generated by accretive operators
Authors:
Pedro Pinto,
Nicholas Pischke
Abstract:
In this paper, we provide quantitative versions of results on the asymptotic behavior of nonlinear semigroups generated by an accretive operator due to O. Nevanlinna and S. Reich as well as H.-K. Xu. These results themselves rely on a particular assumption on the underlying operator introduced by A. Pazy under the name of `convergence condition'. Based on logical techniques from `proof mining', a…
▽ More
In this paper, we provide quantitative versions of results on the asymptotic behavior of nonlinear semigroups generated by an accretive operator due to O. Nevanlinna and S. Reich as well as H.-K. Xu. These results themselves rely on a particular assumption on the underlying operator introduced by A. Pazy under the name of `convergence condition'. Based on logical techniques from `proof mining', a subdiscipline of mathematical logic, we derive various notions of a `convergence condition with modulus' which provide quantitative information on this condition in different ways. These techniques then also facilitate the extraction of quantitative information on the convergence results of Nevanlinna and Reich as well as Xu, in particular also in the form of rates of convergence which depend on these moduli for the convergence condition.
△ Less
Submitted 11 October, 2023; v1 submitted 17 January, 2023;
originally announced January 2023.
-
Quantitative results on algorithms for zeros of differences of monotone operators in Hilbert space
Authors:
Nicholas Pischke
Abstract:
We provide quantitative information in the form of a rate of metastability in the sense of T. Tao and (under a metric regularity assumption) a rate of convergence for an algorithm approximating zeros of differences of maximally monotone operators due to A. Moudafi by using techniques from `proof mining', a subdiscipline of mathematical logic. For the rate of convergence, we provide an abstract and…
▽ More
We provide quantitative information in the form of a rate of metastability in the sense of T. Tao and (under a metric regularity assumption) a rate of convergence for an algorithm approximating zeros of differences of maximally monotone operators due to A. Moudafi by using techniques from `proof mining', a subdiscipline of mathematical logic. For the rate of convergence, we provide an abstract and general result on the construction of rates of convergence for quasi-Fejér monotone sequences with metric regularity assumptions, generalizing previous results for Fejér monotone sequences due to U. Kohlenbach, G. López-Acedo and A. Nicolae.
△ Less
Submitted 3 May, 2022;
originally announced May 2022.
-
Logical metatheorems for accretive and (generalized) monotone set-valued operators
Authors:
Nicholas Pischke
Abstract:
Accretive and monotone operator theory are central branches of nonlinear functional analysis and constitute the abstract study of set-valued map**s between function spaces. This paper deals with the computational properties of certain large classes of operators, namely accretive and (generalized) monotone set-valued ones. In particular, we develop (and extend) for this field the theoretical fram…
▽ More
Accretive and monotone operator theory are central branches of nonlinear functional analysis and constitute the abstract study of set-valued map**s between function spaces. This paper deals with the computational properties of certain large classes of operators, namely accretive and (generalized) monotone set-valued ones. In particular, we develop (and extend) for this field the theoretical framework of proof mining, a program in mathematical logic that seeks to extract computational information from prima facie `non-computational' proofs from the mainstream literature. To this end, we establish logical metatheorems that guarantee and quantify the computational content of theorems pertaining to accretive and (generalized) monotone set-valued operators. On one hand, our results unify a number of recent case studies, while they also provide characterizations of central analytical notions in terms of proof theoretic ones on the other, which provides a crucial perspective on needed quantitative assumptions in future applications of proof mining to these branches.
△ Less
Submitted 9 May, 2022; v1 submitted 3 May, 2022;
originally announced May 2022.
-
Quantitative analysis of a subgradient-type method for equilibrium problems
Authors:
Nicholas Pischke,
Ulrich Kohlenbach
Abstract:
We use techniques originating from the subdiscipline of mathematical logic called `proof mining' to provide rates of metastability and - under a metric regularity assumption - rates of convergence for a subgradient-type algorithm solving the equilibrium problem in convex optimization over fixed-point sets of firmly nonexpansive map**s. The algorithm is due to H. Iiduka and I. Yamada who in 2009…
▽ More
We use techniques originating from the subdiscipline of mathematical logic called `proof mining' to provide rates of metastability and - under a metric regularity assumption - rates of convergence for a subgradient-type algorithm solving the equilibrium problem in convex optimization over fixed-point sets of firmly nonexpansive map**s. The algorithm is due to H. Iiduka and I. Yamada who in 2009 gave a noneffective proof of its convergence. This case study illustrates the applicability of the logic-based abstract quantitative analysis of general forms of Fejér monotonicity as given by the second author in previous papers.
△ Less
Submitted 1 September, 2021; v1 submitted 16 August, 2020;
originally announced August 2020.
-
On Intermediate Justification Logics
Authors:
Nicholas Pischke
Abstract:
We study abstract intermediate justification logics, that is arbitrary intermediate propositional logics extended with a subset of specific axioms of (classical) justification logics. For these, we introduce various semantics by combining either Heyting algebras or Kripke frames with the usual semantic machinery used by Mkrtychev's, Fitting's or Lehmann's and Studer's models for classical justific…
▽ More
We study abstract intermediate justification logics, that is arbitrary intermediate propositional logics extended with a subset of specific axioms of (classical) justification logics. For these, we introduce various semantics by combining either Heyting algebras or Kripke frames with the usual semantic machinery used by Mkrtychev's, Fitting's or Lehmann's and Studer's models for classical justification logics. We prove unified completeness theorems for all intermediate justification logics and their corresponding semantics using a respective propositional completeness theorem of the underlying intermediate logic. Further, by a modification of a method of Fitting, we prove unified realization theorems for a large class of intermediate justification logics and accompanying intermediate modal logics.
△ Less
Submitted 16 August, 2020; v1 submitted 28 May, 2020;
originally announced May 2020.
-
Standard Gödel modal logics are not realized by Gödel justification logics
Authors:
Nicholas Pischke
Abstract:
We show that the standard Gödel modal logics, as initially introduced by Caicedo and Rodriguez in \cite{CR2009,CR2010}, are not realized by the basic Gödel justification logics although being related by the forgetful projection.
We show that the standard Gödel modal logics, as initially introduced by Caicedo and Rodriguez in \cite{CR2009,CR2010}, are not realized by the basic Gödel justification logics although being related by the forgetful projection.
△ Less
Submitted 10 July, 2019;
originally announced July 2019.
-
A note on strong axiomatization of Gödel Justification Logic
Authors:
Nicholas Pischke
Abstract:
Justification logics are special kinds of modal logics which provide a framework for reasoning about epistemic justifications. For this, they extend classical boolean propositional logic by a family of necessity-style modal operators "t:", indexed over t by a corresponding set of justification terms, which thus explicitly encode the justification for the necessity assertion in the syntax. With the…
▽ More
Justification logics are special kinds of modal logics which provide a framework for reasoning about epistemic justifications. For this, they extend classical boolean propositional logic by a family of necessity-style modal operators "t:", indexed over t by a corresponding set of justification terms, which thus explicitly encode the justification for the necessity assertion in the syntax. With these operators, one can therefore not only reason about modal effects on propositions but also about dynamics inside the justifications themselves. We replace this classical boolean base with Gödel logic, one of the three most prominent fuzzy logics, i.e. special instances of many-valued logics, taking values in the unit interval [0,1], which are intended to model inference under vagueness. We extend the canonical possible-world semantics for justification logic to this fuzzy realm by considering fuzzy accessibility- and evaluation-functions evaluated over the minimum t-norm and establish strong completeness theorems for various fuzzy analogies of prominent extensions for basic justification logic.
△ Less
Submitted 5 September, 2021; v1 submitted 25 September, 2018;
originally announced September 2018.
-
On Infinitary Gödel logics
Authors:
Nicholas Pischke
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-Ta…
▽ More
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].
△ Less
Submitted 5 September, 2021; v1 submitted 25 August, 2017;
originally announced August 2017.
-
A note on public announcements in standard Gödel modal logic
Authors:
Nicholas Pischke
Abstract:
We study public announcement operators in the context of standard Gödel modal logic as introduced by Caicedo and Rodriguez. Over that base logic, admitting a natural semantics over [0,1]-valued generalizations of modal Kripke models, we exhibit three possible semantic interpretations of the public announcement operator, all equivalent in a classical setting, and show that these logics are all diff…
▽ More
We study public announcement operators in the context of standard Gödel modal logic as introduced by Caicedo and Rodriguez. Over that base logic, admitting a natural semantics over [0,1]-valued generalizations of modal Kripke models, we exhibit three possible semantic interpretations of the public announcement operator, all equivalent in a classical setting, and show that these logics are all different in terms of expressive strength. We provide partial completeness results for these logics via Hilbert-style calculi.
△ Less
Submitted 13 December, 2021; v1 submitted 18 July, 2017;
originally announced July 2017.
-
Dynamic extensions for the logic of knowing why with public announcements of formulas
Authors:
Nicholas Pischke
Abstract:
In this paper, we address the logic of knowing why, an example of a non-standard epistemic logic dealing with justified knowledge via a new epistemic operator, under the extensions with ideas from dynamic epistemic logic, namely public announcements. Through the additional notions present in the knowing why context, we consider two possible variants, namely the extensions by (i): public announceme…
▽ More
In this paper, we address the logic of knowing why, an example of a non-standard epistemic logic dealing with justified knowledge via a new epistemic operator, under the extensions with ideas from dynamic epistemic logic, namely public announcements. Through the additional notions present in the knowing why context, we consider two possible variants, namely the extensions by (i): public announcements of a formula and by (ii): public announcements of reasons, although the deeper analysis of the latter is left for future work. We consider another logical operator, the conditional knowing-why operator, for which we study the applications to the axiomatization of public announcements as well as the solely framework. At the end, we consider the logical expressivity of these different logics in comparison to each other, and thus we show one of the main problems with the usual process of proving completeness through translation in the context of logics with public announcements.
△ Less
Submitted 20 September, 2018; v1 submitted 18 July, 2017;
originally announced July 2017.
