Логика и методология математики.

[dmitgu]

Не за что! Клевая книга (на мой вкус)

Феликс Шмидель в сообщении #955524 писал(а):

dmitgu в сообщении #955437

писал(а):
. И тогда в случае $\neg Bew(a) \to \neg A$ по правилу вывода MP будет $\neg A$, а это может быть и противоречивое утверждение для данной новой теории.
Мы рассматриваем конкретное утверждение $A$ ("ВТФ - ложна"). Каким образом из $\neg A$ следует в новой теории противоречие?

Я с трудом привыкаю к непривычной терминологии, поэтому боюсь, что пока не все понял. Отреагировал только на импликацию. Про $\neg A$ отвечать не буду, потому что я как раз возражал против импликации, контрапозиции и $\neg A$ :)

Но я так понимаю, что спор про теорию множеств и возможность выводить из неё? Можно, но ведь не обязательно только из нее. Хотя кардинальные числа использовались для доказательства непротиворечивости арифметики Пеано (лень сейчас в книгу заглядывать чтоб уточнять). Проблема ведь не устраняется теорией множеств как не устраняется она и логикой 2ого порядка - в которой можно сформулировать всю арифметику в 2 строки! Все равно получается система которая не эффективно аксиоматизируема. И с этим все равно ничего не поделать - все равно приходится опираться на реальность, наименее сомнительные вещи и в любом случае не иметь гарантий от противоречий. Поэтому если уж говорить про числа и теоремы про них - то чем теория арифметики 2ого порядка хуже теории множеств? И там каждое замкнутое утверждение 1го порядка про числа или истинно или ложно - она полная. А самое лучшее - не упираться в какой-то один метод, а быть открытым миру - в котором есть многое, что куда умнее отдельного чела.

[dmitgu]

Кстати,

Феликс Шмидель в сообщении #955524 писал(а):

dmitgu в сообщении #955437

писал(а):
. И тогда в случае $\neg Bew(a) \to \neg A$ по правилу вывода MP будет $\neg A$, а это может быть и противоречивое утверждение для данной новой теории.
Мы рассматриваем конкретное утверждение $A$ ("ВТФ - ложна"). Каким образом из $\neg A$ следует в новой теории противоречие?

я-то решил, что речь идет не про конкретное утверждение, а про общее свойство предиката доказуемости:

Феликс Шмидель в сообщении #954151 писал(а):

Xaositect в сообщении #953969

писал(а):
$A\to Bew(a)$ будет теоремой тогда и только тогда, когда $A$ доказуема или опровержима в PA, если я не ошибаюсь.

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

Поэтому и дал ту ссылку. Сейчас сообразил, что как свойство предиката доказуемости эта импликация невозможно по более очевидной причине:

По лемме диагонализации имеем $G$ такое что $G \Leftrightarrow \neg Bew(g)$, откуда и из $G \to Bew(g)$ получим $\neg Bew(g) \to Bew(g)$. А последнее эквивалентно $Bew(g)$. Но последнея формула - это отрицание утверждения Гёделя из 1ой теоремы. А теория не полна на это утверждение - то есть не доказано ни оно, ни отрицание. Раз у нас это доказано, значит ошибка в предположении об истинности импликации $A\to Bew(a)$ - при произвольных формулах $A$, разумеется.

[Феликс Шмидель]

Вопрос о том, является ли утверждение $A \rightarrow Prov(#A)$ теоремой арифметики Пеано (первого порядка) для утверждений вида $A = \exists x_1, ..., x_k: P(x_1, ..., x_k)=0$ пока не получил убедительного ответа.
Уважаемый Xaositect считает, что является, но мы пока продолжаем в этом сомневаться.
Но независимо от ответа на этот вопрос, истинность утверждения $A \rightarrow Prov(#A)$ не вызывает у нас сомнений. В самом деле, имея целые положительные числа $x_1, ..., x_k$, удовлетворяющие уравнению $P(x_1, ..., x_k)=0$, можно построить доказательство утверждения $A$.
Сомнения уважаемого epros в истинности утверждения $A \rightarrow Prov(#A)$ не принимаются.
Замечание уважаемого epros о том, что аксиомы могут быть неочевидными принимается.
Мы затронули этот вопрос уже в начале темы, и подробно обсудили его в последней версии начала введения.
Мнение уважаемого epros о том, что польза от теории множеств нулевая не принимается.
В настоящее время теория множеств занимает в основаниях математики важное место.
С другой стороны, мнение уважаемого epros о важности логики второго порядка принимается.
Эта логика достаточно важна, чтобы обсудить её и сделать вывод о её месте в основаниях математики.
Этот вопрос мне пока не ясен, поэтому продолжим его обсуждать.
Я не считаю преимуществом логики второго порядка замечание уважаемого epros о том, что она знает ответ на вопрос об истинности континуум-гипотезы.
В последней версии начала введения отмечено, что этот вопрос не имеет смысла: континуум-гипотезу можно считать истинной, а можно считать ложной.
Хотелось бы услышать критику или обсуждение этой позиции.
Уважаемый dmitgu высказал мнение, что арифметика второго порядка не хуже теории множеств.
Я с этим не согласен, поскольку считаю теорию множеств более сильной теорией.
Но я едва знаком с логикой второго порядка и могу ошибаться.
Поэтому хотелось бы это обсудить.

[dmitgu]

Феликс Шмидель в сообщении #955778 писал(а):

Вопрос о том, является ли утверждение $A \rightarrow Prov(#A)$ теоремой арифметики Пеано (первого порядка) для утверждений вида $A = \exists x_1, ..., x_k: P(x_1, ..., x_k)=0$ пока не получил убедительного ответа.

Гм... Вообще можно выдумать бесконечное число вопросов, только нет никакой необходимости их решать. А $P(x_1, ..., x_k)=0$ - это полином? Лень возится (не вижу оснований - но можетя что-то пропустил), но если это диофантово уравнение, то скорее всего импликация ошибочна, потому что корни дают перечислимые множества, это настолько тесно связано с алгоритмами, что похоже там можно выстроить эквивалентность, в том числе и с диагонализацией и аналогом утверждения Гёделя. Это настолько богатые варианты, что вопрос с корнями не является в общем случае разрешимым (десятая проблема Гильберта, решенная).

Феликс Шмидель в сообщении #955778 писал(а):

Но независимо от ответа на этот вопрос, истинность утверждения $A \rightarrow Prov(#A)$ не вызывает у нас сомнений

Но это же не вопрос веры ) В общем случае это неверно, как я дал вывод. А про частный случай Вы пока ничего не доказали. Если же про частный случай не доказано, то разумно исходить из того, что там тоже проблемы общего случая.

[Феликс Шмидель]

dmitgu в сообщении #955797 писал(а):

Но это же не вопрос веры ) В общем случае это неверно, как я дал вывод. А про частный случай Вы пока ничего не доказали. Если же про частный случай не доказано, то разумно исходить из того, что там тоже проблемы общего случая.

Речь не об общем случае, поэтому не будем об этом говорить.
Получается, что Вы, как и уважаемый epros, сомневаетесь в истинности совершенно очевидного утверждения $A \rightarrow Prov(#A)$ (где $A$ утверждение вида: $A = \exists x_1, ..., x_k: P(x_1, ..., x_k)=0$ о существовании решений диофантового уравнения $P(x_1, ..., x_k)=0$).
И это после того, как я объяснил: имея целые положительные числа $x_1, ..., x_k$, удовлетворяющие уравнению $P(x_1, ..., x_k)=0$, можно построить доказательство утверждения $A$.
Это не вопрос веры настолько, насколько аксиомы Пеано не вопрос веры.

[dmitgu]

Если это все так просто, то дайте доказательство. И импликация совершенно не очевидна, потому что ведь не к одному утверждению Гёделя дело сводится - там и всё более сложное в импликацию не уложится. А диофантовы уравнения по своей сложности - тут едва ли уступают и не все они имеют корни (где корни есть там есть и импликация, просто в силу истинности $Prov(A)$ для этого $A$). Вот почему это не только не очевидно - для меня - но напротив, скорее я ожидаю прямо противоположного.

З.Ы. Фишка в том, что если бы про диофантово уравнение всегда можно было решить вопрос - есть корни или нет - то импликация была бы. Тогда в Пеано или более сложной теории было бы доказуемо либо $Prov(A)$, либо $\neg A$. Но в силу неразрешимости (десятая проблема Гильберта) - ни в какой теории нет решения для любых диофантовых уравнений. А это значит, что какие-то из них по сложности не уступают утверждению Гёделя. А такие конструкции импликации не "по зубам". Это не доказательство, а просто пояснение своей интуиции. И почему для меня не очевидно (а наоборот) то, что очевидно Вам.

[Феликс Шмидель]

А то, что утверждение $A \rightarrow Prov(#A)$ истинно в стандартной модели арифметики, и что это можно доказать в теории множеств $ZFC$ Вас не убеждает?

[dmitgu]

Феликс Шмидель в сообщении #955840 писал(а):

А то, что утверждение $A \rightarrow Prov(#A)$ истинно в стандартной модели арифметики, и что это можно доказать в теории множеств $ZFC$ Вас не убеждает?

Это ж другая теория. А теории первого порядка можно расширять и в сторону абсурда про некоторые диофантовы уравнения (раз их совокупность неразрешима, то такие всегда найдутся). И это будет непротиворечиво.

ЗЫ. В стандартной интерпретации (в полной арифметике) это вообще нельзя сформулировать ) Там нет эффективной аксиоматизируемости, а она нужна в $Prov$. Хотя про теории первого порядка которые подчиняются некоторым условиям второго порядка - можно. Но это со стороны. И способа проверить, подчиняется ли действительно теория требованиям арифметики - нет в общем случае.

[Феликс Шмидель]

Хорошо, я буду Вас убеждать. Начнём с того, что отрицание обсуждаемой импликации не является теоремой арифметики. Это понятно?

[dmitgu]

Феликс Шмидель в сообщении #955846 писал(а):

Хорошо, я буду Вас убеждать. Начнём с того, что отрицание обсуждаемой импликации не является теоремой арифметики. Это понятно?

Можно сразу огласить весь список? ) Я сразу не уверен, потому что речь идет о замыкании импликации со значком $\forall A$?

[Феликс Шмидель]

О замыкании импликации речи не идёт. Речь идёт о конкретном утверждении $A$.
Если бы утверждение "не ($A \rightarrow Prov(#A)$)" было теоремой арифметики, то такими были бы и утверждения $A$ и "не $Prov(#A)$", что невозможно. Согласны?

То, что

Цитата:

В стандартной интерпретации (в полной арифметике) это вообще нельзя сформулировать )

Вы ошибаетесь.
Утверждение $A \rightarrow Prov(#A)$ это обычное вполне конкретное арифметическое утверждение.

[dmitgu]

Феликс Шмидель в сообщении #955850 писал(а):

утверждения $A$ и "не $Prov(#A)$", что невозможно. Согласны?

$A \wedge \neg Prov(#A)$ не доказывается? Да, пожалуй.

Феликс Шмидель в сообщении #955850 писал(а):

Цитата:

В стандартной интерпретации (в полной арифметике) это вообще нельзя сформулировать )
Вы ошибаетесь.
Утверждение $A \rightarrow Prov(#A)$ это обычное вполне конкретное арифметическое утверждение.

Я не ошибаюсь. Полная арифметика - это арифметика второго порядка, а Prov - это формула, содержащая проверки выводов на базе опоры на аксиомы первого порядка. Так вот нет способ опиратся на аксиомы второго порядка и получать из них истины первого порядка, вообще говоря. Я настолько не ошибаюсь, что на этом основано доказательство того, что полная арифметика не является эффективно аксиоматизируемой. Именно поэтому для нее и невозможна та же теорема Гёделя.

[Феликс Шмидель]

Арифметика второго порядка ни при чём. Я говорил о доказательстве в теории множеств первого порядка $ZFC$, что в стандартной модели арифметики утверждение $A \rightarrow Prov(#A)$ истинно.
Извиняюсь, что на обратил внимание на то, что цитирую.

[dmitgu]

Феликс Шмидель в сообщении #955857 писал(а):

что в стандартной модели арифметики утверждение $A \rightarrow Prov(#A)$ истинно.

В общем случае нет - и я это показал (доказал). А в частном случае - про диофантовы уравнения - тоже скорее всего нет. Но тут доказательства пока нет.

Я не понял про цитирование. Я чего-то не заметил наверно )

[Феликс Шмидель]

Если утверждение $A$ истинно в стандартной модели арифметики, то оно истинно в любой модели арифметики.
Следовательно, если утверждение $A$ истинно в стандартной модели арифметики, то оно доказуемо в арифметике Пеано (первого порядка).
Следовательно, если утверждение $A$ истинно в стандартной модели арифметики, то импликация $A \rightarrow Prov(#A)$ является теоремой арифметики Пеано.
Следовательно, если утверждение $A$ истинно в стандартной модели арифметики, то импликация $A \rightarrow Prov(#A)$ истинна в любой, в том числе и стандартной модели арифметики.
Если же утверждение $A$ ложно в стандартной модели арифметики, то импликация $A \rightarrow Prov(#A)$ истинна в стандартной модели арифметики.
Согласны?