Re: "Proofs of life"
Rene Vestergaard <[email protected]> Fri, 9 Nov 2018 16:27:21 +0900
| Newsgroups | gmane.science.mathematics.logic.coq.club,gmane.science.mathematics.logic.isabelle.user,gmane.comp.mathematics.hol,gmane.science.mathematics.prooftheory |
|---|---|
| Message-ID | <[email protected]> |
I should have mentioned earlier that there's an accompanying video, with proof visualization and more: http://ceqea.sourceforge.net/extras/instructionalPoL.mp4 On 11/7/18 10:37 AM, Rene Vestergaard wrote: > "Proofs of life: molecular-biology reasoning simulates cell behaviors > from first principles" is now available at http://arxiv.org/abs/1811.02478 > > The work springs from computer-verified reasoning and establishes wider > utility by means of a reasoning-computation correspondence, including > for long-standing critical problems in biology that have defied standard > approaches. > > Sincerely, > Rene > > ----- > > ESSENCE > Mathematics-style correctness works for molecular biology and enables > phenotype and life-cycle prediction from genotypes. Formally, > reductionist science involves constructive reasoning, i.e., executable > simulation. > > SIGNIFICANCE > Axiomatic reasoning provides an alternative perspective that allows us > to address long-standing open problems in biology. Our approach is > supported by meta-theory and likely applies to any reductionist discipline. > > ABSTRACT > Science relies on external correctness: statistical analysis and > reproducibility, with ready applicability but inherent false > positives/negatives. Mathematics uses internal correctness: conclusions > must be established by detailed reasoning, with high confidence and deep > insights but not necessarily real-world significance. Here, we formalize > the molecular-biology reasoning style; establish that it constitutes an > executable first-principle theory of cell behaviors that admits > predictive technologies, with a range of correctness guarantees; and > show that we can fully account for the standard reference: Ptashne, A > Genetic Switch. Everything works for principled reasons and is presented > within an open-ended meta-theoretic framework that seemingly applies to > any reductionist discipline. The framework is adapted from a > century-long line of work on mathematical reasoning. The key step is to > not admit reasoning based on an external notion of truth but work only > with what can be justified from considered assumptions. For molecular > biology, the induced theory involves the concurrent running/interference > of molecule-coded elementary processes of physiology change over the > genome. The life cycle of the single-celled monograph organism is > predicted in molecular detail as the aggregate of the possible > sequentializations of the coded-for processes. The difficult question of > molecular coding, i.e., the specific means of gene regulation, is > addressed via a detailed modeling methodology. We establish a > complementary perspective on science, complete with a proven correctness > notion, and use it to make progress on long-standing and critical open > problems in biology.