ЭРБРАН

ЭРБРАН (Herbrand) Жак (12 февраля 1908, Париж – 27 июля 1931, Изер, Франция) – французский логик и математик; окончил Высшую Нормальную школу (1928), защитил докторскую степень с отличием (1930); как стипендиат рокфеллеровского фонда последние два года своей короткой жизни провел в Германии: сначала у фон Неймана в Берлине, затем в Геттинтене у Гильберта. Творческий путь Эрбрана оборвался трагически: он погиб в результате несчастного случая в альпийских горах в районе Берарда (La Bérarde). Научные интересы Эрбрана определились рано, после знакомства с Principia mathematica (Уайтхеда и Рассела). В Германии он активно участвовал в реализации гильбертовской программы (см. Формализм [ФОРМАЛИЗМ]), выбрав для себя две основные проблемы доказательств теории [ДОКАЗАТЕЛЬСТВ ТЕОРИЯ] – проблему непротиворечивости арифметики и проблему разрешения (см. Разрешения проблема [РАЗРЕШЕНИЯ ПРОБЛЕМА]). Свой взгляд на философские принципы финитизма [ФИНИТИЗМ]Эрбран изложил в статье «Об основах гильбертовской логики» (1930), а на его логические задачи – в заметке «О фундаментальной проблеме математики» (1929). Основная теорема Эрбрана, открытая им в 1929, является, по оценке П.Бернайса, «центральной теоремой логики предикатов». К этой теореме (названной теперь его именем) Эрбран пришел, отправляясь от идей Лёвенгейма и Скулема. Суть теоремы в том, что она гарантирует формальную выводимость (доказуемость) формулы элементарной (первопорядковой) логики из аксиом, если методом Эрбрана можно показать общезначимость этой формулы в т.н. эрбрановском универсуме, представляющем из себя чисто синтаксическую (эффективно порождаемую) конструкцию. При этом в основе метода Эрбрана лежат идея косвенного доказательства и идея сведения формулы логики предикатов в скулемовской нормальной форме (возможно, с функциональными символами) к некоторому частному случаю (пропозициональной формуле в канонической форме), который позволил бы сделать вывод об общезначимости исходной формулы. В результате такой процедуры перехода «от частного к общему» проблема доказуемости (выводимости) в некоторой первопорядковой системе аксиом сводится к проблеме общезначимости в логике высказываний. Выдающееся значение работы Эрбрана стало очевидным, во-первых, в свете более поздних теорем Чёрча и Шеннона об алгоритмической неразрешимости проблемы разрешения (общезначимости в любом универсуме) для формул элементарной логики, а во-вторых, в свете алгоритмических задач в области искусственного интеллекта, которые опираются на логику. До сих пор метод Эрбрана «служит основой для большинства современных автоматических алгоритмов поиска доказательства» (Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем, пер. с англ. М., 1983, с. 52).

Сочинения:

1. Écrits logiques. P., 1968.

Литература:

1. Минц Г.Е. Теорема Эрбрана. – В кн.: Математическая теория логического вывода. М., 1967;

2. Dreben В., Denton J. A supplement to Herbrand. – «The Jornal of symbolic logic». Vol. 31, 1966;

3. Heijenoort J. van. A source book in mathematical logic 1879–1931. Cambr. (Mass.), 1967.

Μ.Μ.Новосёлов