Введение

Голландский философ и логик Эверт Виллем Бет (7 июля 1908 – 12 апреля 1964) был нидерландским философом и логиком, чьи работы были посвящены главным образом основаниям математики. Он являлся членом группы «Сигнификс».

Биография

Бет родился в Альмело, небольшом городке на востоке Нидерландов. Его отец изучал математику и физику в Амстердамском университете, где получил докторскую степень. Эверт Бет изучал те же предметы в Утрехтском университете, но затем также изучал философию и психологию. Его диссертация 1935 года была по философии. В 1946 году он стал профессором логики и основ математики в Амстердаме. За исключением двух кратковременных перерывов – работы в 1951 году научным ассистентом Альфреда Тарского и в 1957 году в качестве приглашенного профессора в Университете Джона Хопкинса – он непрерывно занимал эту должность в Амстердаме до своей смерти в 1964 году. Это была первая академическая должность в его стране в области логики и основ математики, и на протяжении этого времени он активно содействовал международному сотрудничеству в утверждении логики как академической дисциплины. В 1953 году он был избран членом Королевской нидерландской академии искусств и наук. Он умер в Амстердаме.

Теорема определённости Бет

Теорема Бета об определимости утверждает, что для логики первого порядка свойство (или функция, или константа) является неявно определимым тогда и только тогда, когда оно является явно определимым. Дополнительные пояснения приведены в разделе "Определяемость Бета".

Семантические таблицы

Самый известный вклад Бета в формальную логику — семантические таблицы, которые являются процедурами принятия решений для пропозициональной логики и логики первого порядка. Это семантический метод, подобный таблицам истинности Витгенштейна или резолюции Робинсона, в отличие от доказательства теорем в формальной системе, такой как аксиоматические системы, используемые Фреге, Расселом и Уайтхедом, и Гильбертом, или даже натуральная дедукция Гентцена. Семантические таблицы являются эффективной процедурой принятия решений для пропозициональной логики, в то время как для логики первого порядка они являются лишь полуэффективными, поскольку логика первого порядка неразрешима, как показала теорема Черча. Многие считают этот метод интуитивно простым, особенно для студентов, не знакомых с изучением логики, и он быстрее метода таблиц истинности (который требует таблицы с 2<sup>n</sup> строками для формулы с n пропозициональными переменными). По этим причинам, например, Уилфрид Ходжес представляет семантические таблицы в своем вводном учебнике «Логика», а Мелвин Фиттинг делает то же самое в своей работе по логике первого порядка для специалистов в области компьютерных наук — «Логика первого порядка и автоматическое доказательство теорем». Отправной точкой является намерение доказать, что определенное множество формул влечет другую формулу, исходя из набора правил, определяемых семантикой логических связок формул (и кванторов в логике первого порядка). Метод заключается в предположении об одновременной истинности каждого элемента множества и отрицания , а затем в применении правил для ветвления этого списка в древовидную структуру (более простых) формул, пока каждая возможная ветвь не будет содержать противоречие. В этом случае будет установлено, что несостоятельно, и, следовательно, что формулы из совместно влекут .

Модели Бет

Это класс реляционных моделей для неклассической логики (см. семантику Крипке).