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…

## Syntactic Proofs of the Analytic Cut Property

An instance of the cut rule is called analytic if the cut formula already appears as a subformula of the lower sequent. For example, the cut is analytic because the cut formula is contained in . Analytic cut can be seen as a deep inference rule. In classical and modal logic it corresponds to a…

## Second-order-ish mathematics I

The English language uses the modifier “-ish” for “sort of”. A “sort of yellow” object is called “yellow-ish”. This post describes a class of third-order objects that are “sort of second-order”, i.e. second-order-ish. First of all, fix a function on the reals that is continuous everywhere and a real . A moment of thought reveals…