что следует из теоремы Геделя

[epros]

Alexey Romanov в сообщении #224237 писал(а):

Если $A \nvdash p$, это совсем не значит, что это можно доказать в метатеории (опять-таки, в любой фиксированной метатеории первого порядка).

Может можно доказать, а может и нельзя. Но речь идёт о чём? Мы рассуждаем об "истинности вообще"? Если так, то я не понимаю что это такое. Или речь идёт об утверждении (теореме или аксиоме) в рамках некоторой теории (метатеории по отношению к $A$, раз она использует такой синтаксис)?

Alexey Romanov в сообщении #224237 писал(а):

Напомню, что первая теорема Гёделя имеет вид не $A \nvdash G$, а $A \nvdash 0 = 1 \rightarrow A \nvdash G$.

Угу, я в курсе. Но напомню также, что есть такой вариант формулировки, где в метатеории, принимающей аксиому истинности арифметики, выводится непосредственно $A \nvdash G$.

Вывод достаточно простой. Ранее посредством арифметизации предиката доказуемости Гёдель продемонстрировал существование арифметического высказывания $G$, для которого:
$G \leftrightarrow (A \nvdash G)$

Из предположения $A \vdash G$ в силу аксиомы истинности арифметики следует $G$, а отсюда в силу указанной выше равносильности следует $A \nvdash G$. Противоречие. В силу закона $(p \rightarrow \bot) \rightarrow \neg p$ это означает доказанное отрицание предположения, т.е.:
$A \nvdash G$.

Вот Вам пример доказательства недоказуемости без использования теории моделей.

Alexey Romanov в сообщении #224237 писал(а):

Более того, классическим методом доказательства в метатеории $A \nvdash p$ является предъявление модели $A$, в которой ложно $p$. У Вас этого ресурса нет.

И я об этом не очень жалею. Знаете почему? Потому что доказательство с предъявлением модели на самом деле является доказательством в теории множеств, т.е. в теории, содержащей весьма сильную аксиоматику (по крайней мере куда более сильную, чем аксиоматика арифметики). Если я доверяю арифметике, но не доверяю теории множеств, то я могу объявить такое доказательство ложным (сказать, что "на самом деле" $A \vdash p$) и это не приведёт к противоречиям в моей метатеории.

Alexey Romanov в сообщении #224237 писал(а):

epros в сообщении #224232 писал(а):

в какой теории сформулировано утверждение о существовании этого "бесконечного списка утверждений".

В неформальной метатеории.

В неформальной метатеории можно доказать что угодно.
Нет, я не против неформальных рассуждений, но только до тех пор, пока есть уверенность, что в принципе они формализуемы.

Alexey Romanov в сообщении #224237 писал(а):

Мои возражения начались вот с этого:

epros в сообщении #223333 писал(а):

Для доказательства $(\forall n \in \mathbb{N})(A \vdash G(n))$ нужно стандартное исчисление предикатов первого порядка + индукция по натуральным числам.

И на чём в итоге остановились? Я по-прежнему полагаю, что все мои неформальные метатеоретические рассуждения могут быть формализованы с использованием стандартного исчисления предикатов первого порядка + индукции по натуральным числам. Вы нашли что-то ещё?

[Alexey Romanov]

epros в сообщении #224275 писал(а):

Мы рассуждаем об "истинности вообще"? Если так, то я не понимаю что это такое. Или речь идёт об утверждении (теореме или аксиоме) в рамках некоторой теории (метатеории по отношению к $A$, раз она использует такой синтаксис)?

Ну в таком случае Вы никак не должны принимать закон исключённого третьего для утверждений вида $A \vdash p$, потому что мы заведомо знаем, что метатеория не полна.

epros в сообщении #224275 писал(а):

метатеории, принимающей аксиому истинности арифметики

Если арифметика противоречива, то эта метатеория тоже Принять эту метатеорию так же интересно, как добавить к арифметике аксиому "арифметика непротиворечива".

Можете ли Вы доказать невыводимость чего-то в теории, которую Вы не готовы принять за истину?

[epros]

Alexey Romanov в сообщении #224281 писал(а):

Ну в таком случае Вы никак не должны принимать закон исключённого третьего для утверждений вида $A \vdash p$, потому что мы заведомо знаем, что метатеория не полна.

Вообще-то я и не принимаю, нафига он нужен.

Но Вашего утверждения я всё-таки не понял: Почему из неполноты метатеории мы должны заключить, что закон исключённого третьего неприемлем? Он всего лишь часть исчисления. Например, чтобы включить его в арифметику, мы должны заложить схему $A \vdash p \vee \neg p$ для каждого $p$ - высказывания арифметики. В метатеорию он закладывается аналогичным образом (на уровне мета-метатеории). Т.е. если мы в метатеории применяем классическую логику, то $(A \vdash p) \vee (A \nvdash p)$ мы должны считать теоремой метатеории. Хотя толку от этого никакого.

Или Вы имели в виду что-то другое? Например вот это: $(A \vdash p) \vee (A \vdash \neg p)$? Так это вообще какая-то ерунда - верный путь прийти к противоречию в метатеории.

Alexey Romanov в сообщении #224281 писал(а):

epros в сообщении #224275 писал(а):

метатеории, принимающей аксиому истинности арифметики

Если арифметика противоречива, то эта метатеория тоже Принять эту метатеорию так же интересно, как добавить к арифметике аксиому "арифметика непротиворечива".

Пока не знаем, что арифметика противоречива, интересно. Ежели вдруг узнаем, то не будем считать её истинной.

Alexey Romanov в сообщении #224281 писал(а):

Можете ли Вы доказать невыводимость чего-то в теории, которую Вы не готовы принять за истину?

Ну, не знаю. Мало ли какие могут быть теории. Может быть это можно будет "в лоб" доказать.

Вообще-то, насколько я понимаю, невыводимость чего-нибудь в теории означает её непротиворечивость. В связи с этим хочу заметить, что теория множеств содержит арифметику, так что она автоматически принимает её за истину. Поэтому вряд ли выводы теории моделей о невыводимости чего-либо в арифметике можно считать более ценными, чем выводы метатеории, непосредственно принимающей истинность арифметики за аксиому. Как и ценность её выводов о непротиворечивости арифметики.

[Alexey Romanov]

epros в сообщении #224341 писал(а):

Вообще-то я и не принимаю, нафига он нужен.

Я имею в виду

epros в сообщении #224232 писал(а):

Во-вторых, я не понял про "частный случай": Если высказывание $p$ недоказуемо в арифметике, т.е. $A \nvdash p$

Я так понял, что Вы использовали здесь $(A \vdash p) \vee (A \nvdash p)$. Есть много арифметических предложений таких, что у нас нет доказательства $A \vdash p$ (в слабом смысле, а не в том, что предположение о его существовании ведёт к противоречию). Использует ли Ваше доказательство т.Гудстейна где-нибудь аксиому истинности для таких предложений?

epros в сообщении #224341 писал(а):

Например вот это: $(A \vdash p) \vee (A \vdash \neg p)$

Разумеется, нет.

epros в сообщении #224341 писал(а):

Например, чтобы включить его в арифметику, мы должны заложить схему $A \vdash p \vee \neg p$ для каждого $p$

Нет, $\forall p ~ A \vdash p \vee \neg p$. Это существенно более сильное утверждение.

[epros]

Alexey Romanov в сообщении #224386 писал(а):

Я имею в виду

epros в сообщении #224232 писал(а):

Во-вторых, я не понял про "частный случай": Если высказывание $p$ недоказуемо в арифметике, т.е. $A \nvdash p$

Я так понял, что Вы использовали здесь $(A \vdash p) \vee (A \nvdash p)$. Есть много арифметических предложений таких, что у нас нет доказательства $A \vdash p$ (в слабом смысле, а не в том, что предположение о его существовании ведёт к противоречию).

Из чего Вы это заключили? Если у нас нет доказательства ("в слабом смысле"), то это не даёт нам оснований утверждать, что его не существует. Утверждение о недоказуемости я всегда интерпретирую как доказанную невозможность существования доказательства (доказывается это обычно, действительно, путём приведения предположения к противоречию).

Alexey Romanov в сообщении #224386 писал(а):

Использует ли Ваше доказательство т.Гудстейна где-нибудь аксиому истинности для таких предложений?

Может быть Вы его всё-таки почитаете?

Если Ваши вопросы имеют целью разведать, пользовался ли я классическим или интуиционистским исчислением предикатов, то можете смело считать, что интуиционистским, ибо доказательств от противного и т. п. я не использовал. Однако, как Вы понимаете, такое доказательство останется в силе и в классическом исчислении предикатов.

Alexey Romanov в сообщении #224386 писал(а):

epros в сообщении #224341 писал(а):

Например, чтобы включить его в арифметику, мы должны заложить схему $A \vdash p \vee \neg p$ для каждого $p$

Нет, $\forall p ~ A \vdash p \vee \neg p$. Это существенно более сильное утверждение.

Вы при цитировании обрезали существенный хвостик: "... для каждого $p$ - высказывания арифметики". Так что я имел в виду это:
$\forall p ~ F(p,0) \rightarrow (A \vdash p \vee \neg p)$,
где предикат $F(p,0)$ читается как: "$p$ является формулой арифметики с 0 свободных переменных" (т.е. высказыванием).

Это - формализация той фразы, которую я записал на русском языке.

[Виктор Викторов]

Я прочитал всё это несколько поздновато. Но некоторые высказывания, по-моему, требуют реакции.

nikov в сообщении #202009 писал(а):

Skipper писал(а):

А с какой стати мы имеем право объявлять такое утверждение, как новую аксиому? Если мы не знаем, истинно оно или ложно. Это оправданно еще для очевидных вещей типа "две плоскости пересекаются по прямой" - аксиома геометрии. Но неочевидные аксиомы плодить никак нельзя.

Можно добавлять только интуитивно истинные аксиомы.

А как же аксиома Лобачевского вместо аксиомы Евклида? Вы её тоже назовёте «интуитивно истинные аксиомы» и очевидной? А как с очевидностью и интуитивной истинностью аксиомы выбора?

epros в сообщении #202725 писал(а):

Pi писал(а):

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

Ну и ну
А я-то полагал, что "теоремой" по определению называется то, что доказуемо в теории.

Уважаемый epros!
Никто не сомневается, что Вы знаете смысл термина «теорема» в математической логике. Но смысл высказывания Pi Вы ведь тоже поняли? Или разъяснить?

[nikov]

Виктор Викторов в сообщении #232581 писал(а):

А как с очевидностью и интуитивной истинностью аксиомы выбора?

Это определяется примерно так: Вы собираетесь сесть на самолет, а рядом с Вами оказывается его конструктор, и говорит: в расчетах этого самолета мы использовали теорему, которая опирается на аксиому A. Если аксиома A верна, то самолет долетит, а если неверна, то развалится в полете.

[AGu]

nikov в сообщении #232648 писал(а):

Виктор Викторов в сообщении #232581 писал(а):

А как с очевидностью и интуитивной истинностью аксиомы выбора?

Это определяется примерно так: Вы собираетесь сесть на самолет, а рядом с Вами оказывается его конструктор, и говорит: в расчетах этого самолета мы использовали теорему, которая опирается на аксиому A. Если аксиома A верна, то самолет долетит, а если неверна, то развалится в полете.

... где A -- это аксиома, утверждающая существование выбора деталей, при котором самолет не развалится.

[Виктор Викторов]

nikov в сообщении #232648 писал(а):

Виктор Викторов в сообщении #232581 писал(а):

А как с очевидностью и интуитивной истинностью аксиомы выбора?

Это определяется примерно так: Вы собираетесь сесть на самолет, а рядом с Вами оказывается его конструктор, и говорит: в расчетах этого самолета мы использовали теорему, которая опирается на аксиому A. Если аксиома A верна, то самолет долетит, а если неверна, то развалится в полете.

Уважаемый nikov! Во-первых, надо аккуратно цитировать оппонента.

Виктор Викторов в сообщении #232581 писал(а):

А как же аксиома Лобачевского вместо аксиомы Евклида? Вы её тоже назовёте «интуитивно истинные аксиомы» и очевидной? А как с очевидностью и интуитивной истинностью аксиомы выбора?

Во-вторых, (опустив пассаж про самолёт) какая с Вашей точки зрения аксиома верна Евклида или Лобачевского? Обратите внимание, что эти аксиомы противоречат одна другой. Подсказка: ошибочна постановка вопроса.

[nikov]

Виктор Викторов в сообщении #232653 писал(а):

Во-вторых, (опустив пассаж про самолёт) какая с Вашей точки зрения аксиома верна Евклида или Лобачевского?

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

А вот, например, аксиомы Пеано являются интуитивно истинными, для них не требуется экспериментальная проверка, и никакой эксперимент никогда не сможет их опровергнуть. Такой же интуитивной истинностью обладает утверждение о непротиворечивости системы аксиом Пеано (хотя оно и невыводимо из них), поэтому оно может быть добавлено в качестве аксиомы без опасений, что мы получим неадекватную теорию. Утверждение о непротиворечивости полученной теории опять является интуитивно истинным, и также может быть добавлено, и т.д.

Для ясности я еще предлагаю рассмотреть формальную теорию, обладающей теми же символами, что и арифметика Пеано, но единственной аксиомой $2 + 2 = 5$. Эта теория будет непротиворечивой, и в ней будет тривиально доказуемо утверждение $2 + 2 = 5$. Однако, это не сделает данное утверждение истинным. Не говоря уже о применениях в повседневной жизни, можно рассмотреть метаматическое применение: к формуле формального языка, состоящей из двух символов, приписали справа другую формулу, состоящую из двух символов. Сколько символов содержит результат этой операции?

[AGu]

nikov в сообщении #202009 писал(а):

Можно добавлять только интуитивно истинные аксиомы.

nikov в сообщении #232660 писал(а):

С моей точки зрения аксиомы геометрии вообще не являются интуитивно истинными.

Поскольку всякая теория определяется набором своих аксиом, из приведенных выше двух цитат следует, что Вы не считаете геометрию теорией. Не лишая Вас этого права, хочу лишь заметить, что с Вами не согласится куча математиков -- просто потому, что они используют другие определения. И на всякий случай замечу также, что спорить об определениях бессмысленно. Поэтому и не спорю. По Вашему определению геометрия -- это не теория, по «нашему» -- теория. Ну и славно.

nikov писал(а):

Для ясности я еще предлагаю рассмотреть формальную теорию, обладающей теми же символами, что и арифметика Пеано, но единственной аксиомой $2 + 2 = 5$. Эта теория будет непротиворечивой, и в ней будет тривиально доказуемо утверждение $2 + 2 = 5$. Однако, это не сделает данное утверждение истинным. Не говоря уже о применениях в повседневной жизни, можно рассмотреть метаматическое применение: к формуле формального языка, состоящей из двух символов, приписали справа другую формулу, состоящую из двух символов. Сколько символов содержит результат этой операции?

Ответ: $5$. Потому что символ $5$ «по определению» равен $2+2$. (Заметьте, я не спорю с таким определением. Просто временно переключаюсь на предложенную нетрадиционную систему определений.)

[Виктор Викторов]

nikov в сообщении #232660 писал(а):

С моей точки зрения аксиомы геометрии вообще не являются интуитивно истинными.

Дайте, пожалуйста, определение (критерий) интуитивной истинности аксиомы.

[nikov]

AGu в сообщении #232667 писал(а):

nikov в сообщении #202009 писал(а):

Можно добавлять только интуитивно истинные аксиомы.

nikov в сообщении #232660 писал(а):

С моей точки зрения аксиомы геометрии вообще не являются интуитивно истинными.

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

Нет, я так не считаю. Я двусмысленно выразился в первой из цитат. Следует читать так: "мы можем решить, что будем добавлять только интуитивно истинные аксиомы". В этом случае у нас не возникнет сомнений по поводу адекватности расширенной теории. А можем решить добавить и сомнительные аксиомы (или вообще ложные), и посмотреть, что получится. Это тоже будет теория, но ее выводы не будут безусловно справедливы.

-- Пн авг 03, 2009 15:31:48 --

Виктор Викторов в сообщении #232668 писал(а):

nikov в сообщении #232660 писал(а):

С моей точки зрения аксиомы геометрии вообще не являются интуитивно истинными.

Дайте, пожалуйста, определение (критерий) интуитивной истинности аксиомы.

Ну имейте в виду, что так как это не математика, а философия математики, то здесь нельзя дать определения в математическом смысле.
А так, пожалуйста:
Истинное утверждение - утверждение, соответствующее действительности.
Интуитивно истинное утверждение - истинное утверждение, несомненная истинность которого подтверждается интуицией.

[AGu]

nikov в сообщении #232669 писал(а):

Я двусмысленно выразился в первой из цитат. Следует читать так: "мы можем решить, что будем добавлять только интуитивно истинные аксиомы". В этом случае у нас не возникнет сомнений по поводу адекватности расширенной теории. А можем решить добавить и сомнительные аксиомы (или вообще ложные), и посмотреть, что получится. Это тоже будет теория, но ее выводы не будут безусловно справедливы.

Учитывая неформализуемость понятий интуитивной истинности, адекватности и «безусловной справедливости» (вах, какой термин!), с готовностью соглашаюсь. Выходит, я напрасно спорил.

[nikov]

AGu в сообщении #232667 писал(а):

nikov писал(а):

Для ясности я еще предлагаю рассмотреть формальную теорию, обладающей теми же символами, что и арифметика Пеано, но единственной аксиомой $2 + 2 = 5$. Эта теория будет непротиворечивой, и в ней будет тривиально доказуемо утверждение $2 + 2 = 5$. Однако, это не сделает данное утверждение истинным. Не говоря уже о применениях в повседневной жизни, можно рассмотреть метаматическое применение: к формуле формального языка, состоящей из двух символов, приписали справа другую формулу, состоящую из двух символов. Сколько символов содержит результат этой операции?

Ответ: $5$. Потому что символ $5$ «по определению» равен $2+2$.

Заметьте, что $+$ - это всего лишь значок предложенной формальной теории. С чего Вы решили, что он имеет отношение к тому, что происходит с количеством знаков при приписывании одной формулы к другой?