Э.В.Бет. Заметки о натуральной дедукции © 1992 перевод С.В.Свистунова посвящается Роберту Фейсу на основе беседы с проф.А.Гейтингом при встрече 26 февраля 1955 г. E.W.Beth. Remarks on natural deduction. Proceedings Kon.Ned.Akad.van Weten., vol.53, N.3, 1955, ser.A., Amsterdam (Записки Нидерландской Королевской Академии Наук, сер.А,т.53,N3, 1955, Амстердам) 1. Семантические таблицы Допустим, мы хотим показать, что формула: (x)(y) [A(x) --> B(y)] является логическим следствием1 формулы: (Ex) A(x) --> (y) B(y) Тогда мы можем построить семантическую таблицу следующим образом: Истинно Ложно 1. (Ex) A(x) --> (y) B(y) 5. A(a) (i) (ii) 7. (y) B(y) 9. B(a) 10. B(b) 2. (x)(y) [A(x) --> B(y)] 3. (y) [A(a) --> B(y)] 4. A(a) --> B(b) 6. B(b) (i) (ii) 8. (Ex)A(x) 11. A(a) Хотя эта таблица предельно понятна, слудующие замечания могут оказаться полезными. Мы вписываем формулу (1) как начальную в левый столбец, а формулу (2) как начальную в правый столбец. Если формула (2) ложна, то тогда должно иметься такое значение x, что (y) [A(x) -->B(y)] ложно; если это значение назвать «a», то мы получаем строку (3); и.т.д. Если формула (1) истинна, то либо (i) формула (8) должна быть ложной, либо (ii) формула (7) должна быть истинной. Таблица ясно показывает, что на основе семантических правил для элементарной логики, всякие попытки построить подходящий контрпример для доказательства того, что (2) не есть логическое следствие формулы (1), оказваются тщетными2. 2. Перестройка таблицы в формальный вывод Давайте теперь расположим формулы в нашей таблице несколько иначе, опуская формулы (10) и (11), которые уже появлялись в строках (6) и (5), соответственно, выписывая формулы из правого столбца в обратном порядке. 1. (Ex) A(x) --> (y) B(y) ..... (доп) ----------------------------------- 5. A(a) ............................. (+ гип.1) 8. (Ex) A(x) 7. (y) B(y) 9. B(a) 10. B(b) ----------------------------------- 4. A(a) --> B(b) ................. (- гип.1) 3. (y) [A(a) --> B(y)] 2. (x)(y) [A(x) --> B(y)] ...... (закл.) Получившаяся последовательность формул сильно напоминает вывод в некоторой Системе Натурального Вывода; для того, чтобы подчеркнуть это сходство и были добавлены две горизонтальные линии и несколько пояснений к материалу взятому из первоначальной таблицы. Однако, никаких других изменений не вносилось. 3. Общие положения Действительно, существует некоторая формальная система F, для которой можно доказать в общей форме следующее утверждение : Всякая семантическая таблица, которая показывает несуществование подходящего контрпримера для доказательства того, что некоторая формула V не есть логическое следствие определенных формул U1, U2, ... может быть преобразована так, чтобы обеспечить в F формальный вывод заключения V из посылок U1, U2, ...; и, наоборот, всякий формальный вывод в F можно преобразовть в соответствующую семантическую таблицу. Для доказательства этого утверждения потребуются следующие шаги : Необходимо сформулировать точные правила для построения семантической таблицы; Необходимо дать точное описание формальной системы F; Необходимо сформулировать точные правила для преобразования семантической таблицы в формальный вывод, и наоборот; Необходимо указать, что в тех случаях, когда (эксперементальное) построение семантической таблицы включает бесконечно много шагов, всегда существует подходящий контрпример. 1. Формулировка таких правил не представляет особого труда. Следовательно, будет достаточно указать те правила, которые не очевидны. Появление (Ex) X(x) в левом столбце требует введения нового индивида p, а X(p) затем вписывается в тот же столбец; но если (Ex) X(x) появляется в правом столбце, то X(p) вписывается в тот же столбец для всех индивидов p, как старых так и новых. Аналогично для (x) X(x). Если X v Y или X -> Y появляется в левом столбце, или если X & Y в правом, то таблицу необходимо расщепить на две подчиненные таблицы. Левый и правый столбцы принадлежащие одной и той же (под)таблице называются сопряженными столбцами. Если одна и та же формула появляется в двух сопряженных стоблцах, то (под)таблица к которой они принадлежат закрыта; и если обе подтаблицы некоторой (под)таблицы закрыты, то и сама эта таблица также закрыта. 2. Эта проблема теперь легко разрешима следующим образом : формальный вывод в F заключения V из посылок U1, U2, ... есть закрытая таблица, в которой начальными формулами в левом столбце являются U1, U2, ... и V в правом. 3. Используя подход для решения задачи 2, данная задача оказывается тривиальной. Однако, не возникло бы никаких трудностей, если бы появилось желание придать выводам в F более знакомую форму. 4. Заключительные замечания Приведенные соображения тесно связаны с моими исследованиями по методу Падоа3 и с другой работой, которая пока не опубликована4. Становится ясно, что упомянутая формальная система F заслуживает названия «Системы Натуральной Дедукции» как своим сходством с системами построенными Генценым, Кетоненом, Шутте, Клини, Карри, Куайном и другими, так и тесными связями с семаническим подходом к этим проблемам логики. Относительно формальной системы F, доказательства таких метаматематических теорем как теорема Эрбрана, теорема Левенхейма-Сколема-Геделя, теорема о непротиворечивости Бернайса оказываются крайне постыми, естественными и элегантными5. Если для любых произвольных формул U1, U2, ..., V, мы могли бы вычислить натуральное число n такое, что после введения n индивидов a,b, ... мы могли бы решить будет таблица закрыта или нет, то мы бы имели разрешающую процедуру для выводимости. Однако, на основе хорошо известного результата А.Черча известно, что такой разрешающей процедуры не существует, и, следовательно, никакого вычисления n вообще невозможно. С другой стороны, критическое число n индивидов a,b, ..., которые были введены до закрытия таблицы, ясно показывает сколько раз мы переходили от некоторой формулы X(p) к формуле (x)X(x) или от формулы (Ex) X(x) к формуле X(p) в соответствующем выводе системы F заключения V из посылок U1, U2, ... Следовательно, по-видимому, решающее число n представляет собой некий инвариант, который врядли можно существенно свести, если мы заменим систему F на другую формализацию элементарной логики (например, систему Гильберта-Аккермана). Допустим теперь, что мы сталкиваемся с каким-то сомнительным выводом V из U1, U2, ... в некоторой формальной системе G. Тогда, на основе проверки того вывода (и, возможно, также формальной системы G), мы сможем приблизительно подсчитать критическое число n. А затем указанный метод6 позволит нам решить, следует ли принимать результат данного вывода. Поскольку, если наша таблица закрыта, то мы имеем правильный вывод вместо сомнительного; а если таблица не закрыта, то следовательно сомнительный вывод не может быть правильным; следовательно нет и не может быть основаниний доверять его результату. Ясно, что раз мы вычислили критическое число n, все остальное может выполнить машина. Другое замечание касается интуиционистской логики Гейтинга. Хорошо известно, что если мы удобно ограничиваем правила формальной системы F, мы получаем соответствующую интуиционистскую систему F'. Теперь допустим, что у нас есть вывод D в F, критическое число которого n. Тогда проблема «имеется или не имеется аналогичный вывод в F'» (т.е. вывод, начинающийся с тех же посылок и дающий то же самое заключение) D', имеющий то же критическое число n, сводится к проблеме затрагивающей выводимость в интуиционистском исчисслении высказываний и, следовательно, она эффективно может быть разрешена на основе генценовских результатов. Конечно, отрицательный результат разрешающей процедуры не исключает prima facie (лат. на первый взгляд) возможности нахождения в F' аналогичного вывода D', имеющего критическое число n' большего чем n. Но, по крайней мере, в практическом отношении ситуация, по-видимому, менее запутана; поскольку в конкретных случаях7 анализ семантической таблицы, соответствующей выводу D, (i) объясняет почему невозможно найти аналогичный вывод в D', имеющей то же критическое число n, и (ii) сделает ясным, что замена n большим числом n' не может вызвать каких-либо затруднений. Не помешает также предположить, что можно доказать для этого общую теорему; такая теорема обеспечивала бы нас разрешающей процедурой для решения проблем: можем мы найти для данного вывода D в F аналогичный вывод D' в F' или нет. Институт по исследованиям оснований философии и точных наук, Амстердамский Университет П р и м е ч а н и я A.Tarski, Ueber den Begriff der logischen Folgerung, Actes du Congres International de Philosophie Scientifique, fasc.VII: Logique, pp.1-11 (Paris, 1936) Таблица построена по методу строго следующему семантическим правилам, но отличается от современной процедуры как она описана, например, у Тарского в Introduction to Logic, pp.40, 41 (2nd ed., New York, 1946) Beth E.W., On Padoa's Method in the Theory of Definition, эти же «Записки» 56(1953); ср. A Topological Proof of the Theorem of Lowenheim-Skilem-Godel, там же 54 (1951). Я использую данную возможность, чтобы исправить оплошность, допущенную мной в последней из упомянутых статей и на которую позже обратил мое внимание Дж.К.К.Маккинси: подобное доказательство сделал Archie Blake в своей диссертации: Canonical Expressions in Boolean Algebras (Chicago, 1938) E.W.Beth, L'existence en mathematiques, готовится к выпуску Доктор Гизберт Хазенъегер (Мюнстер) оказал мне честь, сообщив, что близкие идеи представил К.Шютте в ноябре 1954 г. на Симпозиуме по логике, состоявшемся в Марбурге. Я также в долгу у доктора Хазенъегера за данный выпуск. Я использую эту возможность, чтобы выразить благодарность профессору Леону Генкину (Калифорнийский университет в Беркли, находящемуся сейчас в отпуске в Амстердаме) за очень полезный разговор по всем темам, обсуждаемым в этом сообщении. И, вероятно, также процедура построенная Р.Стэнли, An Extended Procedure in Quantificational Logic, Journal of Symbolic Logic 18 (1953). Однако, как сама эта процедура, так и ее описание автором настолько подробны, что я не в состоянии дать более ясное изложение. Как обсуждается, например, у S.C.Kleene, Introduction to Metamathematics pp.487-91 (Amsterdam-Groningen, 1952) Ниже приводится реферат на работу Бета, написанный В.А.Янковым Замечания к натуральной дедукции. Э.Бет.1955 Строится формальная система F, в которой выводом формулы B в исчислении предикатов из формулы A является построенная некоторым образом закрытая таблица. Эта система родственна генценовскому исчислению секвенций. В ней, в частности, можно ответить на вопрос, существует ли вывод B из A, содержащий не более n введений кванторов общности и существования. По утверждению автора, в ней особенно легко доказывается ряд математических теорем. В.А.Янков РЖ Математика 1959, 3433 Санкт-Петербург, апрель 1992 *