Мы ни в чём не уверены?

[EminentVictorians]

Anton_Peplov в сообщении #1684350 писал(а):

Не понимаю этого "значит".

Лямбда исчисление - это буквально основа основ теории языков программирования. Спроектировать современный язык программирования не зная лямбда исчисление (и все остальные известные модели вычислений) - невозможно.

[Anton_Peplov]

EminentVictorians в сообщении #1684366 писал(а):

Лямбда исчисление - это буквально основа основ теории языков программирования. Спроектировать современный язык программирования не зная лямбда исчисление (и все остальные известные модели вычислений) - невозможно.

Язык программирования низкого, среднего или высокого уровня? Невозможно в том же смысле, в каком невозможно понять математику без теории категорий, или в другом?

[EminentVictorians]

Anton_Peplov в сообщении #1684368 писал(а):

Язык программирования низкого, среднего или высокого уровня?

Любые. Это может звучать категорично, но насколько я понимаю, это буквально так и есть.

Anton_Peplov в сообщении #1684368 писал(а):

Невозможно в том же смысле, в каком невозможно понять математику без теории категорий, или в другом?

Я про проектирование. Понять многие языки наверное можно и без всякого лямбда исчисления. Спроектировать (чтобы это удовлетворяло современным стандартам) - нет.

[kolyanchick]

mihaild в сообщении #1684342 писал(а):

Очевидно, что ZF непротиворечива.

Наивная теория множеств тоже сначала может показаться очевидно непротиворечивой, но это ведь не так.

[Red_Herring]

kolyanchick в сообщении #1684377 писал(а):

Наивная теория множеств тоже сначала может показаться очевидно непротиворечивой, но это ведь не так.

А вы в этом уверены?

ПС. По правилам форума вы обязаны ответить на этот вопрос. :

[Ende]

Red_Herring в сообщении #1684379 писал(а):

ПС. По правилам форума вы обязаны ответить на этот вопрос. :

Red_Herring, не пугайте новичка. Это правило существует, чтобы помешать авторам странных идей уходить от неудобных вопросов. Топикстартер пока не высказывает ничего криминального.

[kolyanchick]

Red_Herring в сообщении #1684379 писал(а):

kolyanchick в сообщении #1684377 писал(а):

Наивная теория множеств тоже сначала может показаться очевидно непротиворечивой, но это ведь не так.

А вы в этом уверены?

В том, что наивная теория множеств может показаться очевидной я уверен, потому что она мне самому сначала показалась очевидной. В её противоречивости я уверен, потому что парадокс Рассела показвает противоречивость наивной теории множеств.

[Red_Herring]

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

Разумеется, ничего ТС криминального не высказал, он просто дурью мается, что, прямо вредит его сну, пищеварению и вообще здоровью.

[EminentVictorians]

kolyanchick, Вас еще вот какое соображение может успокоить.

Многие математические утверждения верны не потому что мы там как-то это в ZFC доказали, а просто потому что иначе быть не может. Например, целые числа коммутативны даже не столько потому что мы там в ZFC сконструировали какую-то хитрую модель на упорядоченных парах и как-то из акисом ZFC вывели их коммутативность. Скорее тут обратная логика: не быть коммутативности не могло, потому что сама наша цель была расширить $\mathbb N$ без потери алгебраических свойств. Более того, моделировать те же целые числа не обязательно именно в теории множеств. Их можно моделировать буквально как записи вида $\pm n$, где n - натуральное число.

Соответственно, многие доказательства опираются непосредственно на такие истины, которые по сути являются аксиомами (хотя формально, почти все такие "аксиомы" могут быть доказаны из "настоящих" zfc-шных аксиом как теоремы). Поэтому, даже если ZFC противоречива, на такие доказательства это никак не скажется.

[mihaild]

EminentVictorians в сообщении #1684392 писал(а):

Скорее тут обратная логика: не быть коммутативности не могло, потому что сама наша цель была расширить $\mathbb N$ без потери алгебраических свойств.

Нам нужна какая-то теория, чтобы доказать, что так расширить вообще можно. А то давайте расширим $\mathbb N \setminus \{0\}$ до коммутативного кольца, являющегося группой одновременно по сложению и по умножению.

[EminentVictorians]

mihaild в сообщении #1684395 писал(а):

Нам нужна какая-то теория, чтобы доказать, что так расширить вообще можно.

Почему теория? По-моему, просто модель. В данном случае состоящая буквально из записей вида $\pm n$.

Я согласен, что без модели может оказаться так, что наши требования противоречивы.

[mihaild]

EminentVictorians в сообщении #1684396 писал(а):

По-моему, просто модель.

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

[EminentVictorians]

mihaild в сообщении #1684398 писал(а):

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

Я в этой теме неявно предполагаю, что все происходит в рамках неформальной метатеории под названием "обычная математическая практика". Ну то есть, пусть я хочу смоделировать, например, натуральные числа. Я беру и моделирую их просто как их записи в десятичной системе: 1 2 3 4 5 6 7 8 9 10 11 12 13 ... Нету никаких формальных теорий, никакой логики первого порядка, предикатных символов и т.д. А модель есть. Пусть и не в формальном смысле.

[dgwuqtj]

kolyanchick в сообщении #1684377 писал(а):

Наивная теория множеств тоже сначала может показаться очевидно непротиворечивой, но это ведь не так.

Если немного углубиться в теорию множеств, то окажется, что изначальную интуицию надо корректировать. Сначала может показаться, что любую коллекцию объектов можно обозвать множеством, но тогда можно придумать странные объекты вида $x = \{x\}$, которые даже непонятно, как проверять на равенство. В рамках ZFC всё устроено довольно разумно: все множества можно построить по порядку, начиная с $\varnothing$, причём элементы множества на $\alpha$-м шаге — это множества, полученные на предыдущих шагах. Разве что $\alpha$ пробегает ординалы, а не только натуральные числа.

[Red_Herring]

EminentVictorians в сообщении #1684399 писал(а):

Я в этой теме неявно предполагаю, что все происходит в рамках неформальной метатеории под названием "обычная математическая практика".

известный анекдот писал(а):

приехал поручик Ржевский с ведром водки, и тут начался такой разврат...