Publisher Summary This chapter discusses the theory of F2 and the properties concerning ∞. The system of axiom schemes used for deduction theorem treats the resulting system with Gentzen techniques to obtain the proof of “Q-consistency.” This latter proof will involve the definition of a set of canonical obs or canobs, which have a rank on which an induction can be carried out to prove the elimination theorem. The methods of formulating the conditions on canonicalness within the system are considered and hence, replacing the axiom schemes by constant axioms. Then, inclusion of predicate calculus is treated. The objective is to formulate a set of axioms, preferably a small number of schemes from which will follow a deduction principle, which is a generalization of the deduction theorem of the ordinary logical calculus and thus, apply Gentzen techniques to the system.