  More than half a century has passed with no constructive proof of the consistency of full second-order arithmetic in sight. Early pioneers  in this field included Kurt Schütte and Gaisi Takeuti. The  former created in 1951 an infinitary sequent calculus to present  consistency proofs in a perspicuous way, the latter instead used a  more traditional Gentzen-style calculus (see Takeuti 1987).