По мотивам арифметики Пеано

Вот аксиоматизация (одна из возможных) теории двоичных строк.

Теория содержит исчисление предикатов с равенством, а так же дополнительно константу \(\varepsilon\) (пустая строка), два унарных функциональных символа \(+0, +1\) (приписывание нуля и единицы справа) и бинарный функциональный символ \(+\) (конкатенация). (На этом конец, т. к. лексикографический порядок вводить лень.)

Собственные (т. е. не относящиеся к исчислению предикатов с равенством) аксиомы таковы:

  1. \(x+0\ne\varepsilon\),
  2. \(x+1\ne\varepsilon\),
  3. \(x+1\ne x+0\),
  4. \(x+0=y+0\to x=y\),
  5. \(x+1=y+1\to x=y\),
  6. \(x+\varepsilon=x\),
  7. \(x+(y+0) = (x+y)+0\),
  8. \(x+(y+1) = (x+y)+1\) — три аксиомы, индуктивно определяющие конкатенацию,
  9. \(\phi[\varepsilon/x] \wedge \forall x\left( \phi\to\phi[x+0/x]\wedge\phi[x+1/x] \right) \to \forall x(\phi)\) — это схема аксиом индукции, по аксиоме на каждую формулу \(\phi\).

Вроде, ничего не упущено. (По крайней мере, с этим набором точно можно доказать простые факты вида \(\varepsilon+0+\varepsilon+1=\varepsilon+0+1\) ("0" + "1" == "01") и другие формулы, аналогичные \(2+2=4\) арифметики.)

Не знаю, кому и зачем это могло бы вообще пригодиться, так как пишется за раз.

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

:) :D :( :E: ;) :yes: :no: :donno: more »