Dmitry67 wrote:Ну так что вы думаете когда читаете что
exists такое множество X что blah blah blah (*)
Что такое множество СУЩЕСТВУЕТ или что Выводима строка (*) ?
PS
Никто не знает нет ли прогресса в токазательстве непротиворечивости теории множеств ?
Если теории, более мощные чем теория множеств, то есть относящиеся к теории множеств как последняя относится к PA ?
Я думаю, что говоряшему известны модели формальной системы, которую он использует, в которых такое множество есть. Если же говоряший приводит доказательство, то я в добавок убеждаюсь, что формула выводима.
Я никогда не буду спрашивать говоряшего, о какой конкретно модели идет речь. Ето не важно.
Но есть более интересный случай. Вы знаете об одной модели, а я о другой. В каждой из них некое утверждение истинно. Однако, с точки зрения Вашей модели ето утверждение
в моей модели ложно.
К примеру, я оперирую щетной моделью ZF, и говорю Вам (у которого стандартная модель): "континуумы есть". Вы говорите: "согласен, но хочу увидеть пример". Я вам показываю континуум, а Вы говорите "никакой ето не континуум".
Теперь представьте, что Вы используете стандартную модель PA, а я - нестандартное расширение: модель PA + ~Con(PA). Вы: "2*2=4", я :"да", вы: "Великая Теорема Ферма", я:"да". И тут я чисто для поддержания разговора заявляю: "~Con(PA)". Так же и подраться можно

И как при таком раскладе с инопланетянами контакт устанавливать?

По поводу прогресса, недавно чуть не доказали
противоречивость ZF
Попозже найду ссылку. Ошибку вроде уже нашли, но она была нетривиальной.
VC wrote:The second GT is sort of about impossibility of the proof.
Just "sort of". It actually says that if we do prove that (e.g. by presenting a model), that would mean ZF is inconsistent.
Btw, by "category theory" do you mean the so called "abstract nonsense" ("meta-algebra")? I never heard it was considered a Foundations thing.