Premium
Much shorter proofs: A bimodal investigation
Author(s) -
Carbone Alessandra,
Montagna Franco
Publication year - 1990
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19900360107
Subject(s) - mathematical proof , computer science , humanities , artificial intelligence , mathematics , philosophy , geometry
(*) 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.)