Именно эта неформальная интерпретации нас и интересует.
Не могли бы вы дать какие-то ссылки на описание
этой неформальной интерпретации?

Я не совсем понимаю вопрос, стандартная ссылка -- Такеути,
Takeuti, Proof theory (2nd edition is better), Введение.

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

Доказательство Генцена является именно таким: Тheory of primitive recursive arithmetic имеет весьма ограниченный принцип индукции: для формул -- только по бескванторным формулам, для построения функций -- примитивная рекурсия

the function h defined by
h(0,x1,...,xk) = f(x1,...,xk) and
h(n+1,x1,...,xk) = g(h(n,x1,...,xk),n,x1,...,xk) is primitive recursive
if g,h are.

(В арифметике, кажется, единственное использование "актуальной бесконечности"---в принципе индукции.)

При этом, вполнеупорядоченность каждого кардинала меньше епсилон_0 можно
доказать в арифметике Пеано, если не ошибаюсь.


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

(Reply to this) (Parent) (Thread)

> Философский смысл доказательства Генцена
> примерно такой; нас интересует, насколько и в какой форме
> понятие "актуальной бесконечности" требуется для обоснования арифметики.

?! И где же в генценовских ординалах (кои суть конструктивные объекты, с вполне "конечными" операциями над ними) содержится актуальная бесконечность?

> (В арифметике, кажется, единственное использование "актуальной бесконечности"---в принципе индукции.)

?! И где же содержится актуальная бесконечность в индуктивном доказательстве тотальности примитивно рекурсивных функций, например? Я здесь вижу только обычное "сведение задачи к предыдущей".

> Без сомнения, в какой-то форме используется (при абсрагировании от конструктивных особенностей)

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

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

?! И где же в генценовских ординалах (кои суть конструктивные объекты, с вполне "конечными" операциями над ними) содержится актуальная бесконечность?

Она нужна для обоснования трансфинитной индукции и, вообще говоря, даже индукции по формулам с кванторами.

! И где же содержится актуальная бесконечность в индуктивном доказательстве тотальности примитивно рекурсивных функций, например? Я здесь вижу только обычное "сведение задачи к предыдущей".

там ее как роаз и нет

> Без сомнения, в какой-то форме используется (при абсрагировании от конструктивных особенностей)

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


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

(Reply to this) (Parent)

Уважаемый bbixob прислал мне сообщение и попросил высказаться на тему моего предмета, который тут обсуждается. СознАюсь, глубоко не вчитывался, уж очень много всего написано!

1) Про длинные ветки с обсуждением ZF и конструктивной математики - получилось интересно, но спорящие не слышали друг друга, т.к. оба порой говорили разумные вещи, но оставались неуслышанными.

2) Дискуссия была "в стиле ретро" (~1956-1963), т.к. современные аргументы (например обратная математика) не использовались.

3) Про то, есть ли "актуальная бесконечность" в утверждении про трансфинитную индукцию до эпсилон_0 - я согласен с __gastrit, и тоже не вижу здесь актуальную бесконечность.

Обычно актуальную бесконечность подразумевают в уже непредикативных системах, выше ATR_0, или в других системах где явным образом выписано (forall X) (exists Y), где кванторы бегают "по множествам". Т.е. в системах, где явно постулируется существование законченной "актуальной" бесконечности.

Однако я и раньше слышал слова, что трансфинитная индукция до какого-нибудь ординала - это слабое использование бесконечности, в том смысле, что ординалы продолжают натуральные числа и вот оно, первое место alpha, когда данная формула (ТR(alpha)) оказывется недоказуемой. В этом смысле я согласен с bbixob, просто слово "актуальная" было не к месту.

Если идти по разным веткам в дереве логической силы наверх, то оказывается, что ветки - разные: в некоторых ветках арифметические утверждения добавляются с помощью сильных аксиом существования про идеальные придуманные объекты: про труляляшек, про ZFC-множества, про NF-множества, а в некоторых снизу, находя новые и новые недоказуемые арифметические утверждения и добавляя их в мешок.

(Reply to this) (Parent) (Thread)

Cпасибо за приход.


3) А как *доказать* трансфинитную индукцию без использования актуальной бесконечности?
сформулировать мы можем, да, без.. И правильно ли я понимаю, что индукция по формулам с кванторами -- не"актуальная" бесконечность? А какая?

(Reply to this) (Parent) (Thread)

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

Например примитивно рекурсивные бесконечные множества - это просто пустышки набитые точками. Их "существование" или "несуществование" - это вопрос удобства записи. Философия, признающая такие множества называется финитизм.

АCА_0, арифметика пеано определяет все арифметические множества. Здесь из любого множества можно выделять подможества с помощю формул первого порядка с кванторами и использовать индукцию. Математика с ТАКИМИ бесконечными множествами называется конечной математикой.

Дальше идут АCA^'_0, АТR_0, Pi_1^2 CA_0 и Z_2.
До АТR_0 бесконечность еще не называют актуальной, потому что нет сильных формул выделения.

На твой вопрос как обоснуется ТR(эпсилон_0) - ответ такой: доказывается в АCA^'_0, например следует из бесконечной теоремы Рамсея или из трансфинитной индукции до ординала эпсилон_{эпсилон_0}.

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent) (Thread)

ACA^'_0 nu ili 1-neprotivorechivost' PA ne
soderzhat ssylok na aktualnuju beskonechnost' i
dokazyvajut TR(epsilon_0).

(Reply to this) (Parent)

> Дискуссия была "в стиле ретро" (~1956-1963), т.к. современные аргументы (например обратная математика) не использовались.

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

> Если идти по разным веткам в дереве логической силы наверх, то оказывается, что ветки - разные: в некоторых ветках
> арифметические утверждения добавляются с помощью сильных аксиом существования про идеальные придуманные объекты: про
> труляляшек, про ZFC-множества, про NF-множества, а в некоторых снизу, находя новые и новые недоказуемые арифметические
> утверждения и добавляя их в мешок.

Основной вопрос, который тут волнует лично меня — наличие семантики. Для первопорядковой арифметики она определена (башня Маркова), и потому тут добавлять новые утверждения мы можем хоть прямо наугад: в крайнем случае, ошибку потом можно будет найти и исправить. А где семантика у формул с множественными переменными?

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

> Понятия, честно говоря, не имею, что такое "обратная математика", и какие
> новые аргументы она добавляет к старому спору о том, идеальны или же материальны математические объекты.

--- Спор за последние два-три поколения изменился и трансформировался. Его костяк может и похож на старый, но сейчас новое понимание.
Прогресс у человечества идет вперед. И история конструктивной математики и неконскруктивной тоже (но связанной) тоже идет вперед.
Когда-то был только Кронекер, а потом Пуанкаре, потом Брауэр, Хейтинг, Марков, Шанин. Неужели с 1960х годов мы не стали понимать больше?
Стали и очень много! Несколько революций в математической логике с 1960х годов совершенно всё изменили.
(Разница между 2000-ми годами и 1960-ми примерно такая же как между 1960-му и серединой ХиХ века.)

Я примерно на эту тему недавно даже книжку заказал в магазине, под названием "Крейзелиана".

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

--- Нет в наше время одной "теоретико-множественной" парадигмы, да и нескольких нет. Всё сложнее. Z_2 - это теория множеств или нет? Или АТR_0 или АCА_0?
как насчет интуиционистской теории множеств Микаэла Ратьена?
Да и конструктивизмов разных дюжина. Который чьему сердцу ближе?

> Поэтому сия деятельность, честно говоря, не
> представляется мне особо интересной (если я неправ, то с интересом выслушал бы, почему).

--- В логике творятся чудеса, по всему спектру филосовских фонов. Поинтересуйтесь! Очень интересно!

> Основной вопрос, который тут волнует лично меня — наличие семантики. Для первопорядковой арифметики она определена (башня Маркова), и потому
> тут добавлять новые утверждения мы можем хоть прямо наугад: в крайнем случае, ошибку потом можно будет найти и исправить.

--- Я имел в виду классическую логику. Кстати, про конструктивную арифметику: как насчет семантики Шанина?

> А где семантика у формул с множественными переменными?

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

(Reply to this) (Parent) (Thread)

Я примерно на эту тему недавно даже книжку заказал в магазине, под названием "Крейзелиана".

Дай пожалуйста ссылку на какой-нибудь обзор. А слово топос
в этой науке произносится ?

(Reply to this) (Parent) (Thread)

> Дай пожалуйста ссылку на какой-нибудь обзор.

---- Миша, на обзор чего? Логики?

> А слово топос в этой науке произносится ?

---- В которой науке??? В логике???

.

.

.

Помню, Миша, у нас с тобой был разговор зимой 1995/1996 года на лестнице в Ломи.
Я тогда, начитавшийся про конструктивную математику, интуиционизм и топосы (гольдблаттову книжку) тебе про это рассказывал страстно.
Ты послушал-послушал, покачал головой и сказал: "Это всё не интересно. Меня интересует только Сложность [вычислений]".

(Reply to this) (Parent) (Thread)

Дальше идут АCA^'_0, АТR_0, Pi_1^2 CA_0 и Z_2.
До АТR_0 бесконечность еще не называют актуальной, потому что нет сильных формул выделения.

обзор и топос в науке про эти системы и особенно бесконечности..

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

(Reply to this) (Parent) (Thread)

Misha, okroj pozhalusta novuju, otdelnuju temu pro eto. Ja chto-nibud' esche umnoe skazhu.

Pro eti sistemy - pochti vse logicheskie knizhki v mire. V Kleene oni vypisany v jazyke p[ervogo porjadka
i nazyvajutsya

RCA_0 --- primitivno rekursivnaja arifmetika

ACA_o --- arifmetika Peano

ACA^'_0 --- arifmetika Peano rasshirennaja mnogochislennymi dobavlenijami principa refleksii (rovno epsilon_{epsilon_0} raz.

(Reply to this) (Parent)

sovsem novuju temu (novyj post).

(Reply to this) (Parent) (Thread)

mozhno. no luchshe by ego sdelat' citatoj ili naborom citat
(wse eti spory uzhe sporeny-peresporeny..) any ideas ?

(Reply to this) (Parent) (Thread)

ne znaju dazhe chto i posovetovat'... Ty v kakoj sejchas strane (kotoraja biblioteka pod rukoj)?

Ja dumal chto raz u tebja PhD po logike, to ty vsyo eto ne xuzhe menja znaesh'?

Mozhno simpsonovu knizhku pochitat' konechno, no tam ne vsyo.

(Reply to this) (Parent)

> --- Спор за последние два-три поколения изменился и трансформировался.
> Его костяк может и похож на старый, но сейчас новое понимание.

Что "спор трансформировался", это понятно. Вопрос в том, шагом куда является эта трансформация: вперёд или в сторону. Когда, допустим, происходил переход от интуиционизма к метаинтуиционизму, то это, конечно, было "трансформацией" спора. Вот только Гейтинг, вместо того, чтобы этому радоваться, начал жалеть, что вообще написал свою работу 1930-го года: с его точки зрения метаинтуиционизм был извращением, а не прогрессом (помните слова Инта, что «логика — не та почва, на которой мы стоим», что «формализовать можно только завершённую часть теории, но не развивающуюся»?).

> Неужели с 1960х годов мы не стали понимать больше? Стали и очень много!
> Несколько революций в математической логике с 1960х годов совершенно всё изменили.

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

> --- Нет в наше время одной "теоретико-множественной" парадигмы, да и нескольких нет.
> Всё сложнее. Z_2 - это теория множеств или нет? Или АТR_0 или АCА_0?

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

> Да и конструктивизмов разных дюжина. Который чьему сердцу ближе?

Дюжина не конструктивизмов; дюжина направлений, называющих себя конструктивными. Из них некоторые конструктивизмами не являются вообще (ну, какой конструктивист из того же Бишопа, у которого «нет позиции»? или из Мартин-Лёфа с его расплывчатыми ординалами?), а некоторые представляют собой механическое ковыряние в примитивно-рекурсивной арифметике (тот же Гудстейн). Чтобы где-либо формулировалась материалистическая конструктивная установка, принципиально отличная от марковской, мне неизвестно.

> --- В логике творятся чудеса, по всему спектру филосовских фонов. Поинтересуйтесь! Очень интересно!

Дайте ссылки, поинтересуюсь. Если там действительно не будет идеальных тоже-"объектов".

> --- Я имел в виду классическую логику.

Если ограничиться нормальными формулами (или механически навешивать на всё два отрицания, что то же самое), то классическая и будет.

> Кстати, про конструктивную арифметику: как насчет семантики Шанина?

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

> --- В этом смысле и для формул первого порядка нет фиксированной семантики

С моей точки зрения, нефиксированной является всё же не сама семантика, а ответы на вопросы о верности той или иной конкретной формулы в рамках этой семантики. Хотя что это интересно, не спорю.

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

> С моей точки зрения, нефиксированной является всё же не сама семантика, а ответы на вопросы о верности

> той или иной конкретной формулы в рамках этой семантики. Хотя что это интересно, не спорю.

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

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

(Reply to this) (Parent) (Thread)

> Разные "семантики" возникают на разных ветках (добавлять и добавлять непротиворечивые утверждения)

Разве что именно "семантики". Меня как-то больше интересует семантика без кавычек (с вопросом о непротиворечивых расширениях исчислений не связанная).

> Есть основания математики, где математики "ищут правду",

Угу. ИМХО, именно это и называется наукой.

> некоторые - где "ищут красоту",

ИМХО, это называется искусством.

> некоторые - стремятся примирить постгёделево Понимание
> с господствующими среди математиков предрассудками.

ИМХО, это называется профанацией.

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

ИМХО, это называется безграмотностью.

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

> И многие из них непротиворечивы.

«Неверная теория, не натолкнувшаяся на противоречие, столь же не становится от этого верной, как преступление, не наказанное правосудием, не превращается от этого в добродетель» (Брауэр). «Вопрос о непротиворечивости для конструктивиста не стоит» (Марков). А я что — я согласен :-)

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

ja imel v vidu neprotivorechivost' v vysshem smysle: razumnost' i obosnovannost'.

Sovremennyj pljuralizm baziruetsya ne na nevezhestve, a na tom, chto est' neskol'ko tipov mozga, neskol'ko tipov rassuzhdenij, neskol'ko tipov ponimanija, chto takoe matematika.

Esche igraet rol' nedavnjaja nauchnaja revoljutsija v evrope: um evropejtsa podelen mezhdu temnymi vekami (s traditsiej pochitanija avtoriteta, ne znaju dazhe nazyvat' li etix ljudej sxolastami) i Prosvescheniem.

Bez kavychek ne ponimaju: kakie arifmeticheskie utverzhdenija schitat' za pravdu bez kavychek? Mnogo let starajus': poka ne ponjal.

(Reply to this) (Parent) (Thread)

> Sovremennyj pljuralizm baziruetsya ne na nevezhestve,
> a na tom, chto est' neskol'ko tipov mozga,
> neskol'ko tipov rassuzhdenij,
> neskol'ko tipov ponimanija, chto takoe matematika.

2+2=4. Последовательность частичных сумм ряда \(\sum_{n=0}^{\infty} 1/n!\) фундаментальна (с эффективным регулятором). Я не знаю, какой нужно иметь тип мозга, чтобы сделать эти факты неверными (по крайней мере, в рамках доступной нам сегодня практики). Сколько не пытался запускать программу, последовательно вычисляющую вышеуказанные частичные суммы и выдающую результаты на печать — у меня никогда до 3 не доходило. Хотя, может, у буддийских бхикшу действительно всё иначе.

> Esche igraet rol' nedavnjaja nauchnaja revoljutsija v evrope:
> um evropejtsa podelen mezhdu temnymi vekami (s traditsiej
> pochitanija avtoriteta, ne znaju dazhe nazyvat' li etix ljudej
> sxolastami) i Prosvescheniem.

А у европейских ЭВМ тоже процессоры поделены таким же образом? И в одно время 7*8 у них =56, а в другое =89? Действительно, очень интересно. Я не знал.

> Bez kavychek ne ponimaju: kakie arifmeticheskie utverzhdenija schitat' za pravdu bez kavychek?
> Mnogo let starajus': poka ne ponjal

2+2=4. Собственно, вообще любое полуразрешимое утверждение допускает чисто механическую верификацию, не зависящую ни от чьего склада ума. Да, разумеется, верификация эта релятивизирована современным уровнем практики; да, ЭВМ в процессе её проведения могла дать сбой (даже перманентно повторяющийся) — однако на большее мы ни в какой науке не можем претендовать (сбой может дать и синхрофазотрон, и атомная бомба). Так что скептицизм в отношении "правды без кавычек", имхо, если и допустим, то разве применительно к более навороченным языкам, чем полуразрешимый. Но даже там вопрос будет стоять не об общих принципах понимания замкнутых формул, а о том, правильно или нет мы прилагаем эти принципы к той или иной конкретной формуле.

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

ja imel v vidy formuly s kvantorami.

(Reply to this) (Parent) (Thread)

Кванторами общности, то бишь (т.к. одни существования полуразрешимости не умаляют)? Ну, тамошнюю ситуацию я тоже охарактеризовал: принцип действия у нас чёткий — \(\forall xA\) означает, что при любом выборе натурального числа \(n\) результат подстановки \([A]^x_n\) будет верной формулой — проблемы могут быть только с применением этого правила к конкретным случаям.

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

ne ponimaju, v kakom smysle "pri ljubom vybore naturalnogo chisla"?
tak mozhno tseluju vechnost' prozhdat' (poka naturalnye chisla ne konchatsya)!!!!!

Ja tolko pro Delta_0-formuly ponimaju, a pro vse ostalnye ne ochen'.

Ja podozrevaju, chto ja konstruktivist. :)))

(Reply to this) (Parent) (Thread)

> tak mozhno tseluju vechnost' prozhdat' (poka naturalnye chisla ne konchatsya)!!!!!

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

В физике у всех общих законов ровно такая же судьба.

> Ja podozrevaju, chto ja konstruktivist. :)))

Вы, похоже, клятый финитарист, то бишь еретик и отступник :-))

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

v obschem ja soglasen, tak i est'... no uzh ochen' mnogo nejasnostej...

Da, i finitist tozhe. (Finitizm u menja po vtornikam.)

(Reply to this) (Parent)

i kak naschet neskolkix kvantorov?

(Reply to this) (Parent) (Thread)

Индукция по логической длине рулит :)

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

net, ne poluchaetsya po induktsii. kvantory cheredujutsya.

Kak ponjat' pravda ili net Pi-2 formula (forall x)(exists y) phi(x,y)
esli uzhe pri x=1 slishkom dolgo zhdat' i ne dozhdat'sja?

(Reply to this) (Parent) (Thread)

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

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

С уважением,
Гастрит

(Reply to this) (Parent)

da i s kvantorom suschestvobanija tozhe problemy. Esli realizujuschee naturalnoe chislo uzhe najdeno - to ponjatno, a esli net - to chto? naprimer neg(Con(NF))?

Polovina logikov ischet primer, drugaja polovina - naoborot, probuet dokazat' ZF |- Con(NF) ili chto esche kto-nibud' |-Con(NF).

(Reply to this) (Parent) (Thread)

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

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

ja interesujus' arifmeticheskimi utverzhdenijami A takimi chto i A i ne A simmetrichny:
intuitivno ravnopriemlimy, ravnointeresny, nu i,konechno, neoproverzhimy ni v odnoj iz izvestnyx teorij.

Neuzheli Vy budete utverzhdat', chto odno iz nix-taki pravda?

(Reply to this) (Parent) (Thread)

Я утверждаю только то, для чего имею основания. Утверждение, что "одно из них таки правда", записывается формулой \(A\lor(\neg A)\). В рамках КПМС эта формула может считаться верной только в том случае, если верная какая-то из \(A\) и \(\neg A\). Пока вопрос не решён (что Вами и предполагается), приходится помалкивать в тряпочку.

Главное здесь состоит не в том, что "одна из формул таки верна", а в том, что у каждой из них есть смысл, что вопрос о верности формулы является содержательным (а не чисто формальным).

С уважением,
Гастрит

(Reply to this) (Parent) (Thread)

mojo "OR" - eto meta-ili.

mojo "OR" - ne vnutri formuly!

(Reply to this) (Parent) (Thread)

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

С уважением,
Гастрит

(Reply to this) (Parent)

Вдогонку: в конструктивной математике (в отличие от "конструктивной" в кавычках) мета-этаж вообще не выделяется. В этом просто нет смысла:

1) Математические суждения в рамках конструктивной установки столь же содержательны, сколь и метаматематические;

2) Метаматематические суждения представляют собой, по сути, математические высказывания, причём даже не очень высокой "степени сложности".

С уважением,
Гастрит

(Reply to this) (Parent)