Финитный подход к задаче оптимизации алгорифмов установления выводимости

Рассматриваются алгорифмы установления выводимости в конечном множестве $S$ формул логики предикатов. Пусть $F$ – непротиворечивая и достаточно сильная формальная система, и “доказательство корректности” означает доказательство в $F$. Если множество $S$ достаточно богато, то невозможен ни разрешающий алгорифм, корректность которого доказуема в $F$ (при $\operatorname{cord}(s)\geq C$ длина $(F)$), ни “практически просто работающий” алгорифм поиска в $S$, у которого было бы достаточно короткое доказательство корректности. Библ. – 8 назв.