Professor Peter B. Andrews and Ken Kubota (2010)
Foto Copyright © 2017 Ken Kubota

The picture above with Peter B. Andrews and me was made on January 14, 2010, at Carnegie Mellon University in Pittsburgh, Pennsylvania (USA). It is published first here in 2017.

Professor Andrews is the creator of the higher-order logic Q0, the leading mathematical system in terms of elegance and expressiveness among the logistic systems publicly available as of today. Formal logic and most of mathematics can be expressed in it in a very natural way, on the basis of two primitive symbols only (identity/equality and its counterpart, description).

Andrews’ type theory Q0 is further developed in my still unpublished logic and software implementation R0, which has type variables and type abstraction allowing for dependent types. (Some excerpts are available online.)

For an overview about logics including Q0 and R0, please see the Foundations of Mathematics (Genealogy and Overview).

I would like to thank Peter for his kind permission to place the picture on my homepage.

Further Resources