Разрешимость
Как я отмечал в аннотации, в [1] утверждается, что в Tutorial D допускается отсутствие разрешимости; более точно, утверждается, что в Tutorial D некоторые логические выражения являются неразрешимыми. Что это значит?
Во-первых, каждое выражение можно считать правилом вычисления значения; поэтому, в частности, логическое выражение можно считать правилом вычисления истинностного значения. Итак, логическое выражение – это выражение, сформулированное на некотором языке L, про которое подразумевается, что оно обозначает TRUE или FALSE. Пусть exp является таким выражением; тогда exp называется неразрешимым, если это выражение правильно построено – т.е. сконструировано в полном соответствии с синтаксическими правилами языка L, – но при этом не существует алгоритм, который за конечное время может определить, является ли результатом вычисления exp TRUE. В расширительном смысле, язык L называется неразрешимым в том и только в том случае, когда существует, по крайней мере, одно неразрешимое выражение, представляемое средствами L. Замечу, между прочим, что исчисление высказываний является разрешимым, а исчисление предикатов – нет.
Если язык L является разрешимым, то по определению существует универсальный алгоритм («разрешающая процедура») для определения за конечное время того, является ли TRUE результатом вычисления произвольного выражения, представленного на языке L. Наоборот, если L является неразрешимым, то такой алгоритм не существует. Более того, если L является неразрешимым, отсутствует даже алгоритм для определения за конечное время того, является ли выражение L разрешимым (если бы такой алгоритм существовал, система могла бы (по крайней мере, частично) избежать проблемы, даже и не пытаясь вычислять неразрешимые выражения).
Из сказанного выше следует, что если, в частности, Tutorial D является неразрешимым, то будут иметься некоторые выражения, представленные с использованием этого языка, и, следовательно, некоторые запросы, представленные на Tutorial D (а именно, запросы, включающие такие выражения), с которыми система не сможет справляться удовлетворительным образом. В связи с этим тот факт, что Tutorial D является неразрешимым, выглядит как серьезный дефект.
