-
проблема нахождения для данной дедуктивной теории общего
метода, позволяющего решать, может ли отдельное
утверждение, сформулированное в терминах теории, быть доказано в ней или нет. Этот
общий метод, являющийся эффективной процедурой (алгоритмом), называется процедурой разрешения или разрешающей процедурой, а
теория, для которой такая процедура существует, - разрешимой теорией. Р. п. решается в классической логике высказываний с помощью таблиц истинности. Разрешающий
алгоритм существует и для логики одноместных предикатов, для
силлогизма категорического и других простых дедуктивных теорий. Но уже для логики предикатов общего решения Р. п. не существует. В математике также невозможно установить общий метод, который дал бы
возможность провести
различие между утверждениями, которые могут быть доказаны в ней, и теми, которые в ней недоказуемы.
Невозможность найти для теории общий разрешающий метод не исключает поиска процедуры разрешения для отдельных классов ее утверждений.