Much shorter proofs: A bimodal investigation

(*) g(pUz. P r f P A ( Z , rprPA(rP1)l)) < pz. P r f P A ( Z , ‘P1) * If g is rapidly increasing, we can express this result saying that PrpArpl has a much shorter proof (modulo 9 ) than p . This is based on the fact that (*) has only provable fixed points. In DE JONGH-MONTAGNA [2] and [3] the previous result is analyzed in a modal context. il characterization is given of pairs of modal formulas B p , C p such that for each arithmetical interpretation * and each provably recursive function g, if PRA t p* H ( n B p ) * <, ( o C p ) * , then PRA k p*. (If g is total recursive and increasing and p = 3x.pox, y = 3x.y0x (yo, yo E do) are 2,-formulas, then p Xg y means 3x.pox A Vy 5 gx . iyoy . The formalization of Vy 5 gx will be made precise later.)