Вообще-то принцип Парриса-Харрингтона доказывается, причём в одну строчку. Voilà:

Доказательство. Принцип Парриса-Харрингтона верен. Следовательно, принцип Парриса-Харрингтона верен.

Чем плохо? Тем, что не в PRA проведено? А кто Вам сказал, что выводы в PRA исчерпывают суть понятия «доказательство»? Или просто дело в том, что под "недоказуемость" гранты дают (т.к. слово звучит для неспециалиста заманчивой музыкой), а вот под "невыводимость в PRA" — уже нет (что-то узкоспециальное и неинтересное)? Где же, господа логики, ваша научная честность, без которой, Как Учил Нас Великий Фейнман, наука вырождается в карго-культ?

Стоп: а может, Вы как раз и есть служители карго-культа от логики? Так Вы ж признайтесь — мне можно, я Вашим грантодателям не расскажу. Честное пионерское :-)

> Не найти их так просто

Доказательство теоремы Гёделя состоит в предъявлении алгорифма, перерабатывающего любое $\Sigma_1$-полное семантически пригодное логическое исчисление в невыводимую вместе с отрицанием замкнутую $\Sigma_1$-формулу. Чего тут искать-то?

> Я ищу утверждения, которые ни истинные ни ложные

Опять "истинное" отождествлено с "выводимым в PRA"? Всё надеетесь, что самолёты с тушёнкой прилетят? :-)

> что-то из книжки Мартин-Лёфа

Да, великая книжка. Я о ней ещё ни одного положительного отзыва не слышал — в том числе от себя :-) Так что у Вас есть шанс стать тут Первым!

> что-то из воспоминаний детства: последовательность Шпеккера, квадрат Оревкова

...ленинградский принцип в качестве самостоятельной вещи (хотя он уж сорок почти лет как теорема)...

> в детской форме

В кои-то веки — честно :-)

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

(Reply to this) (Parent) (Thread)

Не понял "доказательство". PH не является истинным утверждением.

Чем плоха последовательность Шпеккера - тоже не понял.

При чем здесь доказательство теоремы Гёделя? Я же писал, что не в нём дело. А замечание с алгоритмом я исключил, так как исключил синтаксические трюки (оставив лишь интересную содержательную математику).

Денег на мою науку никогда не давали. Я много лет был безработным, до недавнего времени. Не понимаю что за выпады!

Да, ленинградский принцип я не принимаю (недавно меня явным образом выявили): действительно я никогда не говорю про теорию "consistent".
Говорю только "not inconsistent".

Мне этот разговор надоел. Пожалуй, если содержательная часть закончилась, пойду обяснять детям как ZF+ (V=L) влечет существование деревьев Суслина.

Андрей

(Reply to this) (Parent) (Thread)

> Не понял "доказательство". PH не является истинным утверждением.

Но ведь, коль скоро оно независимо от формальной арифметики, его можно добавить к последней в качестве доп.аксиомы (и в полученном новом исчислении оно — являясь аксиомой — будет выводимо даже без всякой апелляции к истинности)?

> Чем плоха последовательность Шпеккера - тоже не понял.

Последовательность Шпеккера замечательна, как и сингулярные покрытия. Это книжка Мартин-Лёфа плоха (бессистемное скакание по верхам).

> интересную содержательную математику

Ну вот ppkk только что спрашивал, что же такого в PH и BRT содержательного (упоминание про "интересное" отклоняется как субъективное). Ответа я не пока не вижу.

> Не понимаю что за выпады!

Эти выпады вызваны тем, что Вы постоянно утверждаете, что PH и BRT нужны для конструктивной математики — но при этом старательно уходите от вопроса, для чего же именно они ей нужны (вместо этого идут попытки элементарного запугивания: "можно отстать"). Я вижу в таком положении вещей нарушение научной честности:

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

Возможно, конечно, что это просто столкновение советского/западного научных стилей: на Западе, НЯМС, бездоказательная самореклама в порядке вещей уже не одно поколение (при грантовой системе иначе затопчут). Меня же она раздражает.

> Мне этот разговор надоел.

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

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

(Reply to this) (Parent) (Thread)

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

(Reply to this) (Parent)

(Mizar упорно не качается.)

http://kgs.logic.at/goedel-fellowship/index.php?winners — деньги дают под "Independence results in concrete mathematics", а не за "недоказуемость". Вы неправы.

Но, боюсь, независимость имеется в виду именно от презренной ЦФ…

(Reply to this) (Parent) (Thread)

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

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

(Reply to this) (Parent) (Thread)

Насколько я знаю, в русскоязычной литературе считается, что Коэн доказал "независимость гипотезы континуума от остальных аксиом аксиоматической теории Цермело-Френкеля". И интересно это 1) методом вынуждения 2) тем, что континуум-гипотеза важная (как проблема Гильберта, например). Разве все остальные доказательства независимости от ЦФ удостаивались Филдсовской медали? Что-то Вы мудрите.

Мне рекламировали как раз "утверждения о натуральных числах" зависящие от аксиом о больших кардиналах (со ссылкой на труд Фридмана; в статье Бовыкина "new" об аксиомах о больших кардиналах пишется только как об аналогии, кажется, хотя есть ссылка Friedman, H. (1998). Finite functions and the necessary use of large cardinals. Annals of Mathematics 148, pp. 803-893). Возможно, сам Андрей независимостью от ЦФ и не занимается.

(Reply to this) (Parent) (Thread)

«Проблема непротиворечивости аксиоматической теории множеств — это своего рода "любимая мозоль" специалистов по данному вопросу. Её пытаются решить, но "добровольно" признаваться в том, что она пока ещё не решена, у них как-то не принято. Нередко даже у самых крупных специалистов можно встретиться с точными утверждениями, в которых она фактически фигурирует в качестве решённой (!) в положительном смысле. Это делается таким образом, что вместо верной импликации читателю в качестве верного преподносится её заключение, что, конечно же, в высшей степени курьёзно для математика». А.А.Марков, Н.М.Нагорный, «Теория алгорифмов», 2-е изд., 1996, стр. XVI.

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

(Reply to this) (Parent)

нет, там в двух местах две разные истории: одна про аналогии, а одна про недоказуемость в ZFC + кардиналы Мало.

(Reply to this) (Parent) (Thread)

Там как-то обзорно написано.

Another series of H. Friedman’s results under the general name of “boolean relation theory” can be found in [38]: if we list all (second-order) statements of a certain simple shape (all of them a priori equally simple and natural) and try to classify them according to their truth, some of them turn out to be unprovable in some theories stronger than ZF, e.g. the following statement from [38] is provably in ACA0 equivalent to 1-consistency of the theory ZFC+{there is an n-Mahlo cardinal}(n∈ω)

А ссылка на "Interpreting set theory in discrete mathematics" — я это тоже счёл чем-то типа аналогии.

(Reply to this) (Parent)