dmitgu в сообщении #1322514 писал(а):
Вы не соглашались, что во входном слове есть и другие слова
Опять либо врёте, либо ошибаетесь. Я писал
mihaild в сообщении #1310548 писал(а):
Понятие "внутреннее содержание слова" не определено.
Ну и что-то подобное.
Почитал дискуссию с декабря 2017 г.
Не сразу вспомнил, почему про весь вход – слово
![$(w_1, w_2)$ $(w_1, w_2)$](https://dxdy-03.korotkov.co.uk/f/2/2/4/2249c9240bed7dce7847a29d2c391b8482.png)
– я не упоминал в декабре 2017, что разбираемый
![$NP$ $NP$](https://dxdy-03.korotkov.co.uk/f/a/a/1/aa1bd49a4578d83ef6f508fb0a9e728982.png)
-алгоритм в спец. случае зависит только от
![$w_1$ $w_1$](https://dxdy-01.korotkov.co.uk/f/4/b/4/4b4518f1b7f0fb1347fa21506ebafb1982.png)
и время его работы полиномиально от размера
![$|w_1|$ $|w_1|$](https://dxdy-01.korotkov.co.uk/f/4/7/0/4701d66383c10d51b58d21b4ea56a2c382.png)
. Затем вспомнил, что это как раз из-за спора о возможности выделить из слова
![$ (w_1, w_2) $ $ (w_1, w_2) $](https://dxdy-04.korotkov.co.uk/f/3/8/e/38e6d9a8dca9edf8b7095c8bebfe6e8e82.png)
его «внутренние слова». И если вопрос о «внутренних словах» стоял для
![$P$ $P$](https://dxdy-02.korotkov.co.uk/f/d/f/5/df5a289587a2f0247a5b97c1e8ac58ca82.png)
-алгоритма, то он так же стоял и для
![$NP$ $NP$](https://dxdy-03.korotkov.co.uk/f/a/a/1/aa1bd49a4578d83ef6f508fb0a9e728982.png)
-алгоритма. И полиномиальность относительно размера
![$|w_1|$ $|w_1|$](https://dxdy-01.korotkov.co.uk/f/4/7/0/4701d66383c10d51b58d21b4ea56a2c382.png)
будет и полиномиальностью относительно размера
![$|(w_1, w_2)| $ $|(w_1, w_2)| $](https://dxdy-04.korotkov.co.uk/f/b/3/0/b300fa4ae0843d7089928f48ab9597c582.png)
и про слово
![$w_1$ $w_1$](https://dxdy-01.korotkov.co.uk/f/4/b/4/4b4518f1b7f0fb1347fa21506ebafb1982.png)
тогда и говорить нечего, если не доказано, что это именно слово – что его можно считать словом.
Именно тогда я сделал перерыв в дискуссии (до 18.04.2018) и думал (свободного времени на это было мало тогда), в чём Ваши аргументы не верны, так как «внутреннее слово» (уточню формально ниже) явно имеется. «Врёте или ошибаетесь» как раз Вы:
mihaild в сообщении #1308833 писал(а):
dmitgu: Такой выбор слова (весь вход) вовсе не выводится из формализма слов. Это -- Ваш произвол, пусть так «принято», но это же не доказано!
mihaild: Это и не надо "доказывать", это часть определения.
Когда мы определяем
![$МТ$ $МТ$](https://dxdy-03.korotkov.co.uk/f/a/5/a/a5a8dbe7b48e36e280efd0efbe5f891b82.png)
, мы фиксируем специальный символ , …
Но мы-то с Вами согласны, что язык существует независимо от «представляющих» его алгоритмов. ...
Вы опять отправили дискуссию про «неправильные» термины (хотя я старался разъяснить, какой смысл я вкладываю) «представляющих», «внутренние слова», а не о том, что «специальный символ» не имеет отношения к собственно языку и во входе имеются и другие слова – подстроки.
Определение. Словом длины
![$n$ $n$](https://dxdy-02.korotkov.co.uk/f/5/5/a/55a049b8f161ae7cfeb0197d75aff96782.png)
в алфавите
![$A$ $A$](https://dxdy-02.korotkov.co.uk/f/5/3/d/53d147e7f3fe6e47ee05b88b166bd3f682.png)
называется функция
![$f: \{1, 2, \ldots, n\} \to A$ $f: \{1, 2, \ldots, n\} \to A$](https://dxdy-01.korotkov.co.uk/f/8/1/c/81c788ed378f2006351b74b107e5a36e82.png)
.
![$n$ $n$](https://dxdy-02.korotkov.co.uk/f/5/5/a/55a049b8f161ae7cfeb0197d75aff96782.png)
в этом случае называется длиной слова, а
![$f(i)$ $f(i)$](https://dxdy-01.korotkov.co.uk/f/4/5/c/45c28aa22b76a35840b12e4d8fe90a9482.png)
-
![$i$ $i$](https://dxdy-04.korotkov.co.uk/f/7/7/a/77a3b857d53fb44e33b53e4c8b68351a82.png)
-м символом слова.
Непонятно, из какого формализма это должно следовать. Это базовое определение, на котором строится всё остальное.
Разумеется, это определение не годится, потому что если выбрать подстроку с любого символа кроме первого, то подстрока уже не будет словом – нумерация не с 1. Поэтому такое определение не может быть «базовым» - оно ошибочное.
То есть, опять не я, а Вы «врете или ошибаетесь» вот тут:
dmitgu в сообщении #1322514 писал(а):
Сколько уже недель определение составить не получается
Либо врёте, либо ошибаетесь.
Определение я вам привел сразу, и пока никаких принципиальных недостатков в нем не указано.
Затем вы привели англичанина, который «допускает дыры» в нумерации «как и вы» - по Вашим словам (про меня). Но про класс эквивалентности он не написал и равенство одинаковых строк у него не выводится – если символы в этих одинаковых строках пронумерованы разным образом (но символы и порядок одинаковые).
потому что я считаю, что именно эти определения (с точностью до несущественных отличий) даст любой профессиональный математик, если его спросить. Someone уже подтвердил,
Да хоть сто миллиардов человек «подтвердит» Ваше ошибочное суждение – от этого оно ошибочным быть не перестанет. Я уже писал, что математика – это монархия истины, а не демократия кого угодно.
dmitgu в сообщении #1322514 писал(а):
никто набор символов через один, выдернутых из строки не считает строкой
Вот строка
![$abcde$ $abcde$](https://dxdy-01.korotkov.co.uk/f/4/9/8/498bf2abfa2e8530ef15e5db1bab198d82.png)
. Покажите мне человека, который
![$ace$ $ace$](https://dxdy-02.korotkov.co.uk/f/9/1/4/914136e9550b6e944a013b8089cd55b182.png)
не считает строкой.
Это отличный пример для разбора и опровержения Вашего «определения». Смотрите – Вы с таким же успехом могли бы написать «Покажите мне человека, который
![$\text{«fgk»}$ $\text{«fgk»}$](https://dxdy-03.korotkov.co.uk/f/6/3/c/63cb781a5c062e4fc0b30933031b6fb482.png)
не считает строкой». Какое отношение Ваше предложение имеет к строке
![$\text{«abcde»}$ $\text{«abcde»}$](https://dxdy-03.korotkov.co.uk/f/2/1/2/212667ecbc485242ec1a3a6e13f465ca82.png)
? Никакого.
Вот теперь мы добираемся до формализма про «внутреннее слово». Формализация уже сделана в моей теории первого порядка и представлена функцией
![$find$ $find$](https://dxdy-01.korotkov.co.uk/f/4/8/2/482ae9cbfdd3e880c58d963fddc6851482.png)
. То есть, «внутреннее слово» - это то слово, которое можно найти внутри данного слова. И
![$find$ $find$](https://dxdy-01.korotkov.co.uk/f/4/8/2/482ae9cbfdd3e880c58d963fddc6851482.png)
в моей теории завязана именно на подстроки (смотрите аксиому про
![$find$ $find$](https://dxdy-01.korotkov.co.uk/f/4/8/2/482ae9cbfdd3e880c58d963fddc6851482.png)
– я её уточнил в следующем своем сообщении после изложения всех аксиом).
А теперь скажите-ка мне, нормальные люди (те же программисты) согласятся, что внутри строки
![$\text{«abcde»}$ $\text{«abcde»}$](https://dxdy-03.korotkov.co.uk/f/2/1/2/212667ecbc485242ec1a3a6e13f465ca82.png)
можно найти строку
![$\text{«ace»}$ $\text{«ace»}$](https://dxdy-01.korotkov.co.uk/f/c/8/a/c8a266ce27f27dbeecc64b72d167e36f82.png)
? Нет. Потому что её там нет. Потому что правильный ответ такой:
![$find(\text{«abcde»}, \text{«ace»}) = 0$ $find(\text{«abcde»}, \text{«ace»}) = 0$](https://dxdy-02.korotkov.co.uk/f/9/4/8/948e191740b550ee8e67070dd7af8b8882.png)
.
То есть, подпоследовательности (когда не «сплошные» подстроки, а «через символ» и типа того) надо исключить из числа «внутренних строк», чтобы соответствовать общепринятой интерпретации. Но относительно общепринятой интерпретации у Вас есть возражение про Ваши желания (!!):
чего при определении фундаментальных понятий делать не хотелось бы).
Неужели Вы думаете, что Вас вместе с любым количеством «профессионалов» не вынудят принять для слов (строк!) теорию с
![$find(\text{«abcde»}, \text{«ace»}) = 0$ $find(\text{«abcde»}, \text{«ace»}) = 0$](https://dxdy-02.korotkov.co.uk/f/9/4/8/948e191740b550ee8e67070dd7af8b8882.png)
? Вынудят, даже не сомневайтесь )
Что касается желаний – то это непригодный метод для стандартизации (определений, аксиом и т.п.), потому что у каждого свои желания.
Поэтому в основе стандартов, как правило, лежит нечто объективное – в частности, конкретные практические задачи могут выступать в таком качестве. Я бы сказал ещё «творение Божие», но Вы атеист, наверное, и тут наши исходные посылки несовместимы.
А конкретно в отношении слов и языков источник вопросов (и про
![$NP \ne P$ $NP \ne P$](https://dxdy-03.korotkov.co.uk/f/e/0/d/e0d25c0347b71f7f98cf8459812c829882.png)
тоже) – потребности криптографии. А это – программистские стандарты операций со строками, подстроками и тому подобным. Вот из этого и следует исходить.
И вообще, не хотите явно вводить индексацию - давайте назовем словами над
![$A$ $A$](https://dxdy-02.korotkov.co.uk/f/5/3/d/53d147e7f3fe6e47ee05b88b166bd3f682.png)
элементы свободного моноида, порожденного
![$A$ $A$](https://dxdy-02.korotkov.co.uk/f/5/3/d/53d147e7f3fe6e47ee05b88b166bd3f682.png)
. Стало легче?
Так я уже сделал этот Ваш «моноид» - почитайте аксиомы моей теории страницей раньше. Наконец-то Вы со мной согласились )))
«Моноид». О! Опять Вы со своими гладиолусами, Михаил )) Одна из задач стандартизации основ – это максимальная понятность для наибольшего круга пользователей. Вы можете для тонких ценителей профессиональных терминов пытаться развивать свою элитарную теорию. Но большинство прикладников – такие же простые валенки, как и я )))
Им-то нужна нормальная теория первого порядка (пример – те аксиомы, которые написал я), чтобы ей пользоваться и иметь общие понятные исходные посылки. Это нужно для взаимодействия людей, а не для того, чтобы «элитарные профи» показывали другим, какие эти другие тёмные обормоты )))
Можете, наконец, написать в инстутут Клея: "ваше описание неполное, используется термин string, но нигде не написано, что он значит
Да всё написано в сформулированных мной аксиомах ) Или в институте Клея тоже - противники аксиоматизации? ))
Кстати, если фраза "
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
- внутреннее подслово слова
![$y$ $y$](https://dxdy-02.korotkov.co.uk/f/d/e/c/deceeaf6940a8c7a5a02373728002b0f82.png)
" означает что-то кроме "
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
- подстрока
![$y$ $y$](https://dxdy-02.korotkov.co.uk/f/d/e/c/deceeaf6940a8c7a5a02373728002b0f82.png)
" - то я всё еще не понимаю, что.
Всё правильно – только подстрока и никаких подпоследовательностей. Наконец-то я Вам что-то объяснил ))
dmitgu в сообщении #1322514 писал(а):
Да, но не все свойства, которые выводятся из Вашего (а вовсе не стандартного) определения являются свойствами некоторых слов
Ничего страшного, этими свойствами пользоваться не будем.
В принципе, да, но сам по себе факт отсутствия вменяемой теории даже для слов (не говоря про языки) крайне удивляет и нуждается в исправлении. Потому что хоть для данной дискуссии можно обойтись (видимо) тем, что общее у моей теории и Вашего «определения», но как быть с другими вопросами? Тоже люди будут по много месяцев спорить невесть о чём? Поэтому и нужна стандартизация.
dmitgu в сообщении #1322514 писал(а):
А почему Вы так боитесь теории первого порядка?
Потому что непонятно, зачем нужно плодить лишние сущности.
Смотря какие «сущности» считать лишними. Вы-то хотите строить определение на базе теории Пеано и теории множеств? Для подавляющего большинства практиков «лишней сущностью» является как раз теория множеств, а вот отдельная теория для слов – вполне их «епархия» и стандарты без «излишеств нехороших».
К тому же у меня обоснованные сомнение, что Вы (и сто миллиардов профессионалов вместе с Вами, конечно :) имеете теорию первого порядка для слов на выбранной Вами базе:
Вообще-то заготовку «определения» для слов тоже придумал я – введение эквивалентности – это от меня. Да, с участием Михаила – это его термин (на моё «Никакой разницы!»), он понял мою мысль. Но я при этом не давал строгого определения и не выбирал теорию первого порядка, на базе которой пытался бы формулировать определение. А это значит – что никакой готовой теории, в которой было бы корректное определение для слов – нет до сих пор, и не было раньше.
Я снова (через надцать лет) прочитал поверхностно аксиомы теории множеств NBG («Введение в математическую логику», Э. Мендельсон, Глава 4 «Аксиоматическая теория множеств», раздел 1 «Система аксиом») и не нашёл ничего, что могло бы быть формализацией для создания нужного класса эквивалентности.
Есть определения для пустого множества и множества двух множеств и т.п. определения, но – на основе аксиом. И есть специальная теорема в логике, которая доказывает, что введение таких определений не добавляет в теорию ничего существенного. Иначе это были бы, фактически – аксиомы. Ссылка на данную теорему стоит в упомянутом чуть выше Разделе 1 сразу после определений для пустого множества и множества для пары классов
![$\{X, Y\}$ $\{X, Y\}$](https://dxdy-03.korotkov.co.uk/f/2/5/8/258d73b247e7e6e62bf820b448862a1082.png)
. А сами эти определения – после «Аксиомы N» для пустого множества.
Другое дело, что как слова могут служить базой для построения чисел, так и числа могут, в принципе, выступать базой для построения слов (Гёделевы номера – включая и позиционную запись текстов – как в «Вычислимости и логике», например). Это я высказываю просто мнение, но, видимо, его технически не сложно (что не значит «коротко») доказать – если иметь теорию и для слов. Однако для начала надо иметь теорию для слов.
То есть, можно выбрать числа определённого вида и построить соответствующие алгоритмы для работы с ними – по аналогии с реализацией программы Гильберта в период великих логических открытий – и создать те объекты и способы работы с ними, которые будут соответствовать логике работы со словами.
Но это не будут те объекты, которые автоматически приобретут свойства слов, а напротив – они должны будут строиться так, чтобы соответствовать общепринятой интерпретации для слов. И про них ещё надо будет доказать, что они соответствуют правильной теории (которая в свою очередь должна соответствовать стандартной интерпретации).
А вот для построения теории слов конкретика реализации должна быть изгнана – только тогда и будет получена теория, которая будет соответствовать самым разным вариантам реализации рассматриваемых в ней объектов. А способов создания теории для особых объектов (а не отдельной конкретной реализации этих объектов) внутри другой теории первого порядка методом определения – нет и быть не может, иначе это было бы не определение, а замаскированная аксиома.
Таким образом, никакой теории первого порядка с определением для слов у нас не было, и нет. Есть моя теория первого порядка для слов – что давно надо было сделать профессионалам, но сделано дилетантом мной ) И хватит защищать корпоративную «чистоту мундира», Михаил – она тут не защитима. Профессионалы в данном случае лопухнулись, а дилетант рулит ) Это я, Я, Я! ))))
Хоть я и не юрист Ферма и не телеграфист Хевисайт, но уверенным шагом иду в их направлении )))
Поэтому просьба - покажите, пожалуйста, свою теорию первого порядка (на базе теории множеств и теории Пеано – хотя аксиомы Пеано можно и не писать, а истинные утверждения оттуда выдавать сразу, если они простые). И покажите то, как в этой теории доказывается одно тестовое утверждение – равенство некоторой подстроки с некоторым словом. При этом надо, чтобы данная подстрока была подстрокой в некотором слове (строке), в которой данную подстроку можно было бы найти, и надо, чтобы подстрока отличалась от данной строки. Нужен вывод от аксиом выбранных Вами готовых теорий и Вашего определения (составленного средствами логики 1-го порядка) до результата. Вывод при помощи правил логического вывода.
В качестве примера приведу вывод предложенного для доказательства утверждения в рамках своей теории, аксиомы для которой сформулированы тут:
Давайте напишем аксиомы, что ли ) ...
И немного подправлены тут (и Вы там одну аксиому упростили, кстати):
Я заметил, что кое-что прозевал. Вот такие исправленные аксиомы нужны: ...
Считаем, что:
0.
![$I_{ChrLim} > 0$ $I_{ChrLim} > 0$](https://dxdy-04.korotkov.co.uk/f/f/b/c/fbc96e0fbfa4650cd63e53e8c709ed8782.png)
– у наc не унарный алфавит, но есть хотя бы «азбука Морзе» и возможность записи тех же чисел позиционным способом.
Доказывать будем
![$Str( ChrStr(0) \cdot ChrStr(1), 2, 1 ) = ChrStr(1)$ $Str( ChrStr(0) \cdot ChrStr(1), 2, 1 ) = ChrStr(1)$](https://dxdy-04.korotkov.co.uk/f/3/e/7/3e7150bcd176a2a110c310136ef23e2282.png)
Использовать будем аксиомы
1.
![$a = b \Leftrightarrow \forall i: str(a, i, 1) = str(b, i, 1)$ $a = b \Leftrightarrow \forall i: str(a, i, 1) = str(b, i, 1)$](https://dxdy-02.korotkov.co.uk/f/d/5/f/d5f3ad25f7400c3e8843a7170be9fa6882.png)
, что такое равенство слов
2.
![$str(a, i, 1) = \emptyset \Rightarrow str(a, i + 1, 1) = \emptyset$ $str(a, i, 1) = \emptyset \Rightarrow str(a, i + 1, 1) = \emptyset$](https://dxdy-03.korotkov.co.uk/f/e/f/c/efcfb8c5e44ae337c7c1b9fa0524849a82.png)
, что такое конец слова (если он есть)
![$( \exists len(a) ) \Rightarrow$ $( \exists len(a) ) \Rightarrow$](https://dxdy-01.korotkov.co.uk/f/0/7/d/07d5b309051b151a15c569c63eb0952f82.png)
![$( \exists c = a \cdot b )$ $( \exists c = a \cdot b )$](https://dxdy-04.korotkov.co.uk/f/3/0/9/309ed6b860037e61b3984c74fb2403d382.png)
![$\wedge ( i \le len(a) \Rightarrow str(c, i, 1) = str(a, i, 1) )$ $\wedge ( i \le len(a) \Rightarrow str(c, i, 1) = str(a, i, 1) )$](https://dxdy-04.korotkov.co.uk/f/f/9/0/f90972d6d9e0ab2473eff0f6203b8c7182.png)
![$\wedge ( i > len(a) \Rightarrow str(c, i, 1) = str(b, i - len(a), 1) )$ $\wedge ( i > len(a) \Rightarrow str(c, i, 1) = str(b, i - len(a), 1) )$](https://dxdy-01.korotkov.co.uk/f/4/d/2/4d2d7e8375b32a02c61c395b8cc2f7c182.png)
- 2-я Аксиома конкатенации, а раз будем рассматривать конечные слова, то сократим её до такого вида:
![$( \exists c = a \cdot b )$ $( \exists c = a \cdot b )$](https://dxdy-04.korotkov.co.uk/f/3/0/9/309ed6b860037e61b3984c74fb2403d382.png)
![$\wedge ( i \le len(a) \Rightarrow str(c, i, 1) = str(a, i, 1) )$ $\wedge ( i \le len(a) \Rightarrow str(c, i, 1) = str(a, i, 1) )$](https://dxdy-04.korotkov.co.uk/f/f/9/0/f90972d6d9e0ab2473eff0f6203b8c7182.png)
![$\wedge ( i > len(a) \Rightarrow str(c, i, 1) = str(b, i - len(a), 1) )$ $\wedge ( i > len(a) \Rightarrow str(c, i, 1) = str(b, i - len(a), 1) )$](https://dxdy-01.korotkov.co.uk/f/4/d/2/4d2d7e8375b32a02c61c395b8cc2f7c182.png)
И нас не будет интересовать член конъюнкции с
![$i \le len(a)$ $i \le len(a)$](https://dxdy-04.korotkov.co.uk/f/7/f/a/7facd4fb28a221c9d25d6ce29ff4260882.png)
, поэтому сократим до:
3.
![$( \exists c = a \cdot b ) \wedge ( i > len(a) \Rightarrow str(c, i, 1) = str(b, i - len(a), 1) )$ $( \exists c = a \cdot b ) \wedge ( i > len(a) \Rightarrow str(c, i, 1) = str(b, i - len(a), 1) )$](https://dxdy-02.korotkov.co.uk/f/d/7/0/d7033ead5be12f94422eb73df7d1a28582.png)
Понятно, что сделанные сокращения используют правило вывода
![$MP$ $MP$](https://dxdy-02.korotkov.co.uk/f/1/7/e/17ee8f6f0ca2f2433b512f44cdf83f4c82.png)
и тавтологии – например
![$A \wedge B \Rightarrow B$ $A \wedge B \Rightarrow B$](https://dxdy-04.korotkov.co.uk/f/f/b/d/fbd4f92330173e0a717924e11c1a871882.png)
. Если надо, я могу всё расписать, включая вывод тавтологий.
4.
![$( \forall i > I_{ChrLim}: ChrStr(i) = \emptyset )$ $( \forall i > I_{ChrLim}: ChrStr(i) = \emptyset )$](https://dxdy-03.korotkov.co.uk/f/e/5/d/e5de09822545998a6e0fb1469cf9296c82.png)
![$\wedge ( \forall i \le I_{ChrLim} \forall j \le I_{ChrLim}: i = j \Leftrightarrow ChrStr(i) = ChrStr(j) )$ $\wedge ( \forall i \le I_{ChrLim} \forall j \le I_{ChrLim}: i = j \Leftrightarrow ChrStr(i) = ChrStr(j) )$](https://dxdy-03.korotkov.co.uk/f/6/f/4/6f416d262c99b9523ba5d51c8e7615bc82.png)
![$\wedge ( \forall i \le I_{ChrLim}: ChrStr(i) = Str(ChrStr(i), 1, 1) \wedge Str(ChrStr(i), 2, 1) = \emptyset )$ $\wedge ( \forall i \le I_{ChrLim}: ChrStr(i) = Str(ChrStr(i), 1, 1) \wedge Str(ChrStr(i), 2, 1) = \emptyset )$](https://dxdy-03.korotkov.co.uk/f/2/b/5/2b53346cd2fac6763c460c34ea5f7b2282.png)
- Аксиома для символов
Доказательство (вывод)
Перепишем 3 для
![$a = ChrStr(0) $ $a = ChrStr(0) $](https://dxdy-03.korotkov.co.uk/f/a/7/f/a7f9bd49afe751d1d1f913250207e9b682.png)
,
![$b = ChrStr(1) $ $b = ChrStr(1) $](https://dxdy-02.korotkov.co.uk/f/1/4/7/1477d8b3cc1ca002595558c419dc5f9482.png)
, при этом
![$len(a) = 1$ $len(a) = 1$](https://dxdy-04.korotkov.co.uk/f/b/c/3/bc35ea82800a884a58c60eae3314581882.png)
из определения
![$len()$ $len()$](https://dxdy-03.korotkov.co.uk/f/a/2/5/a25ede651273d6912d162e6a7872939382.png)
. Получим
5.
![$\exists c: (c = ChrStr(0) \cdot ChrStr(1) ) \wedge ( i > 1 \Rightarrow str(c, i, 1) = str(ChrStr(1), i - 1, 1) )$ $\exists c: (c = ChrStr(0) \cdot ChrStr(1) ) \wedge ( i > 1 \Rightarrow str(c, i, 1) = str(ChrStr(1), i - 1, 1) )$](https://dxdy-03.korotkov.co.uk/f/a/2/7/a27cdf2d1d9f7dfc0f15120d3bda5e6982.png)
Подставим вместо
![$i$ $i$](https://dxdy-04.korotkov.co.uk/f/7/7/a/77a3b857d53fb44e33b53e4c8b68351a82.png)
число
![$2$ $2$](https://dxdy-04.korotkov.co.uk/f/7/6/c/76c5792347bb90ef71cfbace628572cf82.png)
и уберем истинную посылку
![$2 > 1$ $2 > 1$](https://dxdy-02.korotkov.co.uk/f/d/0/f/d0f6129d71177eac794390248ba2a8cc82.png)
(не расписываю тавтологии, логический вывод, но приведу их – неохотно и не сразу :), если кому надо – так как работа с определением неравенства и его использование в выводе из Пеано потребует много шагов). Получим:
6.
В силу равенства
![$c = ChrStr(0) \cdot ChrStr(1) $ $c = ChrStr(0) \cdot ChrStr(1) $](https://dxdy-02.korotkov.co.uk/f/9/7/8/9789cd9c403062a553bc91dac0a6e74282.png)
подставим вместо
![$c$ $c$](https://dxdy-04.korotkov.co.uk/f/3/e/1/3e18a4a28fdee1744e5e3f79d13b9ff682.png)
внутри
![$str()$ $str()$](https://dxdy-03.korotkov.co.uk/f/6/8/9/68996671d1aeb10ffb60138fdd8ad04782.png)
в 6 (технику вывода для «влезания» под квантор существования покажу ниже в пункте 9). Получим:
7.
Из тавтологии
![$A \wedge B \Rightarrow B$ $A \wedge B \Rightarrow B$](https://dxdy-04.korotkov.co.uk/f/f/b/d/fbd4f92330173e0a717924e11c1a871882.png)
получим:
8.
![$c = ChrStr(0) \cdot ChrStr(1) \wedge str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1) \Rightarrow$ $c = ChrStr(0) \cdot ChrStr(1) \wedge str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1) \Rightarrow$](https://dxdy-02.korotkov.co.uk/f/1/f/b/1fb0eabb8c2f5e4a8971921a7534fc9882.png)
![$str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1) $ $str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1) $](https://dxdy-03.korotkov.co.uk/f/e/7/f/e7fad2ebd3b180f6b1cdac25889b8d6882.png)
Из правила вывода для квантора существования (из «Оснований математики» Гильберта и Бернайса) и 8 получим:
9.
![$\exists c: c = ChrStr(0) \cdot ChrStr(1) \wedge str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1) \Rightarrow$ $\exists c: c = ChrStr(0) \cdot ChrStr(1) \wedge str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1) \Rightarrow$](https://dxdy-04.korotkov.co.uk/f/7/d/8/7d8dea42a64ea7350b773d2db9a0411f82.png)
![$str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1) $ $str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1) $](https://dxdy-03.korotkov.co.uk/f/e/7/f/e7fad2ebd3b180f6b1cdac25889b8d6882.png)
, это пример, как переносить результаты из логики высказываний под квантор существования.
Из 7 и 9 по правилу MP получим:
10.
![$str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1)$ $str(ChrStr(0) \cdot ChrStr(1), 2, 1) = str(ChrStr(1), 1, 1)$](https://dxdy-02.korotkov.co.uk/f/5/0/d/50d46874228bc187956f48561061647482.png)
А из пунктов 0 и 4 получаем
![$ChrStr(i) = Str(ChrStr(i), 1, 1)$ $ChrStr(i) = Str(ChrStr(i), 1, 1)$](https://dxdy-02.korotkov.co.uk/f/1/3/9/1391293aac6983b2862f55833850457582.png)
– см. последнюю строку в пункте 4, вывод утверждения методом подстановок и извлечения одного утверждения из конъюнкции утверждений пропускаю. Итак:
11.
![$ChrStr(i) = Str(ChrStr(i), 1, 1) $ $ChrStr(i) = Str(ChrStr(i), 1, 1) $](https://dxdy-04.korotkov.co.uk/f/3/5/2/352b421b1c3af31561880b4a3cda0bda82.png)
И из 10 и 11 и из
![$i=1$ $i=1$](https://dxdy-01.korotkov.co.uk/f/0/8/1/081b3265e50f611c00daeffa9193187382.png)
получаем:
12.
![$str(ChrStr(0) \cdot ChrStr(1), i, 1) = ChrStr(1) $ $str(ChrStr(0) \cdot ChrStr(1), i, 1) = ChrStr(1) $](https://dxdy-03.korotkov.co.uk/f/a/a/2/aa2674ef502d5897eadab8a3f3cc957682.png)
Что и требовалось доказать. Я облегчил себе задачу из-за того, что выбрал строку из одного символа. Иначе пришлось бы использовать пункт 2 и доказывать равенство строк по индукции. Но и там принципиальных трудностей нет.
Очевидно, что искомая строка
![$ChrStr(i)$ $ChrStr(i)$](https://dxdy-04.korotkov.co.uk/f/f/0/b/f0b97a431fe9306b815f71efc123696082.png)
будет найдена и функцией
![$find$ $find$](https://dxdy-01.korotkov.co.uk/f/4/8/2/482ae9cbfdd3e880c58d963fddc6851482.png)
в строке
![$ChrStr(0) \cdot ChrStr(1)$ $ChrStr(0) \cdot ChrStr(1)$](https://dxdy-02.korotkov.co.uk/f/1/1/3/1134c5ba966688b706188fc1cc10520782.png)
(см. соответствующую аксиому) и что верно неравенство
![$ChrStr(0) \cdot ChrStr(1) \ne ChrStr(i)$ $ChrStr(0) \cdot ChrStr(1) \ne ChrStr(i)$](https://dxdy-03.korotkov.co.uk/f/6/6/d/66d0e026363a5f3012fd34489d0a66d582.png)
– см. аксиому для равенства строк. Но, если нужны соответствующие выводы для доказательства этого – я тоже их приведу.
Вот примерно такой вывод, как представлен выше, я жду и от Михаила Д, чтобы увидеть, что у него (и сотен миллиардов профессионалов по всему миру :)) есть соответствующая теория первого порядка.
У меня сейчас отчётный период, поэтому не гарантирую ответов в июле. Всё же просьба – не использовать всякие «Ерунда», «Врёте или ошибаетесь» и т.п. Тем более, что «ерунда» и «враньё или ошибка» обычно не у меня )