Существует ли биекция между вычислимыми числами и нат.?

[epros]

маткиб писал(а):

Если Вы принимаете аксиому индукции в арифметике Пеано без всяких ограничений...

Принимаю схему индукции без ограничений как в самой арифметике, так и в любой мета-теории, использующей понятие натурального числа.

маткиб писал(а):

... т.е., добавив к арифметике Пеано схему аксиом $(\forall x)((\mathrm{PA}\vdash\Phi(x))\rightarrow\Phi(x))$ (т.е. равномерную схему рефлексии), получим теорему Гудстейна.

Идея заключается в том, что нам не надо добавлять к арифметике новые аксиомы, то бишь "обогащать её содержание". Достаточно расширить возможности синтаксиса.

маткиб писал(а):

На каком основании конструктивисты принимают аксиому индукции в таком "общем" виде, я, естественно, не понял. Мне кажется, что такое принятие автоматически зачисляет конструктивиста в ряды классических математиков.

Очевидно, что это не так. Конструктивисты как правило не брезгуют идукцией, и это ещё никого из них не сделало классическим математиком, т.е. не заставило принять закон исключённого третьего, аксиому бесконечности и т.п.

маткиб писал(а):

Проверить Ваше доказательство я не готов, ибо это тяжкий труд (на который я не способен), поэтому я верю Вам на слово.

Мне это странно, ибо с моей точки зрения это есть довольно простое доказательство самым прямым методом, т.е. "в лоб".

маткиб писал(а):

epros писал(а):

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

Продемонстрируйте, и укажите эти средства, потом я скажу своё мнение на этот счёт.

Для доказательства в арифметике нам не хватает возможности записать серию формул (0) - (m+2) одной общей формулой $\Phi(k,m)$ с параметрами k (номер формулы) и m ("этажность" чисел, до которой распространяется доказательство).

Поглядев на общий вид формулы (k), легко заметить, что единственное препятствие этому - невозможность записать одним арифметическим выражением список переменных переменной длины, т.е. то, что я обозначал как $m_1, ... ,m_k$. Если добавить эту возможность к стандартному синтаксису, то мы получим:
- Определение функции $\Lambda_k(n, m_1, ... , m_k)$ запишется формулой арифметики. (До сих пор мы могли выписать определения только до некоторого заданного m, но не общее определение для любого m).
- Формулы (0) - (m+2) запишутся одной общей формулой $\Phi(k,m)$.
- Индукцией (в рамках арифметики) по параметру $m_k$ можно будет доказать $(\forall k,m)(\Phi(k+1,m) \to \Phi(k,m))$.
- Индукцией (в рамках арифметики) по параметру $k$ от $k=m+2$ до $k=0$ можно будет доказать $(\forall m)\Phi(0,m)$.
- А поскольку $(\forall m)\Phi(0,m)$ сама по себе является предпосылкой индукции, то индукцией (в рамках арифметики) по параметру $m$ можно будет доказать Теорему Гудстейна.

маткиб писал(а):

Последний абзац не осилил. Сначала нужно придумать правдоподобные аксиомы для теории T, а потом уже рассуждать о том, что из них что-то там следует.

Считайте, что аксимоматика теории $T$ определена (и включает схему индукции).

маткиб писал(а):

У Вас же первая формула не определяет никаких аксиом T, ни даже правил вывода, но Вы почему-то делаете вывод, что аксиомы индукции оттуда следуют как теоремы. Каков смысл?

Первая формула и не должна определять никаких аксиом. И из неё не следуют аксиомы индукции для теории $T$. Эта формулировка означает, что мы можем применять индукцию на мета-уровне. Т.е. если мы можем в метатеории доказать, что $P(n) \to P(n+1)$ доказуемо в $T$ для любого $n$, то мы можем отсюда заключить, что $P(n)$ доказуемо в $T$ для любого $n$. Почему? А потому, что метатеория может продемонстрировать вывод для любого заданного $n$, пройдя все шаги индукции до него и на каждом шаге приводя отдельное доказательство $P(n) \to P(n+1)$ в $T$. Это не смотря на то, что в $T$ может не быть общего доказательства $P(n) \to P(n+1)$ для всех $n$, т.е. вот этого: $(\forall n)(P(n) \to P(n+1))$.

[маткиб]

epros писал(а):

маткиб писал(а):

На каком основании конструктивисты принимают аксиому индукции в таком "общем" виде, я, естественно, не понял. Мне кажется, что такое принятие автоматически зачисляет конструктивиста в ряды классических математиков.

Очевидно, что это не так. Конструктивисты как правило не брезгуют идукцией, и это ещё никого из них не сделало классическим математиком, т.е. не заставило принять закон исключённого третьего, аксиому бесконечности и т.п.

Не очевидно. И некоторые "настоящие" конструктивисты принимают индукцию только в ограниченном виде.

epros писал(а):

Для доказательства в арифметике нам не хватает возможности записать серию формул (0) - (m+2) одной общей формулой $\Phi(k,m)$ с параметрами k (номер формулы) и m ("этажность" чисел, до которой распространяется доказательство).

Если имеются в виду формулы отсюда, то они прекрасно записываются одной формулой без всяких расширений. Так что ищите ошибку в доказательстве (либо другое место, которое не делается в арифметике).

epros писал(а):

маткиб писал(а):

Последний абзац не осилил. Сначала нужно придумать правдоподобные аксиомы для теории T, а потом уже рассуждать о том, что из них что-то там следует.

Считайте, что аксимоматика теории $T$ определена (и включает схему индукции).

Это плохо. Неконструктивно.

epros писал(а):

маткиб писал(а):

У Вас же первая формула не определяет никаких аксиом T, ни даже правил вывода, но Вы почему-то делаете вывод, что аксиомы индукции оттуда следуют как теоремы. Каков смысл?

Первая формула и не должна определять никаких аксиом. И из неё не следуют аксиомы индукции для теории $T$. Эта формулировка означает, что мы можем применять индукцию на мета-уровне. Т.е. если мы можем в метатеории доказать, что $P(n) \to P(n+1)$ доказуемо в $T$ для любого $n$, то мы можем отсюда заключить, что $P(n)$ доказуемо в $T$ для любого $n$. Почему? А потому, что метатеория может продемонстрировать вывод для любого заданного $n$, пройдя все шаги индукции до него и на каждом шаге приводя отдельное доказательство $P(n) \to P(n+1)$ в $T$. Это не смотря на то, что в $T$ может не быть общего доказательства $P(n) \to P(n+1)$ для всех $n$, т.е. вот этого: $(\forall n)(P(n) \to P(n+1))$.

Вся эта хрень относится к такому правилу вывода в теории T:

$$ \frac{P(0),\ (\forall n)(P(n)\rightarrow P(n+1))}{(\forall n)P(n)} $$

Это правило я готов принять как конструктивное, но оно скорее всего слабее схемы индукции.

[epros]

маткиб писал(а):

Не очевидно. И некоторые "настоящие" конструктивисты принимают индукцию только в ограниченном виде.

Например? Что это за "ограниченный вид"?

маткиб писал(а):

Если имеются в виду формулы отсюда,

Можете взять здесь те же формулы, которые чуть позже были записаны чуть более формально:

(0)

$$\forall n (Z_n(\Lambda_{m+2}(n,2,0,...,0))) \to \forall n (Z_n(\Lambda_{m+3}(n,2,0,...,0)))$$

(k)

$$\forall m_1,..., m_k (\forall n (Z_n(\Lambda_{m+2}(n,m_1,..., m_k, 0,..., 0))) \to \forall n (Z_n(\Lambda_{m+2}(n,m_1,..., m_{k-1}, m_k+1, 0,..., 0))))$$

маткиб писал(а):

то они прекрасно записываются одной формулой без всяких расширений.

В таком случае некоторые бы спросили: "Доказательство?"

Для начала хотя бы продемонстрируйте как записать одной формулой арифметики определение функции $\Lambda_k(n,m_1,...,m_k)$. Нет, я прекрасно понимаю, как одной формулой записываются рекурсивные определения функций. Например, рекурсивное определение функции $r_k(x)$:

$$(\forall x,k)(r_{k+1}(x) = f(r_k(x),k,x) \wedge r_1(x) = g(x))$$

где $g(x)$ и $f(y,k,x)$ - арифметические функции.

Но попробуйте проделать то же самое для функции, количество аргументов которой зависит от $k$.

маткиб писал(а):

epros писал(а):

Считайте, что аксимоматика теории $T$ определена (и включает схему индукции).

Это плохо. Неконструктивно.

Это почему? Мы рассматриваем некую теорию, у которой есть некая аксиоматика. Это - вполне конструктивно. А уж конструктивна или нет сама рассматриваемая теория - это другой вопрос.

маткиб писал(а):

Вся эта хрень относится к такому правилу вывода в теории T:

$$ \frac{P(0),\ (\forall n)(P(n)\rightarrow P(n+1))}{(\forall n)P(n)} $$

Это правило я готов принять как конструктивное, но оно скорее всего слабее схемы индукции.

маткиб, Вы меня разочаровываете. Внимательнее что-ли будьте. Речь шла о том, что теоремы $(\forall n)(P(n)\rightarrow P(n+1))$ нет в теории, так что Ваше правило вывода бесполезно. Кстати, оно не слабее и не сильнее аксиомы индукции, ибо вместе с правилом вывода modus ponens аксиома индукции означает в точности то же самое.

[маткиб]

epros писал(а):

Например? Что это за "ограниченный вид"?

Например, такие формулы, у которых под квантором $(\exists x)$ стоят формулы вида $(x\leq 2^y\&\Phi)$, а под квантором $(\forall x)$ - вида $(x\leq 2^y\rightarrow\Phi)$, при этом способ записи $x\leq 2^y$ в исходном синтаксисе заранее оговаривается. Тем самым мы как бы заранее определяем, сколько значений нужно перебрать для вычисления значения формулы, т.е. исключаем бесконечный перебор и неразрешимости.

epros писал(а):

маткиб писал(а):

Если имеются в виду формулы отсюда,

Можете взять здесь те же формулы, которые чуть позже были записаны чуть более формально:

(0)

$$\forall n (Z_n(\Lambda_{m+2}(n,2,0,...,0))) \to \forall n (Z_n(\Lambda_{m+3}(n,2,0,...,0)))$$

(k)

$$\forall m_1,..., m_k (\forall n (Z_n(\Lambda_{m+2}(n,m_1,..., m_k, 0,..., 0))) \to \forall n (Z_n(\Lambda_{m+2}(n,m_1,..., m_{k-1}, m_k+1, 0,..., 0))))$$

маткиб писал(а):

то они прекрасно записываются одной формулой без всяких расширений.

В таком случае некоторые бы спросили: "Доказательство?"

А что тут доказывать, если всё делается стандартной техникой, которая громоздка, но описана в любом учебнике по матлогике?

epros писал(а):

Для начала хотя бы продемонстрируйте как записать одной формулой арифметики определение функции $\Lambda_k(n,m_1,...,m_k)$. Нет, я прекрасно понимаю, как одной формулой записываются рекурсивные определения функций. Например, рекурсивное определение функции $r_k(x)$:

$$(\forall x,k)(r_{k+1}(x) = f(r_k(x),k,x) \wedge r_1(x) = g(x))$$

где $g(x)$ и $f(y,k,x)$ - арифметические функции.

Но попробуйте проделать то же самое для функции, количество аргументов которой зависит от $k$.

Переменное число переменных - не проблема, ибо векторы (в том числе переменной длины) можно кодировать числами. Конечно, формулы немного переделать придётся, но суть от этого не меняется.

Кстати, у меня есть предположение, где у Вас ошибка в доказательстве теоремы Гудстейна. В индуктивном переходе от n-этажных выражений к (n+1)-этажным. Дело в том, что Ваши формулы утверждают о сходимости конкретного процесса, в котором на каждом шагу числа уменьшаются ровно на единицу, и основание системы счисления тоже увеличивается ровно на единицу. А для доказательства сходимости (n+1)-этажных выражений Вам видимо приходится пользоваться утверждением о сходимости n-этажных, где, например, уменьшение на 1 происходит не обязательно на каждом шаге. Например, если понаблюдать за n-этажными показателями степеней (n+1)-этажных выражений в процессе преобразования, то можно заметить, что они уменьшаются далеко не на каждом шаге (даже если не рассматривать ситуации, когда они увеличиваются). Короче говоря, в Вашей индукции каждая формула не будет иметь никакой пользы для доказательства следующей.

epros писал(а):

маткиб писал(а):

epros писал(а):

Считайте, что аксимоматика теории $T$ определена (и включает схему индукции).

Это плохо. Неконструктивно.

Это почему? Мы рассматриваем некую теорию, у которой есть некая аксиоматика. Это - вполне конструктивно. А уж конструктивна или нет сама рассматриваемая теория - это другой вопрос.

Вот именно этот вопрос наиболее интересен.

epros писал(а):

маткиб писал(а):

Вся эта хрень относится к такому правилу вывода в теории T:

$$ \frac{P(0),\ (\forall n)(P(n)\rightarrow P(n+1))}{(\forall n)P(n)} $$

Это правило я готов принять как конструктивное, но оно скорее всего слабее схемы индукции.

маткиб, Вы меня разочаровываете. Внимательнее что-ли будьте. Речь шла о том, что теоремы $(\forall n)(P(n)\rightarrow P(n+1))$ нет в теории, так что Ваше правило вывода бесполезно.

Я перестаю это понимать.

epros писал(а):

Кстати, оно не слабее и не сильнее аксиомы индукции, ибо вместе с правилом вывода modus ponens аксиома индукции означает в точности то же самое.

Я не понимаю, как из моего правила вывода и modes ponens получить схему индукции.

[epros]

маткиб писал(а):

Например, такие формулы, у которых под квантором $(\exists x)$ стоят формулы вида $(x\leq 2^y\&\Phi)$, а под квантором $(\forall x)$ - вида $(x\leq 2^y\rightarrow\Phi)$, при этом способ записи $x\leq 2^y$ в исходном синтаксисе заранее оговаривается. Тем самым мы как бы заранее определяем, сколько значений нужно перебрать для вычисления значения формулы, т.е. исключаем бесконечный перебор и неразрешимости.

И сколько же именно значений "нужно перебрать"? Вы понимаете, что $y$ - это лишняя свободная переменная в формуле, а значит, чтобы с формулой можно было работать, нужно определить, что с этой переменной делать (варианты: 1. квантифицировать, 2. заменить конкретной константой)?

Вообще, к конструктивизму это всё уже не имеет непосредственного отношения. В конструктивном анализе принята абстракция потенциальной осуществимости, которая как раз и означает, что конкретный предел для индукции нам устанавливать не нужно.

маткиб писал(а):

Переменное число переменных - не проблема, ибо векторы (в том числе переменной длины) можно кодировать числами. Конечно, формулы немного переделать придётся, но суть от этого не меняется.

Мне эта "суть" пока что не очевидна. Я не понимаю, как можно записать формулу с квантором по $m_k$, если эта переменная - одна из списка, "закодированного" числами.

маткиб писал(а):

А для доказательства сходимости (n+1)-этажных выражений Вам видимо приходится пользоваться утверждением о сходимости n-этажных,

Разумеется так. Я не понял, Вы вообще смотрели мои посты? Именно этому и посвящена формула (0): Она утверждает, что если сходятся m-этажные выражения, то сходятся и m+1-этажные.

маткиб писал(а):

где, например, уменьшение на 1 происходит не обязательно на каждом шаге.

А нигде и не утверждается, что уменьшение этажности происходит "на каждом шаге".

маткиб писал(а):

Например, если понаблюдать за n-этажными показателями степеней (n+1)-этажных выражений в процессе преобразования, то можно заметить, что они уменьшаются далеко не на каждом шаге (даже если не рассматривать ситуации, когда они увеличиваются). Короче говоря, в Вашей индукции каждая формула не будет иметь никакой пользы для доказательства следующей.

Здесь я совершенно ничего не понял. Каждая формула "имеет пользу для доказательства предыдущей" не потому, что где-то что-то утверждается про уменьшение показателей степеней "на каждом шаге". Просто если положить в предпосылке $m_k = 0$, то это совпадает с предпосылкой предыдущей формулы. А если выполнить индукцию с $m_k = 0$ до $m_k = (n-1) n^{\Lambda_{k-1}(n,m_1, \cdots ,m_{k-1})}$, то в качестве следствия получим правую часть предыдущей формулы.

маткиб писал(а):

epros писал(а):

Это почему? Мы рассматриваем некую теорию, у которой есть некая аксиоматика. Это - вполне конструктивно. А уж конструктивна или нет сама рассматриваемая теория - это другой вопрос.

Вот именно этот вопрос наиболее интересен.

Что интересно? Конструктивна ли арифметика? Насколько я знаю, есть даже такое понятие как "интуиционистская арифметика" или "арифметика Гейтинга", которая отличается от классической арифметики первого порядка только отсутствием закона исключённого третьего.

маткиб писал(а):

epros писал(а):

маткиб писал(а):

Вся эта хрень относится к такому правилу вывода в теории T:

$$ \frac{P(0),\ (\forall n)(P(n)\rightarrow P(n+1))}{(\forall n)P(n)} $$

Это правило я готов принять как конструктивное, но оно скорее всего слабее схемы индукции.

маткиб, Вы меня разочаровываете. Внимательнее что-ли будьте. Речь шла о том, что теоремы $(\forall n)(P(n)\rightarrow P(n+1))$ нет в теории, так что Ваше правило вывода бесполезно.

Я перестаю это понимать.

Ваша неожиданно появившаяся непонятливость меня озадачивает. Чтобы воспользоваться указанным Вами правилом вывода, нам нужно иметь доказанным в теории следующее утверждение: $(\forall n)(P(n)\rightarrow P(n+1))$. А этого-то у нас как раз и нет. Мы можем доказать только $P(n)\rightarrow P(n+1)$ для любого наперёд заданного $n$.

маткиб писал(а):

epros писал(а):

Кстати, оно не слабее и не сильнее аксиомы индукции, ибо вместе с правилом вывода modus ponens аксиома индукции означает в точности то же самое.

Я не понимаю, как из моего правила вывода и modes ponens получить схему индукции.

Вы опять же невнимательны. Я не сказал: "Ваше правило вывода вместе с modes ponens". Я сказал "аксиома индукции вместе с modus ponens". Аксиома индукции имеет вид $A \wedge B \rightarrow C$, так что когда мы имеем $A$ и $B$, то по правилу modus ponens мы получаем вывод $C$. Это буквально то же самое, что делает Ваше правило вывода.

[маткиб]

epros писал(а):

И сколько же именно значений "нужно перебрать"? Вы понимаете, что $y$ - это лишняя свободная переменная в формуле, а значит, чтобы с формулой можно было работать, нужно определить, что с этой переменной делать (варианты: 1. квантифицировать, 2. заменить конкретной константой)?

Ну в индукции вообще-то рассматривается формула $P(n)$ со свободной переменной (схема индукции $P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n)$), а остальные свободные, естественно, нужно заменить константами.

epros писал(а):

Вообще, к конструктивизму это всё уже не имеет непосредственного отношения. В конструктивном анализе принята абстракция потенциальной осуществимости, которая как раз и означает, что конкретный предел для индукции нам устанавливать не нужно.

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

epros писал(а):

маткиб писал(а):

Переменное число переменных - не проблема, ибо векторы (в том числе переменной длины) можно кодировать числами. Конечно, формулы немного переделать придётся, но суть от этого не меняется.

Мне эта "суть" пока что не очевидна. Я не понимаю, как можно записать формулу с квантором по $m_k$, если эта переменная - одна из списка, "закодированного" числами.

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

epros писал(а):

маткиб писал(а):

А для доказательства сходимости (n+1)-этажных выражений Вам видимо приходится пользоваться утверждением о сходимости n-этажных,

Разумеется так. Я не понял, Вы вообще смотрели мои посты? Именно этому и посвящена формула (0): Она утверждает, что если сходятся m-этажные выражения, то сходятся и m+1-этажные.

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

epros писал(а):

маткиб писал(а):

где, например, уменьшение на 1 происходит не обязательно на каждом шаге.

А нигде и не утверждается, что уменьшение этажности происходит "на каждом шаге".

А я и не пишу про уменьшение этажности. Меня интересуют уменьшение числа и увеличение основания системы счисления (т.е. две основные операции, на основе которых строится последовательность Гудстейна).

epros писал(а):

Здесь я совершенно ничего не понял. Каждая формула "имеет пользу для доказательства предыдущей" не потому, что где-то что-то утверждается про уменьшение показателей степеней "на каждом шаге". Просто если положить в предпосылке $m_k = 0$, то это совпадает с предпосылкой предыдущей формулы. А если выполнить индукцию с $m_k = 0$ до $m_k = (n-1) n^{\Lambda_{k-1}(n,m_1, \cdots ,m_{k-1})}$, то в качестве следствия получим правую часть предыдущей формулы.

Я не буду утверждать, что это неправда, ибо до конца "ниасилил" доказательство. Просто приведу пример. Пусть, например, Вы доказали теорему Гудстейна для какого-то числа этажей. А теперь рассмотрим процесс, при котором основание системы счисления на каждом шаге увеличивается не на 1, а на 2. Тогда Ваше доказательство уже применить не получится, придётся писать новое доказательство. А если оно изменяется как-то ещё более хитро, например, увеличивается в 2 раза, то придётся писать ещё одно доказательство. И так далее: для каждого конкретного случая своё доказательство. И при сведении случая с каким-то числом этажей к случаю с меньшим числом этажей возникают как раз такие ситуации.

epros писал(а):

Что интересно? Конструктивна ли арифметика? Насколько я знаю, есть даже такое понятие как "интуиционистская арифметика" или "арифметика Гейтинга", которая отличается от классической арифметики первого порядка только отсутствием закона исключённого третьего.

Есть много всего. Другой вопрос, а имеет ли это смысл.

epros писал(а):

Ваша неожиданно появившаяся непонятливость меня озадачивает.

А что Вы хотите после 30-страничного переливания из пустого в порожнее?

epros писал(а):

Чтобы воспользоваться указанным Вами правилом вывода, нам нужно иметь доказанным в теории следующее утверждение: $(\forall n)(P(n)\rightarrow P(n+1))$. А этого-то у нас как раз и нет. Мы можем доказать только $P(n)\rightarrow P(n+1)$ для любого наперёд заданного $n$.

И что в этом хорошего для конструктивности арифметики?

epros писал(а):

маткиб писал(а):

epros писал(а):

Кстати, оно не слабее и не сильнее аксиомы индукции, ибо вместе с правилом вывода modus ponens аксиома индукции означает в точности то же самое.

Я не понимаю, как из моего правила вывода и modes ponens получить схему индукции.

Вы опять же невнимательны. Я не сказал: "Ваше правило вывода вместе с modes ponens". Я сказал "аксиома индукции вместе с modus ponens". Аксиома индукции имеет вид $A \wedge B \rightarrow C$, так что когда мы имеем $A$ и $B$, то по правилу modus ponens мы получаем вывод $C$. Это буквально то же самое, что делает Ваше правило вывода.

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

[epros]

маткиб писал(а):

Ну в индукции вообще-то рассматривается формула $P(n)$ со свободной переменной (схема индукции $P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n)$),

Вы меня просто ошарашиваете. Где же здесь $n$ свободная переменная, если она везде квантифицирована?

маткиб писал(а):

а остальные свободные, естественно, нужно заменить константами.

Какими константами?

маткиб писал(а):

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

Не понял проблемы. Можно на примере?

маткиб писал(а):

А если несколько одинаковых кванторов в формуле идут подряд (пусть даже это количество переменно), то это без проблем заменяется одним квантором по кодам векторов. У Вас, как я понимаю, именно такая ситуация (число перемен кванторов везде ограничено).

А можно продемонстрировать? Мне, например, непонятно, какими "векторами" заменятся списки переменных, которых $k$ штук под квантором и $m+2$ штук в списке аргументов функции, причём из последних $k$ штук заполняются переменными, а остальные - нулями.

маткиб писал(а):

Меня интересуют уменьшение числа и увеличение основания системы счисления (т.е. две основные операции, на основе которых строится последовательность Гудстейна).

И что? Где проблема-то в доказательстве? Каждая формула построена как утверждение, что: "Если выражение такого-то вида сойдётся, то и выражение такого-то вида сойдётся". Причём тут Ваши сомнения относительно того, что числа могут увеличиваться быстрее, чем уменьшаются?

маткиб писал(а):

А теперь рассмотрим процесс, при котором основание системы счисления на каждом шаге увеличивается не на 1, а на 2. Тогда Ваше доказательство уже применить не получится, придётся писать новое доказательство.

Ну и что? Я же доказывал сходимость последовательности Гудстейна, а не какой-то другой последовательности.

маткиб писал(а):

А если оно изменяется как-то ещё более хитро, например, увеличивается в 2 раза, то придётся писать ещё одно доказательство. И так далее: для каждого конкретного случая своё доказательство.

Ну и что? Если Вы хотите получить доказательство сходимости последовательностей какого-то более общего вида, то это - отдельная задача. Причем её ещё надо сначала сформулировать.

маткиб писал(а):

И при сведении случая с каким-то числом этажей к случаю с меньшим числом этажей возникают как раз такие ситуации.

Какие здесь ситуации? Я просто вижу, что одноэтажные числа обнуляются за конечное число шагов, а отсюда можно вывести, что двуэтажные числа обнуляются за конечное число шагов и т.д. Вот совершенно тупая идея доказательства "в лоб".

маткиб писал(а):

Есть много всего. Другой вопрос, а имеет ли это смысл.

Вы про арифметику Гейтинга? Наверное, то множество математиков, которые ей занимаются, не совсем уж бестолковые альты.

маткиб писал(а):

И что в этом хорошего для конструктивности арифметики?

А что плохого? И вообще, какое отношение это имеет к конструктивности арифметики? Если не доказано, что $(\forall n)(P(n)\rightarrow P(n+1))$, то хоть в конструктивной, хоть в классической арифметике, но Вы индукцию применить не сможете.

маткиб писал(а):

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

Наоборот тоже можно. И это доказуемо элементарным мета-торетическим рассуждением: Если $P(0)$ и $(\forall n)(P(n) \rightarrow P(n+1))$ - теоремы, то согласно этому правилу вывода $(\forall n)P(n)$ - тоже теорема, а значит $P(0) \wedge (\forall n)(P(n) \rightarrow P(n+1)) \rightarrow (\forall n)P(n)$ - тоже теорема. А последнее - это и есть утверждение об индукции.

маткиб писал(а):

Но я отказываюсь принимать схему индукции как конструктивную.

Ну, это Ваша проблема. Конструктивисты принимают, а Вы - нет...

маткиб писал(а):

Вот если она вытекает как теорема из чего-то конструктивного, то это было бы хорошо.

Она вытекает из конструктивного понимания конструктивности :
Если алгоритм, проверяющий $P(n) \rightarrow P(n+1)$, заканчивается успехом для любого $n$, то проверку $P(n)$ для любого $n$ можно реализовать как алгоритм, по шагам выполняющий индуктивный вывод $P(0) \Rightarrow P(1) \Rightarrow \cdots P(n)$. Это гарантирует, что он закончится успехом.

маткиб писал(а):

Вот конструктивность правила вывода я готов признать (скрипя зубами), и все Ваши "мета-теоретические" соображения обосновывают в лучшем случае именно это правило вывода, но никак не схему индукции.

Да это одно и то же - Ваше правило вывода и аксиома индукции.

[Someone]

Someone в сообщении #186657 писал(а):

epros писал(а):

маткиб писал(а):

По поводу прикладной пользы: погрешность численных методов легче оценивать, если известно, что решение существует (можно рассматривать разность между найденным решением и настоящим и вывести для этой разности какие-то соотношения).

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

Простенький пример, демонстрирующий полезность неконструктивной теоремы существования.
...

epros в сообщении #186765 писал(а):

Здесь мне не очевидно только одно: Как этот пример демонстрирует "полезность" неконструктивной теоремы существования? Не мудрствуя лукаво, я бы на практике начал решение этой задачи с Вашего п. 4, т.е. с решения соответствующего квадратного уравнения.

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

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

epros в сообщении #186765 писал(а):

Если мне вдруг потребуется доказать, что получившаяся величина является пределом данной последовательности

В моём решении сначала доказано, что предел существует, потом выведено (с существенным использованием существования предела) и решено уравнение. У этого уравнения есть только один корень, поэтому он и является искомым пределом. На этом решение заканчивается, то есть, пункт 5 не обязателен.
Если же Вы не хотите строить регулятор фундаментальности, то Вам придётся сначала предположить, что предел существует, так как иначе неоткуда взять уравнение, а после решения уравнения обязательно доказать, что полученный корень является пределом данной последовательности, то есть, для такого способа решения пункт 5 обязателен. Без этого могут быть сюрпризы. Рассмотрите, например, последовательности, задаваемые уравнениями $x_{n+1}=\sqrt{1-x_n}$ (может быть, $x_{n+1}=\sqrt{|1-x_n|}$, чтобы избежать некоторых конструктивистских заморочек) или $x_{n+1}=1-x_n^2$ с тем же начальным условием $x_1=1$.

epros в сообщении #186765 писал(а):

Я не уверен в том, что это вполне корректная интерпретация. Дело в том, что отрицание аксиомы бесконечности судя по всему не выводимо из аксиом арифметики.

Судя по чему? Вообще, там, где я об этом прочитал, никаких комментариев нет, так что точный смысл того, что имел в виду автор, мне не очень ясен.

Аксиома бесконечности ($\exists x(\varnothing\in x\&\forall y(y\in x\to y\cup\{y\}\in x))$) выглядит чуть сильнее, чем просто утверждение о существовании бесконечного множества, поэтому её отрицание, может быть, и не равносильно утверждению, что все множества конечны. Не знаю. Впрочем, Гёдель формулировал эту аксиому в более слабом варианте: $\exists x(x\neq\varnothing\&\forall y(y\in x\to\exists z(z\in x\& y\subseteq z)))$. Но и эта формулировка мне кажется более сильной, чем просто утверждение о существовании множества, не равномощного никакому натуральному числу.

Пусть у нас есть арифметика Пеано (с символами "$0$", "$+$" и "$\cdot$" для нуля, сложения и умножения, поскольку без двух последних теория будет слишком бедной: только забор из палочек, а не арифметика). Закодируем множества натуральными числами следующим образом. Пустому множеству $\varnothing$ сопоставим число $0$. Если множествам $x_1,x_2,\ldots,x_k$ сопоставлены числа $c_1,c_2,\ldots,c_k$, то множеству $\{x_1,x_2,\ldots,x_k\}$ сопоставим число $2^{c_1}+2^{c_2}+\ldots+2^{c_k}$. Например, число $51719=2^0+2^1+2^2+2^9+2^{11}+2^{14}+2^{15}$ соответствует множеству

$$\{\varnothing,\{\varnothing\},\{\{\varnothing\}\},\{\varnothing,\{\varnothing,\{\varnothing\}\}\},\{\varnothing,\{\varnothing\},\{\varnothing,\{\varnothing\}\}\},\{\{\varnothing\},\{\{\varnothing\}\},\{\varnothing,\{\varnothing\}\}\},\{\varnothing,\{\varnothing\},\{\{\varnothing\}\},\{\varnothing,\{\varnothing\}\}\}\}.$$

Множества, которые таким образом получаются, называются наследственно конечными. (4/II-2012 исправил предыдущую длинную формулу, которая отображалась неправильно - без двух последних скобок. Someone)

По-моему, нетрудно показать, пользуясь аксиомами арифметики, что для этих множеств выполняются все аксиомы ZFC, кроме аксиомы бесконечности. Поэтому в данной модели ZFC мы можем обычным образом определить "натуральные числа" как множества, определяемые соотношениями $n_0=\varnothing$, $n_{k+1}=n_k\cup\{n_k\}$. Соответствующие коды будут определяться условиями $c_{n_0}=0$, $c_{n_{k+1}}=c_{n_k}+2^{c_{n_k}}$. Коды первых "натуральных чисел" такие: $0$, $1$, $3$, $11$, $2059$; код следующего "натурального числа" содержит $620$ десятичных цифр. Каждое множество в этой модели равномощно какому-нибудь "натуральному числу" и в этом смысле конечно.

Я не знаю, выводимы ли аксиомы индукции для "натуральных чисел" из аксиом ZFC без аксиомы бесконечности, но в рассмотренной модели их можно вывести из аксиом индукции арифметики Пеано. Коэн для своей теории $Z_2$ формулирует аксиомы индукции явным образом (П.Дж.Коэн. Теория множеств и континуум-гипотеза. "Мир", Москва, 1969. \глава I, § 6).

Наоборот, если у нас есть модель аксиом ZFC с отрицанием аксиомы бесконечности (и аксиомами индукции, если они вдруг не выводимы), то, как объясняет Коэн, из неё выводима арифметика Пеано. Поэтому эти теории эквивалентны.

Очень забавная ситуация получается, если взять нестандартную модель арифметики Пеано. Натуральный ряд в таких моделях устроен следующим образом: некоторый начальный отрезок натурального ряда состоит из стандартных натуральных чисел, но существуют нестандартные натуральные числа, которые больше всех стандартных ("бесконечные" натуральные числа). Однако, оставаясь внутри арифметики, мы никаким способом не можем отличить стандартные натуральные числа от нестандартных.
Выполнив описанное выше построение, получим такую же нестандартную модель теории наследственно конечных множеств.

Я как-то писал о нестандартных моделях вычислительного процесса, связанных с нестандартными моделями арифметики. Что такое вычислительный процесс? Рассмотрим, например, машину Тьюринга. Её конфигурацию можно закодировать натуральным числом. Есть начальная конфигурация $a_0$ и есть функция, вычисляющая следующую конфигурацию $a_{k+1}=\varphi(a_k)$. Это даёт рекурсивное определение последовательности (функции, определённой на всех натуральных числах). Если натуральные числа нестандартные, то и вычислительный процесс будет нестандартным: с точки зрения стандартной модели арифметики, этот процесс может содержать бесконечное число шагов, даже если он останавливается. Как я уже писал, такой "вычислительный процесс" противоречит моим интуитивным представлениям о вычислительном процессе, но исключить нестандартную модель без аксиомы бесконечности, видимо, нельзя. Доводы в пользу этого могут быть такими.

Стандартная модель арифметики среди прочих моделей выделяется тем, что в ней совокупность натуральных чисел является наименьшей. Сформулировать это условие, имея возможность говорить только о конечных множествах, нельзя. Об этом свидетельствует само существование нестандартных моделей. Поэтому для того, чтобы сказать что-то о совокупности натуральных чисел, нужно иметь её (совокупность натуральных чисел) среди объектов теории. А это условие, как легко видеть, влечёт аксиому бесконечности.

epros в сообщении #186765 писал(а):

Утверждение о "существовании решения" не обязательно означает, что решение построено. Оно означает, что существует способ (например, алгоритм) его построить. А существование способа (например, алгоритма) означает, что существует способ его построить. Вот только, в отличие от классической математики, эту цепочку утверждений о существовании мы не можем упереть в произвольным образом придуманную аксиому существования. Мы должны будем её упереть во что-то, что действительно построено.

Нет. "Упереть" нам придётся в нашу собственную способность что-то построить. Каковая способность не сводится к заранее написанному кем-либо алгоритму.

epros в сообщении #186765 писал(а):

Someone писал(а):

Это не обобщение. Фактически Ваш "(n)-алгоритм" и есть алгоритм, решающий задачу. Что он там делает, прежде чем выдать ответ - это его проблема.

Это Вы его так интерпретируете, ибо полагаете, что знание о том, что делает этот алгоритм, "существует независимо" от моего конкретного знания.

Вообще странное заявление. Знание не может существовать независимо от субъекта - носителя знания.

epros в сообщении #186765 писал(а):

А я, записав этот алгоритм, не имею права утверждать, что он выдаёт ответ на исходную задачу, потому что мне это сначала нужно доказать, т.е. проследить всю цепочку алгоритмов.

Ага. Вы мне это только что продемонстрировали на примере вычисления предела: «Я напишу неизвестно откуда взявшееся уравнение, найду его корень и выдам в качестве ответа. А доказывать, что ответ правильный, буду только в случае, когда меня поставят к стенке перед расстрельной командой и скажут: "Доказывай, иначе расстреляем."»

epros в сообщении #186765 писал(а):

Someone писал(а):

я вообще перестал понимать, о чём Вы говорите. Разве классическая математика каким-то образом отрицает возможность ситуаций, когда задача неразрешима? К тому же, "задача неразрешима" - это не логическое значение. Это утверждение.

Вот я и говорю не просто о том, что "возможны ситуации, когда задача неразрешима", а о том, имею ли я право рассматривать такие ситуации как соответствующее логическое значение высказывания, составляющего формулировку задачи?

Видите-ли, в интуиционистской логике фактически логическим значением высказывания является само это высказывание (вместе с эквивалентными ему). Что, с моей точки зрения, означает отсутствие логических значений как таковых. Утверждение "задача неразрешима" относится к метатеории и не может рассматриваться как логическое значение в предметной теории. Если Вы закодируете метатеорию в предметной теории, то получите какое-то высказывание предметной теории, интерпретируемое (через метатеорию) как утверждение о неразрешимости исходной задачи, но не равносильное этой задаче. Вдобавок, как бы мы ни интерпретировали это утверждение, фактически оно является некоторым высказыванием об объектах предметной теории, отличающимся от той задачи, неразрешимость которой утверждается. Поэтому и в таком варианте утверждение "задача неразрешима" нельзя рассматривать как логическое значение высказывания, составляющего формулировку задачи.

epros в сообщении #186765 писал(а):

Предлагается аксиоматизировать обычное общеупотребимое понятие строки, в которой каждый символ однозначно распознаваем, которые равны тогда и только тогда, когда соответствуют посимвольно, которые могут быть любой длины, но конечны, и т.п. Только не говорите мне, что никто не знает "что это такое".

Нет, не скажу, что «никто не знает "что это такое"». Поскольку я с самого начала настаивал на том, что необходимо формализовать все нужные нам свойства строк, прежде чем использовать их как обоснование то ли арифметики Пеано, то ли CRA. В итоге мы расстаёмся с "интуитивно очевидными" свойствами строк и приходим к "обоснованию", которое

epros в сообщении #186765 писал(а):

заключается в сочинении невесть откуда взятой аксиомы

epros в сообщении #186765 писал(а):

Между прочим, это понятие предлагается использовать в качестве "базового" не потому, что так мне больше нравится, а потому, что сложившийся способ формализации понятия "формальная теория" основан на понятиях символов и составляемых из них строк (именно в этом "обычном" смысле).

Разумеется. Мы никогда не можем дать полную формализацию, иначе мы должны будем строить бесконечную цепочку метатеорий , формализующих друг друга. Где-то надо остановиться. Почему бы не остановиться на строках? Фактически это означает, что всякая формальная теория содержит массу не формализованных предположений, которые неявно участвуют в рассуждениях. Но нужно понимать, что что такие предположения есть, и что в случае со строками они столь существенны, что позволяют "обосновать" арифметику Пеано. В этом смысле мы не можем сформулировать математическую логику, не имея достаточно развитых представлений об арифметике, несмотря на то, что логика не содержит арифметику в явном виде.

epros в сообщении #186765 писал(а):

Someone писал(а):

Постарайтесь понять, что никаких "общеочевидных" свойств нет, а если они кому-то кажутся "общеочевидными", то это, очевидно, заблуждение.

Если бы это было так, то никакой обмен знаниями был бы невозможен. Я не могу "формально опровергнуть" это Ваше утверждение, но я всё же исхожу из обратного, т.е. из того, что некоторые "общеочевидные" (хотя и неопределимые формально через другие вещи) понятия всё же существуют. Только за них мы можем "зацепиться" при построении теорий, в однозначном понимании которых всеми мы могли бы быть уверены.

Нет. У каждого из нас есть богатый опыт взаимодействия с внешним миром и, в частности, друг с другом. Мы давно уже договорились о неких общих понятиях и способах их выражения. Этого достаточно, чтобы мы могли договориться о формальных правилах записи строк и правилах их преобразования (я имею в виду математику). Это всё, что нам нужно, чтобы понимать друг друга. При этом вовсе не требуется, чтобы мы интерпретировали эти строки одинаково. Как бы мы их не интерпретировали, писать мы будем одинаковые строки и преобразовывать их будем по одинаковым правилам, поэтому в этой части разногласий у нас не возникнет.

epros в сообщении #186765 писал(а):

Someone писал(а):

Точно так же никто не видел неограниченно продолжаемых строк. А ссылка на абстракцию потенциальной осуществимости даёт результат, не имеющий отношения к реальности, на которую Вы так любите ссылаться.

На это я уже ответил маткибу. Судя по Вашим дальнейшим комментариям, Вы мой ответ не восприняли. Никто на самом деле не говорит, что некую строку длиной $10^{10^{10}}$ символов мы сможем "реально" продолжить (не исключено, что мы у неё и конца-то не найдём). Речь в абстракции потенциальной осуществимости идёт только о том, что когда мы будем иметь дело с конкретной задачей, то это ограничение всегда можно будет считать выходящим за её рамки.

Не всегда. Если для решения какой-то задачи потребуется реально "нарисовать" $10^{10^{10}}$ "палочек", то эта задача реально никогда не будет решена таким способом, хотя решение "потенциально осуществимо".

epros в сообщении #186765 писал(а):

Аксиома бесконечности (а ведь это, как я понимаю, и есть утверждение о существовании актуальной бесконечности)

Вообще, я устал толочь воду в ступе. Аксиома бесконечности не есть утверждение о "существовании актуальной бесконечности". Я в курсе, что существуют всякие "абстракции" типа "актуальной бесконечности", "потенциальной осуществимости" и т.д, и т.п.. Этих "абстракций", скорее всего, гораздо больше, просто, видимо, никому не приходит в голову заняться их выявлением и явной формулировкой. Все они относятся не к математике, а к околоматематической философии. Они не являются математическими утверждениями и не могут использоваться в математических рассуждениях. Эти "абстракции" не могут служить обоснованием каких-либо математических утверждений. В практическом плане они означают только одно: математические понятия и объекты не принадлежат реальному миру, хотя и происходят оттуда, являясь логическими моделями нашего практического опыта.

Математические понятия, аксиомы и объекты являются логическими конструкциями. Их нельзя обосновывать какими-то "процедурами проверки", апеллирующими к реальному миру, потому что логические конструкции этому миру не принадлежат. В реальном мире нет множеств, ни конечных, ни бесконечных. В нём нет ни натуральных чисел, ни машин Тьюринга, ни нормальных алгорифмов Маркова. Все эти "процедуры" могут быть полезными только в том смысле, что могут подсказать выбор интересных аксиом. Но обосновывать аксиомы таким способом нельзя.

Вы же понимаете, что физическая процедура проверки утверждения "за каждым натуральным числом следует ещё большее натуральное число" путём рисования "забора" рано или поздно столкнётся с невозможностью пририсовать ещё одну палочку ввиду исчерпания физических ресурсов, поэтому никакой проверки не получается. И аксиому бесконечности эта процедура "обосновывает" ровно в такой же степени. Вам не нравится, что аксиома бесконечности утверждает "одновременное" существование "заборов" всевозможной длины? А что это значит, что они существуют "одновременно", и, главное, где они "существуют" и в каком смысле "существуют"? Где, в каких математических рассуждениях используется это "одновременное" существование? Можно ли рассмотреть множество голов, забитых футболистом Сергеем Перхуном за его футбольную карьеру? Забил ли он их все "одновременно"? Лучше забросьте эту околоматематическую псевдофилософию и не вспоминайте о ней.

epros в сообщении #186765 писал(а):

Если интерпретировать аксиому бесконечности как утверждение о строках (из символов "{", "," и "}"), то она утверждает существование бесконечной строки.

Ничего подобного она не утверждает. Она утверждает существование (если хотите - возможность построения) сколь угодно длинных строк и возможность мыслить совокупность этих строк как единое понятие. Для записи которого, очевидно, придётся придумать такой способ, который не требует написания бесконечно длинных строк. Сама аксиома бесконечности и демонстрирует один из таких способов, поскольку её запись содержит лишь конечное число символов.

epros в сообщении #187306 писал(а):

Я кажется сообразил как можно конструктивно доказать эту теорему. Правда доказательство может быть только мета-теоретическим, ибо оно использует индукцию по формулам арифметики. Щас продемонстрирую:

Мероприятие, на мой взгляд, совершенно безнадёжное.

http://en.wikipedia.org/wiki/Goodstein%27s_theorem писал(а):

While this proof of Goodstein's theorem is fairly easy, the Kirby-Paris theorem which says that Goodstein's theorem is not a theorem of Peano arithmetic, is technical and considerably more difficult. It makes use of countable nonstandard models of Peano arithmetic.

Прежде всего, что такое метатеория? Это теория, которая используется для формального описания языка предметной теории. У предметной теории и метатеории разные объекты, даже если они называются одинаково (и даже если обе теории, в некотором смысле, одинаковы). Метатеория не может доказывать теоремы об объектах предметной теории, она может доказывать теоремы только о своих объектах. В данном случае, о формулах предметной теории и самой предметной теории как совокупности формул: их доказуемость или недоказуемость, противоречивость или непротиворечивость.

Далее, как сказано в цитате, недоказуемость теоремы Гудстейна средствами арифметики Пеано обусловлена существованием нестандартной модели, в которой эта теорема неверна. Исключить такую модель можно только одним способом: добавить новые аксиомы к предметной теории, то есть, перейти к её расширению. Метатеория не является расширением предметной теории и потому никаких моделей её исключить не может. Максимум, на что можно было бы рассчитывать - это что средствами метатеории удастся доказать утверждение предметной теории, истинное в любой модели. Теорема Гудстейна к таковым не относится.

В теории множеств теорема доказуема благодаря тому, что теория множеств позволяет определить стандартную модель арифметики, что отсекает все нестандартные модели. Как я объяснял выше, в теории, не имеющей аксиомы бесконечности, отсечь нестандартные модели вряд ли удастся.

Добавлено спустя 5 минут 31 секунду:

epros в сообщении #189508 писал(а):

маткиб писал(а):

Ну в индукции вообще-то рассматривается формула $P(n)$ со свободной переменной (схема индукции $P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n)$),

Вы меня просто ошарашиваете. Где же здесь $n$ свободная переменная, если она везде квантифицирована?

Вы меня тоже ошарашиваете. В формуле $P(n)$ переменная $n$ - свободная.

[Виктор Ширшов]

Посмотрел тему, но комментировать не буду, так как не знаю ни биекции, ни вычислимых чисел. И хорошо, что не знаю.

[Алексей К.]

Виктор Ширшов в сообщении #189587 писал(а):

И хорошо, что не знаю.

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

[epros]

Someone писал(а):

epros в сообщении #189508 писал(а):

маткиб писал(а):

Ну в индукции вообще-то рассматривается формула $P(n)$ со свободной переменной (схема индукции $P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n)$),

Вы меня просто ошарашиваете. Где же здесь $n$ свободная переменная, если она везде квантифицирована?

Вы меня тоже ошарашиваете. В формуле $P(n)$ переменная $n$ - свободная.

Я вижу, что в формуле $P(n)$ есть свободная переменная $n$. Но мы говорили не об этом, а о высказываниях, участвующих в индукции. Таковыми являются $P(0)$, $(\forall n)(P(n)\rightarrow P(n+1))$, $(\forall n)P(n)$, собственно сама аксиома индукции и т.п. Поскольку это высказывания, от свободных переменных они так или иначе избавлены. А что делать с предлагаемой лишней переменной - "пределом индукции" - пока что непонятно.

[маткиб]

epros писал(а):

маткиб писал(а):

Ну в индукции вообще-то рассматривается формула $P(n)$ со свободной переменной (схема индукции $P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n)$),

Вы меня просто ошарашиваете. Где же здесь $n$ свободная переменная, если она везде квантифицирована?

маткиб писал(а):

а остальные свободные, естественно, нужно заменить константами.

Какими константами?

Чем отвечать на дурацкие вопросы, лучше приведу пример конструктивной (по моему мнению индукции):

$$ (\forall x\leq 0)(\exists y\leq 2^0)(y=x\cdot x)\&(\forall n)((\forall x\leq n)(\exists y\leq 2^n)(y=x\cdot x)\rightarrow(\forall x\leq n+1)(\exists y\leq 2^{n+1})(y=x\cdot x))\rightarrow(\forall n)(\forall x\leq n)(\exists y\leq 2^n)(y=x\cdot x) $$

epros писал(а):

маткиб писал(а):

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

Не понял проблемы. Можно на примере?

Пример уже был: $P(n)\equiv(\forall x)(\exists y)Q(x,y,n)$, где $Q$ -.... что-то неочевидное.

epros писал(а):

маткиб писал(а):

А если несколько одинаковых кванторов в формуле идут подряд (пусть даже это количество переменно), то это без проблем заменяется одним квантором по кодам векторов. У Вас, как я понимаю, именно такая ситуация (число перемен кванторов везде ограничено).

А можно продемонстрировать? Мне, например, непонятно, какими "векторами" заменятся списки переменных, которых $k$ штук под квантором и $m+2$ штук в списке аргументов функции, причём из последних $k$ штук заполняются переменными, а остальные - нулями.

Кодируем вектор $(x_1,\ldots,x_n)$ числом $p_1^{x_1+1}\cdot\ldots\cdot p_n^{x_n+1}$, где $p_i$ - $i$-ое простое число, а дальше выражения вида, например, $(\forall x_1)\ldots(\forall x_n)\ldots$ заменяются на $(\forall x)\ldots$, где $x$ рассматривается как код вектора, выражение под квантором заменяется соответствующим образом с помощью техники арифметизации вычислимых функций (вместо переменных выуживаются компоненты $x$).

epros писал(а):

И что? Где проблема-то в доказательстве?

Хорошо, я не буду больше рассуждать о Вашем доказательстве, пока его не прочитаю (гарантии, что прочитаю, нет, искренне надеюсь, что прочитает кто-нибудь другой )

epros писал(а):

Вы про арифметику Гейтинга? Наверное, то множество математиков, которые ей занимаются, не совсем уж бестолковые альты.

Да не альты они, просто фигнёй страдают, да и всё.

epros писал(а):

маткиб писал(а):

И что в этом хорошего для конструктивности арифметики?

А что плохого? И вообще, какое отношение это имеет к конструктивности арифметики? Если не доказано, что $(\forall n)(P(n)\rightarrow P(n+1))$, то хоть в конструктивной, хоть в классической арифметике, но Вы индукцию применить не сможете.

Смогу. Я могу рассматривать

$$ P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n) $$

как теорему, она сама и есть применение (и для неё не нужно доказанного $(\forall n)(P(n)\rightarrow P(n+1))$).

epros писал(а):

маткиб писал(а):

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

Наоборот тоже можно. И это доказуемо элементарным мета-торетическим рассуждением: Если $P(0)$ и $(\forall n)(P(n) \rightarrow P(n+1))$ - теоремы, то согласно этому правилу вывода $(\forall n)P(n)$ - тоже теорема, а значит $P(0) \wedge (\forall n)(P(n) \rightarrow P(n+1)) \rightarrow (\forall n)P(n)$ - тоже теорема. А последнее - это и есть утверждение об индукции.

А если $P(0)$ и $(\forall n)(P(n) \rightarrow P(n+1))$ - не теоремы?

epros писал(а):

маткиб писал(а):

Но я отказываюсь принимать схему индукции как конструктивную.

Ну, это Ваша проблема. Конструктивисты принимают, а Вы - нет...

Это какие-то неправильные конструктивисты... Наверно, они дают неправильный мёд

epros писал(а):

маткиб писал(а):

Вот конструктивность правила вывода я готов признать (скрипя зубами), и все Ваши "мета-теоретические" соображения обосновывают в лучшем случае именно это правило вывода, но никак не схему индукции.

Да это одно и то же - Ваше правило вывода и аксиома индукции.

Не одно и тоже. См. выше (случай, когда слева - не теоремы).

[epros]

маткиб писал(а):

Чем отвечать на дурацкие вопросы, лучше приведу пример конструктивной (по моему мнению индукции):

$$ (\forall x\leq 0)(\exists y\leq 2^0)(y=x\cdot x)\&(\forall n)((\forall x\leq n)(\exists y\leq 2^n)(y=x\cdot x)\rightarrow(\forall x\leq n+1)(\exists y\leq 2^{n+1})(y=x\cdot x))\rightarrow(\forall n)(\forall x\leq n)(\exists y\leq 2^n)(y=x\cdot x) $$

Что-то я не въехал, что конструктивного в том, чтобы подставить в аксиому индукции $P(n) = (\forall x\leq n)(\exists y\leq 2^n)(y=x\cdot x)$?

маткиб писал(а):

Пример уже был: $P(n)\equiv(\forall x)(\exists y)Q(x,y,n)$, где $Q$ -.... что-то неочевидное.

Так я ж уже отвечал: Вся проблема в том, откуда Вы возьмёте предпосылки индукции: $(\forall x)(\exists y)Q(x,y,0)$ и $(\forall n)((\forall x)(\exists y)Q(x,y,n) \rightarrow (\forall x)(\exists y)Q(x,y,n+1))$. Если ниоткуда не возьмёте, то не будет Вам индукции. А если откуда-то возьмёте, то в чём проблема выполнить индукцию до любого $n$?

маткиб писал(а):

Кодируем вектор $(x_1,\ldots,x_n)$ числом $p_1^{x_1+1}\cdot\ldots\cdot p_n^{x_n+1}$, где $p_i$ - $i$-ое простое число, а дальше выражения вида, например, $(\forall x_1)\ldots(\forall x_n)\ldots$ заменяются на $(\forall x)\ldots$, где $x$ рассматривается как код вектора,

Здесь идея понятна.

маткиб писал(а):

выражение под квантором заменяется соответствующим образом с помощью техники арифметизации вычислимых функций (вместо переменных выуживаются компоненты $x$).

А вот здесь можно поподробнее? Я понимаю, что значение любой k-той переменной можно "выудить с помощью техники арифметизации". Но как записать одной общей формулой функцию от неизвестного количества переменных?

маткиб писал(а):

epros писал(а):

Если не доказано, что $(\forall n)(P(n)\rightarrow P(n+1))$, то хоть в конструктивной, хоть в классической арифметике, но Вы индукцию применить не сможете.

Смогу. Я могу рассматривать

$$ P(0)\&(\forall n)(P(n)\rightarrow P(n+1))\rightarrow(\forall n)P(n) $$

как теорему, она сама и есть применение (и для неё не нужно доказанного $(\forall n)(P(n)\rightarrow P(n+1))$).

Ну и что толку? Естественно, утверждение о применимости индукции к $P(n)$ можно "рассматривать как теорему". Но какой толк от этой теоремы, если предпосылок индукции у Вас нет, а значит вывода $(\forall n)P(n)$ Вы из неё всё равно сделать не можете?

маткиб писал(а):

А если $P(0)$ и $(\forall n)(P(n) \rightarrow P(n+1))$ - не теоремы?

Тогда вообще ничто не мешает считать аксиому индукции верной.

[epros]

Someone писал(а):

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

Я уже как-то потерял эту нить обсуждения. Но, насколько я помню, конструктивно доказать сходимость той последовательности к решению того квадратного уравнения не составляет труда. Насколько я понимаю, я не обязан кому-то объяснять, откуда взялось "неизвестно откуда взявшееся уравнение", ибо если доказано, что последовательность имеет пределом такое-то число, то задача решена.

Someone писал(а):

... то Вам придётся сначала предположить, что предел существует, так как иначе неоткуда взять уравнение,

И предположить это не составит никакого труда.

Someone писал(а):

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

И это разрешимо без особого труда.

Someone писал(а):

epros в сообщении #186765 писал(а):

Я не уверен в том, что это вполне корректная интерпретация. Дело в том, что отрицание аксиомы бесконечности судя по всему не выводимо из аксиом арифметики.

Судя по чему? Вообще, там, где я об этом прочитал, никаких комментариев нет, так что точный смысл того, что имел в виду автор, мне не очень ясен.

То, что арифметика прекрасно живёт без использования аксиомы бесконечности, иллюстрирует многолетняя практика интуиционистов. Но это не означачает, что арифметика = теория множеств, в которой аксиома бесконечности заменена её отрицанием. Ибо из аксиом Пеано (включая схему индукции), насколько я знаю, никто ещё не доказал утверждение о том, что не существует совокупности всех натуральных чисел.

Someone писал(а):

Аксиома бесконечности ($\exists x(\varnothing\in x\&\forall y(y\in x\to y\cup\{y\}\in x))$) выглядит чуть сильнее, чем просто утверждение о существовании бесконечного множества

Вы имеете в виду, что бесконечные множества не обязаны быть только индуктивными? В этом смысле да: утверждение о существовании индуктивного множества "сильнее" утверждения о существовании бесконечного множества.

Someone писал(а):

По-моему, нетрудно показать, пользуясь аксиомами арифметики, что для этих множеств выполняются все аксиомы ZFC, кроме аксиомы бесконечности.

По-моему это вполне может быть.

Someone писал(а):

Наоборот, если у нас есть модель аксиом ZFC с отрицанием аксиомы бесконечности (и аксиомами индукции, если они вдруг не выводимы), то, как объясняет Коэн, из неё выводима арифметика Пеано. Поэтому эти теории эквивалентны.

Против выводимости арифметики из ZFC с отрицанием аксиомы бесконечности у меня нет возражений. А вот Ваше "поэтому" вызывает сомнения: Я не вижу, чтобы ZFC с отрицанием аксиомы бесконечности выводилась из арифметики. Точнее, ZFC без аксиомы бесконечности наверняка выводится, а вот собственно отрицание аксиомы бесконечности - вряд ли. А ещё точнее, ZFC без аксиомы бесконечности наверняка выводится из арифметики плюс отрицание аксиомы бесконечности.

Someone писал(а):

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

К сожалению, я эти теоретико-множественные прибабахи не вполне понимаю. Всё выглядит так, что сначала мы (посредством излишне "богатой" аксиоматики) заложили возможность существования этих самых "нестандартных моделей", а потом начали думать о том, как их исключить.

В конструктивизме этой проблемы, как я понимаю, нет просто потому, что изначально рассматривается одна "стандартная" модель чисел, а именно - те самые нелюбимые Вами заборы из палочек.

Someone писал(а):

epros в сообщении #186765 писал(а):

Утверждение о "существовании решения" не обязательно означает, что решение построено. Оно означает, что существует способ (например, алгоритм) его построить. А существование способа (например, алгоритма) означает, что существует способ его построить. Вот только, в отличие от классической математики, эту цепочку утверждений о существовании мы не можем упереть в произвольным образом придуманную аксиому существования. Мы должны будем её упереть во что-то, что действительно построено.

Нет. "Упереть" нам придётся в нашу собственную способность что-то построить. Каковая способность не сводится к заранее написанному кем-либо алгоритму.

К сожалению, наша "способность" - это неопределённое понятие. Кстати, в этом состоит возражение Маркова против Гейтинговского интуиционизма (в частности, против "свободно продолжающихся последовательностей"). Гейтинг утверждает, что его "математическая интуиция" подсказывает ему, что он "способен" построить такую последовательность. А Марков возражает, что пока строго не определён способ построения, он не может признать последовательность построенной.

Someone писал(а):

epros в сообщении #186765 писал(а):

Someone писал(а):

Это не обобщение. Фактически Ваш "(n)-алгоритм" и есть алгоритм, решающий задачу. Что он там делает, прежде чем выдать ответ - это его проблема.

Это Вы его так интерпретируете, ибо полагаете, что знание о том, что делает этот алгоритм, "существует независимо" от моего конкретного знания.

Вообще странное заявление. Знание не может существовать независимо от субъекта - носителя знания.

Это Вы сказали, что этот "(n)-алгоритм" - "и есть алгоритм, решающий задачу". Откуда Вы это знаете? Вам записали на бумажке код алгоритма, который строит ещё какой-то код, откуда Вы знаете, какая задача в итоге решается? А я Вам говорю, что я не знаю, что делает этот алгоритм, пока не прослежу всю цепочку. И я не вижу смысла предполагать, что это знание лежит где-то и ждёт, пока я его подберу.

Someone писал(а):

Видите-ли, в интуиционистской логике фактически логическим значением высказывания является само это высказывание (вместе с эквивалентными ему). Что, с моей точки зрения, означает отсутствие логических значений как таковых.

Ну, Вы правы в том, что конструктивизм не озабочен задачей построения исчерпывающего множества логических значений своих высказываний. Я об этом как-то говорил. Важно не то, каково у высказывания "логическое значение", а то, доказано ли оно в теории.

Someone писал(а):

Утверждение "задача неразрешима" относится к метатеории и не может рассматриваться как логическое значение в предметной теории.

С тем, что утверждение о неразрешимости является утверждением метатеории, я соглашусь. Но с тем, что факт доказательства такого метаутверждения нельзя рассматривать как логическое значение применительно к предметной теории, не соглашусь.

Скажем, у нас есть предметная теория, которая "принята" т.е. мы считаем её в рамках соответствующей предметной области верной. Сформулируем в ней некоторое высказывание $P$ и зададимся вопросом: откуда нам взять соображения о его верности, т.е. "логическое значение"? Мой ответ таков:
- Если мы доказали $P$ в этой теории, то оно "истинно".
- Если мы свели $P$ к противоречию с другими выводами этой теории (т.е. опровергли его), то оно "ложно".
- Если мы доказали, что в этой теории $P$ нельзя ни доказать, ни опровергнуть (а это, естественно, возможно только с привлечением мета-теоретических средств), то оно "неразрешимо".
- Если мы доказали, что с помощью мета-теоретических средств неразрешимость $P$ в этой теории нельзя ни доказать, ни опровергнуть (а это, естественно, возможно с привлечением мета-мета-теоретических средств), то для него "вопрос разрешимости неразрешим".
- и т д.

Someone писал(а):

Если Вы закодируете метатеорию в предметной теории, то получите какое-то высказывание предметной теории, интерпретируемое (через метатеорию) как утверждение о неразрешимости исходной задачи, но не равносильное этой задаче. Вдобавок, как бы мы ни интерпретировали это утверждение, фактически оно является некоторым высказыванием об объектах предметной теории, отличающимся от той задачи, неразрешимость которой утверждается. Поэтому и в таком варианте утверждение "задача неразрешима" нельзя рассматривать как логическое значение высказывания, составляющего формулировку задачи.

В итоге я так и не понял почему нельзя. Вот мы совершенно строго (хотя и мета-теоретически) доказали, что в исходной постановке задача неразрешима. Почему я должен "исправлять" постановку задачи, добавляя к аксиоматике предметной теории какие-то новые аксиомы, ради того, чтобы всё-таки сделать задачу разрешимой, а не могу просто успокоиться на том, что она "в такой постановке неразрешима"?

Someone писал(а):

В итоге мы расстаёмся с "интуитивно очевидными" свойствами строк и приходим к "обоснованию", которое

epros в сообщении #186765 писал(а):

заключается в сочинении невесть откуда взятой аксиомы

Я же не утверждаю, что конструктивизм может вообще обойтись без аксиом. "Невесть откуда взятыми" являются только такие аксиомы, которые утверждают непонятные (хоть кому-то) свойства или говорят о существовании объектов, которые непонятно (хоть для кого-то) что собой представляют.

Someone писал(а):

Разумеется. Мы никогда не можем дать полную формализацию, иначе мы должны будем строить бесконечную цепочку метатеорий , формализующих друг друга. Где-то надо остановиться. Почему бы не остановиться на строках? Фактически это означает, что всякая формальная теория содержит массу не формализованных предположений, которые неявно участвуют в рассуждениях.

Разумеется "формальная теория содержит массу не формализованных предположений", но все они сводятся к пониманию того, что такое символы, строки из них и операции с ними. Если мы все эти неформализованные вещи понимаем одинаково, то никаких проблем не возникнет. Задача ведь заключается не в том, чтобы найти такое обоснование, которое "абсолютно во всех смыслах", а чтобы исключить возможность неоднозначного понимания того, что такое "теория" в самом общем мыслимом случае.

Someone писал(а):

Но нужно понимать, что что такие предположения есть, и что в случае со строками они столь существенны, что позволяют "обосновать" арифметику Пеано. В этом смысле мы не можем сформулировать математическую логику, не имея достаточно развитых представлений об арифметике, несмотря на то, что логика не содержит арифметику в явном виде.

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

Someone писал(а):

Нет. У каждого из нас есть богатый опыт взаимодействия с внешним миром и, в частности, друг с другом. Мы давно уже договорились о неких общих понятиях и способах их выражения. Этого достаточно, чтобы мы могли договориться о формальных правилах записи строк и правилах их преобразования (я имею в виду математику). Это всё, что нам нужно, чтобы понимать друг друга.

Дьявол всегда в деталях. В некоторых предметных областях для адекватных коммуникаций достаточно разговорного языка. Бывает так, что и математика-то не нужна. Где-то вопросы сложнее и требуется более глубокая проработка "правил общения". Там уже нужна какая-то математическая формализация. А где-то могут возникнуть ситуации, когда достигнутый уровень "математической формализации", кажущийся Вам сейчас достаточным, может породить недоразумения. Например, Вы полагаетесь на доказанный кем-то где-то результат, но не знаете, что он получен с использованием аксиомы выбора (которую Вы не принимаете). Невозможно же по каждому возникающему вопросу подробнейшим образом описывать всю аксиоматику, которую принимает данный автор.

Someone писал(а):

При этом вовсе не требуется, чтобы мы интерпретировали эти строки одинаково. Как бы мы их не интерпретировали, писать мы будем одинаковые строки и преобразовывать их будем по одинаковым правилам, поэтому в этой части разногласий у нас не возникнет.

Здесь Вы рассуждаете прямо-таки как конструктивист. Действительно, математическими результатами в итоге всегда являются какие-то строки, которые в принципе применительно к конкретной ситуации ещё можно и интерпретировать по-разному. Например, вот Вы доказали, что существует нелинейная аддитивная функция на $\mathbb{R}$, и записали это утверждение строкой по всем правилам логики первого порядка. Я посмотрел и согласился: Да, действительно, из вот таких-то аксиом по таким-то правилам следует эта строка. И всё, если Вы меня спросите, "значит" ли этот вывод что-то для меня, я скажу "нет". Потому что моя "интерпретация" такова, что раз строки, которыми записаны некоторые исходные аксиомы, "ничего не значат", то и вывод "ничего не значит".

Someone писал(а):

epros в сообщении #186765 писал(а):

Речь в абстракции потенциальной осуществимости идёт только о том, что когда мы будем иметь дело с конкретной задачей, то это ограничение всегда можно будет считать выходящим за её рамки.

Не всегда. Если для решения какой-то задачи потребуется реально "нарисовать" $10^{10^{10}}$ "палочек", то эта задача реально никогда не будет решена таким способом, хотя решение "потенциально осуществимо".

Это не противоречит моему утверждению, потому что конкретной задачей в конструктивной постановке здесь является "нарисовать $10^{10^{10}}$ палочек" и конструктивным выводом является, что "это потенциально осуществимо". Т.е. ситуация ограниченности срока жизни реального исполнителя выходит за рамки конструктивной постановки задачи. Просто нужно отличать конкретную задачу в рамках математики от применения её результатов в реальности.

Someone писал(а):

Аксиома бесконечности не есть утверждение о "существовании актуальной бесконечности".

Индуктивное множество - это и есть "актуальная бесконечность". Раз есть утверждение о его существовании, значит мы имеем "абстракцию актуальной бесконечности".

Someone писал(а):

Я в курсе, что существуют всякие "абстракции" типа "актуальной бесконечности", "потенциальной осуществимости" и т.д, и т.п.. Этих "абстракций", скорее всего, гораздо больше, просто, видимо, никому не приходит в голову заняться их выявлением и явной формулировкой.

Может быть их и больше, но что касается различий между "актуальной" и "потенциальной" бесконечностями, то они сформулированы явно. И я уже где-то Вам о них писал:
- Абстракция актуальной бесконечности есть утверждение о существовании бесконечной совокупности объектов (пример таковой - индуктивное множество).
- Абстракция потенциальной бесконечности (или "осуществимости") есть утверждение о НЕсуществовании конечной совокупности всех объектов соответствующего типа.

Чувствуете разницу? Первую контруктивизм не принимает, а вторая является одной из его основ (т.е. признаются объекты потенциально бесконечных типов, например - строка или натуральное число).

Someone писал(а):

В практическом плане они означают только одно: математические понятия и объекты не принадлежат реальному миру, хотя и происходят оттуда, являясь логическими моделями нашего практического опыта.

В моём понимании "математическими объектами" являются строки символов. Хотя возможны и другие интерпретации, но суть та же.

Someone писал(а):

Но обосновывать аксиомы таким способом нельзя.

Без такого обоснования аксиома остаётся просто строкой символов, которая совершенно ничего не значит, а значит для нас нет никакого смысла её принимать. Процедура (или алгоритм) проверки, связанная с высказыванием, является ничем иным, как указанием на способ его применения. Когда утверждается, что "у любого натурального числа есть последователь", то я подразумеваю под этим не просто некий набор слов, которые каждый "понимай как хочешь", а указание на способ построения последователя. Например, в представлении строками палочек - это добавление палочки к строке. А в представлении символами, принятыми для описания множеств (фигурными скобками и запятыми), - это построение строки "{s,{s}}", где "{s}" - строка, описывающая исходное число .

Someone писал(а):

epros в сообщении #186765 писал(а):

Если интерпретировать аксиому бесконечности как утверждение о строках (из символов "{", "," и "}"), то она утверждает существование бесконечной строки.

Ничего подобного она не утверждает. Она утверждает существование (если хотите - возможность построения) сколь угодно длинных строк

Ну, ну. Если последователем строки "{s}" является строка "{s,{s}}", то как бы могла выглядеть строка, включающая всех последователей? Аксиомой-то несложно декларировать, что "такая строка существует", а вот попробуйте указать способ как такую строку построить. Это отнюдь не просто "сколь угодно длинная строка", а именно бесконечная.

Someone писал(а):

и возможность мыслить совокупность этих строк как единое понятие. Для записи которого, очевидно, придётся придумать такой способ, который не требует написания бесконечно длинных строк.

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

Someone писал(а):

Сама аксиома бесконечности и демонстрирует один из таких способов, поскольку её запись содержит лишь конечное число символов.

Способ недостаточно записать формулой. Нужно ещё продемонстрировать, что он завершается успехом. Код алгоритма построения строки, который никогда не завершится, написать нетрудно.

Someone писал(а):

epros в сообщении #187306 писал(а):

Я кажется сообразил как можно конструктивно доказать эту теорему. Правда доказательство может быть только мета-теоретическим, ибо оно использует индукцию по формулам арифметики. Щас продемонстрирую:

Мероприятие, на мой взгляд, совершенно безнадёжное.

Полагаю утверждение $(\forall x)(\mathrm{A} \vdash (\exists k)(g_k(x) = 0))$, где $\mathrm{A}$ - арифметика, а $g_k(x)$ - последовательность Гудстейна, начинающаяся с $x$, здесь доказанным. Если не согласны, найдите ошибку.

Someone писал(а):

Прежде всего, что такое метатеория? Это теория, которая используется для формального описания языка предметной теории.

Да.

Someone писал(а):

У предметной теории и метатеории разные объекты, даже если они называются одинаково (и даже если обе теории, в некотором смысле, одинаковы).

Да.

Someone писал(а):

Метатеория не может доказывать теоремы об объектах предметной теории, она может доказывать теоремы только о своих объектах.

Да. Зато она может доказывать утверждения о таких своих объектах, как утверждения предметной теории. Например, она может доказать, что для любого натурального $x$ в предметной теории существует доказательство $P(x)$.

Someone писал(а):

Теорема Гудстейна к таковым не относится.

Я не утверждаю, что теорема Гудстейна, т.е. $(\forall x)(\exists k)(g_k(x) = 0)$, как таковая доказана непосредственно в самой метатеории и не глядя на предметную теорию, т.е на арифметику. То, что доказано, я записал выше.