Peter B. Andrews, an American mathematician and Professor Emeritus at Carnegie Mellon University, passed away on April 21, 2025, at the age of 87. Andrews was a leading figure in the theory and applications of higher-order logic and automated reasoning. Peter Andrews received his Ph.D. in Mathematics from Princeton University in 1964, where he was…
Exponentials vs fixed points in linear logic
It has been known for a while that the exponential modalities of linear logic may be simulated by least and greatest fixed point operators. However it is apparently not widely known whether this simulation was faithful. In this post we explain that this is not the case, using only first principles of linear logic.
A note on conservativity in constructive modal logics
This short post is a follow-up to Sonia and Anupam’s blog post on constructive modal logics; I present a quick direct proof that the constructive modal logic is conservative over on the -free fragment. This was first discussed in the comment section to the aforementioned blog post (as an open problem), and eventually obtained in…
A question from a colleague about non-well-founded proofs
The following explanation was given to a math colleague concerning nonstandard models: if Con(PA) fails in a non-standard model, it means it contains a“proof of non-standard length” of a contradiction from PA. With alittle work, one can externalise that to some non-well-founded “prooftree”, which has at each node a possibly-non-standard formula (whichin turn externalises to…