epros писал(а):
Я же говорю о расширении синтаксиса в общем смысле. Могут быть такие расширения языка, что некоторые расширенные формулы не переводятся в формулы исходного языка. При этом с использованием исходной аксиоматики оказывается возможным доказать некоторые высказывания исходного языка, которые были недоказуемы в исходном варианте теории.
Весело. Я раньше не сталкивался с такого рода расширениями синтаксиса, но не отказался бы столкнуться (честно). Не поделитесь определением, ссылкой или хотя бы примером?
Эта задача не очень тривиальная, ибо речь идёт о моих собственных соображениях, так что ссылку на авторитетные источники дать не могу
, а формулировка примера в двух словах вряд ли получится. Но попробую. Как известно, арифметика Пеано неполна, т.е. в ней есть недоказуемые (но "содержательно истинные" высказывания). Одним из живых примеров таких высказываний является
теорема Гудстейна. Идея заключается в том, чтобы расширить язык арифметики Пеано таким образом, чтобы теорема Гудстейна стала доказуемой без изменения аксиоматики теории.
У меня есть доказательство "метатеоремы" Гудстейна (
ссылку на кусок своей статьи я здесь где-то уже приводил, если интересно, можете относительно его содержания поводить меня мордой по столу
). От собственно теоремы Гудстейна она отличается тем, что первая утверждает конечность любой последовательности Гудстейна, а вторая утверждает, что для каждой конкретной последовательности Гудстейна в арифметике Пеано есть доказательство её конечности (чувствуете разницу?). Метатеория, которая используется для доказательства, не прибегает ни к каким теоретико-множественным аксиомам. Хотя доказательство изложено большей частью "в прозе", я утверждаю, что для его формализации достаточно исчисления предикатов первого порядка, плюс индукции по натуральным числам (можете на этот счёт меня тоже повозить мордой по столу
).
Следующий вопрос, который возникает, заключается в том, что мешает выполнить доказательство этой метатеоремы в самой арифметике Пеано. Собственно, у меня есть некие идеи относительно того, как этого добиться посредством некоего расширения синтаксиса: нужно добавить средства для записи примитивно-рекурсивных функций. Правда я пока не уверен, что это возможно без выхода за пределы стандартного исчисления предикатов.
epros писал(а):
Я вовсе не возражаю против манипуляций с абстрактными объектами в математических теориях (точнее - с именами абстрактных объектов).
Это принципиальный момент в нашей дискуссии. Вы действительно настаиваете на том, что всякий абстрактный объект должен иметь имя? Если это так, то Вы ввели меня в заблуждение своими рассуждениями об объектах. Тогда уж лучше вообще не употреблять термин «абстрактный объект» и даже «объект», а говорить исключительно об «именах». И тогда начавшаяся было дискуссия, по всей видимости, будет скоропостижно завершена (и мне останется лишь погрустить о том, что мы до сих пор рассуждали о вещах, которые Вы изначально отвергали).
Я не понимаю Вашего разочарования. Что особенного в требовании, чтобы каждый объект теории можно было назвать именем собственным? Как я уже говорил, с моей точки зрения математика оперирует не "самими объектами" (кстати, независимо от того, существует ли этот объект в реальности или является абстракцией), а как раз их именами. Если она при этом признаёт, что некоторому количеству объектов она в принципе не в состоянии присвоить имена ... ну, тогда я просто не понимаю, что означает "работать в этими объектами". Это как с нелинейными аддитивными функциями
- утверждается, что они как бы есть, и их даже много, но каким-то образом идентифицировать хотя бы одну из них (например, записать для неё формулу) мы не можем.
Ниже я все же временно предполагаю, что говорить об абстрактных объектах пока еще можно -- в умозрительно-психологическом смысле -- как о неких гипотетических элементах абстрактного «универсума теории» (ибо я уже знаю, что слово «модель» Вы не любите).
Конечно же "говорить"-то я могу. Например, я в принципе понимаю что Вы имеете в виду, если говорите о нелинейной аддитивной функции
, но против того, чтобы признать их "существование" (хотя бы теоретически) моё сознание сопротивляется. Наверное так же, как Ваше - против признания существования множества всех множеств.
Скажем, достаточно ли будет привести пример непротиворечивой теории, которая расширяет арифметику Пеано, имеет очень мало дополнительных аксиом (очень простых и даже отдаленно не напоминающих аксиомы теории множеств) и в которой доказуемо существование «объекта», не имеющего имени -- ни в смысле Вашего старого определения, ни в смысле нового, приведенного ниже?
Честно говоря, вряд ли я смогу признать теорию, которая доказывает существование объекта, который не определен ни в одном из понятных для меня смыслах. Даже если дополнительных аксиом очень мало и они очень простые, это не исключает возможности их совершенной неконструктивности. Впрочем, кто знает...
(1) Начиная определение со слов «Объект
определен...», Вы либо предполагаете уже введенным термин «объект», либо хотя бы знаете (но скрываете), что такое
. Пожалуйста, уточните.
- это собственное имя (строковая константа), присвоенное объекту теории метатеорией. Что такое "сам объект" я сказать не могу, ибо полагаю, что математика работает только с именами (обозначениями).
(2) Фрагмент
метаформулы корректен только в том случае, когда
-- метапеременная. Поскольку символ
встречается отдельно от
, я заключаю, что
является не метапеременной, а метатермом. Пожалуйста, исправьте ошибку или выразитесь точнее и формальнее.
Вообще-то я здесь, конечно, ступил. Просто я хотел иметь имена объектов теории, присвоенные метатеорией (
), независимые от соответствующих им формул теории (
), но это потребует определения алгоритма, присваивающего имена, и, в общем, усложнит определение. Фиг со всем этим, давайте лучше считать, что соответствующие формулы теории - это и есть имена объектов. Тогда
вообще не нужно, а "объектами теории" следует называть непосредственно
,
и
.
Поэтому так:
является "объектом, определёным в теории
" тогда и только тогда, когда
.
P.S. Поскольку дело идет к тому, что это не последняя версия Вашего определения
, давайте будем их нумеровать или как-то называть. А поскольку определения -- Ваши, предлагаю Вам их и нумеровать/называть/обзывать.
Я в общем-то не дезавуирую первого определения. Как Вы можете заметить, объектам первого рода (замкнутым термам, примеры:
) соответствуют объекты второго рода (формулы теории, примеры:
). Так что второе определение в некотором смысле расширяет первое: я учёл Вашу претензию (которая показалась мне обоснованной), что теории без констант не следует лишать прав "определять объекты". Называть определения пока никак не буду, давайте уж пользоваться номерами.