{"id":72,"date":"2017-02-05T19:19:23","date_gmt":"2017-02-05T18:19:23","guid":{"rendered":"http:\/\/owlofminerva.net\/kubota\/?p=72"},"modified":"2017-02-06T00:41:15","modified_gmt":"2017-02-05T23:41:15","slug":"photograph-with-peter-b-andrews-the-creator-of-the-logic-q0","status":"publish","type":"post","link":"https:\/\/owlofminerva.net\/kubota\/photograph-with-peter-b-andrews-the-creator-of-the-logic-q0\/","title":{"rendered":"Photograph with Peter B. Andrews, the Creator of the Logic Q0"},"content":{"rendered":"
<\/a>

Professor Peter B. Andrews and Ken Kubota (2010)
Foto Copyright \u00a9 2017 Ken Kubota<\/p><\/div>\n

The\u00a0picture above\u00a0with Peter B. Andrews and me\u00a0was made\u00a0on January\u00a014, 2010, at\u00a0Carnegie Mellon University in\u00a0Pittsburgh,\u00a0Pennsylvania\u00a0(USA). It is published first here in 2017.<\/p>\n

Professor Andrews is the creator of the higher-order logic Q0<\/span>, the leading mathematical system in terms of elegance\u00a0and expressiveness among the logistic systems\u00a0publicly 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).<\/p>\n

Andrews’ type theory\u00a0Q0<\/span> is further developed in my still unpublished logic and software implementation R0<\/span>, which has type variables and type abstraction allowing for dependent types. (Some excerpts are available online<\/a>.)<\/p>\n

For an overview about logics including Q0<\/span> and R0<\/span>, please see the\u00a0Foundations of Mathematics (Genealogy and Overview)<\/a>.<\/p>\n

I would like to thank\u00a0Peter for his kind permission to\u00a0place the picture on my homepage.<\/p>\n

Further Resources<\/h5>\n