.
completed the list of Basic axioms, following Buss, in the appendix
Revised the definitions at the beginning of sect 4, and added after Def 14 a comment about B^i and integer positive formulas.
Modified lemma 19 on well-typed proofs, and gave a proof sketch.
Modified sequent calculus rules (weakening in axioms)
B^i sequent calculus
added polynomial induction definition
added the sequent calculus rules and a free-cut elimination theorem
witness functions
characteristic functions
predicative minimisation
corrected polynomial checking lemma
+ 1 reference
preliminaries: definitions PH
added in preliminaries the polychecking lemma
added definitions mubc
added basic template
added csl17 dir