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

[dmitgu]

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

Полным образом эта модель интерпретации описывается теорией 2-го порядка и эта теория – полна.
mihaild: Такого быть не может - иначе бы мы смогли из этого сделать полное эффективное непротиворечивое расширение PA.

Конечно можем, и конечно сделали но не эффективное )) Только сделано это для теории, которая не является эффективно аксиоматизируемой. Вы вспомните доказательство теорем Гёделя – они существенно опираются на доступность всех аксиом 1-го порядка, а для теории 2-го порядка свести дело к аксиомам 1-го порядка не получается.

«Стандартная интерпретация арифметики» - да, так правильно, без «модель». Про выразимость её в логике 2-го порядка для арифметики – Дж. Булос, Р.Джеффри «Вычислимость и логика», Глава 18 «Логика второго порядка». Там в начале главы ставятся вопросы – вот как раз (5) о полной теории для арифметики. Все аксиомы Пеано плюс всего одна аксиома второго порядка – аксиома индукции, но с квантором общности по любым формулам теории Пеано. Собственно, эту аксиому я и упоминал в контексте практической бесполезности (отсутствия возможности получить аксиомы 1-го порядка из неё в общем случае).

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

Что такое "стек" в математике - не знаю, и за 30 секунд не придумал, как можно было бы разумно определить.

Представляйте себе свою интерпретацию, если хотите ) В теории слов (базе для теории языков) все её свойства будут соответствовать данной теории.

В моей интерпретации со стеком я прозевал возможность циклов. Устранить её можно и устраняю так:

5+. Нельзя выделить ни одно подмножество элементов среди множества элементов стека, чтобы среди всех их $id_{this}$ не нашёлся хотя бы один такой, который не используется ни в одном $id_{next}$ данного подмножества.

Ну, и ещё я допустил бы бесконечные строки (начало есть, а конца – нет). В Вашей интерпретации это тоже возможно. Для бесконечных строк для интерпретации «стек» только один $id_{this}$, который не равен никакому $id_{next}$. А вот каждый $id_{next}$ соответствует одному и только одному $id_{this}$.

Все эти построения с номерами – это всего лишь интерпретации. Кому-то важны приложения слов и языков в теории множеств, кто-то исследует слова как сплошные записи в клетках ленты МТ, для кого-то нужны ДНК, в которых минимальные "внутренние слова"- аминокислоты и т.д. и т.п. Как видите, в некоторых интерпретациях номера и близко не присутствуют. А теория для языков должна работать для всех этих случаев, отражая общие для них свойства «слов» и «языка». Это как теория гармонических колебаний - годится для массы процессов, но сама не содержит специфических свойств ни для маятника, ни для пружинок, ни для электрических контуров, ни для ещё миллиона возможных способов получить гармонические колебания.

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

И, кстати, у Вас есть основание сказать мне как Шерлок Холмс: «Как Вы были правы, Ватсон -«Определения не будет» )))) А прав я в данном случае потому, что раз нет теории, то и нет ничего такого, на основе чего можно давать определение. А поскольку термин «слово» является ключевым для теории языков, то это – неопределяемое понятие. А его свойства задаются соответствующими аксиомами, которые ещё только предстоит написать.

Да, и всякие «неделимые слова» я думаю не рассматривать и п.8 из своей интерпретации выбросить. В Вашей интерпретации тоже любое подмножество оказывается словом – с символами и порядком – то есть – словом, а это тоже означает «делимость» слов.

Давайте напишем аксиомы, что ли ) Аксиомы для слов – что даст основу для теории языков. Для предметных переменных типа «слово» буду использовать все переменные, кроме $i$, $j$, $k$, $l$, $m$, $n$ – которые оставлю для натуральных чисел.

$a = b \Leftrightarrow \forall i: str(a, i, 1) = str(b, i, 1)$, что такое равенство слов

$str(a, i, 1) = \emptyset \Rightarrow str(a, i + 1, 1) = \emptyset$, что такое конец слова (если он есть)

1-я аксиома «рекурсии» для $str()$:

$\forall a \forall i \exists b: b = str(a, i, 1) \wedge ( \exists j: b = ChrStr(j) )$, из каких элементарных слов состоит слово

$\forall i \exists a: a = ChrStr(i)$, как получить элементарное слово (про ограниченность алфавита – ниже)

2-я аксиома «рекурсии» для $str()$ и одновременно – 1-я аксиома конкатенации:

$str(a, i, j+1) = str(a, i, j) \cdot str(a, i + j, 1)$, подстрока – это цепочка простейших строк

$\forall a \forall i \forall j \exists b: b = str(a, i, j)$, подстрока – это слово

Что такое символ:

$\exists I_{ChrLim}:$

$( \forall i > I_{ChrLim}: ChrStr(i) = \emptyset )$

$\wedge ( \forall i \le I_{ChrLim} \forall j \le I_{ChrLim}: i = j \Leftrightarrow ChrStr(i) = ChrStr(j) )$

$\wedge ( \forall i \le I_{ChrLim}: ChrStr(i) = Str(ChrStr(i), 1, 1) \wedge Str(ChrStr(i), 2, 1) = \emptyset )$

Определение для $Len(a)$:

1. $len(\emptyset) = 0$

2. $( \exists i: str(a, i, 1) \ne \emptyset \wedge str(a, i + 1, 1) = \emptyset ) \Rightarrow len(a) = i$

3. $len(a)$ не определено в ином случае

2-я Аксиома конкатенации:

$( \exists len(a) ) \Rightarrow$

$( \exists c = a \cdot b )$

$\wedge ( i \le len(a) \Rightarrow str(c, i, 1) = str(a, i, 1) )$

$\wedge ( i > len(a) \Rightarrow str(c, i, 1) = str(b, i - len(a), 1) )$

Аксиома для поиска и его однозначности (самое короткое слово перед найденным):

$find(in, what) \Leftrightarrow$

$( \exists a \exists b (a \cdot what \cdot b = in) \wedge \forall c \forall d (c \cdot what \cdot d = in \wedge c \ne a \Rightarrow str(c, len(a)+1, 1) \ne \emptyset ) )$

Аксиома о времени поиска:

Это уже для приложения к алгоритмам – время линейно от $len(a \cdot what)$

Наверно (хайли лайкли :)) какие-то нюансы прозевал.

[mihaild]

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

Конечно можем, и конечно сделали но не эффективное

Как же не эффективное? Множество доказательств даже в арифметике второго порядка перечислимо. Если бы она была полна (т.е. для каждого утверждения выводилось бы либо оно, либо его отрицание), то делаем следующее: берем формулу первого порядка, перебираем все возможные строки, каждую из них проверяем, является ли она доказательством этой формулы или ее отрицания; останавливаемся, когда найдем. Если нашли доказательство формулы - объявляем ее аксиомой нашей теории $T$. Т.к. арифметика второго порядка полна, то наш алгоритм проверки всегда останавливается.
Таким образом, теория $T$ является теорией первого порядка, разрешимой, непротиворечивой, и содержащей все аксиомы арифметики Пеано. А такой не бывает.

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

вот как раз (5) о полной теории для арифметики

Там говорится, что существует теория второго порядка, все модели которой изоморфны $\mathbb{N}$ (если я правильно понял обозначения). Для теории первого порядка это бы действительно означало, что теория полна - ее теоремами были бы в точности все утверждения, истинные в этой модели. Для теорий второго порядка это неверно.

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

Представляйте себе свою интерпретацию, если хотите

Я не могу себе представить интерпретацию "того, не знаю чего".

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

кто-то исследует слова как сплошные записи в клетках ленты МТ, для кого-то нужны ДНК, в которых минимальные "внутренние слова"- аминокислоты и т.д. и т.п. Как видите, в некоторых интерпретациях номера и близко не присутствуют

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

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

Все эти построения с номерами – это всего лишь интерпретации

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

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

Определения не будет

Ну, значит вам как минимум надо смириться с тем, что вы занимаетесь чем-то сильно отличным от известного вопроса равенства P и NP.

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

Давайте напишем аксиомы

Прежде чем писать аксиомы, нужно указать сигнатуру - что будет константами, что предикатными символами, что функциональными, и какой валентности. Напишите, и желательно с краткими комментариями, что каждый символ будет означать. Хотя бы что значит третий аргумент у $str$?

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

$( \exists len(a) )$

Так писать нельзя чисто синтаксически.
Кстати, аксиомы вида $\exists x: x = f(y)$ в теории первого порядка не нужны - они выполнены автоматически.
(если уж вы так хотите свою теорию, а не расширение ZF )

Я не всматривался тщательно в ваши аксиомы, но кажется если мы будем считать словом функцию $\mathbb{N} \to A \cup \{\varnothing\}$, не равную $\varnothing$ до какого-то номера и равную $\varnothing$, начиная с этого номера, то получится примерно то же самое.
$str(a, i, 1)$ - это же $i$-й символ строки $a$?

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

$\forall a \forall i \exists b: b = str(a, i, 1) \wedge ( \exists j: b = ChrStr(j) )$

Это эквивалентно $\forall a \forall i \exists j: str(a, i, 1) = ChrStr(j)$? (sanity check на одинаковость понимания)

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

[dmitgu]

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

dmitgu в сообщении #1317546
писал(а): вот как раз (5) о полной теории для арифметики

mihaild: Там говорится, что существует теория второго порядка, все модели которой изоморфны $\mathbb{N}$ ... Для теории первого порядка это бы действительно означало, что теория полна ... Для теорий второго порядка это неверно.

Ну да, надо было мне сослаться на следствие 18.1 из этой теоремы 18.1 (про вопрос 5) – это как раз ответ на вопрос (4), про полноту. Полнота — это верно для теории второго порядка про арифметику.

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

dmitgu в сообщении #1317546
писал(а): Конечно можем, и конечно сделали но не эффективное

mihaild: Как же не эффективное? Множество доказательств даже в арифметике второго порядка перечислимо. Если бы она была полна (т.е. для каждого утверждения выводилось бы либо оно, либо его отрицание), то делаем следующее: берем формулу первого порядка, перебираем все возможные строки ...

Да нет такой возможности для теории 2-го порядка – см. Следствие 18.2. Там прямо Ваши рассуждения, но они опровергаются (хоть доказательство и неконструктивное) – Не существует эффективного позитивного теста на общезначимость в логике 2-го порядка.

Могу, наверно, пояснить (добавить конструктивности), почему. Мы в этой дискуссии разбирали утверждение, которое алгоритм Sol (произвольный, но соответствующий утверждению) не может ни подтвердить, ни опровергнуть – его ответ окажется противоположным факту. Да, это теория первого порядка и поэтому она не полна. Но сам принцип наличия «неподъемного» утверждения для алгоритма не из неполноты следует, а как раз наоборот!

А в условиях логики 2-го порядка можно формулировать утверждения, основанные на невозможности сделать что-либо алгоритмом – притом для каждого произвольного алгоритма – с квантором всеобщности. Вот такое расширение, да оно и есть фактически как часть арифметики – поэтому и доказаны теоремы о неполноте. И как тогда алгоритм сможет «перебрать» доказательства/опровержения для этого расширения, если оно основано на невозможности для данного алгоритма это сделать?

И заметим, что выводимость – будет. Просто если использовать условие «использовать для решения другой алгоритм» и взять некий более сложный – и получишь правильный ответ, и не зациклишься. То есть, для построения доказательств в логике второго порядка требуется менять алгоритмы (способы) для этих построений – вообще говоря. Или, как написано в конце Следствия 18.2 «Это не логика <второго порядка> неполна, неполны предлагаемые нами формализации».

И, кстати, проверка доказательств – это не их поиск. То, что в нашей дискуссии используется как $NP$-алгоритм вполне может подтвердить доказательство для того утверждения, для которого корректный алгоритм $Sol$ может выдать лишь ноль («не подтверждаю»).

И, разумеется, «неполнота» логики 2-го порядка (условная) не имеет отношения к теории 2-го порядка для арифметики – для арифметики-то теория полная.

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

dmitgu в сообщении #1317546 писал(а): Представляйте себе свою интерпретацию, если хотите

mihaild: Я не могу себе представить интерпретацию "того, не знаю чего".

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

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

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

Именно это я и стараюсь выразить аксиомами.

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

dmitgu в сообщении #1317546 писал(а): Определения не будет

mihaild: Ну, значит вам как минимум надо смириться с тем, что вы занимаетесь чем-то сильно отличным от известного вопроса равенства P и NP.

Это Вам надо смириться с тем, что есть неопределяемые понятия )) Это основы математики. И свойства неопределяемых понятий задаются аксиомами. Вот в теории Пеано аксиомы – о натуральных числах. Вы видите там какие-то определения чисел? Нет. Вы видите в геометрии определение для «прямая», «точка»? Нет. Может, Вы в теории множеств видите какое-то определение для множеств? Тоже нет. Смиритесь )

А обсуждать, почему аксиомы такие и что они обозначают – да, можно и нужно. Что обозначают мои аксиомы о «словах» – вполне понятно. И они в равной степени подходят и к вашей интерпретации с нумераторами и к моей со стеком. И к фанерке, на которой написаны клеточки в одну линию, куда вписаны символы.

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

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

что значит третий аргумент у $str$?

Длина подстроки (точнее, максимальная длина – слово может кончиться и раньше). Это понятно из 2-й аксиомы «рекурсии» для $str()$.

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

dmitgu в сообщении #1317546 писал(а): $( \exists len(a) )$

mihaild: Так писать нельзя чисто синтаксически.
Кстати, аксиомы вида $\exists x: x = f(y)$ в теории первого порядка не нужны - они выполнены автоматически.

Да ради Бога ) Это просто сокращение для более длинного повтора куска из определения $len(a)$ – о существовании такого $i$, что на $i$-м месте ещё есть символ, а на $i+1$ – уже пусто. Я рассматриваю ещё и бесконечные слова, и не у всех слов имеется конец (начало есть у всех). И $\exists x: x = f(x)$ здесь не всегда верно – смотрите определение $len()$, пункт 3.

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

$str(a, i, 1)$ - это же $i$-й символ строки $a$?

Это строка из $i$-го символа строки $a$. Символы как отдельные объекты (со своими предметными константами и переменными) не требуются. Можно обойтись конкатенацией «простейших строк». Так я и сделал.

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

dmitgu в сообщении #1317546 писал(а): $\forall a \forall i \exists b: b = str(a, i, 1) \wedge ( \exists j: b = ChrStr(j) )$

mihaild: Это эквивалентно $\forall a \forall i \exists j: str(a, i, 1) = ChrStr(j)$? (sanity check на одинаковость понимания)

Да. Наверно, Ваш вариант практичней. То, что $str(a, i, 1)$ является словом, понятно и из других аксиом. Я в своем варианте аксиомы это лишний раз показываю, но можно этого не делать.

Я заметил, что кое-что прозевал. Вот такие исправленные аксиомы нужны:

1-я аксиома «рекурсии» для $str()$ (дополнил для 0-го места и учёл Ваше улучшение):

$\forall a: str(a, 0, 1) = \emptyset \wedge \forall i \exists j: str(a, i, 1) = ChrStr(j)$, из каких элементарных слов состоит слово.

Можно, конечно, нумеровать символы в строке и с $0$, но ноль удобен для «технических нужд» (в той же функции $find()$, например, аксиома про которую ниже), да и ошибки делаешь реже, когда длина строки равна номеру места её последнего символа.

Что такое символ: (добавил, что не равны пустым строкам те простейшие строки, которые сделаны из символа с кодом в пределах $I_{ChrLim}$)

$\exists I_{ChrLim}:$

$( \forall i > I_{ChrLim}: ChrStr(i) = \emptyset )$

$\wedge ( \forall i \le I_{ChrLim} \forall j \le I_{ChrLim}: i = j \Leftrightarrow ChrStr(i) = ChrStr(j) )$

$\wedge ( \forall i \le I_{ChrLim}: ChrStr(i) \ne \emptyset \wedge ChrStr(i) = Str(ChrStr(i), 1, 1) \wedge Str(ChrStr(i), 2, 1) = \emptyset )$

Аксиома для поиска и его однозначности (самое короткое слово перед найденным – уточнил, в какой позиции найдено):

$find(in, what) = i \wedge i \ne 0 \Leftrightarrow$

$str(in, i, len(what)) = what \wedge \forall a: ( a \cdot what = str(in, 1, len(a \cdot what)) \Rightarrow len(a) \ge i )$

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

Пока что ничего нового, только слегка запутанное старое.

Я же не из любви к первооткрывательству это всё пишу. Давайте готовую адекватную (где нормальные аксиомы, а не утверждения типа «слово это цепочка…») теорию языков, если она есть и меня это устроит гораздо больше, чем самому делать нужные прямо сейчас основы теории языков. Но где эти «закрома формализма»? Нету их, вот и приходится самим делать, так что новое это, чего уж там )) Ну, ведь «не Боги горшки обжигают».

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

(и как вы собираетесь из этого выруливать на алгоритмы - совершенно непонятно)

Да очень просто ) Для алгоритмов запись слова – это символы «в клеточках на фанерке» )) И мне важно, что часть слова – тоже слово. И вот отсюда как раз и будет завершение доказательства. Потому что $NP$-алгоритм для специальных утверждений работает полиномиальное время от размера слова из языка $C$:

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

Зафиксированные договоренности
…
7. $C$ - язык из слов вида $Anti_{Sol, S}, Sol, S$, где $Sol$ - некоторый алгоритм от трех аргументов, $S$ - число в двоичной записи, $Anti_{Sol, S}$ - формула, получаемая применением леммы о диагонализации к формуле $Sol(x, S, ss(S)) = 0$ (считая $x$ свободной переменной)

8. $LS = A \cup B \setminus C$

И соответствующий $P$-алгоритм $Sol$, решающий ту же задачу – тоже должен будет работать полиномиальное время именно от размера слова из $C$, пусть оно и будет частью слова из $B$, которое подано на «вход», но и слово из $C$ внутри слова из $B$ там тоже будет.

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

Теперь мы, вроде бы, наконец выяснили, что внутри слова другое слово быть может )) Из этого (далее план завершения доказательства описываю) получим, что конкретно $Sol$ выдаст $0$ за полиномиальное время от размера некоторого слова из $C$. А если не выдаст за полиномиальное время от размера данного слова – тогда он не корректен и конкретно данный алгоритм $Sol$ не сводит разбираемый язык из $NP$ в $P$. Потому что $Sol$ в принципе не может утверждать истинность специального утверждения, содержащего данное слово из $C$, что отражает результат (ноль) работы $NP$-алгоритма за время, полиномиальное от размера этого слова из $C$.

Поэтому рассмотрим корректный $Sol$, который вернёт $0$ за полиномиальное от размеров слова из $C$ время и этим сообщит «НЕ подтверждаю» что это специальное утверждение истинно (истина означала бы принадлежность разбираемому языку).

А вот другие алгоритмы вполне смогут подтвердить принадлежность данного специального утверждения языку, потому что для них никакого слова из $C$ во входе не будет – у них другой программный код и специальное утверждение для $Sol$ не является специальным для них. А программный код в разбираемом мной случае – часть доступного алгоритму «слова» в силу «аксиомы рефлексии» — это уже моё дополнительное наблюдение. А раз нет слова из $C$, то нет и полиномиальных ограничений от его размера. Вот и времени у других алгоритмов на решение будет экспоненциально больше, чем у $Sol$ (так построен язык – размер $s$ экспоненциально велик относительно размера $S$).

И после ответа $0$ от корректного $Sol$ доказательство у специального утверждения непременно есть и будет полиномиального размера от размера слова из $C$ – так мы его и строили. И поэтому корректный $Sol$ не сможет подтвердить то утверждение, которое имеет доказательство и которое может быть использовано исходным $NP$-алгоритмом в качестве сертификата для принятия специального утверждения в качестве слова языка. А поскольку $Sol$ произвольный, то вообще нет алгоритма для сведения нашего языка из $NP$ к $P$, в силу чего $NP \ne P$. Вот и всё доказательство )

Притом все специальные утверждения и язык уже построены и тут обсуждались. Вы сами сделали соответствующие построения немного иначе и в чём-то лучше (аккуратнее в том числе), чем у меня – было интересно это увидеть. И приведённый выше кусочек про языки $B$ и $C$ – из сводки результатов, которую тоже сформулировали Вы, пользуюсь – спасибо. Осталось разобрать уже не столько техническую часть доказательства, сколько идеологическую )) Но вот как раз обсуждения такого («идеологического») плана и составляют львиную долю всей нашей дискуссии, что я не предвидел, но тем более нужно с этим разобраться.

[mihaild]

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

Да нет такой возможности для теории 2-го порядка – см. Следствие 18.2.

Там написано, что нет теста на общезначимость. Общезначимость и выводимость - это не одно и то же.

Возможно, вас путает то, что полнотой называют два разных понятия.
Когда говорят о полноте / неполноте [b] исчисления - например, "логика первого порядка полна", "логика второго порядка неполна" и т.д. - подразумевают полноту относительно некоторого класса моделей. Исчисление полно относительно класса моделей, если истинное в каждой из этих моделей утверждение выводимо.
Когда говорят о полноте / неполноте теории - имеется в виду, что для каждого утверждения в этой теории выводимо либо оно само, либо его отрицание.
Это два разных понятия. Любая теория первого порядка полна в первом смысле (по теореме Гёделя о полноте).

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

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

Да кванторы по всем алгоритмам можно и в логике первого порядка ставить, толку-то?

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

И как тогда алгоритм сможет «перебрать» доказательства/опровержения для этого расширения, если оно основано на невозможности для данного алгоритма это сделать?

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

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

Вы же её сами написали – класс эквивалентности функций, отображающих подмножество натуральных чисел на некое подмножество символов.

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

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

Именно это я и стараюсь выразить аксиомами.

А зачем? То, что существует единственное отображение линейных порядков на конечных мультимножествах символов в функции $\{1,\ldots,n\} \to A$, сохраняющее порядок - всем итак понятно и очевидно.

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

Это Вам надо смириться с тем, что есть неопределяемые понятия

Так вопрос о равенстве P и NP формализуется в ZF и даже PA: "верно ли, что для любой полиномиальной недетерменированной МТ существует экивалентная ей полиномиальная детерменированная"? (понятия "(не) детерменированная МТ" и "эквивалентность МТ" в арифметике формализуются, хотя это и не слишком просто технически)

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

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

Пока что всех это устраивало.
Еще раз: от слова нам нужно уметь получать $i$-й символ и длину. Определение "слова - это функция $\{1,\ldots,n\} \to A$ это делать позволяет.

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

Ладно, кажется всё что вы пока сформулировали, можно подвести к стандартному определению (алфавит $A$ считаем фиксированным).
конечное слово - это функция из начального отрезка натурального ряда в алфавит; множество всех конечных слов обозначим $A^*$
бесконечное слово - это функция из $\mathbb{N}$ в алфавит
длина конечного слова - понятно что
$ChrStr(x)$ - это функция $\{1\} \to \{x\}$
$Str$ - это функция $A^* \times \mathbb{N} \times \mathbb{N} \to A^*$, $Str(a, i, j)(k) = a(i + k)$ при $k < j$, если $i + j - 1 \leqslant |a|$ (что у вас происходит при "выходе за границу" - не понял; если это важно - напишите, можно словами)

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

Теперь мы, вроде бы, наконец выяснили, что внутри слова другое слово быть может

Нет, не выяснили. Я всё еще не знаю, что вы понимаете под всякими "внутренними словами".

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

И соответствующий $P$-алгоритм $Sol$

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

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

алгоритм $Sol$ не сводит разбираемый язык из $NP$ в $P$

Давайте всё-таки стараться выражаться точнее. У алгоритма есть три интересных нам в данном случае свойства: детерменирован он или нет, распознает он данный язык или нет, работает ли он за полиномиальное время или нет.
Фразы типа "алгоритм сводит язык в $P$" непонятно что значат, и, скорее всего, не значат ничего важного, что нельзя выразить в терминах выше (ну а если всё же значат - нужно расписать определения явно).

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

Потому что $Sol$ в принципе не может утверждать истинность специального утверждения

$Sol$ - это алгоритм, алгоритм в принципе не может утверждать вообще ничего. Алгоритм может максимум отработать на каком-то входе за какое-то время с каким-то результатом.

[dmitgu]

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

dmitgu в сообщении #1318670 писал(а):
Да нет такой возможности для теории 2-го порядка – см. Следствие 18.2.

mihaild: Там написано, что нет теста на общезначимость. Общезначимость и выводимость - это не одно и то же.

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

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

mihaild: Как же не эффективное? Множество доказательств даже в арифметике второго порядка перечислимо. Если бы она была полна (т.е. для каждого утверждения выводилось бы либо оно, либо его отрицание), то делаем следующее: берем формулу первого порядка, перебираем все возможные строки ...

dmitgu: Да нет такой возможности для теории 2-го порядка – см. Следствие 18.2. Там прямо Ваши рассуждения, но они опровергаются (хоть доказательство и неконструктивное) – Не существует эффективного позитивного теста на общезначимость в логике 2-го порядка.

Ведь опровергаются ;) Почитайте текст доказательства. Вот выпишу итоговый вывод «А так как не существует разрешающей процедуры для распознания истинности в $\mathcal{N}$, то не существует эффективного позитивного теста на общезначимость предложений второго порядка». Ваш «перебор доказательств» - и был бы такой «разрешающей процедурой» для истинных утверждений в $\mathcal{N}$, но такой процедуры – нет.

Вы ошиблись, когда решили, что метод перебора доказательств можно распространить на теорию 2-го порядка. А почему Вы так решили? На основании теоремы Гёделя о полноте, может быть? Но эта теорема доказана для логики первого порядка, а вовсе не второго.

Теперь про полноту. Невозможно непротиворечиво расширить $\mathcal{N}$ на неполные для неё утверждения – потому что любое корректное расширение будет некой моделью для $PA$, а в силу изоморфности с $\mathcal{N}$ совпадёт с ней (с $\mathcal{N}$). Поэтому любое расширение даст те же истинные утверждения, которые истинны в $\mathcal{N}$. Это и есть полнота! Некуда расширяться. Любое утверждение, отличающееся от истинных в $\mathcal{N}$ войдёт в противоречие с истинными в $\mathcal{N}$ утверждениями и окажется невыполнимым.

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

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

Та же ошибка. Для теорий 2-го порядка это не верно. Опровержение для ошибочных утверждений есть (на уровне некой интерпретации, возможно - как строятся доказательства без вывода из аксиом типа проверки тавталогий если совсем примитивный пример), но заведомо пригодной «точки входа» (пригодного для перебора набора аксиом 1-го порядка, например) нет.

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

Да кванторы по всем алгоритмам можно и в логике первого порядка ставить, толку-то?

Разве? )) Кванторы в логике 1-го порядка применяются только к предметным переменным, но не к формульным переменным. И если Вы почитаете доказательство о изоморфности моделей для $PA$, то Вы увидите разницу («толку-то» :) между конкретной формулой, которые есть в аксиомах индукции теории Пеано и «неизвестно какой» по своему конкретному виду формулой, на рассуждениях о которой и строится доказательство (пункт (iii) в начале доказательства Теоремы 18.1).

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

Вы же её сами написали – класс эквивалентности функций, отображающих подмножество натуральных чисел на некое подмножество символов.

mihaild: Это не интерпретация. Это определение.

Ну какое ещё определение? )) Ничуть не лучше моего «определения» через стек, а вообще – хуже, так как обладает некоторыми избыточными свойствами.

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

А зачем? То, что существует единственное отображение линейных порядков на конечных мультимножествах символов в функции $\{1,\ldots,n\} \to A$, сохраняющее порядок - всем итак понятно и очевидно.

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

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

Это Вам надо смириться с тем, что есть неопределяемые понятия

mihaild: Так вопрос о равенстве P и NP формализуется в ZF и даже PA

Вообще-то речь шла о «слове» и теории для "объектов" такого типа. Это ответ не о том или просто у Вас какой-то отдельный вопрос – поясните, пожалуйста, если это нужно.

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

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

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

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

$Str$ - это функция $A^* \times \mathbb{N} \times \mathbb{N} \to A^*$, $Str(a, i, j)(k) = a(i + k)$ при $k < j$, если $i + j - 1 \leqslant |a|$ (что у вас происходит при "выходе за границу" - не понял; если это важно - напишите, можно словами)

У Вас опечатка: $Str(a, i, j)(k) = a(i + k – 1)$ правильно. А при выходе «за границу» результат «обрезается». Если всё «за границей», начиная с $i$, то – пустая строка.

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

Теперь мы, вроде бы, наконец выяснили, что внутри слова другое слово быть может

mihaild: Нет, не выяснили. Я всё еще не знаю, что вы понимаете под всякими "внутренними словами".

$Str(a, i, j)$. Я думал, это понятно по равенствам с участием предметных переменных для слов. Напомню, что все предметные переменные у меня для слов кроме $i, j, k, l, m, n$.

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

Потому что $Sol$ в принципе не может утверждать истинность специального утверждения

mihaild: $Sol$ - это алгоритм, алгоритм в принципе не может утверждать вообще ничего. Алгоритм может максимум отработать на каком-то входе за какое-то время с каким-то результатом.

Короче, если он вернёт $1$, что по соглашению должно означать принадлежность специального утверждения языку, то утверждение языку принадлежать не будет – у него не будет доказательства. Так построено специальное утверждение.

[mihaild]

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

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

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

Цитата:

Предложение $S$ следует из множества $\Delta$ предложений тогда и только тогда, когда не существует интерпретации, в которой все предложения из $\Delta$ были бы истинны, а $S$ - ложно.

И я у товарищей вообще не могу найти правил вывода для логики второго порядка и определения значка $\vdash$. Раз вы читали, то вам наверное будет проще дать ссылку на эти части?

Пока что у меня есть впечатление, что вы, говоря про полноту арифметики второго порядка, подразумеваете что во всех моделях $PA$ второго порядка выполнены те и только те утверждения, которые выполнены в $\mathbb{N}$. Это правда.
Я же, говоря о неполноте, имею в виду, что для любой эффективной корректной дедуктивной системы второго порядка существует утверждение, такое что ни оно, ни его отрицание этой системой из аксиом $PA$ второго порядка не выводится.

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

Кванторы в логике 1-го порядка применяются только к предметным переменным, но не к формульным переменным.

Тем не менее в можно написать такую арифметическую формулу $P(x, a, b, c)$, что она доказуема в $PA$ тогда и только тогда, когда $x$ - код алгоритма, останавливающегося на входе $a$ с выходом $b$ за время $c$.

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

разницу между конкретной формулой, которые есть в аксиомах индукции теории Пеано и «неизвестно какой» по своему конкретному виду формулой

Возможность ставить кванторы по произвольным функциям увеличивает выразительность. Возможность ставить кванторы по вычислимым функциям - нет.

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

Ну какое ещё определение?

Предлагаете устроить спор об определении определения?)
Определение. Определением (в данной теории) называется строка вида "$x - это $y$, такой что $z$".

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

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

Кому "вам"? Поскольку обычно всё равно работаем в какой-то окрестности ZF, то определять в ее терминах всё вполне удобно.
Установить биекцию между линейными порядками на конечных мультимножествах и функциях из начально отрезка натурального ряда в алфавит - тривиально.

Еще раз. Что нам нужно от слов? Уметь определять их длину и $i$-й символ от начала. Через эти свойства можно уже выражать утверждения вида "строка $a$ получается конкатенацией строк $b$ и $c$". Ну и нам понадобится, чтобы для любой пары слов существовало слово, являющееся их конкатенацией, чтобы любое слово длины $n$ можно было получить конкатенацией слов длиы $k$ и $n - k$ и т.д.
Еще мы захотим работать со множествами слов, сопоставлять слова натуральным числам и т.д. - поэтому от ZF отказываться не хочется. Но, к счастью, существует очень простое множество, для элементов которого очень легко определить "длину" и "$i$-й символ" так, чтобы все нужные нам свойства выполнялись.

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

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

Это ответ не о том или просто у Вас какой-то отдельный вопрос – поясните, пожалуйста, если это нужно.

Ну, если вы придумываете свои определения P и NP и доказываете, что они не равны, то, чтобы это было интересно в контекста стандартной задачи тысячелетия, вам надо показать связь определенных вами объектов со стандартными.

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

$Str(a, i, j)$.

По-русски это называется "подстрока". И подстрока, конечно, является строкой.
У вас кстати $Str( или нет?

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

Короче, если он вернёт $1$, что по соглашению должно означать принадлежность специального утверждения языку, то утверждение языку принадлежать не будет – у него не будет доказательства.

Кажется, мы возвращаемся к тому, что уже проходили.

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

Мы берем некоторый алгоритм $Sol$, работающий за время $p$ от длины входа. Мы хотим найти либо слово из языка $LS$ такое, что он на нем выдает $0$, либо слово не из языка $LS$, такое, что он на нем выдает $1$. Так?

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

[Someone]

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

Впрочем, я тут увидел у товарищей странную фразу

Ну да, есть такая метатеорема для теорий первого порядка в классической логике: формула выводима тогда и только тогда, когда она истинна во всех моделях. Распространяется ли она на теории второго порядка, я не знаю. Просто никогда ничего серьёзного о теориях второго порядка не читал.

[mihaild]

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

Распространяется ли она на теории второго порядка, я не знаю.

Нет, не распространяется: для логики второго порядка не существует эффективной полной дедуктивной системы (т.е. набора правил вывода, позволяющих вычислимо проверять доказательства, такого, что любое утверждение, выполненное во всех моделях теории, можно получить с помощью этих правил). Например потому что все модели арифметики второго порядка изоморфны $\mathbb{N}$, и если бы существовала полная эффективная дедуктивная система, то можно было бы перечислить все формулы второго порядка, истинные в $\mathbb{N}$ - а следовательно, и все такие формулы первого порядка.

[dmitgu]

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

И я у товарищей вообще не могу найти правил вывода для логики второго порядка и определения значка $\vdash$. Раз вы читали, то вам наверное будет проще дать ссылку на эти части?

Дж. Булос, Р. Джеффри "Вычислимость и логика"

Гл.9. «Логика первого порядка: напоминание». Пример 9.4 (Предложение 9.1) – после его доказательства:

Цитата:

Для обозначения общезначисмости предложения $S$ мы пишем $\vdash S$, а записью $S_1 \vdash S_2$ показываем, что из $S_1$ следует $S_2$, то есть, что вывод из $S_1$ (в качестве посылки) утверждения $S_2$ (в качестве заключения) является общезначимым.

Логическое следование: $S_1 \vdash S_2$ тогда и только тогда, когда для всякой интерпретации $I$, служащей одновременно интерпретацией и для $S_1$ и для $S_2$, из условия $I(S_1) = 1$ следует, что $I(S_2) = 1$.

Пример 9.3 из той же главы, абзац перед перечислением «Случай 1 …» и т.д.:

Цитата:

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

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

Глава 18 «Логика второго порядка») Теорема 18.1.

Цитата:

Любая интерпретация языка $L$, являющаяся моделью для $PA$, изоморфна $N$.

Модель предложения(й) – стр. 143 (Гл. 9 «Логика первого порядка: напоминание», сразу после доказательства Примера 9.5).

Интерпретации изоморфные – стр. 253 (начало Гл.17 «Нестандартные модели арифметики»)

Интерпретация – стр. 134, 135

Интерпретация языка арифметики стандартная $N$ – стр. 135, 214

Так вот, «Интерпретации изоморфные» — это если есть такой переход между интерпретациями, что истинность/ложность на соответствующих значениях и соответствующих предикатах сохраняется.

А модель для предложения ($PA$) – это такая интерпретация, на которой данное предложение истинно.

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

Пока что у меня есть впечатление, что вы, говоря про полноту арифметики второго порядка, подразумеваете что во всех моделях $PA$ второго порядка выполнены те и только те утверждения, которые выполнены в $\mathbb{N}$. Это правда.
Я же, говоря о неполноте, имею в виду, что для любой эффективной корректной дедуктивной системы второго порядка существует утверждение, такое что ни оно, ни его отрицание этой системой из аксиом $PA$ второго порядка не выводится.

Дедуктивной (в смысле допускающей перебор всех доказательств) системы для теорий второго порядка нет – Вы это и сами написали в следующем своём комментарии. В отношении же предложений (без свободных переменных) рассмотрим некоторую модель для $PA$. Как в каждой интерпретации в ней для «неполного» утверждения есть характеристическое 1 для утверждения или (исключающее «или») отрицания. Истинное утверждение из этих двух назовём $R$. Рассматриваемая интерпретация будет моделью для $PA \& R$. И в силу теоремы о изоморфизме у $PA$ есть аналог для $R$ – тоже истинный. То есть тут полнота и в Вашем смысле – хоть и с точностью до переименования, возможно.

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

Возможность ставить кванторы по произвольным функциям увеличивает выразительность. Возможность ставить кванторы по вычислимым функциям - нет.

Не улавливаю смысл – кванторов по «вычислимым функциям» отдельно от остальных нет. Возможно, у Вас какая-то опечатка. А вообще выразительность очень вырастает. Даже простой пример – равенство можно не аксиоматизировать, а определять в логике 2-го порядка.

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

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

Доказательство не категоричности теорий 1-го порядка для арифметики построено на наличии несводимых друг к другу вариантов интерпретаций – как счётной, так и несчётной (теорема Лёвенгейма-Сколема). И если теория 1-го порядка может «убежать» в несчётный вариант интерпретации от счётного (хоть такое расширение и перестаёт быть теорией для арифметики, но имеет смысл в действительных числах, например), то $PA$ может пытаться «убежать» от счётной бесконечной области только в область конечную, а это безнадёжная попытка :)

Из-за НЕ категоричности теорий 1-го порядка (для арифметики) и появляется почва для теорем Гёделя о неполноте – вопрос о «существовании» должен быть решен какой-то конкретной аксиомой, иначе здесь нет однозначной истины и какое-то действительное число, которое не будет шагом работы программы – тоже есть. Я же писал, что доказательство неразрешимости для Пеано не опирается в принципе на её эффективную аксиоматизированность – доказательство пройдёт и для теории 2-го порядка. Но лишь из-за наличия теоремы Гёделя о полноте для теорий 1-го порядка выясняется неполнота в наборе их аксиом. А вот полнота теории 2-го порядка для арифметики вместе с неразрешимостью как раз и приводит к выводу об отсутствии чего-то аналогичного теореме Гёделя о полноте в отношении предложений, «логически следующих» из $PA$.

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

Тем не менее в можно написать такую арифметическую формулу $P(x, a, b, c)$, что она доказуема в $PA$ тогда и только тогда, когда $x$ - код алгоритма, останавливающегося на входе $a$ с выходом $b$ за время $c$.

Да, конечно. Эта теория не менее выразительна чем примитивная Z (для которой Пеано - расширение и в которой нет даже аксиом индукции), в которой нельзя доказать даже коммутативность сложения и кучу простейших свойств чисел, но любые алгоритмы представить – можно. В том числе и эмулятор произвольных алгоритмов, отсчитывающий время их работы, чтобы учесть и его в результате своей работы (1 или 0).

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

Предлагаете устроить спор об определении определения?)
Определение. Определением (в данной теории) называется строка вида "$x - это $y$, такой что $z$".

Не, ну это уже перебор ))) То, что справа – должно соответствовать какой-то теории, иметь какой-то смысл ))

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

Кому "вам"? Поскольку обычно всё равно работаем в какой-то окрестности ZF, то определять в ее терминах всё вполне удобно.
Установить биекцию между линейными порядками на конечных мультимножествах и функциях из начально отрезка натурального ряда в алфавит - тривиально.

О каких «определениях», касающихся формальных языков Вы говорите? Их просто нет. Иначе Вы не пытались бы сформулировать их сами – с ошибками, что вполне нормально для начальных попыток. И не задавали бы мне вопрос о том, что такое внутреннее слово – но знали бы сами этот ответ. Я понимаю, что Вы не уверены в себе и думаете, что в «закромах формализма» есть какие-то определения.

Такое у нас общество со времен СССР – не желающее хвалить людей за их самостоятельность – отсюда запуганность и негативизм. Хотя никакого другого «протокола» объединения людей в общество кроме одобрения в общении просто нет. Я, кстати, стараюсь высказывать Вам одобрения – может недостаточно, но и у меня было очень негативное начало жизни, чтобы научиться этому раньше, но я стараюсь это наверстать.

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

Так вот, не было для термина «слова» до сих пор никакого ни определения, ни теории. Если есть – давайте его сюда. Но – нет. Мы тут делаем необходимое дело, создавая формальные основы для теории языков, отсутствие которой столь долгое время – принципиальная ошибка и она должна быть устранена. Параллельно разбирая некоторые заблуждения, которые разобраны в логике, но снова цветут в не формализованной пока сфере формальных языков.

Ваше «определение» не годится по той причине, что ему не соответствует даже такая простая интерпретация как «символы в клеточках на фанерке в одну линейку».

Вот смотрите – можно каждой клеточке (началу) сопоставить расстояние от начала фанерки – можно даже использовать не линейную линейку (любую шкалу с общей мерой). Но что произойдёт, если мы распилим эту фанерку между некоторыми клеточками? Эта «нумерация» исчезнет – будет не ясно, где начало и что за чем было.

В вашем «определении» у каждой клеточки есть номер (пусть он и допускает перенумерацию по всему слову, но он есть) и порядок имеется даже в «не сплошном» множестве «отрезков». Это не соответствует приведённой мной интерпретации. А она соответствует здравому пониманию «слова» как упорядоченной сплошной цепочки символов.

Моя интерпретация опирается на связь «взявшись за руки» - я вижу, что у данной клетки в начале – тёмный сучок, а у второй – трещина в форме крестика, а у третьей – торчит двойная заноза. Вот в чём порядок (локальный! Это не нумератор) – каждая клетка имеет свой признак и расположена (связана фанерой) за клеткой со своим признаком. Если я разрезаю фанерку на корректные отрезки, то глобальный порядок не сохраняется, но внутри сплошных отрезков – он прежний и так же связан фанерой. И да, я могу менять идентификаторы – заметив некие другие уникальные признаки у клеток, или даже нарисовав их.

Вы сами признали, что не знаете, как определить то предложение, для которого моя интерпретация (слова, представленные как стек) была бы моделью. Но в таком случае Вы не можете – по крайней мере пока – дать нужное определение, допускающее одну из правильных (мою) интерпретаций слов в качестве своей модели. И не Вы один этого не можете – а всё математическое сообщество пока что. Хотя с момента формулировки гипотезы $NP \ne P$ прошло уже сколько? Около 50 лет? Так, может, пора уже признать необходимость составить теорию с соответствующими аксиомами? Раз с «определениями» никак не складывается? К тому же это азы математики – базовые понятия не определяются, а просто составляются аксиомы, отражающие их свойства.

И я вовсе не «корчу из себя самого умного», а просто констатирую факт – тупик, в который зашли математики в сфере формальных языков, необходимость его преодоления и, прилагаю конструктивные усилия для этого. Так поддержите эти усилия, и будете ещё лучше выглядеть позже в истории математики ))))

Тут же не вопрос предпочтения большинства – математика – это ведь не демократия кого ни попадя, а монархия истины. И если я прав (а я думаю, это так, что дискуссионно, конечно), то моя (пусть даже меня забудут, не о том речь) точка зрения будет признана правильной в итоге, даже если «против» десять миллиардов, а «за» - один только я пока что. Так давайте «за» будем хотя бы мы двое ))))) Не волнуйтесь, сейчас не времена Джордано Бруно ;)))) И даже не Гаусса, который знал про неевклидову геометрию, но не решился высказаться, так как опасался «криков беотийцев». Да и вопрос формализации языков и близко не такой «революционный» как в приведённых примерах.

Кстати, как Вы видели выше, для теории первична интерпретация – теория же служит лишь формальным представлением для неё, поэтому приводившаяся Вами идея «определения не бывают ошибочными» - ошибочна. И, кстати, чего же Вы тогда спрашиваете меня об аксиомах – и «аксиомы не бывают ошибочными» тогда )) Если мы исключим случай противоречивости, конечно. Но по противоречивости и определения бывают ошибочными («множество всех множеств», например).

Да и вообще, сильно сомнительно, что можно дать определение термину «слово» через теорию множеств, да и заведомо нельзя дать такое определение на базе теории 1-го порядка. Я сейчас поясню, но Ваша теория множеств – какого порядка? То, что видел я (NBG) – первого порядка.

Так вот, «слово» по своей сложности не уступает «числу». Действительно, 567842 – это слово. И можно задать (определить!) всякие математические операции над такими словами. Более того, такие «специальные слова» удовлетворяют арифметике второго порядка! И как такие объекты могут быть выражены («определены») теорией множеств – теорией первого порядка? Ответ один – никак.

Если же оперировать теорией второго порядка – то, да, у нас есть арифметика. Но есть доказательство того, что теория 2-го порядка для арифметики вместе с теорией множеств позволяет создать теорию 2-го порядка для слов? Не используя для этого новых аксиом? Совсем не факт, что «слово» не является более выразительным объектом, чем число и что теория множеств достаточная добавка для выравнивания выразительностей. А даже если это и так, то у нас есть эквивалентный переход (определения от к в обе стороны) между словами и натуральными числами (хотя тут надо было бы решить вопрос аксиоматизации для слов без использования чисел). И вполне можно числа определять через слова (выполнив аксиоматизацию без чисел - но, возможно, тут потребуется что-то из "идентификаторов" для стека - со своими аксиомами). Тут, кстати, потребуется ещё вводить соответствие между бинарной (где нужен порядок) и унарной (где порядок не требуется) интерпретациями для чисел в их определении через слова – если такое определение возможно.

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

Вообще-то попытка «определить» слово через теорию множеств напоминает те исторические «грабли», когда Рассел и (кажется) Уайтхед пытались определить число при помощи теории множеств. Написали толстую книгу. И уже перед публикацией им указали на ошибку – для построения чисел они использовали «множество всех множеств». Что противоречиво, а из противоречия можно вывести что угодно. Я выше объяснил (на основе достижений в логике 2-го порядка, которых не было во времена Рассела), почему подобная попытка безнадёжна – нельзя определить понятие со сложностью из логики 2-го рода в рамках теории 1-го рода.

И кроме всего сказанного совершенно неправильно подтягивать теорию множеств туда, где можно и нужно обойтись без неё. Слова – это просто строки. А понимание строк востребовано массой программистов, которым теория множеств сто лет не нужна. Есть программисты (их очень мало), которым нужна теория множеств, но загонять всех (подавляющее большинство) к ненужной им теории, чтобы получить нужную теорию, и пользоваться свойствами строк, которые могут быть получены независимо от теории множеств? Это было бы крайне расточительно и не разумно.

Теория множеств вообще довольно невнятная – у неё даже стандартной интерпретации нет – со слов Someone. Так что если без неё можно обойтись, то без неё нужно обойтись, да и не получится «определение 1-го порядка», как было обосновано, а пользоваться чем-то из логики 2-го порядка крайне проблематично. Так что всё равно дело сведётся к теории 1-го порядка – а в ней никаких определений 2-го порядка нет, вот и получается, что аксиомам первого порядка для теории языков и неопределяемому понятию «слово» альтернативы нет.

Даже из-за наличия такого принципиального вопроса как гипотеза $NP \ne P$ есть все основания взять менее сложный подход, изгнав теорию множеств и имея дело лишь со специализированной на словах теорией. Просто чтоб десятилетия не «ломать мозги» себе, путаясь в ненужном постороннем аппарате теории множеств.

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

По-русски это называется "подстрока". И подстрока, конечно, является строкой.
У вас кстати $Str(\text{ или нет?

Так строка – это и есть слово. Упорядоченная последовательность символов. В Вашей формуле опечатка – одна запятая пропущена? Даже цитирование не сработало - пришлось вручную переписывать. Но судя по длине строки (первый аргумент) на выходе слева будет строка (подстрока) длиной 2, а справа – длиной 1. Они не равны, конечно. Вот если бы строковый аргумент в обеих сторонах был «a», например (из одного символа), то было бы равенство. Посмотрите аксиому для равенства слов – там всё есть.

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

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

Да всё там понятно )) Можно придраться к тому, что на вход подаётся утверждение и аргументы предельного размера доказательства, а часть информации – код алгоритма. И, типа, если подать ещё и иной программный код на вход, то будет всё иначе. Но раз требуется решение для произвольных утверждений и размеров, то остальные аргументы должны быть фиксированы, а это сводит дело тоже к программному коду. Просто этот программный код включает в себя несколько фиксированных аргументов, например. Фишка в том, что язык можно сделать заведомо шире алгоритма и на любой Sol заранее предусмотреть нерешаемый для него $Anti_{Sol, S}$. Это и сделано.

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

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

[Someone]

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

Доказательство не категоричности теорий 1-го порядка для арифметики построено на наличии несводимых друг к другу вариантов интерпретаций – как счётной, так и несчётной (теорема Лёвенгейма-Сколема).

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

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

И если теория 1-го порядка может «убежать» в несчётный вариант интерпретации от счётного (хоть такое расширение и перестаёт быть теорией для арифметики, но имеет смысл в действительных числах, например)

Ерунда какая-то. Прежде всего, интерпретация теории не является теорией. Теория и интерпретация теории — совсем разные понятия. Кроме того, теории вообще нет дела до её интерпретаций: теория остаётся сама собой при любых интерпретациях, даже при таких, которые не являются моделями. Наконец, несчётные модели арифметики Пеано вполне возможны. В них все выводимые высказывания арифметики остаются истинными.

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

то $PA$ может пытаться «убежать» от счётной бесконечной области только в область конечную, а это безнадёжная попытка

Арифметика Пеано не имеет конечных моделей.

-- Пн июн 25, 2018 13:52:30 --

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

А Вы всё отсылаете к «обычным определениям слова», которых нет )) Шучу, конечно – будем разбираться, раз у формалистов есть вопросы к формализации понятия «слово» и эта формализация не была сделана раньше.

Общепринятую формализацию термина "слово" mihaild Вам излагал. Вы её почему-то отвергаете.

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

[dmitgu]

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

Теорема Лёвенгейма—Сколема, насколько я помню, утверждает, что, при определённых условиях, если теория первого порядка имеет какую-нибудь модель, то она имеет модель некоторой "не слишком большой"

Да, но есть ещё и "расширение мощности" - в "Вычислимости и логике"

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

Прежде всего, интерпретация теории не является теорией.

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

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

Арифметика Пеано не имеет конечных моделей.

Я тут не совсем формально пишу. Смысл, что несчётного нет, а альтернатива - конечное. Ну и нет - некуда бежать. О том и речь )

[Someone]

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

несчётного нет

Несчётные есть.

[dmitgu]

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

Общепринятую формализацию термина "слово" mihaild Вам излагал. Вы её почему-то отвергаете.

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

-- 25.06.2018, 15:00 --

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

Несчётные есть.

Для $PA$?
Прчитайте начало этой главы. Оно начинается с предложения второго порядка, которое имеет только несчётные интерпретации. А аксиома индукции 2-го порядка - это практически отрицание данного предложения. Так что - нет.

[Someone]

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

Для $PA$?

Да, для PA первого порядка. В соответствии с вашими словами:

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

Доказательство не категоричности теорий 1-го порядка для арифметики …

А теперь Вы почему-то начали ссылаться на теории второго порядка:

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

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

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

Что он излагал? Пронумерованные символы?

Функция, определённая на начальном отрезке натурального ряда.

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

Так он сам это и придумал.

Это общепринятая формализация.

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

И мы после уточняли, что нумерация не фиксированная

Это — несущественное расширение. Оно легко элиминируется.

[mihaild]

Дж. Булос, Р. Джеффри писал(а):

Логическое следование: $S_1 \vdash S_2$ тогда и только тогда, когда для всякой интерпретации $I$, служащей одновременно интерпретацией и для $S_1$ и для $S_2$, из условия $I(S_1) = 1$ следует, что $I(S_2) = 1$.

Ну да, это определение отличается от общепринятого - $\vdash$ обычно означает существование вывода. А общезначимость (то, что указывают авторы), обозначается $\models$.
И дальше есть разные теоремы, связывающие разные дедуктивные системы с разными классами моделей. Например, теоремы о корректности и полноте, говорящие, что формулу можно получить из набора формул $\Gamma$ по таким-то правилам тогда и только тогда, когда в любой модели, где выполнены все формулы из $\Gamma$, выполнена и наша формула.

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

То есть тут полнота и в Вашем смысле – хоть и с точностью до переименования, возможно.

Нет, нету. Полнота "в моем смысле" - про выводимость, то есть про синтаксис.

Ладно, это всё не очень важно, Булос и Джеффри решили вот так определить $\vdash$ и слово "выводимость" - имеют право, можно пользоваться их определениями.

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

То есть тут полнота и в Вашем смысле – хоть и с точностью до переименования, возможно.

Для чего нам нужно ставить квантор по функциям? Чтобы иметь возможность сформулировать, например "$\forall F, \forall G: (F(0) = G(0) \wedge (\forall x: F(x) = G(x) \to F(x + 1) = G(x + 1))) \to \forall x: F(x) = G(x)$. Но

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

можно написать такую арифметическую формулу $P(x, a, b, c)$, что она доказуема в $PA$ тогда и только тогда, когда $x$ - код алгоритма, останавливающегося на входе $a$ с выходом $b$ за время $c$.

Так что аналогичное утверждение для вычислимых функций можно сформулировать и в арифметике первого порядка.

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

Из-за НЕ категоричности теорий 1-го порядка (для арифметики) и появляется почва для теорем Гёделя о неполноте

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

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

Я же писал, что доказательство неразрешимости для Пеано не опирается в принципе на её эффективную аксиоматизированность

Либо вы это не писали, либо я это пропустил. Если не требовать эффективной аксиоматизируемости, то теорема Гёделя перестает выполняться - у арфметики первого порядка существуют полные расширения (например, элементарная теория $\mathbb{N}$).

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

То, что справа – должно соответствовать какой-то теории, иметь какой-то смысл

Я там в знаках доллара запутался. Можно навести курсор на формулу и прочитать. Должно было быть "строка вида $x - \text{это}\ y, \text{такой что}\ z$".

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

О каких «определениях», касающихся формальных языков Вы говорите? Их просто нет.

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

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

Это не соответствует приведённой мной интерпретации.

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

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

с ошибками

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

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

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

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

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

В Вашей формуле опечатка – одна запятая пропущена?

Да, я что-то не то написал там. Должно было быть $Str(\text{. Ну то есть "помнит" ли подстрока, откуда ее извлекли, или нет?

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

Кстати, как Вы видели выше, для теории первична интерпретация

Нет, не видел.
Ну и понятие "первичность" не определено.

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

То, что видел я (NBG) – первого порядка.

Я вообще про ZFC обычно говорил, но они непринципиально отличаются в данном случае.

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

да и заведомо нельзя дать такое определение на базе теории 1-го порядка

Да ладно? Почти вся математика живет в первом порядке, и прекрасно себя чувствует.

(Оффтоп)

И завязывали бы вы с общими философствованиями. Отсылки к Галлилею тут не любят.

-- 25.06.2018, 14:51 --

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

ProofWiki в Definitin:Sequence писал(а):

A sequence is a mapping whose domain is a subset of natural numbers \mathbb{N}.

(кстати тут они согласны с вашим вариантом - "дырки" в нумерации разрешены)

ProofWiki в Definitin:String писал(а):

Let $A$ be an alphabet of symbols. A string (in $A$) is a sequence of symbols from $A$.

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

Просто чтоб десятилетия не «ломать мозги» себе, путаясь в ненужном постороннем аппарате теории множеств.

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

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

И, типа, если подать ещё и иной программный код на вход, то будет всё иначе.

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