III. Стандартная интерпретация арифметики и «не замеченная» логика строк
. К оглавлению . Показать весь текст .
Рассмотрим «стандартную интерпретацию» арифметики, которая соответствует всем аксиомам арифметики, и при этом имеет предельно слабые среди всевозможных интерпретаций арифметики выразительные возможности. Тогда мы получим наглядно ту выразительность, выше которой арифметика в принципе не может подняться. Потому, что если бы арифметика была более выразительной, то её логика выходила бы за рамки логики рассматриваемой модели, и эта модель не прошла бы проверку аксиомами арифметики - более выразительными в таком случае.
Я немного детализирую стандартную интерпретацию (детализирую в сравнении с классическими «Основаниями математики» Гильберта и Бернайса, например), чтоб подчеркнуть слабые стороны в её выразительности.
Числом будем считать «двойную коробочку» - из «основной» и «вспомогательной» коробочек. В основной коробочке - счётные палочки (мы не видим, какая там «куча» палочек), но эти счётные палочки можно перебрасывать по одной во вспомогательную коробочку. Ещё можно сразу все счётные палочки из вспомогательной коробочки «сбросить» в основную коробочку, не видя процесс «сброса», но возвращая наше «число» в «исходное состояние».
Как работает тогда операция равенства a=b? Мы перебрасываем по одной единице в обеих коробочках одновременно. Если единицы в основной коробочке a закончатся одновременно с единицами в основной коробочке b, то числа равны. Иначе - не равны.
А что такое a=b′? Мы перебрасываем по одной единице в обеих коробочках одновременно. Если единицы в основной коробочке b закончатся, а единицы в основной коробочке a не закончатся в этот момент, но закончатся после переброски ещё одной единицы из основной коробочки a - тогда a=b′. Иначе - не равны.
Легко достроить правила данной стандартной интерпретации - в соответствии с аксиомами для сложения и умножения арифметики Пеано. И мы получим стандартную интерпретацию с минимально возможной для арифметики выразительностью, но которая при этом соответствует логике арифметики (соответствует всем её аксиомам).
Представьте - мы ещё не придумали способов записи чисел иных, чем «эталонные количества», которые можем перебирать - но только по одной единице. Нет ни римского, ни арабского способа записи. Есть только счётные палочки. Вот в арифметике формализована именно такая «первозданная сущность» натуральных чисел (количеств).
Почему именно перебираем по единице? Потому, что в арифметике аксиоматизирована только одна предметная константа - 0 (Ноль), а все остальные числа возникают от увеличения на 1 нуля и полученных таким образом чисел. И процесс «сведения» сравнения чисел к сравнению нулей - это переход к «предыдущим» (до их увеличения на 1) числам. И равенство - это когда в итоге одновременно невозможно перебросить из основной коробочки ничего (единиц нет, в основной коробочке ноль единиц).
И такое «перебрасывание по одной единице» - это вовсе не дополнительное замедление из-за неудачной реализации («неудобная» логика реальности в рассматриваемой интерпретации, добавленная к логике собственно теории), а сама логика чисел арифметики.
Поэтому в серьёзных книгах по логике упоминается, что «правильное» представление чисел в арифметике (на примере 10) такое:
0′′′′′′′′′′
Или такое:
11111111111
В последнем случае у нас одиннадцать символов «1» (можно было бы использовать и символ «0»), потому что для обозначения нуля тоже нужно предусмотреть хоть один символ.
Но даже приведенные обозначения не совсем свободны от «внешней» по отношению к арифметике логики. Ведь мы записываем их в рамках логики работы математиков с формулами - а это включает в себя и логику строк, что выходит за рамки арифметики.
Таким образом, числа арифметики являются чрезвычайно простыми объектами, имеющими только одну характеристику - количество (величину). Это отличается от, например, чисел в позиционном представлении, которые имеют множество характеристик - цифры на разных местах, размер числа, величина числа. Например, число сто в обычной десятичной записи:
100
Первая цифра (сотен) - «1», вторая (десятков) - «0», размер (количество цифр) - 3, величина - сто.
В теории мы, обычно, имеем дело с формулами, где используются не конкретные числа, а переменные. Как говорил один из лучших обучавших меня математике преподавателей, некоторые теоретики даже не понимают, как применять свою теорию на практике - и это бывают хорошие, знающие своё дело теоретики. Вот переход от переменных к конкретным числам может быть непривычной «сменой амплуа» для части читателей, поэтому я так подробно останавливаюсь на этом.
Из вышесказанного следует, что логический вывод для конкретных чисел - если делать его строго в рамках арифметики - потребует такого количества шагов, которое не меньше величины конкретных чисел. А величина числа экспоненциально велика, если сравнивать её с размером данного числа в позиционном представлении. Да, мы в своих математических записях и мыслях можем «предвидеть», результат длинного «чисто арифметического» вывода и заменять запись числа:
0′′′′′′′′′′
На:
10
И «сокращать тексты» логического вывода, используя «очевидные» сокращения для «повторяющихся» (если писать их в строгом соответствии с арифметикой) приёмов получения очередных строк вывода из предыдущих строк вывода.
Но при таких «сокращениях» мы - на самом деле - используем ту логику, которой нет в арифметике. Как нет (и не может быть) в арифметике понятия «текст вывода», «сокращение текста вывода» и т.п. Хотя после чтения книг по логике с «гёделевыми номерами», способами «упаковки» нескольких чисел в одно и т.п. приемов, может создаться впечатление, что «тексты» в арифметике всё-таки есть.
Разумеется, «текстов» в арифметике нет, что было разобрано в предыдущем разделе при рассмотрении возможности определять контейнеры (конечные последовательности чисел) в теории компьютерных строк и невозможности подобных операций с числами в арифметике.
Конкретное значение в арифметике можно записывать самыми разными способами. Но нам нужен «канонический вид» для того, чтобы сравнивать конкретные значения на предмет равенства посредством логического вывода в арифметике от 0 (Нуля). Заметим, что числа не хранятся в виде формул. А если брать приведённую стандартную интерпретацию - то там простой перебор и он не противоречит аксиомам арифметики, а соответствует им. Поэтому вид чисел в арифметике может быть любой, но логика его использования не должна превышать возможностей стандартной интерпретации - а они довольно примитивные и связаны с перебором числа по 1.
Как шутил Форд: «Цвет автомобиля может быть любым, при условии, что он чёрный».
То есть - надо, чтобы логика использования выбранного вида данных (каждый шаг логического вывода для них) соответствовала тоже одному шагу логического вывода для стандартной интерпретации. Если это невозможно, значит, мы использовали дополнительную логику относительно арифметики, применяя данный способ записи чисел. Потому что одинаковая логика означает возможность одинаковых логических выводов.
Что можно извлечь из перебора количества по 1 в плане «частичного чтения»? Это ничего не может сказать о первом символе в строке, соответствующем «гёделеву номеру» данного числа, пока ты не перебрал это число (количество) до конца, например. Но не может сказать только в том случае, если речь идёт про строку многосимвольного алфавита. Потому что при односимвольном алфавите про любую непустую строку заранее известно, из каких символов она состоит.
Но нас интересует только строки многосимвольного алфавита, потому что при односимвольном алфавите даже позиционная запись для числа невозможна. И, кстати, мы видим метод исследования вопроса частичного чтения числа через исследование вопроса частичного чтения строк односимвольного алфавита. Как такое частичное чтение строки односимвольного алфавита может (видимо, не может) соответствовать частичному чтению строки многосимвольного алфавита, соответствующих (через какое-то взаимно-однозначное соответствие) строке многосимвольного алфавита?
Практически очевидно, что невозможно в общем случае прочитать часть строки односимвольного алфавита и узнать при этом начальную часть соответствующей строки многосимвольного алфавита - каким бы ни было взаимно-однозначное соответствие между строками односимвольного алфавита и строками многосимвольного алфавита.
Поэтому есть все основания развивать теорию строк, а вполне чёткое доказательство, взамен «практической очевидности», будет найдено по ходу развития теории и подтвердит гипотезу примата целостности для арифметики, что докажет её недостаточную выразительность для задач теории алгоритмов.
Получается, что примат целостности - понятие относительное. Мир допускает частичное чтение - и для чисел тоже. Вопрос только в том, может ли частичное чтение объектов одного типа (с логикой чисел арифметике в нашем случае) давать такое же частичное чтение для соответствующих им более сложных объектов (строк многосимвольного алфавита в нашем случае).
Притом в рамках теории мы не можем сказать, удастся ли нам частично читать объекты, соответствующие теории. Ведь реальность может вносить свои преграды и логику, которая не спрашивает нас - согласны ли мы на такое «добавление». И я приводил в прошлой статье пример «квазистрок» - зашифрованные строки, которые имеют свои специфические «операции со строками», но эти операции укладываются в аксиомы теории компьютерных строк. Числа тоже можно шифровать, в принципе - одни кучи счётных палочек ставить в соответствие другим. И в этих случаях приходится читать до конца - и зашифрованную строку, и зашифрованное число, чтобы узнать его начало.
Впрочем, мы знаем, что реальность позволяет нам объекты, соответствующие упомянутым теориям, строить таким образом, чтобы они были доступны для частичного чтения. И это существенная возможность для скорости вычислений и задач теории алгоритмов, поэтому наличие её логики в теории, и возможность её использования на практике - принципиальны.
Но помимо отношений теории и реальности (это в теории выразить невозможно в общем случае) - есть то, что можно понять в теории. И примат целостности - если он доказан теоретически - будет верен и на практике.
И если в теории (в теории строк - как более выразительной и пригодной для рассмотрения как строк, так и чисел) доказан примат целостности логики чисел относительно логики строк многосимвольного алфавита, то и на практике так и будет. Если уж теоретически нет возможности свести частичное чтение объекта (строки) к частичному чтению менее сложного соответствующего ему объекта (числа арифметики), то реальность это не улучшит - если логика теорий действительно соответствует реальности.
Поэтому частичное чтение строки многосимвольного алфавита не может быть заменено частичным чтением соответствующего ему числа или частичным чтением строки односимвольного алфавита ни теоретически, ни практически - если гипотеза примата целостности чисел относительно строк многосимвольного алфавита будет доказана.
Но помимо задачи частичного чтения, которое имеет принципиальное значение, строки (объекты с логикой строк) используются людьми (включая профессиональных математиков) существенно, но безотчётно во многих сферах, которые считаются «арифметическими». Например, на практике мы почти никогда не используем арифметику Пеано или её арифметические расширения. Вместо этого мы обычно используем более выразительную и не формализованную «арифметику работы с формулами». Как в предыдущем разделе в примере с функцией y=m^n. Логика этой «арифметики работы с формулами» не была формализована ранее. Хотя в рамках теории компьютерных строк она становится частью формальной теории.
Очень часто люди используют «арифметику работы с формулами» в неформализованных сферах. И там нет формальных способов доказать что-то отдельно от «арифметики работы с формулами». Иметь же неформальное представление о том, как объекты этой неформализованной сферы можно «спроецировать» в «арифметику работы с формулами» - зачастую проще, чем строить целую теорию первого порядка для данной неформализованной сферы и доказывать теоремы в ней, а не в «арифметике работы с формулами».
Поэтому нам нужно формализовать в полной мере то («арифметику работы с формулами»), что и без того «исполняет обязанности» теории, не являясь пока теорией 1-го порядка с равенством в полном смысле этого понятия.
После всего обнаруженного «партизанского» использования логики строк возникает вопрос - опираются ли доказательства логиков о неразрешимости, неполноте и т.п. на логику строк или нет? Понятно (благодаря усилиям тех же логиков), что в доказательствах о теориях невозможно обойтись средствами только разбираемой в теореме теории, но в части логики строк формализация достижима и её можно и нужно (в идеале) использовать явно и формально - если эта логика нужна и фактически используется в доказательстве.
Да, такая опора на логику строк бесспорно имеется. Разберём пример.
«Вычислимость и логика», Дж.Булос, Р.Джефри. Глава 15. Неразрешимость, неопределимость и полнота. Лемма 15.3 (о неопределимости в теории множества гёделевых номеров её теорем).
В лемме доказывается, что невозможно построить формулу C(…), которая:
1. Доказывалась бы для гёделевых номеров теорем данной теории T;
2. Доказывалось бы её отрицание для гёделевых номеров не-теорем данной теории T.
Где теория T достаточно выразительна для построения диагонализации. В частности - это теория Пеано и её расширения.
Притом доказательства формулы C(…) или ¬ C(…) про теорию T могут даваться даже в любом непротиворечивом расширении теории T, с тем же языком, что в теории T - это всё равно не поможет построить формулу C(…).
Доказательство невозможности такой формулы строится на лемме о диагонализации (15.2), когда отрицание доказуемости утверждения должно быть эквивалентно самому утверждению. Что для формулы доказуемости - невозможный для решения случай.
То есть, мы ставим (пытаемся, по крайней мере) гёделевым номерам формул в соответствие некоторую логику, и сами же опровергаем выразительную возможность подобного соответствия.
Но при этом мы решающим образом опираемся в своём опровержении на текст тех формул, которые соответствуют этим числам.
Мы смотрим вот на такую формулу:
G ⇔ ¬ C([G]), где [G] обозначает гёделев номер формулы G, а C(…) - искомая нами формула доказуемости/недоказуемости формул в теории T.
И говорим:
«Текст формулы G соответствует гёделеву номеру [G]…», а далее уже из этого делаем выводы о противоречии, если бы действительно формула C(…) была формулой доказуемости/недоказуемости в теории T.
Что в предыдущем абзаце выходит за рамки арифметики? Слово «текст». В арифметике (в её логике) нет текстов (нет логики строк). Пусть это слово «текст» не произносится, но, по сути, мы имеем в виду именно текст - потому что то, что стоит слева от знака эквивалентности в предыдущей формуле - явно не гёделев номер, а формула. А к формулам мы - когда ставим им в соответствие гёделевы номера - подходим именно как к текстам.
А если посмотреть на то, как определяется диагонализация выражения перед леммой 15.1, то мы увидим формулу:
∃ x (x=[A] ∧ A)
Где:
A - формула на языке арифметики с единственной свободной переменной x;
[A] обозначает гёделев номер формулы A.
Как можно было бы написать гёделев номер формулы A, не имея дело со строкой этой формулы? Думаю, что никак. Потому, что разве не требуется для вычисления гёделева номера формулы разбить её на символы? Разве не приходится ставить каждому символу из данной строки в соответствие некоторое число, зависящее не только от символа, но и от его места в строке? Требуется, и приходится.
И вот подобную работу со строками на неформальном уровне логики постоянно проводят в своих построениях и доказательствах, использующих гёделевы номера или аналоги гёделевых номеров формул.
Можно сделать шуточное предположение, что логики сделали вид, что не замечают своей работы со строками, чтобы не формализовать логику строк в теорию первого порядка, потому что тогда им пришлось бы вместо слов писать формулы и логические выводы в теории компьютерных строк.
Если же говорить более серьёзно, то люди часто не замечают самого привычного для себя. А что может быть привычней для математика, чем работа с формулами? У древних греков есть миф, что при движении планет звучит красивая музыка сфер, но мы настолько привычны к ней, что не в состоянии понять, что слышим её.
Конечно, можно было бы рассмотреть некоторую «вселенную», где вместо текстов формул используются числа, и они являются заменой текстов формул. Тогда нам не пришлось бы ссылаться на «текст формулы». Но это была бы «другая вселенная», существенно отличающаяся от нашей реальности. Ещё, кстати, вопрос - возможна ли такая вселенная и математика в ней? Однако не переходить во «вселенную» с числами вместо текстовых формул, и не указывать на то, что текст - вне логики арифметики - это означает создавать иллюзию, что в арифметике есть то, чего в ней нет - логики строк.
Контекст периода великих логических открытий был для математиков наполнен пониманием, что в доказательствах о теориях (об арифметике Пеано и её арифметических расширениях 1-го порядка) используется много логики, выходящей за рамки рассматриваемой теории. И, почти наверняка, в то время логика представления формул текстами воспринималась как выходящая за рамки арифметики.
Поэтому тогда едва ли могла возникнуть мысль подчеркнуть очевидное (очевидное в то время) отличие текстов от чисел арифметики и то, что в этой части доказательства о теориях используют «внешнюю» относительно арифметики логику. Но прошлый контекст постепенно исчезает и сейчас необходимо указывать, что тексты формул используются в доказательствах о теориях, но логика методов работы с текстами (строками) выходит за рамки собственно арифметики.
Вообще же логика работы с текстами (теория компьютерных строк) должна быть явно включена в формализм, используемый в доказательствах теорем логики о теориях. И рассматривать тексты (строки) - если делать всё аккуратно - надо при помощи теории, содержащей логику для текстов (строк).
Что может быть естественней, чем рассматривать объекты, подобные строке «Текст» в теории, где эти объекты являются объектами теории? А не «выкручиваться», используя арифметику и незаметно «подтягивая» сверх того не аксиоматизированную в арифметике логику работы математиков с формулами? Подразумевая, фактически, неявные функции для отображения строк в числа и обратно? Эти переходы от строк (не формализованных явно!) к числам и обратно - не нужны, если формализовать строки и явно использовать их и логику для них - вместо гёделевых (или аналогичных им) номеров.