There is the following Mathematical Challenge Twenty-three

Mathematical Challenge Twenty-three: What are the Fundamental Laws of Biology?

* This question will remain front and center for the next 100 years. DARPA places this challenge last as finding these laws will undoubtedly require the mathematics developed in answering several of the questions listed above.

And I'm just wondering if there's such a mathematical field in which we can formalize and prove biological theorems.

  • $\begingroup$ Given that evolution selects for anything that works, I'm not sure what kind of non-trivial Fundamental Laws of Biology might exist or what "biological theorems" might be. $\endgroup$
    – Armand
    Oct 5 '21 at 6:29
  • $\begingroup$ @Armand I agree with your "evolution selects for anything that works" which in turns implies that biological events are fundamentally contingent and any possible mathematical formal theories must necessarily be of the nature of incompleteness. $\endgroup$
    – Nam Nguyen
    Oct 5 '21 at 7:09
  • $\begingroup$ However, I'm still holding out some hope that knowledge of biological processes could still be had by examining the proof life-cycle of a suspected biological theorem-statement B throughout an ordered sequence of formal theories: - Inception: When B is undecidable. - Conception: When B is provable (thus decidable) - Extinction: When ~B is provable (both B and ~B are decidable). However, all this is purely just a thought (a hope). $\endgroup$
    – Nam Nguyen
    Oct 5 '21 at 7:10

I think the question is too open to give a definitive answer, but several directiosn can be pointed out right away.

Laws of biology are not rigorous
Due to the inherent complexity of biological systems, the laws of biology are less susceptible to mathematical analysis than those in physics or chemistry. Firstly, this is because many of these laws are statistical in nature. Secondly, because there are too many parameters influencing a biological system to study the influence of each of them in a controlled way.

As an example one could give the Central dogma of molecular biology, which holds true for many organisms and serves as an important guiding principle, but doe snot obey in 100% of cases - e.g., it is violated by RNA viruses.

On the other hand, Mendel laws could be formulated in very rigorous mathematical terms, but quickly get obscured when we are dealing simultaneously with many genes and traits, and have to resort to statistical reasoning, see quantitative genetics.

Population genetics
Population genetics puts evolutionary study on a rigorous mathematical basis, and much of the developments are based on simple but powerful mathematical models. Here it si worth looking at Crow&Kimura's An Introduction to Population Genetics Theory,a nd also on the texts on the coalescent theory Gene Genealogies, Variation And Evolution: A Primer in Coalescent Theory and Coalescent theory: an introduction.

Physics of biological systems
Biophysics is a well-developed field, although it studies only specific aspects of biological systems. Good mathematically solid reference here is Keener and Sneyd, Mathematical Physiology: I Cellular physiology. See also this post for more discussion.

Finally, a more fundamental, but also more obscure view on the evolution and function of biological systems is from the point of view of spontaneous symmetry breaking and non-equilibrium thermodynamics, associated with the names of Phil Anderson, Ilya Prigogine and Erwin Schrödinger - you may find the list of references in this post.

  • $\begingroup$ Thanks for the answer and helpful information within. $\endgroup$
    – Nam Nguyen
    Oct 6 '21 at 7:33


Fwiw, I think the situation for the thread question and for the Mathematical Challenge Twenty-three is very bleak, hopeless: It's not possible even in theory (no pun intended) to formally theorize life processes in general — natural biological life on any planets, or ALIFE (Artificial Life, e.g. John Conway's Game of Life).

First of all, there's uncertainty of physical facts. For natural biological life, that's manifested by Heisenberg's Uncertainty Principle which would govern not only sub-atomic particle reactions but also macro biological life's evolution.

Take a particular asteroid for example. Its birth, formation, interstellar trajectory are all but a Karma-Fourier summation/superimposition (so to speak) of physical uncertainties — from the uneven distribution of energy and matter after the Big Bang, to the random matter expansion after the super nova of the first generation star, to the chaotic swirling birth of the second generation star system, all the way to "What did the dinosaurs see before the chicxulub impact ?".

Secondly, although mathematics doesn't have Heisenberg's Uncertainty Principle, it has the counterpart: Axiom of Choice. If two choice functions f1 and f2 exist in which Choice is necessary, it logically entails an uncertainty, non-determinateness on whether or not f1=f2, and truth non-determinateness is also alluded to in the following passage:

"We prove that the satisfaction relation of first-order logic is not absolute between models of set theory having the structure and the formulas all in common. Two models of set theory can have the same natural numbers, for example, and the same standard model of arithmetic, yet disagree on their theories of arithmetic truth".

The answer

So then, it's submitted in this answer, in so far as mathematics is the language of sciences, biology included, mathematical fundamental laws of biology and corresponding proofs are a tall order to accomplish.

However, it's also submitted here, there is a way forward.

As long as we're not naïve thinking that we're entitled know all biological laws – in full details – the way the Creator (Mother Nature?) does, we're endowed to be able to meta-mathematically formalize some kind of a categorization — a tree — of various FOL biological formal theories, and explore subsequent available pathways (branches) toward understanding a variety of different possible life forms, evolutions.

The meta-mathematical formalization of this categorization will still make use of the canonical definitions of FOL formal systems, theorems, provability thereof, but it also includes meta-proofs of syntactical undecidability as occasions arise.

In some details, the meta-mathematical formalization centers around:

  1. Relieving Plato/Tarski/Gödel semantical truths, interpretations of the duty of being valid in making mathematical inferences: There are no longer meaningful semantical truths — only facts of syntactical provability. Iow, the only truth of a formula (interpreted as "sentence" or not) is the fact of it being provable or not, syntactically decidable or not.
  2. A syntactical proof should be investigated in a context of a collection of relevant sets of axioms — not just one single axiom-set. Iow, a proof is only one instance in the set of proof-varieties (or formal-system varieties).

General Definitions

It's not feasible to detail all relevant definitions and proofs in one post so this answer might be a live post. But we can start with some definitions in the following sections.

Def-1 - Formal theories

A formal theory T (of an axiomatic formal system F) is the set of syntactical theorems of F closed under deduction via FOL rules of inference.


  • The language of T is denoted by L(T) which is L(F).
  • (Tf) ⇔ (Ff) [f being a formula written in L(T)].
  • In (Tf), if T is well-known or understood we can omit T and write (⊢ f).
  • proof(f) ⇔ (Tf), where T is understood.

It's trivial that given f is a formula, given any two T1, T2, and given the following set definitions

  • S1 = {f | (T1f) and (T2f)}
  • S2 = { f | undecide(T1f) and undecide(T2f) }

S1 and S2 exist, S1 is non-empty, while whether or not S2 is empty is contingent on the nature of both T1, T2.

Def-2a - Provability inheritance

If (For all proofs of B: proof(B) ⇒ proof(A)) then:

  • theorem A is an ancestor of theorem B: ancestor(A,B)
  • theorem B is a progeny of theorem A: progeny(A,B)
  • theorem B is genetically inherited from theorem A: inherit(A,B).

Def-2b - Provability base-pairing & nucleotides

Let _C1, _C2 be axioms in the following manner

  • _C1C11 ⋁ C12 ... ⋁ C1m
  • _C2C21 ⋁ C22 ... ⋁ C2n

where only one of C11, ..., C1m is provable, and only one of C21, ..., C2n is provable.

Without loss of generality, each of C11 and C1i is then undecidable, and so is each of C21 and C2j.

Consequently, the formula

(C1i ⋀ C2j)

is also undecidable, which we can use as a new axiom and in which case in turn the theorem (C1i ⋀ C2j) is called a provability base-paring where each of C1i, C2j is called complementary nucleotide of the other.

Def-3a - Formal theory addition — f.(T1 + T2)

Let T1, T2 be general, f be a particular formula.

f.(T1 + T2) = S1 union {f} — up to deductive closure, and fS2.

Def-3b - Formal theory multiplication — f.(T1 * T2)

Let T1, T2 be general, f be a particular formula.

f.(T1 * T2) = S1 union {f} — up to deductive closure, and where (undecide(T1 ⊢ f) xor undecide(T2 ⊢ f)).

Def-4 - Grothendieck-Multiverse (gM)

A Grothendieck-Multiverse, denoted by gM, is a non-empty collection of theories in each of which the provability of a formula f is evaluated: gM = { x | (x is a theory) and ((xf) xor neg(xf)) }.

A gM is also called an underlying provability realm (field) of all formulas written in a language L.

Def-5 - Contingency

The formula f is defined to be contingent when the followings are all satisfied:

  • f is not a logical theorem
  • neg({f} ⊢ ~(x=x)).

Proof-to-Truth homology/shadowing

Def-6 - Mathematical truth & falsehood

A mathematical truth is a quadruple (S,T,f,gM) defined per the followings:

  • S and NEG(S) are meta statements — written in natural language — with NEG(S) being the negation of S
  • T stands for TRUE
  • f is a FOL formula of which the provability S asserts
  • Exists(x):
    • TRUE(x ∈ gM)
    • TRUE(neg(x ⊢ ~(n=n))) [i.e., x is syntactically consistent]
    • TRUE(x ⊢ f).

A mathematical falsehood is similarly defined as (NEG(S),T,~f,gM), where (S,T,f,gM) is a mathematical truth.


  • If S is a meta-statement and TRUE(S), then where convenient,
    • S ⇔TRUE(S).
  • Similarly, if S is a meta-statement and TRUE(S) is false,
    • FALSE(S) ⇔ NEG(S) ⇔ NEG(TRUE(S)).

Provability-varieties — Proof lifecycle & extinction

Let f be an underlying formula, gW a Grothendieck multiverse that can be partitioned into the following three equivalence classes C1(f,gW), C2(f,gW), C3(f,gW):

  • C1(f,gW) = { x | (x ∈ gW) and undecide(x ⊢ f) }
  • C2(f,gW) = { x | (x ∈ gW) and decide(x ⊢ f) and neg(x ⊢ ~f)}
  • C3(f,gW) = { x | (x ∈ gW) and decide(x ⊢ f) and neg(x ⊢ f)}.


The set

{C1(f,gW), C2(f,gW), C3(f,gW)}

is called a proof (provability) life cycle relation R of f in gW, and is denoted by f(R(gW)), or f.R.gW or fRgW when convenient.


A triple


is called a life cycle of f in gW — i, j, k being pairwise distinct.


The triple


is called the natural life cycle of f in gW.

In this case,

  • C1(f,gW) is called the inception (of the proof of f) in the cycle
  • C2(f,gW) is called the conception (of the proof of f) in the cycle
  • C3(f,gW) is called the exception/extinction (of the proof of f) in the cycle
  • R is defined to be the underlying natural life cycle relation.


Given a natural life cycle relation fRgW that is unique in a gW, C3(f,gW) is defined to be a Chicxulub extinction, on (the provability of) f, and denoted by Chicxulub(C3(f,gW)), per the following:

Chicxulub(C3(f,gW)) ⇔ (Exists(C3(f,gW)) ⇒ (Choice is necessary)).

  • 1
    $\begingroup$ I think the problem is trying to reduce all of the biology to a simple set of axioms. Even in physics one does not do this. Moreover, in physics one often formulates the laws in axiomatic form, but describing real situations requires combining several laws, taking account for specific geometry, characteristic scales, etc. - none of which is axiomatic or predictable from the first principles. $\endgroup$ Oct 6 '21 at 8:40
  • $\begingroup$ I agree. Such problem of placing importance on the semantics of the individuals in the domain of discourse, imho, also occurs in FOL mathematics and the the remedies seem to be based on two techniques: axiom-schemas (e.g. PA's induction-schema axiom), and going to 2OL, HOL. My suggested answer is based on extending these two techniques a bit further: by going to meta level and inspecting possible homology (in functions, and relations) among related formal theories. $\endgroup$
    – Nam Nguyen
    Oct 6 '21 at 16:17
  • $\begingroup$ This, I think, would be in line with Grothendieck's universe (en.wikipedia.org/wiki/Grothendieck_universe) which is in essence a meta universe comprising of many FOL smaller universes (domains of discourse). $\endgroup$
    – Nam Nguyen
    Oct 6 '21 at 16:18

Not the answer you're looking for? Browse other questions tagged or ask your own question.