basic functions
predicate 0BIT in sect 3.1
done with completeness
.
fixed other basic axioms
done first pass
done with arithmetic
done with soundness
Added the completeness proof sketch
down to 12 pages
Added 2 predicates in 4.1
graphs of basic functions
some graphs of basic functions
bit(l;x) function
basic function addition
added conclusion
intro revised (in progress)
added vl
Completeness: recursion step.
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