[FOM] A proof that cannot be formalized in ZFC- stupid discussion by members of [fom]

Модератор: mike@in-russia

Ответить
Аватара пользователя
Кисантий
Сообщения: 7426
Зарегистрирован: Ср ноя 04, 2009 18:57

[FOM] A proof that cannot be formalized in ZFC- stupid discussion by members of [fom]

Номер сообщения:#1   Кисантий »

[FOM] A proof that cannot be formalized in ZFC stupid discussion by members of [fom]
https://cs.nyu.edu/pipermail/fom/2007-O ... 12009.html
Один неуч задал другим неучам вопрос :?:
I am a mathematician with a layman's interest in logic and
foundations. I would be grateful if someone who knows more than I do
would tell me whether the following remarks make sense -- or have I
perhaps rediscovered a well-known fallacy?

Let con(ZFC) be a sentence in ZFC asserting that ZFC has a model.
Let S be the theory ZFC+con(ZFC). Let con(S) be a sentence in S (or
ZFC) asserting that S has a model. We assume throughout that ZFC is
consistent.

Claim 1. S=ZFC+con(ZFC). is consistent.

Proof. Assume S is inconsistent, that is, has no model. This means
that there is no model of ZFC in which con(ZFC) is true, so the
negation of con(ZFC) has a proof in ZFC. By translating this proof
from the formal language of ZFC into English (that is, by applying
the standard interpretation), we get a proof -- a mathematical proof
in the everyday sense -- that ZFC has no model, contrary to the
assumption that ZFC is consistent.

Claim 2. There is no proof in ZFC that con(ZFC) implies con(S).

Proof. By Claim 1 and Godel's Second Incompleteness Theorem applied
to S, con(S) is unprovable in S.

Thus we seem to have a down-to-earth mathematical statement ("If ZFC
is consistent, so is S") with a proof that, provably, cannot be
formalized in ZFC. This appears to contradict the common belief that
all mathematics can be formalized in ZFC. Is my argument correct?
If so, it must be well known -- are there other such examples? If
not, where is the mistake?

Thanks and best regards,
Finnur Larusson
1.Идиот Larusson очевидно не понимает что непротиворечивость ZFC в смысле теории доказательств (обозначим это как CON[ZFC]) всегда предполагается, иначе там просто делать будет нечего :)
2. В силу теоремы Геделя о полноте справедлива эквивалентность CON[ZFC]<-->con(ZFC) :!:
Коэн П.Дж. Теория множеств и континуум-гипотеза. параграф 4.
http://en.bookfi.net/book/440950
таким образом Larusson не может предположить что S is inconsistent поскольку в силу теоремы Геделя о полноте это предположение тривиальным образом эквивалентно отрицанию стандартной гипотезы CON[ZFC] :?
Последний раз редактировалось Кисантий Сб авг 01, 2020 11:30, всего редактировалось 8 раз.
Кот это очень древнее и неприкосновенное животное. Кот спас жизнь хозяину, позвонив в 911

Аватара пользователя
Кисантий
Сообщения: 7426
Зарегистрирован: Ср ноя 04, 2009 18:57

Re: [FOM] A proof that cannot be formalized in ZFC

Номер сообщения:#2   Кисантий »

Кот это очень древнее и неприкосновенное животное. Кот спас жизнь хозяину, позвонив в 911

Ответить

Вернуться в «Математическая физика, методы вычислений / Mathematical Physics, Computing Technique»