Минимальные аксиомы булевой алгебры
В математической логике минимальные аксиомы булевой алгебры — это предположения, которые эквивалентны аксиомам булевой алгебры (или исчисления высказываний ), выбранным как можно более короткими. Например, аксиома с шестью операциями И-НЕ и тремя переменными эквивалентна булевой алгебре: [1]
где вертикальная черта представляет логическую операцию И-НЕ (также известную как штрих Шеффера ).
Это одна из 25 аксиом-кандидатов на это свойство, определенных Стивеном Вольфрамом путем перечисления тождеств Шеффера длиной меньше или равной 15 элементам (исключая зеркальные отображения), которые не имеют некоммутативных моделей с четырьмя или меньшим количеством переменных, и впервые была доказана эквивалентность Уильям МакКьюн , Брэнден Фительсон и Ларри Вос . [2] [3] Сайт MathWorld , связанный с Вольфрамом, назвал эту аксиому «аксиомой Вольфрама». [4] МакКьюн и др. также нашел более длинную аксиому булевой алгебры, основанную на дизъюнкции и отрицании. [3]
В 1933 году Эдвард Вермили Хантингтон сформулировал аксиому
как эквивалент булевой алгебры в сочетании с коммутативностью операции ИЛИ , , и предположение об ассоциативности, . [5] Герберт Роббинс предположил, что аксиому Хантингтона можно заменить аксиомой
что требует на одно использование оператора логического отрицания меньше . Ни Роббинс, ни Хантингтон не смогли доказать эту гипотезу; не смог этого сделать и Альфред Тарский , который позже проявил к этому значительный интерес. В конечном итоге гипотеза была доказана в 1996 году с помощью программного обеспечения для доказательства теорем . [6] [7] [8] Это доказательство установило, что аксиома Роббинса вместе с ассоциативностью и коммутативностью образует 3-базис булевой алгебры. Существование 2-базиса было установлено в 1967 году Кэрью Артуром Мередитом : [9]
В следующем году Мередит обнаружила 2-основу с точки зрения инсульта Шеффера: [10]
В 1973 году Падманабхан и Квакенбуш продемонстрировали метод, который, в принципе, позволил бы получить 1-базис для булевой алгебры. [11] Простое применение этого метода привело к «аксиомам огромной длины». [3] тем самым поднимая вопрос о том, как можно найти более короткие аксиомы. Этот поиск дал 1-базис в терминах штриха Шеффера, приведенный выше, а также 1-базис
который записан в терминах ИЛИ и НЕ . [3]
Ссылки [ править ]
- ^ Вольфрам, Стивен. «Логика, объяснимость и будущее понимания» . Сочинения Стивена Уорфрема .
- ^ Вольфрам, Стивен (2002). Новый вид науки . Вольфрам Медиа. ISBN 978-1579550080 .
- ^ Jump up to: Перейти обратно: а б с д МакКьюн, Уильям ; Верофф, Роберт; Фительсон, Бранден ; Харрис, Кеннет; Файст, Эндрю; Вос, Ларри (2002), «Краткие одиночные аксиомы булевой алгебры», Journal of Automated Reasoning , 29 (1): 1–16, doi : 10.1023/A:1020542009983 , MR 1940227 , S2CID 207582048
- ^ Роуленд, Тодд; Вайсштейн, Эрик В. «Аксиома Вольфрама» . Математический мир .
- ^ Хантингтон, Э.В. (1933). «Новые наборы независимых постулатов алгебры логики со специальной ссылкой на Principia Mathematica Уайтхеда и Рассела ». Пер. амер. Математика. Соц. 25 : 247–304.
- ^ Хенкин, Леон ; Монк, Дж. Дональд; Тарский, Альфред (1971). Цилиндрические алгебры, часть I. Северная Голландия . ISBN 978-0-7204-2043-2 . OCLC 1024041028 .
- ^ МакКьюн, Уильям (1997). «Решение проблемы Роббинса». Журнал автоматизированного рассуждения . 19 (3): 263–276. дои : 10.1023/А:1005843212881 . S2CID 30847540 .
- ^ Колата, Джина (10 декабря 1996 г.). «Компьютерное математическое доказательство демонстрирует силу рассуждения» . Нью-Йорк Таймс . Информацию об ошибках см. МакКьюн, Уильям (23 января 1997 г.). «Комментарии к истории Роббинса» . Аргоннская национальная лаборатория . Архивировано из оригинала 5 июня 1997 г.
- ^ Мередит, Калифорния ; Приор, А.Н. (1968). «Эквациональная логика» . Нотр-Дам Ж. Формальная логика . 9 (3): 212–226. дои : 10.1305/ndjfl/1093893457 . МР 0246753 .
- ^ Мередит, Калифорния (1969). «Эвациональные постулаты для штриха Шеффера» . Нотр-Дам Ж. Формальная логика . 10 (3): 266–270. дои : 10.1305/ndjfl/1093893713 . МР 0245423 .
- ^ Падманабхан, Р.; Квакенбуш, RW (1973). «Эквациональные теории алгебр с дистрибутивными сравнениями» . Учеб. амер. Математика. Соц. 41 (2): 373–377. дои : 10.1090/S0002-9939-1973-0325498-2 .