Наука и ограничение на объём внимания

[alesha_popovich]

diletto в сообщении #1485795 писал(а):

Что касается огромных ресурсов, потребных для распаковки... Это ведь относительная вещь. Запакуйте "Войну и мир" любым архиватором и отдайте человеку, вооружённому только логарифмической линейкой.

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

diletto в сообщении #1485795 писал(а):

Да, и что понимается под "удобным"?

Удобным для пользования математиками по назначению.

[diletto]

alesha_popovich в сообщении #1485799 писал(а):

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

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

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

Цитата:

Удобным для пользования математиками по назначению.

Ок. Это плохо измеримая характеристика и вряд ли её удастся использовать в обсуждении.

[epros]

diletto в сообщении #1485789 писал(а):

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

Должно очень сильно повезти, чтобы совсем уж без потерь. Обычно всё же с потерями, но они обычно не столь уж существенны для нас. Как правило, то, что теряется, мы просто игнорируем или интерпретируем как "случайные ошибки".

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

[arseniiv]

diletto в сообщении #1485795 писал(а):

Эффективный в смысле коэффициента сжатия.

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

-- Пн окт 05, 2020 20:05:27 --

Иначе говоря удивительная эффективность аксиоматизации — пример ошибки выжившего.

[epros]

diletto в сообщении #1485802 писал(а):

Универсального алгоритма вывода всех следствий из аксиом у нас нет.

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

-- Пн окт 05, 2020 19:13:32 --

arseniiv в сообщении #1485830 писал(а):

Есть теории, которые не только конечно не аксиоматизируемы, они даже не разрешимо аксиоматизируемы и не перечислимо аксиоматизируемы.

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

Что же касается "теорий", не имеющих разрешимой аксиоматики, то я не случайно ставлю слово "теория" в этом случае в кавычки. Т.е. если понятие "теория" определять достаточно широко, то их тоже можно считать "теориями", но уж аксиоматическими теориями их считать никак нельзя. А все нормальные теории (которые имеют хоть какое-то применение) - именно аксиоматические.

[Anton_Peplov]

Anton_Peplov в сообщении #1194051 писал(а):

Munin в сообщении #1194047 писал(а):

Вопрос на засыпку: как по-вашему, можно ли всю математику втиснуть в книгу размером 300-350 страниц? Или в две такие книги (одна - "элементарная", другая - "высшая").

Можно и в страницу. Записать аксиомы ZFC и "следствия из этих аксиом предоставляем читателю в качестве упражнения".

На всякий случай расшифрую сарказм:

1. Система аксиом не говорит нам, какие определения, а тем более утверждения, интересны, а какие нет. Кто, глядя на на аксиомы ZFC и только на них, способен додуматься до понятия производной?

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

[epros]

arseniiv в сообщении #1485830 писал(а):

Иначе говоря удивительная эффективность аксиоматизации — пример ошибки выжившего.

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

-- Пн окт 05, 2020 19:35:10 --

Anton_Peplov в сообщении #1485833 писал(а):

Система аксиом не говорит нам, какие определения, а тем более утверждения, интересны, а какие нет. Кто, глядя на на аксиомы ZFC и только на них, способен додуматься до понятия производной?

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

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

-- Пн окт 05, 2020 19:54:32 --

diletto в сообщении #1485802 писал(а):

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

Тут и понимать особо нечего. Применение правила вывода - это шаг алгоритма конкретного вывода.

[diletto]

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

Тут и понимать особо нечего. Применение правила вывода - это шаг алгоритма конкретного вывода.

Да, это до меня уже дошло.
Я по простоте душевной считал, что если A,B,C совершенно достаточны для вывода D, то в D не содержится информации сверх той, что уже есть в A,B,C.
Но это неверно, т.к. дополнительная информация - это набор шагов конкретного алгоритма, выводящего D.
То есть я проводил ложную аналогию между, скажем, "распаковкой" сколь угодно большого количества знаков трансцендентного числа с помощью заранее известного алгоритма и "распаковкой" же теорем из аксиом - упуская из виду, что там алгоритм неизвестен.

[epros]

diletto в сообщении #1485849 писал(а):

Я по простоте душевной считал, что если A,B,C совершенно достаточны для вывода D, то в D не содержится информации сверх той, что уже есть в A,B,C.
Но это неверно, т.к. дополнительная информация - это набор шагов конкретного алгоритма, выводящего D.

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

Кажется, что из аксиоматики, которую можно записать конечным количеством символов, можно вывести бесконечное множество утверждений, а поэтому "эффективность сжатия" информации бесконечна? Вот только:
1) Далеко не все из этого бесконечного множества выводов нам нужны.
2) Из того конечного подмножества выводов, которые нам действительно нужны, далеко не все абсолютно точно соответствуют той предметной области, к которой применяется теория. Поэтому приходится ещё и делать некоторый допуск на неточность "распакованной информации".
3) Если покопаться, то есть ещё куча нюансов, так что далеко не всегда можно говорить о какой-то необычайно высокой эффективности в смысле степени сжатия информации. Но это всё же одно из важнейших свойств, которые мы ожидаем от хорошей теории.

[arseniiv]

Anton_Peplov в сообщении #1485833 писал(а):

Кто, глядя на на аксиомы ZFC и только на них, способен додуматься до понятия производной?

Кстати, я боюсь, даже до понятия ординала, хотя оно должно быть ближе достижимо — теория множеств же.

diletto в сообщении #1485849 писал(а):

Я по простоте душевной считал, что если A,B,C совершенно достаточны для вывода D, то в D не содержится информации сверх той, что уже есть в A,B,C.
Но это неверно, т.к. дополнительная информация - это набор шагов конкретного алгоритма, выводящего D.

Смотря что мы в точности вычисляем; что мы ожидаем. Лучше определить какую-то случайную величину и измерить её собственную информацию на исходе D. Или несколько величин и что-то подобное посчитать. А то может оказаться и ноль информации, и не ноль, и будет свалка, пока не разберутся, что хотят на самом деле разного и потому и ответы разные.

[Anton_Peplov]

diletto
Сверхкраткое введение в формальные языки и теорию доказательств. А то мне лично кажется (извините, если я ошибся), что Вы не очень понимаете, о чём говорят собеседники.

Подробности можно посмотреть, например, в "Клини. Математическая логика".

1. Определяем алфавит (обычно в него входят латинские буквы, цифры, скобки, логические символы и т.д.). Просто перечисляем символы. Их конечное и обычно небольшое число.
2. Определяем, какие наборы символов являются высказываниями (например, $\forall x \ x > 5 \Rightarrow x > 2$ является высказыванием, а $((8+$ - нет).
Пункты 1-2 называются "определим язык".
3. Определяем, какие высказывания мы принимаем за аксиомы.
4. Определяем, какие конечные цепочки высказываний являются доказательством последнего высказывания в цепочке.
Пункт 4 называется "определяем правила вывода".

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

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

Тривиально строится алгоритм, который для любого высказывания $X$ ищет его доказательство или же доказательство его отрицания.


Ясно, что все строки языка конечной длины можно упорядочить в алфавитном порядке. Определим функцию $G(i)$, которая выводит любую строку языка по её номеру.

(Например, так)

Пусть алфавит состоит из $N$ символов.

- если $i \le N$, то $G(i)$ - $i$-тый в алфавитном порядке символ.
- если $N < i \le 2N$, то $G(i)$ - слово из двух символов, в котором на первой позиции стоит первый в алфавитном порядке символ, а на второй - $(i - N)$-ый в алфавитном порядке символ.
- и т.д., думаю, принцип ясен. Как ясно и то, что любая строка конечной длины будет порождаться при некотором $i$.

Дальше всё просто.

Присваиваем $i := 1$ (сознательно не оформляю как код, в данном случае это неудобно).
1. Вычисляем $G(i)$.
2. Получилось доказательство высказывания $X$? Если да, завершаем работу. Если нет, переходим к следующему пункту.
3. Получилось доказательство высказывания $ \neg X$? Если да, завершаем работу. Если нет, переходим к следующему пункту.
4. Увеличиваем $i$ на единицу и переходим к п. 1.

Ясно, что если в данной теории вообще существует доказательство высказывания $X$ или же его отрицания, то алгоритм рано или поздно их найдёт и остановится. Только вот при попытке сделать это на реальном, а не воображаемом, компьютере ему может понадобиться столько времени, что все умрут, звёзды погаснут, и даже белые карлики взорвутся как термоядерные сверхновые из-за туннельного эффекта. Полный перебор такой полный. Поэтому с практической точки зрения такой алгоритм никакого интереса не представляет.

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

[diletto]

Anton_Peplov в сообщении #1485859 писал(а):

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

В целом так и есть, я слышал звон, и только. Ну, старика Гёделя кто не знает :)
Ваше введение понятно и - на уровне размахивания руками и воспоминания популярных книжек, того же Стюарта, кажется - знакомо. Но, конечно, я не имею никакого опыта и даже представления о конкретных подходах к построению формальных теорий.

Мне кажется, описанный алгоритм мало отличается (с точки зрения вопроса о порождении дополнительной информации) от такого: "возьмём символы английского алфавита, далее примем в качестве тривиального правила составления цепочек, что любой символ можно поставить вслед за любым, и через некоторое время перебора цепочек и сравнения их с нужным томом Шекспира получим этот том."
Убеждает ли нас эта процедура, что все литературные произведения содержат не больше информации, чем алфавит?

-- 06.10.2020, 21:42 --

Я имею в виду (т.е. склонен оспаривать) эту реплику:

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

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

[Anton_Peplov]

diletto в сообщении #1485965 писал(а):

Мне кажется, описанный алгоритм мало отличается (с точки зрения вопроса о порождении дополнительной информации) от такого: "возьмём символы английского алфавита, далее примем в качестве тривиального правила составления цепочек, что любой символ можно поставить вслед за любым, и через некоторое время перебора цепочек и сравнения их с нужным томом Шекспира получим этот том."
Убеждает ли нас эта процедура, что все литературные произведения содержат не больше информации, чем алфавит?

Это глубоко поверхностная (с) аналогия.

Будем понимать под информацией об утверждении ответы на два вопроса: 1) доказуемо ли оно (да/нет) и 2) опровержимо ли оно (да/нет). В этом смысле вся информация почти* обо всех утверждениях теории действительно содержится в связке "аксиомы + правила вывода". А идея полного перебора - это всего лишь демонстрация того, что таки действительно содержится, что её хотя бы в принципе можно оттуда вытащить.
*почти - потому что обо всех, кроме одновременно недоказуемых и неопровержимых (которые будут, согласно Гёделю, если наша теория непротиворечива и содержит хотя бы арифметику).

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

Произведения Шекспира не являются утверждениями и не выводятся ни из каких аксиом, поэтому неясно, что призван иллюстрировать приведённый Вами пример.

[diletto]

Anton_Peplov в сообщении #1485974 писал(а):

Будем понимать под информацией об утверждении ответы на два вопроса: 1) доказуемо ли оно (да/нет) и 2) опровержимо ли оно (да/нет). В этом смысле вся информация почти* обо всех утверждениях теории действительно содержится в связке "аксиомы + правила вывода". А идея полного перебора - это всего лишь демонстрация того, что таки действительно содержится, что её хотя бы в принципе можно оттуда вытащить.
*почти - потому что обо всех, кроме одновременно недоказуемых и неопровержимых (которые будут, согласно Гёделю, если наша теория непротиворечива и содержит хотя бы арифметику).

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

Произведения Шекспира не являются утверждениями и не выводятся ни из каких аксиом, поэтому неясно, что призван иллюстрировать приведённый Вами пример.

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

Поправка:
"на множестве всех текстов" - неверно, перебираем-то ключи, а не тексты.

[diletto]

Мда, что-то не клеится с аналогиями.