Ультрафинитные арифметики

[nasldfhgon]

Пусть n какое-то натуральное число. Формальную систему UF(n), которая будет определена далее, будем называть ультрафинитной арифметикой.
Возьмём логику предикатов с равенством. Пусть "$S$" будет функциональным символ с арностью единица. Введём константу "0". Будем обозначать через $L(k)$ терм $S(S(...S(0)...))$, где $S$ встречается ровно $k$ раз. Хочу обратить внимание, что $L(k)$ -- это не терм формальной системы, это метаобозначение: под ним везде далее нужно понимать вышеприведённый терм. $L(n)$ будем обозначать просто через $L$. Добавим к предикатным символам символ "$<$". Добавим функциональные символы "$+$", "$\cdot$". Аксиомы:
A1. $0<L$
A2. Схема аксиом. Для любого $m<n$: $L(m)<L$
A3. $\forall a(a<L \Rightarrow S(a)\neq 0)$
A4. $\forall a \forall b((a<L\land b<L) \Rightarrow (S(a)=S(b)\Rightarrow a=b))$
A5. Схема аксиом. Для любого предиката $P(x)$: $P(0)\land \forall a (a<L \Rightarrow (P(a)\Rightarrow P(S(a))))\Rightarrow \forall a((a<L \lor a=L)\Rightarrow P(a))$. Для предикатов большей арности формулировка аналогична.
A6. $\forall a ((a<L \lor a=L) \Rightarrow a+0=a)$
A7. $\forall a\forall b(a+b<L\Rightarrow a+S(b)=S(a+b))$
A8. $\forall a ((a<L\lor a=L) \Rightarrow a\cdot 0=0)$
A9. $\forall a \forall b( a+(a\cdot b)<L \Rightarrow a\cdot S(b)=a+(a\cdot b))$
A10. $\forall a \forall b (a<b \Leftrightarrow \exists c(c+a<L\Rightarrow c+S(a)=b))$

(Оффтоп)

Докажем, например, что $0<S(0)$:
(1) $0<S(0)\Leftrightarrow \exists c(c+0<L\Rightarrow c+S(0)=S(0))$ из A10.
(2) $0+0<L\Rightarrow 0+S(0)=S(0+0)$ из A7.
(3) $(0<L \lor 0=L) \Rightarrow 0+0=0$ из A6.
(4) $0+0=0$ из (3) и A1.
(5) $0+0<L\Rightarrow 0+S(0)=S(0)$ из (4) и (2).
(6) $\exists c(c+0<L\Rightarrow c+S(0)=S(0))$ из (5).
(7) $0<S(0)$ из (6) и (1).

Таким образом, мы получили семейство формальных систем UF: при каждом фиксированном $n$ мы получаем формальную систему UF(n). У меня есть подозрение, что каждая UF(n) не полна (хотя, думаю, если добавить ещё одну схему аксиом, что для любого $m>n$: $\neg(L(m)<L)$, то будет полной). Но мне кажется, что можно доказать их непротиворечивость и разрешимость. Честно говоря, у меня пока нету времени на то, чтобы заняться выяснением этих догадок. Также интересно, если они разрешимы, то какова вычислительная сложность.
Кстати, каждый компьютер, очевидно, может работать только в рамках некой UF(n), где $n$ - количество памяти. Поэтому, я считаю, исследование ультрафинитных арифметик имеет очевидное прикладное значение.
Также заранее извиняюсь, если изобрёл очередной велосипед -- не скрываю, что я дилетант.

[migmit]

1) A1 является частным случаем A2 при $m=0$.

2) A10 сформулировано, видимо, неверно, надо так:

$$\forall a\forall b(a<b\Leftrightarrow\exists c(c+a<L\wedge c+S(a)=b))$$

3) Утверждение про компьютер не вполне понятно. Компьютер - физическое устройство, он в рамках формальной системы не работает. А для описания его работы эта UF подходит плохо (хотя бы потому, что L+L для компьютера будет иметь вполне определённое значение).

[nasldfhgon]

migmit в сообщении #814646 писал(а):

1) A1 является частным случаем A2 при $m=0$.

2) A10 сформулировано, видимо, неверно, надо так:

$$\forall a\forall b(a<b\Leftrightarrow\exists c(c+a<L\wedge c+S(a)=b))$$

Да. Согласен.

migmit в сообщении #814646 писал(а):

3) Утверждение про компьютер не вполне понятно. Компьютер - физическое устройство, он в рамках формальной системы не работает.

Я имел в виду, что компьютер не может использовать больше ячеек памяти, чем в нем есть в данный момент.

[migmit]

nasldfhgon в сообщении #814714 писал(а):

migmit в сообщении #814646 писал(а):

Я имел в виду, что компьютер не может использовать больше ячеек памяти, чем в нем есть в данный момент.

Это-то понятно, непонятно, какое отношение к этому имеет UF. Термов там бесконечно много, только известно про них мало что. В компьютере числа ограничены сверху и арифметика на них существенно другая.

[nasldfhgon]

migmit в сообщении #814732 писал(а):

Это-то понятно, непонятно, какое отношение к этому имеет UF.

Например, если $L(k)$ интерпретировать как номер k-й ячейки. Мы не можем сказать верно либо нет $S(L)\neq 0$. Оно не имеет смысла т.к. в данном компьютере нету ячейки с таким номером.
Или другой пример: под сложением чисел $k$ и $m$ понимать, в частности, "записать в память (которая, допустим, представляет собой набор ячеек, которые могут иметь значения $0$ и $1$) ровно $k+m$ единиц последовательно в участок начинающийся с первой ячейки". Тогда $L+L$ и любые высказывания о нём тоже не имеет смысла, т.к. невозможно проделать такую операцию.

[migmit]

Ну дык вот если вы найдёте компьютер, в котором хотя бы основные операции укладываются в эту схему, то можно будет говорить о том, что "компьютер работает в рамках UF". И то, только про этот конкретный компьютер.