В теории моделей все протворечивые теории будут эквивалентны. Но кажется я понял, что ты имеешь в виду.

С точки зрения теории доказательств можно действительно оценить сложность какого-то доказательства. Например в ПА можно считать число индукций. А если, например, индукция используется для доказательства шага индукции, то это будет индукция в квадрате. В итоге у каждого доказуемого утверждения будет своя степень, многочлен в целых числах типа I^2 + 2I.

Тогда для противоречивых теорий можно посчитать степень противоречивости как степень утверждения bot. Модели в теории доказательств вроде не особо расматривается. Но можно попробывать посчитать расстояние от теории до не-модели как минимальную степень утверждения, которое не верно для модели. Потом этих степей можно вычислять численное растояние между теориями и моделями типа как d(T,M) = 2^-(deg(T,M)(2))

(Reply to this) (Parent) (Thread)

Хочется что-то уметь сказать про эту квазимодель, если расстояние мало.
В моем примере утверждения, имеющие обозримые доказательства, истины в достаточно большом и полезном куске квазимодели. (кажется)
Изучается ли что-то такое?

(Reply to this) (Parent) (Thread)

Я прямо такого не встречал.

Вам бы я посоветовал для начала формализовать, что значит "большой и полезный кусок квазимодели", как отличить его от "маленького" или "бесполезного", и что такое "обозримое" и "необозримое" доказательство.

(Reply to this) (Parent) (Thread)

Нет, именно это я это формализовать не хочу, это будет ультрафинитизм, а я не к тому клоню, а думаю про чтото типа этого
https://gowers.wordpress.com/2008/12/28/how-can-one-equivalent-statement-be-stronger-than-another/

(Reply to this) (Parent) (Thread)

Гауэрс еще чтото говорил конкретно о ситуации, когда вывод противоречия очень длинный, но я не могу найти

(Reply to this) (Parent) (Thread)

Ну вот видите, что вы все равно апеллируете к длине доказательств.

Proof Complexity, это вполне себе формальная дисциплина.

Вот, статья например https://arxiv.org/abs/1802.09377

(Reply to this) (Parent) (Thread)

спасибо, попробую подступиться к этой дисциплине.
еще дурацкий вопрос:
как думать про омега-противоречивые теории типа PA+~Con(PA)
тут выполняются условия Гильберта-Бернайса?
эта теория П1-некорректная?

(Reply to this) (Parent) (Thread)

Я не специалисты по этой теме, и точно не знаю. Я видел примеры, что теории типа X= ZF + ~Con(ZF) могут быть относительно непротиворечивы. Тут тонкий вопрос как Сon(Y). Потому что Сon(Y) должен записываться на языке теории множеств или арифметики нужного порядка, а не на мета-языке. Поэтому нельзя просто подставить X само в себя и получить противоречие.

(Reply to this) (Parent) (Thread)

Конечно. Критерий того, что Con выразимо и есть условия Г-Б. Традиционно(*), первая ТГ требует только первые два условия, а вторая - еше третье, потому что не только Con должен выражаться, но и все доказательство первой ТГ.
Это тонкость, которую я понимаю, но обращаться с ней не умею.

(*) Традиционно: заметил, что последнее время роль чисто синтасического док-ва первой ТГ перестали подчеркивать. Рассказывают, что Россер "усилил результат".

(Reply to this) (Parent)