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

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

(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)