Alexandr писал(а):
Вот
здесь есть примеры теорем теории (конечных) графов (Propositions A, B, C, D), недоказуемых в ZFC, но доказуемых в некоторых её расширениях, касающихся существования больших кардиналов.
Завтра по ссылке схожу, сегодня лень.
Но результат не удивителен. Конечные графы кодируют натуральные числа и операции на них, равно как и наоборот. Другой пример --- слова конечного алфавита

Так что всё сводится к теореме Гёделя.
И, навереяка, всё зависит от того, какова сложность кванторной приставки у упомянутых утверждений. Если они

, то их наверняка можно доказать (если они верны), если сложность

--- наверняка можно опровергнуть в случае их ложности. Если же есть перемены кванторов, то с ходу ничего сказать нельзя. (У ВТФ, кстати, сложность

, но её, к счастью, доказали. А какова, кстати, сложность утверждения

,

или меньше?)
P. S. Хотя примеры конкретных истинных утверждений, недоказуемых в

, всегда радуют. Особенно если они имеют "естественную" формулировку, а не являются результатом диагональной конструкции, предназначенной для построения именно этого контрпримера. Тут, насколько я понимаю, есть над чем глубоко и серьёзно поработать.
P. P. S. Подскажите какие-нибудь "естественные" примеры элементарных подмоделей (на примере известных структур, а не те, которые получаются через теорему Левенгейма-Сколема или ультрапроизведение). Недавно семинар был по матлогике на эту тему. Я с ходу сообразил лишь насчёт

и

. Кто-нибудь знает ещё?