Эверт Виллем Бет (7 июля 1908 – 12 апреля 1964) был голландским философом и логиком , чьи работы в основном касались оснований математики . Он был членом Significs Group .
Бет родился в Алмело , небольшом городке на востоке Нидерландов . Его отец изучал математику и физику в Амстердамском университете , где ему была присуждена степень доктора философии . Эверт Бет изучал те же предметы в Утрехтском университете , но затем также изучал философию и психологию . Его докторская степень 1935 года была посвящена философии.
В 1946 году он стал профессором логики и оснований математики в Амстердаме . За исключением двух коротких перерывов — работы в 1951 году в качестве научного ассистента Альфреда Тарского и в 1957 году в качестве приглашенного профессора в Университете Джонса Хопкинса — он занимал эту должность в Амстердаме непрерывно до своей смерти в 1964 году. Его должность была первой академической должностью в его стране по логике и основаниям математики, и в это время он активно способствовал международному сотрудничеству в становлении логики как академической дисциплины.
В 1953 году он стал членом Королевской Нидерландской академии искусств и наук . [1]
Он умер в Амстердаме .
Теорема определимости Бета утверждает, что для логики первого порядка свойство (или функция , или константа ) неявно определимо тогда и только тогда, когда оно явно определимо. Дальнейшее объяснение дано в разделе определимость Бета .
Самый известный вклад Бет в формальную логику — это семантические таблицы , которые являются процедурами принятия решений для пропозициональной логики и логики первого порядка . Это семантический метод, как таблицы истинности Витгенштейна или резолюция Дж . Алана Робинсона , в отличие от доказательства теорем в формальной системе, такой как аксиоматические системы, используемые Фреге , Расселом и Уайтхедом , и Гильбертом , или даже естественная дедукция Генцена . Семантические таблицы являются эффективной процедурой принятия решений для пропозициональной логики, тогда как для логики первого порядка они являются лишь полуэффективными, поскольку логика первого порядка неразрешима , как показано в теореме Чёрча . Многие считают этот метод интуитивно простым, особенно для студентов, которые не знакомы с изучением логики, и он быстрее, чем метод таблицы истинности (который требует таблицы с 2 n строками для предложения с n пропозициональными буквами). По этим причинам Уилфрид Ходжес , например, представляет семантические таблицы в своем вводном учебнике « Логика» , а Мелвин Фиттинг делает то же самое в своем изложении логики первого порядка для специалистов по информатике « Логика первого порядка и автоматическое доказательство теорем» .
Начинается с намерения доказать, что определенный набор формул влечет за собой другую формулу , учитывая набор правил, определяемых семантикой связок формул (и квантификаторов в логике первого порядка ). Метод заключается в том, чтобы предположить совпадающую истинность каждого члена и (отрицание ), а затем применить правила для разветвления этого списка в древовидную структуру (более простых) формул до тех пор, пока каждая возможная ветвь не будет содержать противоречие . На этом этапе будет установлено, что является противоречивым, и, таким образом, что формулы из вместе влекут .
Это класс реляционных моделей для неклассической логики (ср. семантика Крипке ).
