względem zdań realnych. Co więcej: pokazać należy, że istnieje &lt;orig&gt;finitystyczna&lt;/&gt; metoda pozwalająca na transformację każdego &lt;orig&gt;infinitystycznego&lt;/&gt; dowodu zdania realnego na dowód &lt;orig&gt;finitystyczny&lt;/&gt;. Oba te zagadnienia, tzn. problem niesprzeczności i problem zachowawczości, są zresztą wzajemnie powiązane: jeśli bowiem utożsamić zdania realne ze zdaniami klasy % , to - jak pokazał G. Kreisel - rozwiązanie problemu niesprzeczności daje też rozwiązanie problemu zachowawczości.<br>Hilbert zaproponował konkretny program, zwany dziś programem Hilberta, realizacji opisanych wyżej zadań. Składał się on z dwu etapów. Pierwszy etap polegał na formalizacji matematyki, tzn. na rekonstrukcji matematyki &lt;orig&gt;infinitystycznej&lt;/&gt; jako dużego, szczegółowo opracowanego systemu sformalizowanego (zawierającego m. in. logikę klasyczną, nieskończoną teorię mnogości, arytmetykę liczb