Кванторами общности, то бишь (т.к. одни существования полуразрешимости не умаляют)? Ну, тамошнюю ситуацию я тоже охарактеризовал: принцип действия у нас чёткий — \(\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)