Derivability conditions on Rosser's provability predicates.
Toshiyasu Arai · Notre Dame Journal of Formal Logic · 1990
This paper is complementary to a paper by Guaspari and Solovay.Let Ύh(x) denote a Σ t provability predicate 3yθ(y,x) for PRA (Primitive Recursive Arithmetic).We assume that formulas are in negation normal form, and hence -i-iφ is literally equal to φ for a formula φ.The symmetric form of Rosser's provability predicate Th R for Th is defined by Th R (Λr) :where -H denotes a function such that -ή r Φ~] = Γ -'Φ~I with the Gόdel number r Φ~* of φ.For a Canonical* provability predicate P for PRA, we construct Σι formulas Th 2 and Th 3 such that PRA proves yfx 9 y[F(x-^y) -* (F(x) ->F(y))], Vx[G(x) -> G( r G(x) n )] 9 and vx[P(x) ~1 = Γ Φ -> ψ n , F(x) :*=> Thf (JC), and G(ΛΓ) :« Th R (x).Let PRA (Primitive Recursive Arithmetic) denote the theory obtainable from PA (Peano Arithmetic formulated in a language containing function symbols for all primitive recursive functions) by restricting induction axioms to quantifierfree formulas.All results in this paper hold for any 1-consistent r.e.extension of PRA, but for the sake of definiteness we state results only for PRA.We will consider derivability conditions on the symmetric form of Rosser's provability predicates.Let P be a Σ?-formula, 3yθ(y 9 x), with θ quantifier-free.P is said to be a provability predicate (for PRA) if P numerates the theorems of PRA in PRA, i.e., P satisfies the following: DlVφ *=* \-P( Γ φ~]) for every formula φ 9where Vφ means that φ is derivable in PRA and r φ 1 is the Godel number of φ.Then the so-called symmetric form of Rosser's provability predicate P R for P is defined by: P R (x) : *=> 3y[θ(y,x) Λ\fMz -*θ(z 9 v))] *I would like to express my thanks to the referee for some valuable suggestions.