История изменений

Теория моделей там ->

Зачем тут это воспроизводить?

В какой теории типов?

Которая большими буковками Теория Типов (по крайней мере, в некоторой литературе). Но в данном контексте не важно что за метатеория ZF+... / CZF+... / MLTT+..., речь о _метатеории_ в рамках которой можно формулировать другие теории и модели (заниматься теорией моделей).

аксиому арифметики Пеано о непредшествовании нуля она содержит, а значит толку от нее?

См. выше. Например, на уровне теории типов пакуешь себе набор утверждений (аксиом) в теорию, выводишь теоремы которые следуют из них (метатеоретическими силами), любую реализацию этих аксиом видишь как модель — теоремы на них автоматически распространяются.

Например, теория — https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Structures.agda#L83. Её теоремы — https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Properties/Group..... Модель — https://github.com/agda/agda-stdlib/blob/master/src/Data/Integer/Properties.a....

PA (PA++ :)) себе так же можно сделать и взять стандартный \bn за модель. Как и Unsigned : NumberOfBit -> Set — если хочешь рассуждать про такой тип (~ Z/(2^n)Z, да) и такие программы (с переполнениями), то для начала нужно его проговорить, вместе со всем сопутствующим, что предполагает соответствующую теорию, явно или нет. Или лучше не нужно — все эти вещи могут быть неявными, но вполне очевидными.

Естественно, всё в контексте именно компьютерной формализации.

конкретные кольца являются моделями этой общей теории, а не теориями сами по себе

Я имею полное право строить себе теории Z/5Z и т.п. К примеру, теорию для uint64_t, или сразу Z/nZ для всех натуральных n. Но вовсе не общую теорию колец.

Зачем? Надо просто вложить нашу усеченную Пеано в арифметику Пеано. При этом из модели N для усеченной Пеано можно сделать модель Z_n понятным гомоморфизмом.

Сходи сделай («статически доказать, что приведённые fib1 и fib2 эквивалентны на uint*_t»).

Теория моделей там ->

Зачем тут это воспроизводить?

В какой теории типов?

Которая большими буковками Теория Типов (по крайней мере, в некоторой литературе). Но в данном контексте не важно что за метатеория ZF+... / CZF+... / MLTT+..., речь о _метатеории_ в рамках которой можно формулировать другие теории и модели (заниматься теорией моделей).

аксиому арифметики Пеано о непредшествовании нуля она содержит, а значит толку от нее?

См. выше. Например, на уровне теории типов пакуешь себе набор утверждений (аксиом) в теорию, выводишь теоремы которые следуют из них (метатеоретическими силами), любую реализацию этих утверждений видишь как модель.

Например, теория — https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Structures.agda#L83. Её теоремы — https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Properties/Group..... Модель — https://github.com/agda/agda-stdlib/blob/master/src/Data/Integer/Properties.a....

PA (PA++ :)) себе так же можно сделать и взять стандартный \bn за модель. Как и Unsigned : NumberOfBit -> Set — если хочешь рассуждать про такой тип (~ Z/(2^n)Z, да) и такие программы (с переполнениями), то для начала нужно его проговорить, вместе со всем сопутствующим, что предполагает соответствующую теорию, явно или нет. Или лучше не нужно — все эти вещи могут быть неявными, но вполне очевидными.

Естественно, всё в контексте именно компьютерной формализации.

конкретные кольца являются моделями этой общей теории, а не теориями сами по себе

Я имею полное право строить себе теории Z/5Z и т.п. К примеру, теорию для uint64_t, или сразу Z/nZ для всех натуральных n. Но вовсе не общую теорию колец.

Зачем? Надо просто вложить нашу усеченную Пеано в арифметику Пеано. При этом из модели N для усеченной Пеано можно сделать модель Z_n понятным гомоморфизмом.

Сходи сделай («статически доказать, что приведённые fib1 и fib2 эквивалентны на uint*_t»).