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…
Countable sets in the wild
TL;DR: there are various definitions of the notion ‘countable set of reals’ and only one seems to lead to nice equivalences in Reverse Mathematics. In particular, injections and bijections to the naturals à la Cantor are not very suitable. A slightly more general notion leads to many equivalences involving regulated and bounded variation functions, as…