ABSTRACT
The nominalism that motivates ITT is similar in some respects to the views expressed by Martin-Lof in the introduction to [96] and developed into the logic of [97] also described by Beeson in [17]. It is therefore appropriate to consider an intuitionist formulation of ITT
A sequent calculus version ELG [EL Gentzen] of the classical elementary logic EL is described in §1.7.6. As noted in §1.7.7, Gentzen described in [52] sequent calculus formulations of both classical and intuitionist first order logic, the latter as formalized by Heyting in [77]. The intuitionist sequent calculus results from the classical by restricting each sequent in a derivation to having at most one formula in its succedent. These formulations of first order logic can also be found in [88] and in [144]. Looked at from this point of view intuitionist logic can be seen to be a restricted form of the classical. But conversely, results are proved in [88] that provide formulations of classical first order logic as a sublogic of intuitionist logic.
