Ещё про логику: конструктивную, классическую и проч.

[epros]

В ответ на сообщение Sonic86 от Пт Сен 05, 2008 16:38:16 в теме http://dxdy.ru/topic15961-30.html

Sonic86 писал(а):

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

К сожалению, я как раз логики Зиновьева не знаю, поэтому рассуждать о ней не берусь.

Sonic86 писал(а):

Вы писали:
Вы определяете "индетерминизм" как отрицание "детерминизма". И это правильно. Но даже если Вы строго формализуете понятие "детерминизм", это ещё не гарантирует, что кто-нибудь когда-нибудь получит однозначный и окончательный ответ ("да" или "нет") на вопрос о том, существует ли он.
Согласен. Но утверждению "Либо детерминизм, либо индетерминизм" это не противоречит.

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

Sonic86 писал(а):

Классическое "Неверно, что А" делится конструктивным на 2 варианта: "Либо верно, что не-А, либо неверно, что А, и неверно, что не-А" (второй вариант как раз содержит в себе возможность принципиальной невозможности доказать или опровергнуть это утверждение (сущ-ет нечетное совершенное число)).

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

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

[Sonic86]

Блин, неужели я так криво выражаюсь!?
Я же в качестве третьего значения истинности имел ввиду "доказано, что недоказуемо и что неопровержимо".

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

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

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

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

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

Отдельный вопрос: правильно ли я понимаю следующее. Пусть $X = (\forall n)P(n)$ - утверждение в формальной арифметике. Пусть доказано (в метаформальной арифметике), что оно неразрешимо.
Тогда оно истинно (в классическом смысле). То есть если бы для него был контрпример, то Х было бы неистинно, что противоречит его неразрешимости. Это так? Или как?
Второе: если то, что я сказал верно, то оно верно не для всех формальных теорий. Например, для арифметики оно верно, а для геометрии (5 постулат) нет. Это так?
(то есть если верно второе, то тогда действительно классическая и конструктивная логика описывают теории совсем по-разному в общем случае (в геометрии Евклида например (ну там контрпримеров нет))).

Может есть какие-то еще интересные моменты или вопросы? Давайте четко сформулируем и выскажемся.


Хочется в качестве примера привести следующий параграф из комплексной логики Зиновьева в качестве возможной темы для дискуссии:

Универсальность логики.
Существует мнение, будто законы логики не являются универсальными, т.е. имеются случаи, когда один и тот же закон логики в одной области науки ведет к правильным результатам, а в другой - к ошибочным; будто законы логики имеют исключения, зависят от предметной области. Для подкрепления этого мнения (помимо общих пространных соображений) ссылаются на вполне определенные факты. Еще с прошлого века идет традиция, отвергающая закон противоречия в отношении переходных состояний объектов. В современной логико-философской лиетратуре к этому присоединяют ограничения на закон исключенного третьего и двойного отрицания в интуиционистской логике, а также на законы коммутативности и дистрибутивности в "квантовой логике".
Если логика действительно не является универсальной, единой для всех наук, то ее положения не имеют априорной силы для наук, и вопрос о ее использовании в них оказывается сомнительным. Но рассматриваемое мнение есть плод недоразумения. Уместно спросить: 1) Почему именно таке-то законы логики считаются неуниверсальными, а не другие? 2) Могут ли встретиться случаи, когда и другие законы логики окажутся неуниверсальными? 3) Имеются ли все-таки законы логики, являющиеся универсальными? 4) Где грань между универсальными и неуниверсальными законами логики? Ответить на эти вопросы несхоластическим образом невозможно. Законы логики по самой своей природе универсальны, не имеют исключений, не зависят от особенностей той или иной предметной области. От этих особенностей зависит лишь то, какие именно законы из множества возможных законов логики будут использоваться. Что касается фактов, которые якобы подтверждают эту концепцию, то они суть результат смешения различных логических форм.
Не является аргументом в пользу тезиса и факт множественности логических систем. Мы оставляем в стороне различие точек зрения, способностей и интересов логиков, различие интерпретаций логических исчислений, различие направлений в логике, исторический прогресс и прочие общеизвестные вещи. Возьмем наиболее интересный для нас случай: имеются два логических исчисления; они интерпретируются как логические теории, претендующие на описание свойств одних и тех же логических операторов; однако множества доказуемых в них формул (и значит, множества допускаемых ими правил логики) не совпадают. Если дело обстоит именно таким образом, то правильный вывод из этого факта может быть только такой: эти системы определяют различные наборы логических операторов.
Примером такого рода логических систем являются классическое и интуиционистское исчисления высказываний. Если они претендуют на то, чтобы дать определение свойств операторов "и", "или", "не", то их можно представить как различные определения отрицания. И неверно думать, что имеется некое природное отрицание, которое можно познать с различной степенью глубины, полноты и точности, подобно тому, как познают атомы, общества, животных, и свойства которого "интуиционисты" лучше постигли, чем "классики" (или наоборот). Прогресс здесь имеет место. Но он состоит в том, что применительно к некоторым потребностям познания отрицание дифференцировалось, и для различных его форм построены логические системы, определяющие их свойства. Различие логических систем (если, конечно, последние не являются вариациями на одну и ту же тему) есть показатель расширения и обогащения аппарата логики. Но это ни в коем случае не есть показатель того, что одни и те же законы логики верны в одних областях науки и неверны в других.
Иное дело - вопрос об универсальности определенной концепции логики. В этой связи надо заметить, что стремление представить классическую математическую логику в качестве единого средства решения любых проблем логической теории научных знаний (т.е. в качестве единой концепции логики вообще) оказалось неправомерным. Во многих случаях использование ее дало чисто иллюстративный эффект, породило парадоксальные ситуации и тупики. Так что ближе к истине будет оценка классической математической логики лишь как одного из средств логической теории научных знаний и, при условии соответствующих интерпретаций, как одного из ее разделов. В результате критик концепции универсальности логики по тем направлениям, о которых упоминалось выше, рухнула концепция, согласно которой классическая логика пригодна для решения всех проблем логической теории научных знаний (и "универсальна" в этом смысле). Разработка логики по этим направлениям, однако, есть разработка новых разделов универсальной логики.

[epros]

Sonic86 писал(а):

Я же в качестве третьего значения истинности имел ввиду "доказано, что недоказуемо и что неопровержимо".

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

Sonic86 писал(а):

Я так понял, Вы выделяете временной аспект в статусе утверждений.
Например, теорема Ферма была доказана только в 1993 году, поэтому до 1993 года ссылаться на нее как на истинную, ложную или неразрешимую было нельзя. А с 1993 она получила статус истинной и теперь на нее можно ссылаться как на истинную.

Нет, это тоже не так. Логика, в том числе и конструктивная, фактора времени не содержит. Между доказанностью теоремы Ферма после 1993 года и недоказанностью её до этого времени нет противоречия именно потому, что "недоказанность" не является логическим значением. Т.е. логическое значение для теоремы Ферма в 1993 году не изменилось. Просто до этого оно нам было неизвестно.

Sonic86 писал(а):

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

Да, это так.

Sonic86 писал(а):

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

Тут для начала важно понять, в рамках какой теории мы сами находимся. Если мы доказали недоказуемость утверждения в рамках своей теории, то это означает его опровержение. Другое дело, если мы строим рассуждение в рамках метатеории. Здесь мы можем доказать, что в рамках теории утверждение недоказуемо и неопровержимо. Но доказательство недоказуемости будет доказательством метатеории, а не доказательством рассматриваемой теории.

Sonic86 писал(а):

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

Здесь см. выше мой комментарий к понятию "неразрешимости" утверждения. Понимаете к чему я это? А к тому, что сама теория не в состоянии доказать "неразрешимость" своего утверждения.

Sonic86 писал(а):

Наличие смысла...

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

Тем не менее, такое (конструктивное) понимание "смысла" вполне формализуемо.

Sonic86 писал(а):

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

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

Sonic86 писал(а):

Отдельный вопрос: правильно ли я понимаю следующее. Пусть $X = (\forall n)P(n)$ - утверждение в формальной арифметике. Пусть доказано (в метаформальной арифметике), что оно неразрешимо.
Тогда оно истинно (в классическом смысле). То есть если бы для него был контрпример, то Х было бы неистинно, что противоречит его неразрешимости. Это так? Или как?

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

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

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

Sonic86 писал(а):

Второе: если то, что я сказал верно, то оно верно не для всех формальных теорий. Например, для арифметики оно верно, а для геометрии (5 постулат) нет. Это так?
(то есть если верно второе, то тогда действительно классическая и конструктивная логика описывают теории совсем по-разному в общем случае (в геометрии Евклида например (ну там контрпримеров нет))).

Здесь я суть вопроса не уловил. Но могу сказать, что конструктивная логика подходит ко всем теориям одинаково.

Sonic86 писал(а):

Хочется в качестве примера привести следующий параграф из комплексной логики Зиновьева в качестве возможной темы для дискуссии:

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

Как утверждается, Зиновьев в комплексной логике писал(а):

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

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

[Sonic86]

Ага. Рассмотренное соотношение истинности, ложности, недоказанности и доказательства недоказуемости мы понимаем одинаково.
Тут мне толком даже пояснять бессмысленно. Я, кажется, в проблематику въехал.
Мне надо прочитать что-то серьезное по конструктивной логике. Может быть Вы мне что-то предложите для начала (умоляю, только не Клини)?

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

Вы писали:
Тут для начала важно понять, в рамках какой теории мы сами находимся. Если мы доказали недоказуемость утверждения в рамках своей теории, то это означает его опровержение. Другое дело, если мы строим рассуждение в рамках метатеории. Здесь мы можем доказать, что в рамках теории утверждение недоказуемо и неопровержимо. Но доказательство недоказуемости будет доказательством метатеории, а не доказательством рассматриваемой теории.
В данном случае доказательство мета-арифметики о том, что в формальной арифметике утверждение неразрешимо, не является доказательством истинности (ни в арифметике, ни в мета-арифметике). В арифметике - потому что это не её доказательство. А в мета-арифметике - потому что невозможность найти контрпример доказана только для способов поиска, которые предлагает арифметика. Мета-арифметика может оказаться способной предложить способ поиска контрпримера, который завершится успехом.
Ни фига себе! Понял, конечно... Только начинает казаться, что надо смешивать теорию и метатеорию... Так можно было бы бороться с "парадоксальной ситуацией"...
Вот пусть К=конъюнкция теории и метатеории. К - это что? Во всяком случае в К недоказуемое $X=(\forall n)P(n)$ там было бы истинно.
Доказывалось бы это примерно так: $X=P(1) \and P(2) \and P(3) \and ...$. В силу того, что мы в формальной арифметике (это существенно, к примеру, если бы мы были в евклидовой геометрии, то дело обстояло бы уже по-другому), мы можем установить для каждого конкретного $k$ истинно $P(k)$ или ложно. То есть определить: верно $P(1)$ или нет, верно $P(2)$ или нет... Если бы было $k:P(k)$ - ложно, то $X$ было бы ложно, но $X$ - неразрешимо, поэтому $X$ истинно.

Про число значений истинности вроде понял. Это будет естественно, если понимать операцию отрицания так как в конструктивной логике.

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

Про геометрию подробно:
Берем систему аксиом евклидовой геометрии и выбрасываем из нее 5 постулат. На основе новой системы строим теорию и метатеорию. Теперь рассмотрим 5 постулат как некое предложение. В теории оно недоказуемо и неопровержимо. А в метатеории? А в метатеории с точки зрения конструктивного анализа?

Вы писали: В конструктивной логике отрицание обычно определятся как процедура, доказывающая, что процедура доказательства утверждения не может завершиться успехом (сводящая соответствующее предположение к противоречию).
Я это так понял: в теории КЛ оператора отрицания нету, а есть в метатеории КЛ и применяется к доказательствам КЛ?

(Маленькое замечание по поводу чтения текста (например Зиновьева и те 3-4 предложения, которые Вы вначале цитировали): там речь контекстно зависимая. Поэтому когда вы разбиваете текст на несколько предложений, то у этих предложений смысл изменяется. А это понятно к чему ведет. Вот, например, Зиновьев не утверждает, что дело в познании некоего "природного" отрицания.)

Еще я где-то у Вас в тексте видел нужную здесь цитату, но не нашел. Спрошу просто:
В рамках теории источником недоказуемости утверждения может быть только опровержение утверждения?

[luitzen]

Sonic86 писал(а):

Может быть Вы мне что-то предложите для начала (умоляю, только не Клини)?

Если можно, я встряну и порекомендую вот это: Новиков П. С. — Конструктивная математическая логика с точки зрения классической.

Sonic86 писал(а):

надо смешивать теорию и метатеорию

Что-то подобное в интуиционистской пропозициональной логике действительно имеет место: она погружается в D-исчисление Гёделя (читай: в льюисовскую S4), где D-оператор предлагается читать как «доказано, доказуемо».

Вот, кстати, интересная задачка: конечно или бесконечно число попарно неэквивалентных формул от одной переменной в интуиционистской пропозициональной логике?

[epros]

Sonic86 писал(а):

Мне надо прочитать что-то серьезное по конструктивной логике. Может быть Вы мне что-то предложите для начала (умоляю, только не Клини)?

luitzen писал(а):

Если можно, я встряну и порекомендую вот это: Новиков П. С. — Конструктивная математическая логика с точки зрения классической.

Ой, вот этого лучше не надо
Изучать конструктивную логику с точки зрения классической - это всё равно, что изучать ОТО по книжкам одного из её критиков
Я бы порекомендовал почитать кого-нибудь из собственно конструктивистов, например, А.А.Маркова. Есть хорошая книжка А.Гейтинга "Интуиционизм" под редакцией и с комментариями Маркова. В этих комментариях он изложил точку зрения конструктивизма на соответствующие вопросы.
А если уж говорить о "точке зрения одного с точки зрения другого", то лучше, наоборот, почитайте "A constructive interpretation of the full set theory", Valentin F. Turchin.

Вообще-то книжек по конструктивизму довольно много:
П.Мартин-Лёф, "Очерки по конструктивной математике" - краткий обзорный курс под редакцией Драгалина.
А.Г.Драгалин, "Конструктивная теория доказательств и нестандартный анализ" - более толстая книжка, сборник работ указанного автора.
Б.А.Кушнер, "Лекции по конструктивному математическому анализу" - мехматовский курс.
И.П.Натансон "Конструктивная теория функций".

Sonic86 писал(а):

Ни фига себе! Понял, конечно... Только начинает казаться, что надо смешивать теорию и метатеорию... Так можно было бы бороться с "парадоксальной ситуацией"...
Вот пусть К=конъюнкция теории и метатеории. К - это что? Во всяком случае в К недоказуемое $X=(\forall n)P(n)$ там было бы истинно.
Доказывалось бы это примерно так: $X=P(1) \and P(2) \and P(3) \and ...$. В силу того, что мы в формальной арифметике (это существенно, к примеру, если бы мы были в евклидовой геометрии, то дело обстояло бы уже по-другому), мы можем установить для каждого конкретного $k$ истинно $P(k)$ или ложно. То есть определить: верно $P(1)$ или нет, верно $P(2)$ или нет... Если бы было $k:P(k)$ - ложно, то $X$ было бы ложно, но $X$ - неразрешимо, поэтому $X$ истинно.

Хм. Если я правильно понял, то, наверное, так. Т.е. в метатеории $M$ мы можем доказать неразрешимость $X=(\forall n)P(n)$ в теории $T$:
$M \vdash \neg (T \vdash X) \land \neg (T \vdash \neg X)$
Объединяя теории $T$ и $M$, получаем доказуемость $X$:
$(M+T) \vdash X$
Доказательство, естественно, строится на сведении к противоречию предположения о существовании такого $n$, для которого $P(n)$ ложно. Правда там вылезет двойное отрицание, которое в общем случае не сводится к $P(n)$, но если $P(n)$ в силу своей структуры разрешимо для любого $n$, то закон снятия двойного отрицания для него работает...

Брр, что-то Вы меня уже запутали.

Sonic86 писал(а):

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

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

Sonic86 писал(а):

Про геометрию подробно:
Берем систему аксиом евклидовой геометрии и выбрасываем из нее 5 постулат. На основе новой системы строим теорию и метатеорию. Теперь рассмотрим 5 постулат как некое предложение. В теории оно недоказуемо и неопровержимо. А в метатеории? А в метатеории с точки зрения конструктивного анализа?

$M \vdash \neg (T \vdash X) \land \neg (T \vdash \neg X)$
- это формализация Вашего: "В теории оно недоказуемо и неопровержимо". Поскольку сия фраза есть утверждение метатеории, то в самом начале строки стоит буковка $M$. Попробуйте без дополнительных аксиом вывести отсюда что-нибудь вроде $M \vdash X$ или $M \vdash \neg X$. По-моему - дело безнадёжное.

Другое дело, если есть какие-то дополнительные аксиомы. Например, метатеория, в которой сформулирована первая теорема Гёделя о неполноте, cодержит арифметику. А это значит, что в ней доказуема любая теорема арифметики:
$M \vdash (A \vdash X) \to X$
Это уже можно использовать.

Sonic86 писал(а):

Вы писали: В конструктивной логике отрицание обычно определятся как процедура, доказывающая, что процедура доказательства утверждения не может завершиться успехом (сводящая соответствующее предположение к противоречию).
Я это так понял: в теории КЛ оператора отрицания нету, а есть в метатеории КЛ и применяется к доказательствам КЛ?

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

Sonic86 писал(а):

Зиновьев не утверждает, что дело в познании некоего "природного" отрицания

По-моему, в моей цитате это так и звучит.

Sonic86 писал(а):

Еще я где-то у Вас в тексте видел нужную здесь цитату, но не нашел. Спрошу просто:
В рамках теории источником недоказуемости утверждения может быть только опровержение утверждения?

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