<p class="font_8">"Proofs in mathematics often have a narrative quality to them, taking the reader on a long journey. Sometimes the reader has to wait for new mathematical characters (like imaginary numbers) to be created so the journey can be continued. Hilbert called these novel characters ideal elements. His conservation program was the idea that, while being important for the advancement of mathematics, ideal elements should be eliminable from proofs of concrete mathematical theorems. Investigations by a long list of mathematicians/logicians (e.g. Weyl, Hilbert, Bernays, Lorenzen, Takeuti, Feferman, Friedman, Simpson to name a few) have shown that large swathes of ordinary mathematics can be undergirded by theories of fairly modest consistency strength. This confirms what Hilbert surmised in his program, namely that elementary results (e.g. those expressible in the language of number theory) proved in abstract, non-constructive mathematics can often be proved by elementary means. The best known program for calibrating the strength of theorems from ordinary mathematics is reverse mathematics (RM). RM's scale for measuring strength is furnished by certain standard systems couched in the language of second order arithmetic. However, its language is not expressive enough to be able to talk about higher order objects, such as function spaces, directly. Richer formal systems, in which higher order mathematical objects can be directly accounted for, have been suggested. The price for maintaining conservativity over elementary theories, however, is that one has to use different logics for different ontological realms, allowing classical logic to reign at the level of numbers whereas higher type mathematical objects obey only intuitionistic logic. In the talk, I'd like to present some of these semi-intuitionistic systems, give a feel for carrying out mathematics within them, and relate them to systems considered in RM."</p>