NP≠P. Док-во от противного-контрпример алгоритмов из NP

[dmitgu]

Уважаемый mihaild, Вы не разобрали пример про ёжика :) А там есть почти все ответы на Ваши вопросы. Напомню:

dmitgu в сообщении #1311009 писал(а):

Пример - язык из слов - грамматически правильные тексты из русских букв, пробелов и знаков пунктуации. Рассмотрим рассказ:

"Ёжик отправился в ночной блаблабла лес на охоту. <Дальше продолжение текста>". Данный текст будет отвергнут на практике как не соответствующий грамматике на первом же предложении. Потому что "внутреннее слово" с набором символов "блаблабла" не является грамматически правильным. А текст (любой), содержащий грамматически некорректный отрезок - тоже не является грамматически корректным. То есть, мы имеем практический пример языка с "исключающими внутренними словами".

Теперь - про Ваши вопросы.

mihaild в сообщении #1311024 писал(а):

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

Совсем не очевидно. В примере с ёжиком Вам придётся ставить два символа # - в конце текста и сразу после "блаблабла"?
Но тогда Вы испортите слово - ведь в нём не должно быть символов #. А способ выделения слова позволяет сразу его отвергнуть после "блаблабла". То есть - у нас есть слово в самом начале другого слова и читать другое слово не требуется и даже - такое чтение было бы нарушением распознания языка, так как оно игнорирует уже обнаруженное слово.

mihaild в сообщении #1311024 писал(а):

dmitgu в сообщении #1311009
писал(а):
Так как сама теория состоит из утверждений, то $2+2$ не могут дать $4$

mihaild: Первый раз вижу формулировку вида "(терм) не может дать (другой терм)", и не могу представить, что бы она могла означать.

Да нет же ) Я же пишу "сама теория состоит из утверждений". То есть отдельно термы в теории не присутствуют. Нет отдельно терма $2+2$ внутри теории Пеано - он обязательно внутри некоторого утверждения. То же самое и про терм $4$. Поэтому возникает понятие "представляет" про алгоритм. Я же это не выдумываю - Вы спорите тут не со мной, а с формализмом математической логики ))

mihaild в сообщении #1311024 писал(а):

Пусть $f$ и $g$ - слова длины $n$ и $m$ в алфавите $A$, $m \leqslant n$. Слово $g$ называется подсловом (или подстрокой) слова $f$, если существует такое $k \leqslant n - m$, что $f(k) = g(1), f(k + 1) = g(2), \ldots, f(k + m - 1) = g(m)$.
Вы про это?

Да я про это - при этом $k=1$ в примере с ёжиком.

mihaild в сообщении #1311024 писал(а):

Понятие "принадлежность чему-то там противоречит" не определено.

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

dmitgu в сообщении #1305422 писал(а):

В разбираемом нами случае «внутреннее слово» будет отвергнуто при его проверке на принадлежность языку сразу, как только способ выделения слова обнаружит «внутреннее слово» внутри «слова-контейнера». Из этого следует, что слово-контейнер тоже в данном случае не принадлежит языку, потому что до его проверки «целиком» дело не доходит, и оно отвергается фактически вместе со своим «внутренним словом». Если бы было иначе, то в определении языка имелось бы противоречие между проверками для «внутреннего слова» и для «слова-контейнера».

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

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

[mihaild]

dmitgu в сообщении #1312502 писал(а):

Уважаемый mihaild, Вы не разобрали пример про ёжика

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

dmitgu в сообщении #1312502 писал(а):

А способ выделения слова позволяет сразу его отвергнуть после "блаблабла".

mihaild в сообщении #1308833 писал(а):

Понятие "способ выделения слова" не определено.

Кроме того, читайте внимательнее.

mihaild в сообщении #1311024 писал(а):

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

Это значит, что неважно, взять $\#$ или $\star$ - истинность интересных нам утверждений от этого не поменяется.

dmitgu в сообщении #1312502 писал(а):

такое чтение было бы нарушением распознания языка

Понятие "нарушения распознания языка" (как и понятие "распознание языка") не определено.

dmitgu в сообщении #1312502 писал(а):

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

Откуда тут внезапно взялись алгоритмы, вроде же всего лишь об исчислении предикатов говорили?
Ну и в "формализме математической логике" не определяется понятие вида "терм не может дать терм".
(кстати, фраза "$2 + 2$ не могут дать $4$" даже просто грамматически не согласовано - к чему относится глагол "могут"?)
Утверждения вида "$2 + 2$ не могут дать $4$" в стандартных книгах не встречаются, и я не понимаю, что они могли бы означать.

Теория в сигнатуре - это множество замкнутых формул в этой сигнатуре. Что значит "терм внутри теории" - тоже непонятно.
Формулы отличаются от термов (даже просто синтаксически), да. Вы про это?

dmitgu в сообщении #1312502 писал(а):

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

Нет, вы пока что ничего не показали.

Давайте вы либо будете стараться разобраться в стандартных определениях, либо будете предлагать свои, но на хотя бы минимальном уровне строгости. И сначала определения (вида "$X$ - это $Y$, такой что $Z$"), потом (опционально) примеры. Иначе мы так никогда никуда и не уедем.

Пока что даже непонятно, какое именно определение вам не нравится - языка, машины Тьюринга, понятия "машина Тьюринга распознает язык", еще какое-то?

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

[dmitgu]

mihaild в сообщении #1312508 писал(а):

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

Вообще-то я говорил про теорию Пеано.

А «теория представляет алгоритмы» возникло от того, что теория состоит из утверждений (доказанных). И алгоритм «представлен» утверждениями, которые равны либо формуле с подставленными «правильными» значениями («правильными» с точки зрения результата работы данного алгоритма – типа $2+2 = 4$), либо отрицанию этой же формулы - при подставленных неправильных значениях (типа $\neg (2+2 = 5)$ ).

Но Бог с ним – с термином «представлен». Для языка в теории алгоритмов можно не приспосабливать термин «представлен», а использовать, видимо «алгоритм распознаёт язык». Но так же, как в теории Пеано доказывается, что данный алгоритм «представлен» данной логической формулой, так же и в теории алгоритмов необходимо аналогичное доказательство того, что данный алгоритм «распознаёт» данный язык. А вовсе не уповать на то, что если определён протокол работы алгоритма, то этот алгоритм обязательно будет «распознавать» любой обсуждаемый язык. :)

mihaild писал(а):

Утверждения вида "$2+2$ не могут дать $4$" в стандартных книгах не встречаются

Да, я слишком «сократил». Хотя, если быть точным, то я писал «Так как сама теория состоит из утверждений, то $2+2$ не могут дать $4$». Поясняю:

$2+2$ не является утверждением, поэтому отдельно $2+2$ внутри теории нет – а может быть только внутри некоторых утверждений. А раз нет «отдельно» ни $2+2$, ни $4$, то и «отдельно» они не могут следовать друг из друга. А утверждения – могут. Например, доказано утверждение вида:

$A \Rightarrow (A \Rightarrow B)$ из него следует (оно «даёт») утверждение $(A \Rightarrow B)$.

mihaild писал(а):

Что значит "терм внутри теории" - тоже непонятно

Мне это тоже непонятно )) Я писал «Нет отдельно терма $2+2$ внутри теории Пеано - он обязательно внутри некоторого утверждения».

То есть – нет такого "терм внутри теории", я и написал, что «не понятно» в рамках теории Пеано )) А примеры утверждений (отдельных) внутри теории и термов внутри утверждений я дал.

mihaild писал(а):

Формулы отличаются от термов (даже просто синтаксически), да. Вы про это?

Именно. И о том, что теория состоит из отдельных утверждений (они являются «словами» теории как языка) – но не из отдельных термов.

mihaild в сообщении #1312508 писал(а):

все интересные нам утверждения не зависят от того, какой именно символ выбрать Это значит, что неважно, взять $\#$ или $\star$ - истинность интересных нам утверждений от этого не поменяется.

Нет, зависят – Вы сами писали, что символ не должен быть одним из символов слова. И в разбираемом мной примере этот символ «влезал» внутрь слова, так как внутри одного слова находилось другое. И совершенно неважно, какой именно символ туда «влезает» - если он не должен быть внутри слова. Получается, что происходит подмена одного слова другим и с чего тогда будет правильное распознание? У нас на ленте получается слово не из символов языка, да к тому же оно «обрывается посредине» тем символом, который означает конец «входа».

mihaild писал(а):

Примеры могут только дополнять определения, но не заменять их.

Не согласен. Пример может быть определением конкретного языка. Так и есть в моём примере с ёжиком. Да, это не общее определение – так тем проще с ним работать. А после понимания конкретного примера можно переходить к обобщениям и более абстрактным определениям. Или не понятно, что такое «грамматически корректные тексты»? Так я могу упростить это до такого уровня, например:

Если в последовательности упорядоченных символов X встречается строка $Y=\text{«блаблабла»}$, то для языка $G$ (условно назовём его «языком грамматически правильных текстов») словом является $Y$ и это слово не принадлежит языку $G$, равно как не принадлежит языку $G$ и последовательность $X$, независимо от остального (помимо $Y$) своего содержимого.

Строка $Y$ называется «исключающим внутренним словом».

Слово $Y$ отвергается вместе с содержащим его словом $X$ (если это слово! Поясню ниже) в силу «способа выделения слова» (поясню ниже) $Y$, который состоит в обнаружении слова $Y$ внутри $X$. Разумеется, способ мог бы быть и более сложным – в духе регулярных выражений, например, но это был бы другой язык.

То есть, не принадлежность языку $G$ слова означает наличие внутри данного слова подстроки $Y=\text{«блаблабла»}$. При этом данная подстрока $Y$ тоже является словом, не принадлежащим языку $G$.

А это означает, что обнаружение данной подстроки $Y=\text{«блаблабла»}$ логически эквивалентно непринадлежности всей строки языку $G$ как слова.

А это означает, что время работы алгоритма, который распознаёт данный язык должно зависеть именно от времени обнаружения подстроки $Y=\text{«блаблабла»}$, а не от размера слова, которое эту подстроку содержит. Иначе время работы определяется качеством реализации алгоритма, а не природой языка. Мы об этом уже говорили при обсуждении «очистки ленты» при завершении работы алгоритма.

Разница со случаем «нет выделения внутреннего слова» в том, что в «неделимом» слове должен быть обнаружен его конец. Сначала или после этого идёт анализ на наличие $ \text{«блаблабла»}$ - не важно.

Ведь язык - множество конечных слов. Поэтому без «внутреннего слова» необходимо наличие конца всей последовательности символов. Это и будет «способ выделения слова». А при наличии «внутреннего слова» достаточно найти только его. И неважно – внутри чего это «внутреннее слово». Если внутри слова (конечного) – то и оно отвергнуто. Если внутри не-слова (бесконечного) – тогда «внутреннее слово» не «внутреннее», а «само по себе». Такой «способ выделения слова».

Отсюда вывод для конкретного примера:

Алгоритм $A_G$ распознаёт язык $G$, если считывающая головка после чтения слова $Y$ прекращает дальнейшее чтение «входных данных» на ленте и выдаёт $0$ (ноль) – «слово не принадлежит языку $G$».

То есть, конец слова, не принадлежащего языку $G$, обнаруживается на «внутреннем слове». Вот в чём отличие от языка, где внутри слов нет «внутренних слов».

[mihaild]

dmitgu в сообщении #1312857 писал(а):

теория состоит из утверждений (доказанных)

Нет, теория состоит из аксиом (формул). Например, $S(0) \cdot 0 = 0$ доказывается в арифметике, но ей не принадлежит (не является аксиомой).

dmitgu в сообщении #1312857 писал(а):

как в теории Пеано доказывается, что данный алгоритм «представлен» данной логической формулой

В арифметике нет понятия "алгоритм". Для любой МТ можно записать $\Delta_0$ формулу арифметики вида $P(x, y, n)$, означающую, что наша МТ на входе $x$ останавливается с выходом $y$ за не более чем $n$ шагов. Но само по себе это утверждение (про возможность записать формулу) формулируется уже не в арифметике. И доказывается, соответственно, тоже не в ней.

dmitgu в сообщении #1312857 писал(а):

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

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

dmitgu в сообщении #1312857 писал(а):

$A \Rightarrow (A \Rightarrow B)$ из него следует (оно «даёт») утверждение $(A \Rightarrow B)$.

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

dmitgu в сообщении #1312857 писал(а):

отдельно $2+2$ внутри теории нет

Что вообще значит "отдельно внутри теории"?
Формально, теория - это множество слов определенного вида в определенном алфавите. Верно ли, что "слово $x$ есть отдельно внутри теории $T$" означает "$x \in T$"? Если да, то давайте так и говорить (зачем тут слова "отдельно" и "внутри" в таком случае - непонятно).

dmitgu в сообщении #1312857 писал(а):

примеры утверждений (отдельных) внутри теории и термов внутри утверждений

Давайте еще запретим слово "внутри".
Теория содержит утверждения - как элементы множества. Т.е. $a + 0 = a$ принадлежит PA.
Утверждения не содержат термы как свои элементы. Терм $a + 0$ является подстрокой утверждения $a + 0 = a$.
Если оба этих отношения - "быть элементом" и "быть подстрокой" - означать одним словом "внутри", то мы запутаемся (еще больше).

dmitgu в сообщении #1312857 писал(а):

Получается, что происходит подмена одного слова другим и с чего тогда будет правильное распознание?

Потому что нам "неинтересны" утверждения "вот ровно эта МТ, ровно с такими символами, распознает этот язык". Когда нам приносят язык, нам интересно, можно ли его распознать какой-нибудь МТ (и можно ли это сделать "быстро").
Если сильно хочется, можно для каждого языка $L$ и символа $c$ не из алфавита этого языка ввести определение "МТ $c$-распознает $L$ за такое-то время". И доказать, что если для какого-то символа $c$ существует МТ, $c$-распознающая $L$ за время $f$, то для любого $c'$ существует МТ, $c'$-распознающая $L$ за время $f$.
Прочитайте это (и предыдущие сообщения) по этой теме внимательно. Это всё настолько очевидные технические детали, что у меня возникает сильное подозрение, что вы имеете в виду не то, что формулируете.

dmitgu в сообщении #1312857 писал(а):

Если в последовательности упорядоченных символов X встречается строка $Y=\text{«блаблабла»}$, то для языка $G$ (условно назовём его «языком грамматически правильных текстов») словом является $Y$ и это слово не принадлежит языку $G$, равно как не принадлежит языку $G$ и последовательность $X$, независимо от остального (помимо $Y$) своего содержимого.

Что значит "слово $Y$ является словом для языка"?
Ну и непонятно, в каком порядке у вас тут идут кванторы. Давайте попробуем подставить: $X = \text{блаблабла}$, $G = [\text{а-я}]^*$ (все конечные последовательности русских букв).
Получим: Если в $X$ встречается строка $Y$ [да, встречается], то для языка $G$ словом является $Y$ и это слово не принадлежит языку $G$ и ... Получаем, что $Y \notin G$, что неправда.

Вы, возможно, имеете в виду что-то такое: "слово $Y$ называется исключающим внутренним словом словом для языка $G$, если для любого слова $X \in G$ слово $Y$ не является подстрокой $X$"?
Ну и "давайте для слова $Y$ рассмотрим язык $G_Y$, содержащий все слова, для которых $Y$ не является подстрокой".

dmitgu в сообщении #1312857 писал(а):

А это означает, что время работы алгоритма, который распознаёт данный язык должно зависеть именно от времени обнаружения подстроки $Y=\text{«блаблабла»}$, а не от размера слова, которое эту подстроку содержит.

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

dmitgu в сообщении #1312857 писал(а):

Иначе время работы определяется качеством реализации алгоритма, а не природой языка

Время работы алгоритма - это, внезапно, свойство алгоритма, а не языка.
Свойством языка может быть существование распознающего его алгоритма, работающего определенное время.
И тут возникает вопрос - на разных словах языка алгоритм может работать разное время, что тогда значит "алгоритм распознает язык за такое-то время"? Для каждого слова время работы алгоритма на этом слове - число. Давайте каждому слову припишем какое-то число и потребуем, чтобы алгоритм на этом слове работал не дольше этого числа. Но каждому слову приписывать число руками неудобно, давайте возьмем какую-нибудь простую характеристику слова и будем вычислять ограничение на время работы в зависимости от этой характеристики. Чтобы такое можно взять? Можно конечно скажем возвести число разных символов на четных позициях в степень числа разных символов на нечетных позициях, но из этого как-то ничего интересного не получается. Поэтому давайте возьмем длину слова - это и понятно, и отвечает практическому использованию - работать с бОльшими объектами сложнее.

dmitgu в сообщении #1312857 писал(а):

Алгоритм $A_G$ распознаёт язык $G$, если считывающая головка после чтения слова $Y$ прекращает дальнейшее чтение «входных данных» на ленте и выдаёт $0$ (ноль) – «слово не принадлежит языку $G$».

Это определение работает только для языков вида $G_Y$.
Кроме того, это явно неполное определение: например, оно вообще ничего не говорит, что делает МТ на словах, подсловом которых $Y$ не является.
(еще не определено, что значит "считывающая головка после чтения слова $Y$", но это пока можно оставить, хотя возможно дальше и понадобится)

[epros]

mihaild в сообщении #1312881 писал(а):

Нет, теория состоит из аксиом (формул). Например, $S(0) \cdot 0 = 0$ доказывается в арифметике, но ей не принадлежит (не является аксиомой).

Не могли бы Вы пояснить по терминологии? Насколько я понимаю, слова, определяющие "теорию" как "множество формул", например, вот эти:

mihaild в сообщении #1312508 писал(а):

Теория в сигнатуре - это множество замкнутых формул в этой сигнатуре.

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

Вы используете какое-то иное определение термина "теория"?

[mihaild]

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

Вы используете какое-то иное определение термина "теория"?

Верещагин, Шень в Языки и исчисления, стр. 142 писал(а):

Пусть $\Gamma$ - произвольное множество замкнутых формул рассматриваемой нами сигнатуры $\sigma$. (Такие множества называются теориями в сигнатуре $\sigma$)

(курсив авторский)

Беклемишев в Введение в математическую логику, стр. 42 писал(а):

Теорией сигнатуры $\Sigma$ называем произвольное множество $T$ замкнутых формул языка $\mathbf{L}_\Sigma$.

[epros]

КВерещагину, Шеню и Беклемишеву нет вопросов, они не пишут, что теория состоит из аксиом, а теоремы ей не принадлежат. Вопрос к Вашему утверждению, что $S(0) \cdot 0 = 0$ не принадлежит арифметике. Это терминологическое недоразумение?

[mihaild]

У нас есть множество строк в арифметической сигнатуре - аксиомы арифметики Пеано, обозначим это множество $PA$. И у нас есть строка $x = <<S(0) \cdot 0 = 0>>$. При этом по определению $PA$ имеем $x \notin PA$. Именно это я и имел в виду под "$S(0) \cdot 0 = 0$ не принадлежит арифметике".

Авторы пишут, что теория - это произвольное множество замкнутых формул. В том числе и незамкнутое относительно выводимости.

[epros]

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

[mihaild]

Формулировка "что-то там принадлежит теории" сама по себе довольно странная.
Если говорить совсем формально, то символ $S$ не принадлежит ни арифметической сигнатуре, потому что сигнатура - это кортеж из трех элементов, ни даже одному из элементов этого кортежа - потому что внутри кортежа к символам приписана валентность.
(упорядоченное поле - это как морская свинка: и не поле, и не упорядоченное)

Я правильно понимаю, что в вашей интерпретации $PA$ - это множество строк, являющихся теоремами арифметики? Для того, что обычно называют "аксиомами арифметики", у вас какое-то обозначение есть?

[epros]

mihaild в сообщении #1313502 писал(а):

Формулировка "что-то там принадлежит теории" сама по себе довольно странная.

Ну почему же? Раз теория - это множество чего-то там, то это что-то там этому множеству принадлежит.

mihaild в сообщении #1313502 писал(а):

Я правильно понимаю, что в вашей интерпретации $PA$ - это множество строк, являющихся теоремами арифметики?

Да.

mihaild в сообщении #1313502 писал(а):

Для того, что обычно называют "аксиомами арифметики", у вас какое-то обозначение есть?

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

[mihaild]

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

Ну почему же?

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

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

[epros]

mihaild в сообщении #1313545 писал(а):

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

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

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

(Уточнение)

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

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

mihaild в сообщении #1313545 писал(а):

И в любом случае - есть хоть какой-то повод считать этот вопрос важным?

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

[Someone]

(Оффтоп)

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

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

((Уточнение))

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

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

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

[epros]

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

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

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

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