Program hilbertov-ei

EI1.
"Vzhľadom na význam teórie množín pre základy celej matematiky, sa stala ... otázka o jej bezospornosti centrálnym základným problémom nášho storočia. Na jej riešenie rozpracoval r. 1920 D. Hilbert program formalizácie. V ňom sa dôkaz bezospornosti matematickej teórie redukoval na 'hru s číslami', aby sa ukázalo, že konjunkcia výroku a jeho negácia sa nedá z axióm odvodiť. Podľa Hilberta náplňou špeciálnej teórie dôkazov - metamatematiky je prezentácia dôkazov pomocou konečnej mnmožiny symbolov pri aplikácii konečných (finitných) metód. Základom tejto metamatematiky sú zákonitosti vytvárania, preformovania a vzájomného poradia skúmaných postupností symbolov, syntax výrokového počtu (kalkulu). Rozličné možnosti interpretácie výrokového počtu vytvárajú jeho sémantiku." ( L74;60)