Так ведь я согласен с Вами в части
Вашей модели.
А то, что при иной интерпретации правил, отличной от канонических исчислений или К-систем, можно рассматривать Вашу модель - я не спорю. Но это уже другая тема, тоже интересная, но вне рамок К-систем.
Разногласия у нас Вами по поводу того, что выводимо/не выводимо в каноническом исчислении или в К-системе.
Ну почему же? Вы формулируете типичное рекурсивное определение множества
. В нём есть несколько пунктов. Во-первых,
, где
- пустая строка символов. Во-вторых, если
, то и
, где
- строка, получающаяся из строки
приписыванием в конец символа "
". Применив это правило несколько раз, получим, что
,
,
, и так далее, насколько у нас хватит терпения и ресурсов, чтобы рисовать эти палочки. В-третьих (это, видимо, заложено в само определение К-системы, и, возможно, является скрытой формулировкой принципа индукции),
не содержит никаких элементов кроме тех, которые получаются по двум первым правилам.
Возьмём множество
, о котором я
писал, и элемент
. Каким образом Вы опровергнете утверждение, что он присутствует в последовательности
?
Никакого трансфинитного вывода.
Я не достаточно точно выразился. Да,
выводы и в каноническом исчислении и в К-системе - это конечные объекты.
Трансфинитная индукция - это тоже конечное рассуждение. Но когда я говорил "никакого трансфинитного вывода", я вовсе не имел в виду трансфинитную индукцию. Я имел в виду, что индукция в нестандартной модели арифметики - это такая же индукция по натуральным числам, как в стандартной модели. Трансфинитная индукция начинается только после того, как "пройдены" все натуральные числа, не важно, стандартные они или не стандартные. Собственно, сами по себе рассуждения абсолютно не зависят от модели натурального ряда. О модели мы можем говорить только в метатеории.
А вот что я имел в виду. В К-системе для установления истинности/ложности утверждений в общем случае необходимо рассмотреть бесконечную совокупность выводов, поскольку необходимо учесть отношение исключения на множестве выводов.
О, боже! Вы, кажется, говорили о К-системах как о финитном основании математики, или я что-то путаю? Даже классическая математика, которая о финитизме не помышляет, признаёт только конечные рассуждения, а Вы предлагаете от этого отказаться.
Простейший пример - по определению слово ложно в К-системе iff все его выводы являются Л-выводами. В общем случае это может потребовать рассмотрения бесконечного количества выводов.
А если мы обнаружим, что слово имеет и Л-выводы, и И-выводы?
И еще - до меня вдруг дошло, что наш спор о станадартном/нестандартном понимании натуральных чисел не имеет отношения к рассматриваемому вопросу о "доказательстве" принципа математической индукции. Если мне удастся его доказать, то наше с Вами расхождение будет касаться лишь вопроса - а что же мы доказали - обычную индукцию или трансфинитную.
Вы правы, это к доказательству принципа индукции в арифметике отношения не имеет. Я
хотел обратить Ваше внимание на то, что указанные Вами два правила ещё не определяют натуральные числа, поскольку имеют простую модель, явно не имеющую отношения к натуральным числам (даже к нестандартным). И, разумеется, к ординалам и трасфинитной индукции этот пример тоже ни малейшего отношения не имеет.
Но в данном конкретном случае, честно говоря, я не понял Вашу критику конструктивистов. Например, в каноническом исчислении из рассмотренного определния натуральных чисел по определению ничего другого, кроме конечных натуральных чисел, мы вывести не сможем.
Разумеется, ничего, кроме натуральных чисел мы не выведем. Имея в виду, что элементы строки нумеруются натуральными числами. Причём, для любого натурального числа
мы сможем (при наличии достаточных ресурсов) написать строку, элементы которой перенумерованы натуральными числами от
до
(или, если это больше нравится, от
до
. Эпитет "конечное" по отношению к натуральному числу является излишним, поскольку все натуральные числа конечны по определению. Даже если они нестандартные.
А расхождения у нас с Вами ИМХО лежат в области синтаксиса, на котором, как все уже заметили, я не склонен зацикливаться.
Ну, Ваши два правила переводят процесс построения натуральных чисел именно в область синтаксиса.