Library Goedel.PRrepresentable

Original version by Russel O'Connor
This library is dedicated to the proof of the theorem: "Every primitive recursive function is representable in NN"
  • Let f be any n-ary arithmetic function, and p a proof that this function is primitive recursive. Out of p, we can associate a NN-formula which correctly expresses f.
  • The main difficulty is to associate a NN-formula to the case where f can be defined by a primitive recursive scheme. This is made possible with the help of Goedel's beta-function, studied in the ChineseRem library. This function allows to represent a sequence of computation steps through a first-order formula (theorem ChineseRem.BetaTheorem).


Theorem primRecRepresentable :
 ∀ (n : nat) (f : naryFunc n) (p : isPR n f),
 Representable n f (primRecFormula n (fun2PR f)).