В математической логике , Skolem арифметика является теорией первого порядка из натуральных чисел с умножением , названных в честь Thoralf Сколемого . Подписи из сколемовской арифметики содержит только операцию умножения и равенство, опуская операцию сложения полностью.
Сколемская арифметика намного слабее арифметики Пеано , которая включает в себя как операции сложения, так и умножения. В отличие от арифметики Пеано, арифметика Сколема - разрешимая теория . Это означает, что для любого предложения на языке сколемской арифметики можно эффективно определить, доказуемо ли это предложение на основе аксиом сколемской арифметики. Однако асимптотическая вычислительная сложность времени выполнения этой задачи принятия решения является трехкратной экспоненциальной.
Выразительная сила
Логика первого порядка с равенством и умножением положительных целых чисел может выразить отношение . Используя это отношение и равенство, мы можем определить следующие отношения на натуральных числах:
- Делимость:
- Наибольший общий делитель :
- Наименьшее общее кратное :
- постоянная :
- Простое число :
- Число продукт простые числа (для фиксированного ):
- Число это сила какого-то простого:
- Число продукт точно основные полномочия:
Идея разрешимости
Значение истинности формул арифметики Сколема может быть уменьшено до значения истинности последовательностей неотрицательных целых чисел, составляющих их разложение на простые множители, при этом умножение становится точечным сложением последовательностей. Тогда разрешимость следует из теоремы Фефермана-Воота, которую можно показать с помощью исключения кванторов . Другими словами, теория первого порядка целых положительных чисел изоморфна теории первого порядка конечных мультимножеств неотрицательных целых чисел с операцией суммы мультимножества, разрешимость которой сводится к разрешимости теории элементов.
Более подробно, согласно Основной теореме арифметики , положительное целое число можно представить как произведение основных степеней:
Если простое число не фигурирует как множитель, мы определяем его показатель быть нулевым. Таким образом, только конечное число показателей ненулевых в бесконечной последовательности. Обозначим такие последовательности неотрицательных целых чисел через.
Теперь рассмотрим разложение другого положительного числа,
Умножение соответствует точечное сложение показателей:
Определите соответствующее точечное сложение последовательностей следующим образом:
Таким образом, мы имеем изоморфизм между структурой натуральных чисел с умножением, и точечного сложения последовательностей неотрицательных целых чисел, в которых только конечное число элементов ненулевое, .
Исходя из теоремы Фефермана-Воота для логики первого порядка , значение истинности логической формулы первого порядка над последовательностями и точечным сложением на них алгоритмически сводится к значению истинности формул в теории элементов последовательности с сложение, которое в данном случае является арифметикой Пресбургера . Поскольку арифметика Пресбургера разрешима, разрешима и арифметика Сколема.
Разрешаемые расширения
Благодаря приведенной выше редукции с использованием теоремы Фефермана-Воота, мы можем получить теории первого порядка, открытые формулы которых определяют более широкий набор отношений, если мы усилим теорию мультимножеств простых множителей. Например, рассмотрим соотношение это верно тогда и только тогда, когда а также имеют равное количество различных простых множителей:
Например, потому что обе стороны обозначают число, которое имеет два различных простых делителя.
Если мы добавим соотношение для сколемской арифметики она остается разрешимой. Это связано с тем, что теория множеств индексов (структура индексов в теореме Фефермана-Воота) остается разрешимой при наличии оператора равнодоступности на множествах.
Неразрешимые расширения
Расширение сколемской арифметики с предикатом-преемником, можно определить отношение сложения, используя тождество Тарского:
и определяя отношение на натуральные числа на
Поскольку она может выражать как умножение, так и сложение, полученная теория неразрешима.
Если у нас есть предикат упорядочивания натуральных чисел (меньше, ), мы можем выразить от
так что расширение с также неразрешима.
Смотрите также
Рекомендации
Бес, Алексис (2002). «Обзор арифметической определимости» (PDF) . Soc.Math. Belgique, Дань памяти Морису Боффа : 1–54.