Теории с очень длинным доказательством их противоречия

[cscscs]

Каждое формальное доказательство является некоторым словом и поэтому имеет конкретную длину.
Исследовались ли уже такие противоречивые формальные системы, что длина каждого формального доказательства того, что они противоречивы, превышает какое-то большое натуральное число, допустим, $100!^{100!}$?

[Xaositect]

Мне когда-то попадались старые статьи, в которых рассматривалась арифметика с добавленными к ней аксиомами $F(0)$, $F(x)\to F(x+1)$, $F(c)$ для некоторого $c$ и запретом использовать формулы с $F$ в индукции. Там доказывалось, что короткие доказательства для формул из $F$ можно перевести в доказательства в исходной арифметике.

[patzer2097]

cscscs в сообщении #824475 писал(а):

Исследовались ли уже такие противоречивые формальные системы, что длина каждого формального доказательства того, что они противоречивы, превышает какое-то большое натуральное число, допустим, $100!^{100!}$?

конечно, и продолжают исследоваться! Например, ZFC, - Котофеич же все уже объяснил

[cscscs]

patzer2097 в сообщении #824495 писал(а):

конечно, и продолжают исследоваться! Например, ZFC, - Котофеич же все уже объяснил

Так он же вроде бы смешал теорию с метатеорией. Так что угодно доказать можно.
Кстати, увидел там ссылку на статью http://elementy.ru/lib/164681/164686
Цитата оттуда:

Цитата:

Самое короткое доказательство противоречивости аксиом Пеано может занимать миллиард страниц, и мы никогда его не увидим. А раз мы никогда не столкнемся с противоречием, то какая нам разница, противоречива аксиоматика или нет? Мы можем и дальше доказывать теоремы и вскрывать интересные взаимосвязи между понятиями, даже не подозревая об ужасной истине!

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

-- 09.02.2014, 20:06 --

Xaositect в сообщении #824494 писал(а):

Мне когда-то попадались старые статьи, в которых рассматривалась арифметика с добавленными к ней аксиомами $F(0)$, $F(x)\to F(x+1)$, $F(c)$ для некоторого $c$ и запретом использовать формулы с $F$ в индукции.

Может $\lnot F(c)$?

Xaositect в сообщении #824494 писал(а):

Там доказывалось, что короткие доказательства для формул из $F$ можно перевести в доказательства в исходной арифметике.

Не понял, что значит "для формул из $F$"? Т.е. которые содержат в себе $F$?
Вообще, конечно, интересно. Может подскажите по каким словам хоть гуглить?

[Xaositect]

cscscs в сообщении #824609 писал(а):

Может $\lnot F(c)$?

Да.

cscscs в сообщении #824609 писал(а):

Не понял, что значит "для формул из $F$"? Т.е. которые содержат в себе $F$?

Наоборот, без $F$. Писал в спешке, извините.

Статья Париха http://www.jstor.org/discover/10.2307/2 ... 3417831777 и дальше на нее ссылаются.

[cscscs]

Xaositect в сообщении #824626 писал(а):

Статья Париха http://www.jstor.org/discover/10.2307/2 ... 3417831777 и дальше на нее ссылаются.

Спасибо.