Об аксиоматизации арифметики Бюхи

Мы рассматриваем известную арифметику Бюхи В А_р = Th(N,S, +, 0, Vp), где S(n) = п + 1 и Vp(a) = р^к такое, что р^к\а и р^к+1 \ а (р ^ 2 - некоторое фиксированное натуральное число). Структура (N, S, +, 0, Vp) является автоматной и, на самом деле, универсальной для всех автоматных структур относительно интерпретаций первого порядка (см. [1, Теорема 4.5]). Следовательно, ВА_р разрешима, однако явная аксиоматизация этой теории неизвестна. Наша цель - найти такую аксиоматизацию. Хотя наша система аксиом, возможно, и не является вполне естественной, она может быть первым шагом к построению лучшей аксиоматизации арифметики Бюхи.

Наша аксиоматизация состоит из нескольких простых аксиом для S, + и Vp, а также следующей схемы аксиом для всех формул р(ж) с одной свободной переменной:

Зжр(ж) ^ Зж < пр р(ж), где пр подобрано так, чтобы эта формула была истинна в стандартной модели. Здесь через п обозначен нумерал S”(0) числа п. Нашей (довольно грубой) оценкой на пр является р2^ где через 2^ обозначена итерированная экспонента (2q = к, 2^+1 = 22™) и |р| обозначает число символов в формуле р.

Одним из главных свойств арифметики Бюхи является тот факт, что определимые в ней множества - это в точности множества, р-ичные записи которых распознаваемы с помощью конечных автоматов (мы говорим, что язык L распознаваем, существует конечный автомат, который принимает в точности все слова из К).

Теорема 1 ([2,3]). Множество А С N^k определимо в (N, S, +, 0, Vp) тогда и только тогда, когда множество всех р-ичных записей элементов А можно распознать конечным автоматом.

(С) Ковалёв К. А., 2025

@ Федеральное государственное автономное образовательное учреждение высшего образования «Московский физико-технический институт (пациопальпый исследовательский университет)», 2025

Мы будем использовать этот результат для получения упомянутой выше оценки на п^. Также эта теорема влечет алгоритмическую разрешимость ВА_р. Помимо результата выше, ранее изучались множества, определимые в арифметике Бюхи для различных р. А именно, верен следующий результат, полученный сначала А. Кобхэмом для подмножеств N, а затем А. Семёновым в общем случае.

Теорема 2 ([4,7]). Пусть p,q ^ 2 мультипликативно независимы (то есть не существует таких l,r G N \ {0}, что р¹ = q^r). Тогда если А С N^ определимо в арифметике Бюхи по основанию р и по основанию q, то А определимо в арифметике Пресбургера (то есть, в (N, S, +, 0)).

С другой стороны, А. Запрягаев получил следующий результат об интерпретируемости арифметики Бюхи.

Теорема 3 ([10]). При всех p,q ^ 2, теория ВА_Р интерпретируема в В Ад.

В некотором смысле арифметика Бюхи сложнее арифметики Пресбургера, например, не всякая формула эквивалентна экзистенциальной формуле в ВА_р (см. [5]). Поэтому найти аксиоматизацию, аналогичную аксиоматизации арифметики Пресбургера, не представляется возможным. Тем не менее верен следующий результат.

Теорема 4 ([5,9]). Любая формула эквивалентна сК-формуле в ВА_р.

Вопрос об аксиоматизации арифметики Бюхи рассматривался ранее А. Запрягаевым. Им был получен следующий отрицательный результат.

Теорема 5 ([11]). Теория, состоящая из следующих аксиом, является неполной:

• (i)    аксиомы арифметики Пресбургера;

• (ii)    V2(x) =0 о х = 0;

• (iii)    -Су(х = у + у) ^ Vz(x) = 1;

• (iv)    X = t + t ^ V2(х) = V2(t) + V2(t).

2.    Обозначения и соглашения

В частности, эта теория не доказывает следующую формулу, истинную в стандартной модели:

V2(x) = х ^ —Су(х < у < х + х Л Vp(y) = у), которая означает «не существует степени 2 между 2к и 2к+1».

Для целого числа р ^ 2 мы обозначим через Vp функцию N ^ N такую, что Vp(0) = 0 и Vp(n) = р^к для всех п >  0, г де р^к |п и р^к+1 ( п. Через S мы обозначим функцию п ^ п +1.

Стандартной моделью мы называем структуру (N, S, +, 0, Vp). Для сокращения записи мы часто будем обозначать ее через N. Произвольные структуры обычно будут обозначаться каллиграфическими буквами Д, Д,... , а их носители - М, N,...

Арифметика Бюхи с основанием р - это элементарная теория стандратной модели (N, S, +, 0, Vp). Мы будем обозначать эту теорию через ВА_р. Через п обозначается нумерал S(S (. .. S(0) ...)) = Sⁿ(0'), где п G N. Для п G N,п >  0 и терма t через nt обозначается терм

(... ((t + t) + t)... ).

⏟

⏟⏞ n раз

Конечным автоматом (сокращенно КА) над конечным алфавитом X (обычно в качестве X бу,дет {0,1,..., р — 1} пли {0,1,... ,р — 1}к) мы подразумеваем кортеж (X, Q, qo, F, А), где Q - конечное множество состояний, qo G Q - начальное состояние. F С Q - множество завершающих состояний, А С Q х X х Q ~ множество переходов. Детерменированным конечным автоматом (сокращенно ДКА) над алфавитом У мы подразумеваем КА, в котором А является функцией Q х У ^ Q (то еств для всех (q,a) G Q х У существует и единственно q' G Q такое, что (q,a,qr) G А). Для КА М мы обозначим через L(M) язык всех слов, которые принимаются автоматом М (будем также говоритв, что автомат М распознает язык L(M)).

Обозначим через У_р алфавит {0,...,р — 1}. Для произволвного w G У_р мы обозначим через [w]_p число wk-i p^k-1 + ••• + wo, г де w = wo ...wk-i (считаем, что [Л]_р = 0). Кроме того, для w G (У^)* мы положим [w]p = ([w1]_p,..., [w^k ]_р) G N^k, где (w^j )_i = (wi)j. Например, для р = 5 и к = 3 имеем [(1, 2, 3)(2, 3,1)(3,1, 2)]5 = (1 + 2 • 5 + 3 • 52, 2 + 3 • 5 + 1 • 52, 3 + 1 • 5 + 1 • 52) = (86,42, 33). Разумеется, [-]_р не является инъективным.

Будем говоритв, что А С N является р-распознаваемым, если язык L(A) := {w G yp|[w]_p G А} распознается (детерменированным) конечным автоматом. Кроме того, это понятие обобщается для подмножеств N^k. Скажем, что А С N^k является р-распознаваемым, если язык L(A) := {w G (Ур)*|[w]_p G А} распознается (детерменированным) конечным автоматом.

Мы будем использовать следующие хорошо известные факты про конечные автоматы.

Предложение 2.1. (г) Если М =     (У,Q,qo, F, А) является ДКА, то и

М ' := (У, Q, qo, Q \F, А) является ДКА и. кроме того. L(M ') = У* \ L(M ).

• (ii)    Если М₀    =    (У,Q₀,q₀,F₀, А₀) и М1    =    (У,Q₁ ,q1,F1, А1) являются

3.    Аксиоматизация

ДКА. то л М := (У,Q₀ х Q1, (q₀,q1),F₀ х F1, А) является ДКА. где А((q,q^,),a) = (А₀(q, a), А₁(q',a)). ii. кроме того. L(M ) = L(M₀ ) nL(M₁).

(Иг) Если М = (У, Q, qo, F, А) является КА, то существует ДКА М ' со множеством состояний V (Q) такой, что L(M ') = L(M ).

Мы будем обозначать нашу аксиоматизацию через Т ва_р-

Определение 3.1. Т ва_р состоит из следующих аксиом:

• (S 0)    Sx = Sy ^ х = у.

• (S 1)    0 = Sx;

• (S 2)    х = 0 V Эу(х = Sy):

(А0) х + 0 = х:

(А1) х + Sy = S(х + у):

(К0) Кр(0) = 0:

• (V1) Кр(1) = 1:

• ⁽V ²⁾ рр⁽р^х) = ррр^(х):

р—1

(V3) Л (Кр (рх + г) = 1): i=1

(Bound^) Эхр(х) ^ Эх ^ п_р ^(х), для всех формул ^(х) с одной свободной переменной, где 2³

п_р = р + .

Сначала мы покажем, что наша аксиоматизация является корректной.

Теорема 6. (N, S, +, 0, V_p) 1= Т _Ва_р (то есть ВА_Р к Т ва _р)-

Доказательство. Понятно, что аксиомы (S0) - (S2), (А0) - (А1), (V 0) - (V 3) истинны в стандартной модели. Остается показать, что схема (Bounds) выполияется в N.

Основная идея следующая. Рассмотрим произвольную формулу р и автомат М_р, распознающий множество, определяемое формулой р. Если существует слово, принимаемое автоматом М_р (то есть Зхр(х)), то тогда существует путь из начального состояния в некоторое конечное и, следовательно, существует слово, принимаемое этим автоматом, длина которого не превосходит количества состояний в М_р, скажем, т. Это значит, что существует число х G N, длина р-ичной записи которого не превосходит т (то есть х С p^m( такое что формула р(х) выполнена. Таким образом, нам надо оценить количество состояний в М_р.

Обозначим через Ав график функции S, то есть, множество {(х,у) G N|S(х) = у}, аналогично определим Ау_р, А₊ и А₌. Несложно построить ДКА Ms, Му_р, М₊ and М= с С 3 состояниями, которые распознают L(Аs ),L(Аy_р ),L(А₊) и L(А₌) соответственно.

Сначала разберем случай формул р(х±,..., Xk ), в которых все вхождения атомарных формул имеют вид х = у, S (х) = у, х + у = z или V_p(x) = у, где х, у, z суть различные переменные. Индукцией по построению р мы покажем, что существует ДКА, распознающий L({(n-,..., nk ) G N^k |N = р(п-,... ,nk )}) e нс более нем 2^ состояниями, где N_p - число булевых связок Л, V, Ми кванторов в р. Мы обозначим последнее множество через L_p.

Базовый случай атомарных формул уже разобран.

Если р(x₁,...,Xk ) = —ф(х_- ,...,Xk ), то Lф распознается с помощью ДКА М = (^k ,Q,q_o,F, A). IQI С 2^ . По Предложению 2.1. L_p распознается ДКА (KQ,qo,Q \F, A) I i|Q| С 2³^ = 2N/

Если

р(х-, ...,Xk ,у1,.. .,Уl,Z-, ... ,zm) = (фо(х-, ...,Xk ,у1,.. .,уф Лф-(у-, ...,у1 , z-, . . .,zm)), где {х-,... ,Xk,У1,... ,у1} - все различные свободные переменные в ^о и {у-,... ,у1, Z-,..., zm} - все различные свободные переменные в ф-, то Lф0 распознается ДКА

Мо = (Sp+l ,Qo,qo,Fo, Ао), где |Qo| С 2^ , и Lф1 распознается ДКА,

М- =(Sp+m,Qi,qi,Fi, А-), где |Q-| С 2^^ Положим М'о := ((Sp)k+l+m, Qo, qo, Fo, А0), где

A0(q, (a-,..., ak+i+m)) = A0(q, (a-,..., ak+i)), и М- := ((Sp)k+l+m,Q-,q-,F-, A-), где

^Al^(q, ^(al, . . . , ^ak+l+m⁾⁾ — ^Al^(q, ^(ak+-, . . . , ^ak+l+m^)).

Понятно, что L_p = L(M0 ) П К(М-). Используя Лемму 2.1, мы получаем, что существует ДКА М, распознающий L_p, с |Qo| • |Q-1 состояниями. Но ^|Qo| • ^|Q-| ^{С 2}^0 • ²^1 ^{С 2}^0 ₊n^ ₊- = ²N^-

Случаи р = (фо V ф_-) и р = (фо М ф_-) разбираются аналогично предыдущим, используя эквивалентности р о —(—фо Л —ф-) и р о —(фо Л —ф-) соответственно.

Если р(xl,...,Xk)     =      Зхф(хг,..., Xk ,х), то Lф распознается ДКА

М = ((S_p)^k+- ,Q,q_o,F, A). |Q| С 2^- Обозначим через М К A ((S_p)^k ,Q,q_o,F, A’), где A’ = {(q, (ay...,a_k ),q‘) G Q x (S_p)^k x Q|3a G S_p : (q, (ay...,a_k ,a),q‘) G A}. Неформально говоря, мы стёрли последний символ на каждом ребре нашего автомата. Тогда L_p распознается автоматом М ‘, но М ‘ может перестать быть детерминированным.

Для построения ДКА М ‘‘, распознагощего L^, применяем Лемму 2.1, тогда количество состояний в М‘‘ равно 2|^| < 22У¹ = 2^.

Случай р(х₁,... ,xk) = Чхф(х1,..., xk ,х) разбирается аналогично, исполвзуя эквива-лентноств р(х1, ..., xk) о —Зх—ф(х₁, ..., xk , х).

Теперв пуств р(х) - произволвная формула с одной свободной переменной. Тогда существует эквивалентная ей формула ф(х) такая, что все вхождения атомарных формул в ф(х~) имеют вид x = у, S (x) = у, x + у = z или V_p(x) = у, где x,y,z - различные переменные. Несложно видетв, что N_p С |^|- Значит, L({n G N|N k р(п)}) распознается ДКА с С 2^ состояниями.

Далее нам нужно показатв полноту нашей аксиоматизации, то еств что Т ва_р доказуемо каждое предложение в языке арифметики Бюхи, истинное в стандартной модели.

Теорема 7. Т_ВАр к ВА_р.

Мы предъявим два доказательства этого результата: синтаксическое и теоретикомодельное.

4.    Теоретико-модельное доказательство полноты

Напомним некоторые базовые определения (см., например, [8, 4.1]).

Определение 1. Пусть Т - теория первого порядка в некоторой сигнатуре а. (Частичным) типом в теории Т называется множество p(x) ст-формул от свободных переменных х = (xi,...,xn), локально совместное с Т (то есть, для любых т р-фх),..., рт(х) G p(x) теория T + Зх( Д р(х)) совместна).

k=i

Определение 2. Тип p(x) в теории T называется изолированным, если найдется формула р(х) такая, что T + Эхр(х) совместна т Т к Чх(р(х) ^ ф(х)) для всех ф(х) G р(х). В этом случае формулу р(х) называют изолирующей для типа р(х).

Мы начнем со следующей простой общей леммы.

Лемма 1. Пусть T - совместная теория в не более чем счетной сигнатуре, р(х) - неизолированный (возможно, неполный) тип в Тиф- совместное с T предложение. Тогда р(х) пс является изолироваппым в T + ф.

Доказательство. Пусть T, р(х) иф - как в формулировке. Рассуждая от противного, предположим, что существует формула р(х), которая изолирует р(х) в T + ф, то есть (T + ф) + Зх р(х) является совместной ii T + ф к Чх(р(х) ^ у(х)) для всех у(х) G р(х). Тогда для всех у(х) G р(х) имеем

T к ф ^ Чх(р(х) ^ у(х)),

T к Чх(ф ^ (р(х) ^ у(х))),

T к Чх(ф Л р(х) ^ у(х)).

Так как р(х) неизолирован в T, мы получаем, что T + Зх(ф Лр(х)) несовместна. Значит, (T + ф) + Зх р(х) несовместна, противоречие.

Доказательство теоремы 7. Допустим, найдется предложение ф, которое выполняется в стандартной модели и Т ва_р ^ ф- Тогда теория Т ва_р + —ф совместна. Рассмотрим р(х) = {х = п\п G N}.

Мы утверждаем, что р(х) не является изолированным в Т ва-_р- Допустим, найдется формула р(х) такая, что Т ва_р + Зх р(х) совместна и

Т ва_р к Чх(р(х) ^ х = п) для всех п G N.               (*)

Рассмотрим произвольную модель М к Т ва_р + Эхр(х). Используя (Bound_p), мы получаем п^

М к Эх С Пр ^(х). Так как Т ва_р к х С п^ о V (х ⁼ к) найдется некоторое к С п^ такое, k=0

что М к р(к). Но, подставляя к вместо пик вместо х в (*), мы получаем М к к = к, противоречие.

Итак, теория Т ва_р + —Ф совместна, р(х) не изолирован в Т ва-_р, значит, по Лемме 1, р(х) не является изолированным в Т ва_р +—ф- По теореме об опускании типов ([8, Теорема 4.1.2]), существует модель М к Т ва_р + —Ф, опускающая тип р(х). Так как М опускает тип р(х), каждый элемент т G М имеет вид п, п G N. Используя аксиомы (S 0) - (52), (АС) - (А1), (V 0) - (V 3). легко видеть, что + и рр определены стаялартяым образом на М. то есть М = (N, S, +, 0, ф). Но тогда М к ф, противоречие.

Также есть альтернативное теоретико-модельное доказательство, предложенное Э. Ержабеком в переписке. Идея этого доказательства состоит в том, чтобы показать, что стандартная модель элементарно вкладывается в произвольную модель Тва_р (^то есть является простой моделью этой теории), из этого тривиально следует полнота. Схема доказательства следующая: используя аксиомы (S0) - (S2), (АС) - (А1), (V0) - (V3), несложно показать, что стандартная модель является подмоделью произвольной модели, затем из схемы (Bound_^р) следует, что выполнены условия признака Тарского - Воота, следовательно, вложение элементарно.

5.    Синтаксическое доказательство полноты

Нам потребуются следующие элементарные леммы.

Лемма 2.   (1) Т'ва_р к п + т = п + т для всех п,т G N;

• (2)    Т ва_р к Рр(п) = ф(п) для всех п G N;

• (3)    Т ва_р к п = т для всех п,т G N, п = т'

• (4)    если t - замкнутый терм п п - его значение в стандартной модели, то Т ва_р к t = п;

п

• (5)    Тва_р к х С п о V (х = к) для всех п G N. k=0

Доказательство

• (1)    Доказательство может быть найдено в [6, Теорема 1.6].

• (2)    Индукция по п. Если п = 0 пли п = 1. это просто аксиома (V0) или (V1).

Предположим п > 1 и Твар к Vp(nL) = ф(п') для п' < п. Если р\п, то п = рп', п' < пи ф(п) = рVp (п'). Тогда

ТвАр к Ур(п) = Тр(рп');

к V_p(n) = ф(рп');                (применили (1) р раз)

к Ер(п) = рф(п');                                   (V2)

к V_p(n) = рV_p(n');           (предположение индукции)

к V_p(n) = рф(п');                 (применили (1) р раз)

к Ер(п) = Тр(п).

Если р \ п, то п = рп' + i, г де 0 < i < р. Следовательно, имеем

ТвАр к Vp(n) = Vp( рn' + i );

к ф(п) = У_р(рп‘ + i);           (применили (1) р + 1 раз)

кVp(n) = 1;                                            (V 3).

• (3)    Пусть n,m G N, п = т. Без ограничения общности будем считать п < т. Тогда, применяя (S 0) п раз, получаем Т ва_р Ь п = т ^ 0 = т — п . Применяя (S 1), получаем ТвАр Ь п = т-

• (4)    Простая ппдукщгм по построению t.

• (5)    См. [6. Теорема 1.6].

Лемма 3. Пусть 0 - бескванторное предложение. Если 0 истинно в стандартной модели, то Т ва_р Ь 0, иначе Т ва_р ।— '0-

Доказательство. Индукция по построению 0.

Пусть 0 - атомарная формула вида t = s, где t и s являются замкнутыми термами. Пусть п,т G N - значения термов t,s в стандартной модели. По Лемме 2 (4), Т'ва_р Ь t = п и Т ва_р Ь s = т- Ес ли N С t = s, топ = т и Т ва_р Ь t = s. Ес ли N Ь t = s, то п = т и по Лемме 2 (3), Тва_р Ь п = т, следовательно, Т ва_р Ь t = s.

Случаи булевых связок рассматриваются тривиальным образом.

Лемма 4. Пусть р - предложение, тогда существует бескванторное предложение 0 такое, что Т ва_р Ь р О 0.

Доказательство. Индукция по построению р. Заменяя все вхождения Ух на 'Зх', мы можем считать, что кванторы V не входят в р.

Если р атомарная, то доказывать нечего. Случаи булевых связок рассматриваются тривиально .

Пф

Пусть р = Зх^(х). Тогда по (Воипбф ) и Лемме 2 (5) получаем, что Тва_р Ь р О V ^(k). k=0

По предположению индукции найдутся бескванторные предложения 0g,..., 0_Пф такие, что Пф

Твар Ь ^(k) О 0k для всех k < п,ф. Тогда Твар Ь р О \J 0k- k=0

Доказательство Теоремы 7. Допустим N Ср, где р - предложение. Применяя Леммы 4 и 3, получаем Т ва_р Ь р.

Замечание. Как отметил Э. Ержабек, от аксиом (V 0) и (V 1) можно избавиться. Действительно, (V1) - это частный случай (V3), так как 1 = р0 + 1 (по модулю предыдущих аксиом). Аксиома (V0) выводится несколько сложнее. По (V2) мы имеем ф(0) = рф(0). Нам надо показать, что х = рх ^ х = 0. Из схемы (Воипд^) несложно вывести схему бес-параметрической индукции, откуда, в свою очередь, выводится схема индукции для всех формул. С помощью индукции легко выводится закон сокращения х + z = у + z ^ х = у. Тогда получаем, что х = рх ^ 0 = (р — 1)х и, значит, х = рх ^ х = 0 (используя аксиомы для S 11 +).

Данная работа поддеражана фондом «БАЗИС» как часть проекта №22-7-2-32-1.