Тимур Василенко ([info]timur0) wrote,
@ 2007-07-31 19:58:00
Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Entry tags:Наблюдения краем глаза

Противоречие и существование
Девиз Таинственный похож
На опрокинутое 8:
Она - отраднейшая ложь
Из всех, что мы в сознаньи носим.

И. Анненский


В математической логике есть теорема Гёделя о полноте, гласящая, что любая непротиворечивая теория первого порядка имеет модель. То есть если в теории нет противоречия, то описываемый этой теорией объект существует. Более детальный анализ показывает, что если теория имеет конечный или счетный язык, то существует счетная модель этой теории (это уже теорема Левенгейма-Сколема). Возьмем канторовскую теорию множеств в аксиоматике Цермело-Френкеля (ZF). Она утверждает существование несчетных множеств, более того - существование бесконечной последовательности все более мощных ординалов. Одновременно с этим теория множеств в аксиоматике ZF удовлетворяет условиям теоремы Левенгейма-Сколема и, тем самым, имеет счетную модель, в которой все эти бесконечные ординалы счетны. Получили противоречие, которое носит название парадокса Сколема.

Рассмотрим это подробнее. Два множества называются равномощными, если существует взаимно-однозначное соответствие между их элементами; если же такого соответствия нет и первое множество взаимно-однозначно отображается на подмножество второго, то говорят, что мощность второго множества больше. Согласно теореме Кантора мощность множества всех подмножеств непустого множества больше мощности этого множества (P(A)>A), а специальная аксиома ZF (аксиома степени) гарантирует, что вместе с любым множеством существует и множество всех его подмножеств. Как же такая теория может иметь счетную модель?

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

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

Что значит, что теория непротиворечива? Это значит, что сколько бы мы ни проводили логических выводов, понимаемых как цепочка формул, выписываемых по определенным правилам, мы никогда не выведем ложь, т.е. утверждение вида A&¬A. У нас есть непротиворечивость как некое свойство записей, текстов - и больше, в общем, ничего нет. То есть из этого синтаксического материала нам придется строить лингвистическую модель нашей формальной теории: рассмотрим множество термов (выражений вида 1+1, (1+1+1)*(1+1+1+1-1-1+0) и т.п., использующих константы и функции, но не использующих переменные, кванторы и предикаты) и введем на нем отношение эквивалентности такого вида: T1~T2, если в этой теории доказуема формула T1=T2; факторизуем множество всех термов по этому отношению эквивалентности (т.е. разобьем его на непересекающиеся подмножества из эквивалентных элементов) - получаемые классы эквивалентности и служат носителем модели (подробнее можно прочесть в любом учебнике матлогики). Осталось только определить мощность полученной модели. Алфавит теории счетен, длина любой формулы конечна, так что множество всех формул счетно. Классы эквивалентности - это непересекающиеся подмножества формул, т.е. их количество не более чем счетно. Т.о. мы получили счетную лингвистическую модель непротиворечивой теории. При этом счетность модели устанавливается средствами неформальной канторовой теории множеств, так что парадокс Сколема на неформальном уровне остается.

Оставим в стороне теорию множеств и сконцентрируемся на теореме Гёделя о полноте: непротиворечивая теория имеет модель, т.е. описываемые ею объекты в каком-то роде существуют. Насколько вообще правомочна такая лингвистическая модель для непротиворечивой теории? Неужели существование тождественно непротиворечивости (хотя бы в математике)? Неужели способность говорить о чем-то, не запутываясь при этом, доказывает, что это что-то существует? Проанализируем само понятие противоречия, чтобы как-то осмыслить непротиворечивость и существование. Прежде всего, противоречие - единственное абсолютно конструктивное понятие в математике, в любом ее изводе - что в классической, что в интуиционистской. Противоречие всегда строится явно, предъявляется. Возьмем понятие доказательства от противного: мы предполагаем некую гипотезу, противоположную тому, что хотим доказать. Потом самим ходом доказательства мы строим противоречие - выводим одновременно A и ¬A. Хотя доказательство теоремы косвенное (от противного), но само противоречие сконструировано, построено и предъявлено. В принципе, косвенным образом использовать противоречие это предположить, что оно имеет место - тупик с точки зрения логики, поскольку из такого предположения следует все, что угодно. Непродуктивно. Итак, противоречие используется именно конструктивным образом, зато его отрицание - точнее, утверждение о том, что его нет (непротиворечивость) - очень даже используется неконструктивным образом. Условно говоря, непротиворечивость либо доказывается - обычно построением модели одной теории в другой, получается такая относительная непротиворечивость, очень полезная вещь: благодаря ей из натуральных чисел, которые от бога (Кронекер), последовательно строятся целые, рациональные, действительные, комплексные числа, а также модели нестандартного анализа с актуальными бесконечно-малыми величинами; другое использование понятия непротиворечивости - она предполагается для некоторой теории и дальше делаются выводы на основании этого предположения. Один из таких выводов - что любая непротиворечивая теория имеет модель - мы как раз и рассматриваем.

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

Теорему компактности можно доказать и без использования теоремы Гёделя о полноте, с помощью ультрапроизведений и теоремы Лося. Я не буду вдаваться в подробности, отмечу только, что и здесь используются в виде носителя модели классы эквивалентности неких конструктивно построенных объектов. А теперь посмотрим на некоторые следствия из этой теоремы.

Рассмотрим аксиоматику абелевых групп, дополненную бесконечным числом аксиом Cn, утверждающих существование n различных элементов группы. К примеру, это можно записать так:
Существуют x1…xn (x1≠x2) && (x1≠xn) & (x2≠x3) && (xn-1≠xn)

Рассмотрим ее конечноаксиоматизируемые подтеории; можем считать, что в набор аксиом входят все аксиомы абелевой группы и сколько-то аксиом Ck. Моделью такой подтеории является циклическая группа <Zn,+> вычетов по модулю n с операцией сложения (остатки от деления на n) при достаточно большом n. Каждая такая модель является конечной, причем эти модели не вложены друг в друга (достаточно брать простые n). Получается, что из нашего знания бесконечного числа моделей (вернее - умения их построить), ни одна из которых не является моделью анализируемой теории (вся совокупность аксиом Cn говорит о бесконечной группе), вдруг следует существование модели для этой теории. Формально все верно, но здравому смыслу несколько противоречит.

Дальше - больше. Теми же рассуждениями мы можем доказать, что теория конечных абелевых групп неаксиоматизируема. Докажем от противного: пусть есть набор аксиом P1…Pm, утверждающий конечность группы. Добавим их к рассмотренной выше теории. Теперь можем считать, что каждая ее конечноаксиоматизируемая подтеория содержит не только все аксиомы абелевой группы, но и новые аксиомы «конечности». Все рассмотренные модели подтеорий являются конечными, так что удовлетворяют и новым аксиомам. Но тогда по теореме компактности получается, что заведомо противоречивая теория имеет модель (аксиомы P1…Pm не совместимы с бесконечным набором аксиом Cn)! Полученное противоречие показывает, что свойство «быть конечным» не может быть выражено в аксиомах.

А теперь вспомним алгебру. Из нее известно, что любая конечная абелева группа разлагается в прямое произведение циклических групп <Zn,+>. Т.е. мы все-таки имеем конструкцию стандартной модели, т.е. теорию конечных абелевых групп, которую, в то же время, не можем аксиоматизировать. Если это не противоречие, то парадокс во всяком случае. От чего-то стоит отказаться: либо от неформально понимаемой конечности, которая и дает возможность установить общую структуру произвольной конечной абелевой группы, либо от теоремы Гёделя (Левенгейма-Сколема, теоремы компактности…), которые слишком вольно трактуют существование - откуда я знаю, что доказав существование методами формальной логики, я не опровергну его, исходя из неформально постигаемых понятий конечного и бесконечного? Опровергли же мы формально доказанное несуществование.

Прежде, чем перейти к рассмотрению существования, проанализируем понятие конечного. Мы видели, что аксиоматически свойство конечности выразить нельзя, но почему-то можно выразить свойство бесконечности (мы с успехом это сделали). Нетрудно понять, почему так: бесконечность мы смогли выразить через бесконечное число аксиом, т.е. на самом деле мы его не выразили, мы его указали явно. Что значит «явно»? Разве мы выписали все эти аксиомы? Нет, мы указали способ их построения и, по сути, апеллировали к имеющейся у каждого человека интуиции конечного, или, если угодно, к интуиции натурального числа. Натурального, сиречь природного - само название говорит больше, чем любые объяснения. Интуиция бесконечного хорошо выражается словами «и так далее» - т.е. речь идет о собрании однородных элементов (это может быть как потенциальная бесконечность с возможностью продолжать некий процесс, либо актуальная бесконечность, где все элементы ее в каком-то смысле сходны, неразличимы). Получается, что математические объекты в некотором роде антропоморфны - они зависят от способов нашего мышления. В теореме компактности явно используется свойство конечности логического вывода. Да, так мы умеем мыслить. Но почему невозможно допустить, что бог, несоизмеримо превосходящий человека, умеет одновременно учитывать бесконечное количество условий? Вдруг то, чего мы не можем помыслить, одновременная взаимосвязь бесконечного числа утверждений, не возможна в природе, хотя любое конечное их сочетание вполне реализуемо? Это ограничение нашего разума, антропоморфизм. Получается, что вроде бы наиболее абстрактная область - формальные теории - оказывается очень зависящей от человека.

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

Теперь можем рассмотреть то существование, которое доказывается в теоремах Гёделя и Левенгейма-Сколема, конструкцию лингвистической модели. В этой конструкции одним из важнейших элементов является именно конечность - формул, доказательств, иначе мы бы не смогли построить отношения эквивалентности, и уж тем более модель не оказалась бы счетной. Кстати, формально эта теорема допускает использование несчетных алфавитов (тогда мощность модели будет равна мощности алфавита), но это обобщение явно находится за пределами здравого смысла - наше мышление и счетную-то бесконечность включает как конструкцию, т.е. бесконечный алфавит понимается в конечной кодировке (обычно кванторы, знаки операций, индивидные константы и бесконечное количество переменных x1,x2…xn - сама эта запись и является необходимой кодировкой с условием, что индексы записаны в десятичной системе). Как же мы можем осмыслить алфавит, который мы не в силах удержать в памяти целиком, да еще и не можем обозримо закодировать его отдельный символ? Что бы там ни было с алфавитом, конечность конструкций из него явно указывает на их антропоморфность. Поэтому можем поиграть этой антропоморфностью и посмотреть, как изменится само понятие их существования.

Формальные доказательства можно представить в виде своеобразной игры: первый игрок (назовем его «Утверждающий») выписывает некое утверждение (гипотезу) или шаг логического вывода, т.е. формулу, получаемую из ранее им выписанных по какому-либо правилу вывода. На каждый шаг первого игрока второй игрок («Опровергающий») выписывает конечное число формул, образующихся из ранее написанных любым из игроков по какому-либо правилу вывода. Цель Утверждающего: выписать в конце концов требуемую формулу, теорему. Цель Опровергающего: вывести противоречие, заведомо ложное высказывание. Будем считать, что последний ход всегда у Опровергающего, и если он достиг своей цели, то он победил. Позиции игроков асимметричны - Опровергающий может пользоваться плодами трудами обоих игроков, но не имеет права на гипотезы.

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


Для этого подумаем: а уверены ли мы, что арифметика в аксиоматике Пеано непротиворечива? Вопрос не математический, а философский. Вроде как уверены (см. цитированное выше высказывание Кронекера), но вполне может оказаться, что она противоречива, но всего вещества вселенной не хватит для записи вывода противоречия. Т.е. практически она непротиворечива, если противоречие и есть, мы никогда с ним не столкнемся. Пусть противоречие есть, тогда есть минимальный по длине вывод этого противоречия (длину вывода считаем в количестве формул, а не символов). Но тогда любой формальный вывод, имеющий меньшую длину, не может приводить к противоречию и полученный результат верен. К примеру, в теории чисел многое зависит от гипотезы Римана о нулях дзета-функции. Предположим, что мы каким-то способом смогли доказать следующее утверждение: «Формальный вывод доказательства или опровержения гипотезы Римана содержит не менее 1020 шагов (формул)». (интересно отметить, что такие утверждения мы можем делать даже относительно недоказуемых формул - для отсутствующего доказательства годится любая нижняя оценка) Для практического использования этого утверждения нам остается только оценить длину формальной записи доказательства, занимающего N страниц статьи. Думаю, что оценка 100*N2 вполне разумна. Итак, если неформальное доказательство какого-либо факта, использующего гипотезу Римана, занимает не более 109 страниц, то оно верно и этот факт доказан самым строгим образом (если строго доказаны использованные оценки). Миллиард страниц - это не так много: в данном случае надо брать не объем конкретной статьи, а объем всех математических текстов, поскольку эта конкретная статья неявно использует доказанные в них факты (возможно использует). Теперь мы можем добавить аксиому: «Гипотеза Римана верна» (или противоположную аксиому, но не обе сразу), чтобы практически работать в непротиворечивой математике.

Математика, конечно, очень преобразится при использовании такого рода доказательств. Главная загвоздка в том, что мы не умеем оценивать снизу сложность задач, исключения можно перечислить по пальцам: нижняя оценка Бардзиня для распознавания симметрии слова N log(N), оценки сложности распознавания слов и разрешения логических теорий Мейера-Рабина-Сейфераса - вот, практически, и все. Причем если оценка Бардзиня выполняется для «почти всех» слов, то во втором случае доказывается существование слов, на которых алгоритм будет работать не менее чем exp(exp(…(exp(N)…)) шагов. Для общей постановки задачи - определить минимальное время работы при конкретных начальных данных - никаких способов решения не известно, хотя данная задача имеет огромное практическое значение - в криптографии, к примеру. Общее состояние дел с нижними оценками практической сложности чего бы то ни было хорошо описывает цитата из книжки Г. Линдгрена «Занимательные задачи на разрезание»:
В отдельных (увы, очень редких) случаях можно строго доказать, что используемое число разрезов минимально. В некоторых случаях (тоже немногочисленных) у нас есть уверенность в этом, хотя строгое доказательство и отсутствует. Во всех же остальных случаях вполне возможно, что вам удастся найти лучшее или даже качественно новое решение.

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

Самое интересное, что теорема Гёделя о полноте доказана как раз с позиции бога - в ее доказательстве мы используем разбиение всех формул на классы эквивалентности, что предполагает транзитивность: A=B, B=C, тогда A=C. То есть прямое использование такого принципа предполагает, что длина доказательства последнего равенства равна сумме длин доказательств первого и второго равенств. Пока мы на точке зрения бога, т.е. не ограничены по длине используемых доказательств, то все нормально. Если же мы говорим, что можем использовать только «короткие» доказательства, то последнее равенство может оказаться недоказуемым и нам просто не из чего будет стоить лингвистическую модель непротиворечивой теории. Изменилась непротиворечивасть, изменилось и существование.

Вернемся снова к нашей игре. Это ведь конкурентная игра. Почему цели Утверждающего и Опровергающего должны быть противоположны? Переводя на язык математики: почему из противоречия следует все, что угодно? Неужели нельзя поставить себе иные, неконкурентные цели? Как на пикнике играют в бадминтон - цель подольше удержать воланчик в воздухе, кооперативная цель. Сопротивление тут выносится вовне - ветер или просто неуклюжесть. В математике, декларирующей работу с абстрактными объектами, этому «вне» неоткуда взяться, поэтому противоречие в ней подобно сверхтекучей жидкости - в самую маленькую дырочку пролезет и все отравит. В физике все иначе - есть внешняя среда, сама Природа, Реальность - которая и дает достаточно сопротивления для кооперации в игре. Физики делают странные вещи - хотя бы фейнмановское суммирование по всем траекториям частицы. Насколько я знаю, до сих пор не найдено непротиворечивого математического формализма. Но те противоречия, что есть в формализмах - откуда у нас есть уверенность, что они возможны в Реальности? Мы построили математического монстра - почему мы уверены, что возможен ему соответствующий реальный объект? Физики не уверены и потому вполне спокойно относятся к некоторым противоречиям (отнюдь не ко всем!). Есть у них некое чувство физического смысла, и некоторые конструкции им не обладают. С логической точки зрения действия физика можно описать правилом: «Строить только такие доказательства, при которых не возникает противоречия». Некий путь ведет к противоречию - так запретим такой способ доказательства! Эти доказательства уже не формализуешь - вместо конечного набора правил вывода, в которые можно подставлять любые допустимые выражения, мы имеем еще кучу ограничений - так нельзя, и так нельзя (не имеет физического смысла), а почти таким же способом - можно. На языке логики это уже не математика, а метаматематика - в физике они оказываются перемешанными. Физические рассуждения обладают достаточно большой вязкостью (если воспользоваться метафорой текучести), т.е. нам не требуется заделывать дыры полностью, достаточно, чтобы именно эта жидкость через них не лилась. В начале этой статьи я говорил о боге, который может учитывать бесконечное количество условий - в физике это бесконечное количество ограничений. Я не уверен, что это может быть выражено какой-либо математизированной физической теорией, так что они обречены сменять друг друга.
Должна ли, в самом деле, непротиворечивость быть гарантирована на веки вечные или же мы можем не предпринимать без надобности никакой ревизии формализма до тех пор, пока в нем фактически не появится противоречие? Математику такое отречение дается с трудом. Физик работает с физическими законами, которые подтверждаются тем, что находятся в соответствии со всеми известными физическими явлениями. Для него само собой разумеется, что он должен быть готов к тому, что однажды, в силу каких-то новооткрытых фактов, эти законы будут отброшены.

Г. Вейль «О символизме математики»


Итак, в результате мы имеем целый спектр разных существований: существование с точки зрения математического бога (то существование, которое использует математика), существование с наложением бесконечного числа разнородных условий (так по теореме Линденбаума можно расширить любую формальную теорию до полной и как-то так должна существовать Реальность), а также целый спектр временных существований по типу физических теорий. Есть и не охваченные предыдущими рассуждениями социологические реальности: можно ли утверждать, что в 50-х годах у США существовало намерение сбросить атомную бомбу на СССР? Похоже, что единственное, что можно сказать о таком существовании, выражается законом У.А. Томаса: «Если люди определяют ситуации как реальные, они реальны по своим последствиям».

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

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

Итак, короткие верные выводы при длинном доказательстве противоречия. В принципе, этому соответствует движение к недостижимой цели - вопрос лишь в том, успеет ли появиться что-то полезное до того, как противоречивость окажет свое разрушающее влияние. А вот и достаточно большая цитата из философского текста, примечательная именно обоснованием проводимых рассуждений:
Не будем спорить сейчас, возможно ли чистое искусство. Очень вероятно, что и нет; но ход мысли, который приведет нас к подобному отрицанию, будет весьма длинным и сложным. [...] Даже если чистое искусство и невозможно, нет сомнения в том, что возможна естественная тенденция к его очищению. Тенденция эта приведет к прогрессивному вытеснению элементов «человеческого, слишком человеческого», которые преобладали в романтической и натуралистической художественной продукции. И в ходе этого процесса наступает такой момент, когда «человеческое» содержание произведения станет настолько скудным, что сделается почти незаметным. Тогда перед нами будет предмет, который может быть воспринят только теми, кто обладает особым даром художественной восприимчивости. Это будет искусство для художников, а не для масс.

Хосе Ортега-и-Гассет «Дегуманизация искусства»


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



(Post a new comment)

в цейтноте
[info]falcao
2007-08-01 02:51 am UTC (link)
Я очень хотел бы прокомментировать, но никак не успеваю по времени. Но я очень постараюсь отозваться хотя бы частично по некоторым пунктам.

(Reply to this)(Thread)

Re: в цейтноте
[info]timur0
2007-08-01 05:33 am UTC (link)
Помнится, на заметку "Интуитивный образ континуума" я получил от Вас точно такой же комментарий :))

(Reply to this)(Parent)(Thread)

интергрирование по частям :)
[info]falcao
2007-08-01 02:01 pm UTC (link)
Сорри :) Про тот пост я даже забыл. Находился тогда в Швейцарии, у меня даже русской клавиатуры не было, и связь по Интернету была только из офиса. А потом началась вообще дикая свистопляска, и я про всё забыл. Спасибо, что напомнили -- к тому посту я тоже вернусь. А сейчас сделаю вот что. В конце ветки начну делать замечания, разбив всё на части. Разом мне всё одолеть не удастся, а по частям -- вполне. Я буду идти по тексту, и важные замечания будут чередоваться с второстепенными. Но так будет удобнее.

(Reply to this)(Parent)


[info]nigdeja
2007-08-01 08:04 am UTC (link)
Интересно, что это за китайский тест на привидения?

(Reply to this)(Thread)


[info]timur0
2007-08-01 09:14 am UTC (link)
Некий человек овдовел и через непродолжительное время снова женился. Тогда по ночам стал являться к нему дух умершей жены и упрекать, что он так мало времени скорбел по ней. Ни извинения, ни жертвоприношения не помогли - приведение продолжало являться. Тогда этот муж пошел к мудрецу Ли Чжану и рассказал о приведении. Ли Чжан заподозрил, что это не приведение является, а этого человека мучает совесть за столь поспешную женитьбу, и он сказал следующее:
- Сегодня, когда будете ложиться спать, поставьте рядом с ложем горшок с фасолью. Когда дух явится, засуньте руку в горшок и зажмите в кулаке горсть фасоли. Если это действительно дух, то ему не составит труда ответить, сколько зерен фасоли у вас в кулаке.
Этот муж так и сделал, и когда ночью явился дух его умершей жены, он зажал горсть фасоли в кулаке и сказал:
- О бессмертный дух, вы, небожители, знаете все тайны. Скажи мне, сколько зерен фасоли у меня в кулаке?
После этих слов дух пристыженно удалился и больше его не беспокоил.

PS. Ссылка на этот тест сама была тестом - я хотел знать, прочтет ли кто-нибудь кроме [info]falcao до конца этот текст :))

(Reply to this)(Parent)(Thread)

неприводимые привидения :)
[info]falcao
2007-08-01 02:05 pm UTC (link)
Ваша последняя фраза напомнила мне известный "прикол". Из дипломной работы: "А кто дочитает до этого места, тому я ставлю бутылку шампанского" :)

Есть ещё вариант: "А катод сделаем из дерева, потому что дипломную работу всё равно никто не читает" :)

Кстати, я при чтении не понял, что имелось в виду -- там написано "приведения" :)

(Reply to this)(Parent)(Thread)

Re: неприводимые привидения :)
[info]timur0
2007-08-01 02:56 pm UTC (link)
Хорошо хоть не "ПРЕВЕДения"!

(Reply to this)(Parent)(Thread)

topic
[info]falcao
2007-08-01 03:16 pm UTC (link)
Ой, а это вообще блеск! :) Стёб на тему "преведа" -- это один из моих любимых "топиков" :)

(Reply to this)(Parent)


[info]nigdeja
2007-08-01 04:03 pm UTC (link)
:)
А ссылка на теорему Лося - тоже тест? :)

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

(Reply to this)(Parent)(Thread)


[info]timur0
2007-08-01 05:34 pm UTC (link)
Нет, теорема Лося действительно существует :))

(Reply to this)(Parent)

"выпьем за лосЯ" :)
[info]falcao
2007-08-01 07:30 pm UTC (link)
Лось -- это польский математик.

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

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

По поводу вопроса о "длинных" доказательствах я позже хотел кое-что прокомментировать.

(Reply to this)(Parent)(Thread)

Re: "выпьем за лосЯ" :)
[info]nigdeja
2007-08-01 08:41 pm UTC (link)
Я решила, что это француз, причем не Лось, а именно ЛосЯ, но если поляк, тогда, мне кажется, - за ЛОся :)

Математическое обоснование правила компактности доказательств (назовем так условно), как и теорема Гёделя, интересно и важно для многих видов мыслительной деятельности, поэтому постараюсь почитать (и понять!) комментарии.

(Reply to this)(Parent)(Thread)

"пьянству -- бой" :)
[info]falcao
2007-08-01 09:16 pm UTC (link)
Фамилия польского математика пишется Łoś.

В заголовке коммента я просто "прикололся". Мне вспомнилась шутливая песня с таким названием, и там в припеве ударение несколько раз меняется: "за лосЯ, за лОся" :)

К математику это не имеет отношения -- я потому с маленькой буквы и написал.

Принцип компактности -- это хорошая и полезная вещь, хотя он сам по себе очень прост.

У меня в журнале были посты как про теоремы Гёделя о неполноте (наиболее "распиаренные"), так и про ту теорему Гёделя о полноте исчисления предикатов, о которой написано здесь. Если Вы не видели эти посты, я могу найти на них ссылки. Там текст специально рассчитан на то, чтобы не предполагать никаких изначальных знаний.

(Reply to this)(Parent)(Thread)

Re: "пьянству -- бой" :)
[info]nigdeja
2007-08-02 07:17 am UTC (link)
А лично вы как произносите: теорема ЛОся или теорема ЛосЯ?

Была бы вам очень признательна за ссылки.

(Reply to this)(Parent)(Thread)

полнота и неполнота
[info]falcao
2007-08-02 01:08 pm UTC (link)
Ударение приходится на первый слог.

По поводу теорем Гёделя о полноте: проще всего через календарь --

http://falcao.livejournal.com/2006/09/

Там есть подзамочное обсуждение (запись "анонс"), а сами посты открытые. Про функцию Радо -- это продолжение. (так получается покороче).

А это -- насчёт правил логического рассуждения и теоремы Гёделя уже о полноте. Ссылки на пост из трёх частей там внутри.

http://falcao.livejournal.com/50074.html

Слово "неполнота" относится к определённым формальным теориям, а "полнота" -- к исчислению предикатов. Слово используется в совсем разных смыслах.

(Reply to this)(Parent)(Thread)

Re: полнота и неполнота
[info]nigdeja
2007-08-02 02:56 pm UTC (link)
Спасибо. Буду читать.

(Reply to this)(Parent)

ремарки (1)
[info]falcao
2007-08-01 03:15 pm UTC (link)
Я начну, а потом продолжу. Буду нумеровать по пунктам для удобства.

1) Утверждение о наличии модели у любой непротиворечивой теории первого порядка -- это наиболее важный этап в доказательстве теоремы Гёделя о полноте, но она сама является лишь следствием этого результата. Из-за того, что это следствие практически "мгновенное", два утвержения часто отождествляют. При этом используется "логика" математиков: акцент делается на результатах, и если что-то легко получить, то в этом нет проблемы, и математики привыкли эти тонкости игнорировать.

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

Поэтому я бы говорил о факте, который непосредственно влечёт теорему о полноте.

2) Далее, теорема Лёвенгейма - Сколема позволяет "сжать" уже имеющуюся модель. Она более элементарна, нежели результат Гёделя. Обычно второе подсоединяют к первому и называют "теоремой Л. - С.", но мне кажется, что это нежелательно.

3) Парадокс Сколема в той ситуации, о которой Вы говорите, вообще не возникает. Пусть у меня есть счётная модель теории ZF. Элементами модели пусть будут натуральные числа. При этом отношение принадлежности интерпретируется как некое довольно изощрённое отношение на множестве чисел, которое не совпадает с "настоящим" (последнее есть просто отношение "меньше").

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

Далее я буду через M обозначать множество элементов этой модели. Всякое множество x, определимое в ZF (то есть такое, для которого существует однозначно задающий его одноместный предикат) имеет некоторую интерпретацию в M. Я её обозначу через m(x). При этом ясно, что если x "хорошее" (например, конечный ординал), то m(x)=x. Это следует из "настоящести" отношения принадлежности и отражает в некотором роде тот факт, что "натуральные числа создал господь Бог" :) Однако, если c -- это континуум, то есть Pow(omega), то m(c) не равно c: континуум интерпретируется уже не собой. То есть это уже есть (неизбежный) "дефект" модели M.

В чём тут дело? Из чего состоит m(c)? "На самом деле" это есть некоторое счётное подмножество в c=Pow(omega), состоящее только из "нужных" подмножеств в omega. То, что туда не вошло -- это, по остроумному выражению [info]__gasrit (отнесённому к "плохим" вещественным числам) -- это "суслики", то есть нечто в данном случае "неосязаемое".

Я давно заметил, что оборот "все подмножества в omega" не имеет вообще-то никакого смысла. Давайте вдумаемся, что означает "все". Имеется некий "класс", и если мы берём именно его, то это будет "всё". Если что-то не берём, то это будет не "всё". Само понятие "всего" предполагает, что сначала это самое "всё" уже задано, и только потом в процессе некоторого акта мы можем либо повторить это "всё", либо осуществить выбор только собственной части заданного "класса". Налицо акт сравнения, если подходить методологически.

По моим представлениям (и я об этом писал), континуум -- это не множество, а класс. Сам он "размыт" и потому не является объектом, из которого далее можно строить новые множества. Он состоит из всех подмножеств в omega, которые мы рассматриваем. А последнее (то есть то, что мы называем "множествами") -- это конвенция, которая в общем случае неоднозначна.

ПРОДОЛЖЕНИЕ СЛЕДУЕТ

Please do not reply to this comment!

(Reply to this)(Thread)

Re: ремарки (1)
[info]timur0
2007-08-02 07:38 am UTC (link)
1) Я знаю, что теорема о полноте несколько об ином; просто этот факт - что непротиворечивая теория имеет модель - не имеет собственного названия и мне было надо как-то его назвать. Тем более, что в классическом учебнике Дж. Шенфилда это утверждение и приведено как вторая формулировка теоремы о полноте. Отдельно замечу, что написанное - не математическая статья и я не упомянул об исчислении предикатов, логических и математических аксиомах и т.д. - стиль текста несколько иной, я не собираюсь опровергать математику или логику. Все парадоксы, о которых я говорю, возникают не на уровне деятельности (математической), а на уровне осмысления этой деятельности, попытки вписать ее в более широкий жизненный, мыслительный контекст.
2) Я знаю, что теорему Левенгейма-Сколема можно доказать сжатием существующей модели до счетной. В данном случае мне это не интересно - если есть объект, то мы с ним можем что-то сделать и получить другой объект; существование этого второго объекта напрямую зависит от существования первого. Меня же в данном тексте занимает вопрос, а как вообще возникает существование. Тем более что во многих учебниках матлогики (Шенфилд, Мендельсон, тот курс лекций, что я когда-то прослушал) используется именно это доказательство.

(Reply to this)(Parent)(Thread)

по 1 и 2
[info]falcao
2007-08-02 05:20 pm UTC (link)
Я понимаю все Ваши соображения, и мне с самого начала было ясно, чем Вы руководствовались. В данном случае я просто указал на несколько моментов (не самых важных по своей роли), которые можно как-то "улучшить" или "подвинуть".

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

Что касается авторства теорем, то тут меня просто всегда смущало, что авторы учебников "подклеивают" Гёделя к более раннему результату и тем самым фактически приписывают Сколему то, что он не доказывал.

(Reply to this)(Parent)

ремарки (2)
[info]falcao
2007-08-01 03:19 pm UTC (link)
ПРОДОЛЖЕНИЕ

Вернёмся к нашему Сколему. Оба множества omega=m(omega) и m(c) счётны. Между ними есть биекция f. Это множество. Оно определимо, если учесть тот факт, что проведённая конструкция является математической, и потому построение биекции может быть формализовано. То есть множество f определимо в ZF согласно тезису, похожем на тезис Чёрча. Это положение, в которое все верят -- о возможности теоретико-множественной формализации содержательных математических рассуждений из нашей реальной практики.

Итак, можно считать, что f определимо и потому m(f) имеет смысл. Но мы уже знаем, что x в общем случае не совпадает с m(x). Следовательно, f не обязано совпадать со своей интерпретацией m(f). Оно определимо, но определимым ведь будет и сам континуум. Поэтому разрешение парадокса заключается в том, что это рассуждение лишь влечёт факт отличия f от его интерпретации.

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

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

4) Я бы возразил против фразы, выделенной курсивом -- о том, что "противоречие" есть единственная "конструктивная" вещь. На самом деле ведь имелось в виду нечто другое. Я бы как-то скорректировал эту мысль, сделав её более точной по своей форме.

5) Когда Вы говорите о неаксиоматизируемости, желательно убрать обозначение P_1,...,P_m -- набор добавляемых аксиом ведь не обязан быть конечным. Но это мелочь на уровне опечатки. Существенно здесь другое. Когда Вы говорите о классификации конечных абелевых групп, то не отмечаете факт конечности числа слагаемых прямой суммы. Задать эту конечность не проще и не сложнее, чем задать конечность самой группы. Поэтому этот пример выглядит искусственно. Если бы речь шла о всех группах, где классификации нет, то имеет место то же самое.

Можно при этом пойти в другом направлении, рассмотрев группы периода 2. Они задаются условием (\forall x)(x^2=1), и все они абелевы. Для них классификация ещё проще -- это прямые степени группы Z_2. И тут особенно ясно, что утверждение о конечности Z_2^n есть то же, что и утверждение о конечности n. То есть прямые суммы тут просто ни к чему.

Если честно, то я в этой ситуации не вижу противоречия ни на каком уровне -- ну, не выразимо какое-то важное свойство в определённой сигнатуре. Если подходить к этому вопросу "наивно" (а именно такая методология и имеется в виду), то надо просто взять другой язык, где всё выразимо.

Кстати, обратите внимание на то, что понятие конечного в теории множеств (если определять "классически", а не по Дедекинду) даётся ПОСЛЕ понятия "бесконечного", а точнее -- после привлечения одного конкретного бесконечного объекта (ординала omega). И это хорошо согласуется с тем фактом, что у нас есть интуиция конечного. Для меня это значит, что мы имеем право рассматривать omega как актуально заданное множество всех "эталонов" конечного. Ну, а раз есть эта "палата мер и весов", то дальше всё уже просто.

Я пока на этом прервусь, и отмечу только то, что понятие "актуальной бесконечности" -- это на самом деле omega, и все элементы этого множества как раз хорошо различимы. Более того, "различимость элементов" -- это базовое канторовское требование к множеству, о чём часто забывают. Все парадоксы вызваны недостаточным вниманием к этому постулату. Говоря о "неразличимости", Вы явно имеете в виду вещт типа "континуума", но он-то как раз и не является "множеством" в полноценном смысле. Я об этом уже говорил.

ПРОДОЛЖЕНИЕ СЛЕДУЕТ

(Reply to this)(Thread)

Re: ремарки (2)
[info]timur0
2007-08-02 08:21 am UTC (link)
3) Я вообще считаю, что "мощность" в теории множеств - обманчивое понятие, более того - понятие чисто техническое и противоречивое на уровне "наивной теории множеств". Поясню на примере. Мы все знаем, что такое натуральные числа, мы имеем сходные до неразличимости интуиции этого объекта. Он - единственный, т.е. можем считать, что он именно объект, а не свойство. Конечно, теорема Гёделя о неполноте утверждает, что это понимание мы не можем формализовать и при любой попытке формализации будут существовать иные объекты, удовлетворяющие этому формализму; но они не зря называются нестандартными моделями арифметики - поскольку стандартная модель как раз и есть наша общая интуиция натурального ряда.
С другой стороны, есть понятие группы, которому удовлетворяет очень много математических объектов, из которых мы не можем выделить один, стандартный. В этом смысле группа есть не объект, а свойство.
Теперь рассмотрим понятие мощности в теории множеств. Сами множества мы считаем объектами (уж если есть натуральный ряд, то дальше строим из него). И вот тут мы вводим понятие мощности, причем оно не основано на интуиции - сам Кантор был удивлен, когда доказал свою теорему о степени множества. Нам кажется, что мощность существует, что она настолько однозначно определена, что уже не свойство, а объект. Формальный анализ показывает (и Ваши разъяснения в том числе), что это не так - нет какой-то одной мощности, это размытое понятие. Если мы в рамках формальной теории придали ему конкретный смысл - мы можем с ней работать; если же мы считаем, что у него есть какая-то "стандартная" интерпретация, общая для всех интуиция этого свойства - вот тут и начинаются проблемы, в частности - парадокс Левенгейма-Сколема. Понятие мощности возникло при попытке формализации наивного понятия о множестве, у него не было своей наивной интуиции. Собственно, и не обязано быть - далеко не все формальные построения могут обрести неформальную жизнь. Мощность обрела, но, как мне кажется, обманом.
4) Разумеется, есть еще куча других конструктивных объектов. Я здесь имел в виду, что противоречие есть конструктивный объект по преимуществу, что в математической практике оно используется конструктивно, строится. Впрочем, при обсуждении теоремы компактности как раз и отмечается, что противоречие используется и неконструктивно - в предположении о его наличии/отсутствии, так и конструктивно в самом доказательстве от противного.
5) Да, там пропущено многоточие - система аксиом может быть бесконечной. Я прекрасно понимаю, что в теореме о струкуре абелевых групп используется неформальная интуиция конечного - как раз это я и хотел подчеркнуть. Мне важно, что некоторые теоремы матлогики ограниченно применимы в остальной математике именно в силу различия в допустимости использования некоторых интуиций, в частности - конечности и стандартного натурального ряда.

(Reply to this)(Parent)(Thread)

по 3 -- 5
[info]falcao
2007-08-02 05:51 pm UTC (link)
3) Мне кажется, очень важно прояснить, в чём состоит "фантомность" понятия "мощности". Это не так трудно сделать.

Во-первых, понятие равномощных множеств предельно осмысленно. Теорема Кантора о том, что x не равномощна Pow(x) -- тоже. Это же "конструктивно"! Заметьте, что это никак не противоречит вполне разумной "аксиоме Больцано" о равномощности всех бесконечных множеств. Просто Pow(omega), то есть континнум, это не множество. И никакой "мощности" оно априори не имеет.

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

То есть в этом пункте у меня критические аргументы не такие, как у Вас.

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

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

Я бы здесь как "образец" брал не противоречия, а тавтологии. Это лучше. Только это будет "образец" уже не для конструктивности, а для другого.

5) Если даже добавить многоточие, то получится счётная система аксиом. Для того языка счётности достаточно. Но вообще-то добавляемые аксиомы могут быть любыми. Обозначения, как мне кажется, следует вводить только тогда, когда они далее используются. Поэтому там можно просто сказать, что добавили новые аксиомы.

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

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

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

(Reply to this)(Parent)

ремарки (3)
[info]falcao
2007-08-01 07:22 pm UTC (link)
ПРОДОЛЖЕНИЕ

И вот ещё что: как-то Олег, он же [info]az118, обратил моё внимание на то, что слово "актуальный" привлекается неудачно. Ведь это означает "действующий", а подразумевается всего лишь одновременное существование всех элементов сразу. То есть больше подходило бы другое слово. Типа "осуществимости". Здесь подводит язык -- неявно подразумевается, что осуществлённое как-то себя проявит и тем самым подействует, то есть станет "актуальным". Но это вторичный аспект, даже если считать его неизбежным.

Об остальном -- позже.

(Reply to this)(Thread)

Re: ремарки (3)
[info]timur0
2007-08-02 06:55 am UTC (link)
Осуществимость использовал Вопенка в своей альтернативной теории множеств, так что термин уже имеет свой, отличный от актуальности, смысл.

(Reply to this)(Parent)(Thread)