dmitgu

Categories:

3. Язык логики LA.

к Оглавлению

В каком же языке логики (не классическом) LA это может быть выражено? В том же самом языке – если смотреть на «слова» (теоремы) которые принадлежат и утверждения, которые не принадлежат (не доказаны), как и в зыке L. Будем использовать разные обозначения для этих языков только для того, чтобы обозначить, что у языка LA другая 1-я прикладная роль и другой алгоритм проверки, чем мы рассматривали для языка L. 

Не трогая язык, мы изменим алгоритм проверки (с Lc(t, y) на La(t, a, y)). Добавим сертификатов так, чтобы язык не изменился. Добавим, возможно, слов, которые не принадлежат языку, но с которыми работает алгоритм проверки. Затем для единичных задач рассмотрим «персональные» наборы сертификатов, в которых выбросим некоторые из тех подтверждающих сертификатов, которые заведомо не используются в силу теоремы о неопределимости.

Прежние сертификаты мы оставим без изменения, но записывать их будем в двух аргументах для алгоритма проверки: a, y. Где новая часть сертификата в аргументе a – это аргумент для программного кода алгоритма-решения. И для старых сертификатов этот аргумент пуст, но обозначать это будет так: «-». Можно было бы и пустую строку использовать: «», но мы выберем менее «слепой» вариант. В аргументе y по-прежнему находится текст, который в корректном случае является текстом доказательства.

Новые сертификаты тоже будут разбиты на 2 аргумента: a, y. Но в аргументе a будет программный код алгоритма-решения, который выдаёт ответ о (не)принадлежности языку LA проверяемого слова (утверждения) t.

Наш новый алгоритм проверки - алгоритм La(t,a, y). Он же – 1-я прикладная роль (полная!) для языка LA. Работает он так: «Очень быстро» возвращает 0 для случаев вида: La(«AntiSol», «Sol(…)», y), а в остальном работает как Lc(t, y).

Что означают слова «очень быстро» в предыдущем абзаце? Они означают – за полиномиальное количество шагов относительно размеров |t|, |a|. При этом – независимо от доказательства в аргументе y и его размера.

Теперь, допустим, мы рассматриваем (произвольный) алгоритм-решение Sol(t). Какие слова и сертификаты должны быть сопоставлены данному алгоритму из первой прикладной роли языка LA? А вот такие:

t, «Sol(…)»

А всё дело в том, что само использование алгоритма Sol(t) для решения создаёт ту данность, которая в нашем языке LA выражена частью сертификата a = «Sol(…)»: 

Для всех утверждений t, кроме «AntiSol», нет никакой разницы между сертификатом обычным («-», t) и «персонализированным» («Sol(…)», t) – алгоритм проверки работает с ними одинаково.

1. Теперь разберём случай Sol(«AntiSol») и покажем, что никакие доказательства для AntiSol ему недоступны ни в 1-ой прикладной роли языка L, ни в 1-й прикладной роли языка LA – при соответствии с алгоритмом-решением только тех сертификатов, часть a в которых равна программному коду алгоритма-решения.

1.1. Алгоритм-решение может быть корректным и может быть не корректным. Если он не останавливается, то он не корректен. Если он останавливается с результатом, отличным от 1 и 0, то он не корректен. Если он останавливается с 1 (единицей), когда проверяет доказуемость утверждения t, но нет ни одного доказательства утверждения t, то он не корректен. И если он останавливается с 0 (нулём), а есть доказательство для утверждения t, то он не корректен. И если есть хоть одно утверждение t, на котором он не корректен, то он не корректен. В ином случае он корректен. 

Поэтому на утверждении AntiSol алгоритм Sol(…) не корректен.

1.2. Некорректность алгоритма-решения Sol(…) соответствует тому, что он не может найти правильное решение утверждению AntiSol. То есть, ему соответствуют лишь те «сертификаты» (доказательства), которые не подтверждают (не доказывают) утверждение AntiSol. 

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

1.3. И в 1-й прикладной роли языка LA мы собрали все эти сертификаты для алгоритма Sol(«AntiSol») в совокупность всех сертификатов, соответствующих правильной работе Sol(«AntiSol»). И часть a у этих сертификатов равна «Sol(…)» и они все не подтверждают утверждение AntiSol:

И не подтверждают они потому, что одни сертификаты (которые могли бы подтвердить утверждение AntiSol) не доступны Sol(«AntiSol») и в силу этого в данном контексте не подтверждают утверждение AntiSol, а доступные для Sol(«AntiSol») сертификаты так и остаются не подтверждающими. Поэтому построенная нами 1-я прикладная роль языка LA полностью соответствует исходной прикладной роли и тому языку, которому соответствовала исходная прикладная роль языка L. Язык не меняется (LA = L), построенный алгоритм проверки ему соответствует. И каждому алгоритму-решению можно ставить в соответствие лишь те сертификаты в новой прикладной роли, у которых часть a равна программному коду данного алгоритма-решения.

1.4. Если ставится задача, чтобы Sol(«AntiSol») нашёл ответ, который у него есть за конечное количество шагов от алгоритма проверки языка LA, то алгоритм проверки даёт его для Sol(«AntiSol») и этот ответ – ноль: La(«AntiSol», «Sol(…)», …) = 0. При этом на месте аргумента доказательства стоит многоточие – алгоритм проверки не обращается в своей работе к данному третьему аргументу при таких 1-м и 2-м аргументах и в данном случае может быть записан в виде алгоритма с двумя аргументами La(«AntiSol», «Sol(…)») = 0. 

1.5. Модифицированный алгоритм проверки в LA - это ведь лишь «ускорение» обычного алгоритма проверки языка L – не персонализированного. И то, что алгоритм-решение не мог найти в L – он не может найти и в LA, но теперь нет нужды бесплодно перебирать доказательства (сертификаты) в поисках доказательства утверждения AntiSol. Теперь все эти сертификаты, доступные для Sol(…), сразу НЕ подтверждают утверждение AntiSol, в соответствии с теоремой о неопределимости.

Далее упомяну о некоторых возникающих «сопутствующих» вопросах.

2.1. О возможных результатах работы алгоритма Sol(«AntiSol»). 

«Он не сможет найти» - правильная информация. Но когда «он» останавливается с данным результатом («не могу найти» - 0), то доказательство находится. Это и означает, что «он» не полон. То есть – любой алгоритм-решение не полон, так как «он» произволен.

А если заведомо не способный Sol(«AntiSol») не останавливается, чтобы сохранить неопределённость в том, принадлежит или не принадлежит утверждение AntiSol языку LA? В LA это ему заведомо не удастся – с учетом пункта 3 раздела «Алгоритмы-решения. Теорема о неопределимости. Утверждение AntiSol»: 

Вечное затягивание с ответом ничего не даст - Sol(«AntiSol») в итоге всё равно не смог дать ответ «не могу найти доказательство», которого действительно нет – что является доступной «персонализированной» для алгоритма Sol(…) информацией в алгоритме проверки: La(«AntiSol», «Sol(…)») = 0. 

2.2. Зависимость подтверждения слова сертификатом от программного кода алгоритма-решения – не приводит ли к «порче» алгоритмов-решений?

А разве не что угодно можно поставить в зависимость от алгоритма-решения в алгоритме проверки, чтобы алгоритм проверки возвращал «Не могу найти доказательство»? Тут есть два нюанса и первый в том, что от сертификата принадлежность слова не зависит. Просто если его подтверждает не этот, то - другой сертификат. И так же решается вопрос о том, как же принадлежность слова языку может зависеть от алгоритма. Не зависит. Это алгоритм может быть не способен подтвердить слово.

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

Но мы же предполагаем, что наш алгоритм проверки построен корректно – то есть, его сертификаты действительно правильно указывают на слово и в части кода алгоритмов-решений тоже не содержат ошибок. И да, мы строили 1-ю прикладную роль языка LA на основе корректной прикладной роли языка L и теоремы о неопределимости. Поэтому прикладная роль языка LA – корректна. 

Алгоритм – он интересен только как производитель результата. И поэтому его программный код идет только в дополнение к другой части сертификата - доказательству, а доказательство представлено и в независимом от программного кода алгоритма сертификате – при a = «-».

2.3. Почему алгоритм Sol(«AntiSol») не может вернуть правильный результат про утверждение AntiSol, если разбираться в причинах этого не формально?

А откуда возникает обсуждаемая неспособность алгоритма Sol(…)? Алгоритм Sol(…) не констатирует, а делает слово «AntiSol» принадлежащим или не принадлежащим языку LA. И если считать принадлежностью слова «AntiSol» языку то, что происходит после этого действия алгоритма Sol(…), то для Sol(…) слово «AntiSol» действительно ещё не принадлежит.

Алгоритм проверки выдаёт не один из 2-ух вариантов «есть доказательство для данного утверждения» и «нет доказательства для данного решения». Нет, смысл 0 (нуля) в ответе алгоритма проверки – «данный текст не является решением (доказательством) разбираемого утверждения», а вовсе не «нет решения у разбираемого утверждения» и между этими двумя смыслами есть и такой: «Для алгоритма Sol(…) нет решения у разбираемого утверждения».

Чем отличается «это доказательство не годится» от «этот алгоритм не годится»? И как алгоритм-решение может оказаться в состоянии, которое отличается и от «есть решение данного утверждения» и «нет решения данного утверждения»?

А дело в том, что некоторые алгоритмы расположены на причинно-следственной оси ДО ответа о принадлежности данного слова к языку. А в теории, кстати, бывает, что не достигнуто ни одно из этих состояний – с логической точки зрения для данной теории – и это известно ещё из 1-ой теоремы Гёделя. Но фактически, конечно, факт отсутствия доказательства будет иметь место.

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

2.4. Почему раньше в учебниках по теории алгоритмов не рассматривалось соответствие между программным кодом алгоритма-решения и соответствующими ему сертификатами алгоритма проверки? 

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

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

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

Фигурально выражаясь – «быть Джоном Малковичем» - это не только получать почту Джона Малковича, пиццу Джона Малковича и зарплату на карточку Джона Малковича – то есть получать некие «значения» в «аргументы» Джона Малковича, а не в «аргументы» Брюса Уиллиса. И «быть Джоном Малковичем» – это не только (в дополнение к сказанному) оставлять на киноплёнке изображения Джона Малковича (а не Брюса Уиллиса) – результат работы Джона Малковича. 

Но, помимо всего сказанного, «быть Джоном Малковичем» - это ещё иметь лицо, мозги и прочие системы организма Джона Малковича (а не Брюса Уиллиса), потому что именно это лицо, мозги и прочие его системы организма определяют те изображения на киноплёнке Джона Малковича (а не Брюса Уиллиса), которые и являются результатом работы Джона Малковича. 

Error

default userpic

Your reply will be screened

Your IP address will be recorded 

When you submit the form an invisible reCAPTCHA check will be performed.
You must follow the Privacy Policy and Google Terms of use.