Вопрос по теореме Геделя

[arseniiv]

tac14 в сообщении #1037109 писал(а):

Видите ли какое дело, встает вопрос применимости матлогики на практике.

Применима. Ну почитайте о ней, что ли — и сами сделаете вывод. А пока, судя по всему, вы рассуждаете о том, о чём имеете лишь смутное представление.

[epros]

Xaositect в сообщении #1037188 писал(а):

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

Разве доказательство недоказуемости внутри самой системы не означает опровержения?

[Xaositect]

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

Разве доказательство недоказуемости внутри самой системы не означает опровержения?

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

[arseniiv]

(Оффтоп)

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

Полнота языка по Тьюрингу. Если язык теории полон по Тьюрингу

Не совсем понял, тут имеется в виду «полнота по Тьюрингу» языка первого порядка? Это как? В нём кодируются, скажем, частично рекурсивные функции и их вычисление?

[mihaild]

Xaositect в сообщении #1037188 писал(а):

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

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

[Xaositect]

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

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

Да, если в системе можно сформулировать, что такое доказательство. Собственно, теорема Геделя как раз об этом.

[epros]

Xaositect в сообщении #1037201 писал(а):

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

Хм, а зачем тогда в логике высказываний нужна аксиома $(A \rightarrow B) \rightarrow ((A \rightarrow \neg B)\rightarrow \neg A)$? Насколько я понимаю, она как раз и определяет что такое "опровержение $A$". А именно, она утверждает, что если из $A$ выведено нечто, а потом из того же $A$ выведено отрицание этого нечто (т.е. в итоге выведено противоречие), то $A$ -- опровергнуто.

Есть другие (кроме Гильбертовской) аксиоматизации логики высказываний, где аналогичная аксиома формулируется как $(A \rightarrow \perp) \rightarrow \neg A$, что прямо означает, что опровержение $A$ возникает в результате вывода из него "абсурда". Честно говоря, я не знаю, какой ещё смысл может вкладываться в слова "доказать недоказуемость $A$ внутри системы", кроме вывода из $A$ противоречия.

-- Ср июл 15, 2015 02:42:18 --

arseniiv в сообщении #1037205 писал(а):

Не совсем понял, тут имеется в виду «полнота по Тьюрингу» языка первого порядка? Это как? В нём кодируются, скажем, частично рекурсивные функции и их вычисление?

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

-- Ср июл 15, 2015 03:00:41 --

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

Честно говоря, я не знаю, какой ещё смысл может вкладываться в слова "доказать недоказуемость $A$ внутри системы", кроме вывода из $A$ противоречия.

Тьфу, я туплю. Конечно же "доказательство недоказуемости внутри системы" следует понимать в смысле Гёделевской арифметизации доказательств. Такое доказательство эквивалентно опровержению в теории T + аксиома о непротиворечивости теории T. Но без дополнительной аксиомы опровержение может быть невыводимо.

[arseniiv]

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

а в языке теории первого порядка

Под языком первого порядка я как раз это и имел в виду.

[tac14]

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

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

Или пример не удачен, или если этот пример имеет отношение к теореме Геделя - то это слишком банально, и думаю не стоило городить огород ..

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

-- Ср июл 15, 2015 02:46:36 --

arseniiv в сообщении #1037190 писал(а):

Применима. Ну почитайте о ней, что ли — и сами сделаете вывод. А пока, судя по всему, вы рассуждаете о том, о чём имеете лишь смутное представление.

(Оффтоп)

Троллинг засчитан, ага

[iifat]

tac14 в сообщении #1037235 писал(а):

пример показывает, что все формальные системы

Пример в принципе не может ничего показывать про все. Только про некоторые. И отношение к теореме Гёделя имеет исключительно демонстративное. Представленная аксиоматика условиям теоремы Гёделя не удовлетворяет.

[tac14]

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

Религиозное мышление, как я понимаю, принимает за аксиомы некоторые непроверяемые экспериментом вещи. А то, что принято за аксиому -- уже доказуемо (в один ход).

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

[epros]

arseniiv в сообщении #1037229 писал(а):

Под языком первого порядка я как раз это и имел в виду.

Ну вот арифметика Пресбургера тоже является теорией первого порядка, но она полна. А операция факторизации чисел в её языке невыразима.

tac14 в сообщении #1037235 писал(а):

Или пример не удачен, или если этот пример имеет отношение к теореме Геделя - то это слишком банально, и думаю не стоило городить огород ..

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

tac14 в сообщении #1037235 писал(а):

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

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

-- Ср июл 15, 2015 04:13:40 --

tac14 в сообщении #1037240 писал(а):

Только я как то не видел, чтобы аксиомы математики проверяли бы в эксперименте

Математика интересна как инструмент. Причём тут эксперименты?

[arseniiv]

(Оффтоп)

tac14 в сообщении #1037235 писал(а):

Троллинг засчитан, ага

Я серьёзно. Почитайте матлогику, если вам действительно интересно сделать про неё какие-то верные выводы.

[tac14]

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

С какой это стати из существования неразрешимых вопросов должно следовать, что разрешённые вопросы разрешены неверно?

С той стати, что сам ход рассуждений в такой формальной системе не правомочен (в следствии разных причин - не верна аксиома, набор аксиом приводит к противоречию, недостаточно аксиом, недостаточен алфавит системы, не верен алгоритм построения суждений), раз есть такие вопросы, которые не позволяет разрешить такая формальная система. Так например, в эксперименте мы получаем ответ на некий неразрешимый в определенном формализме вопрос. Как нам относится к ответам, которые дает этот формализм? Скорее признается, что этот формализм не достаточен и он выбрасывается, и находится новый формализм. Который также дает ответы - но уже с более глубокой трактовкой, или совсем другой трактовкой. (причем как известно именно трактовка популяризируется в науке, т.е. становится наиболее известной)

[arseniiv]

tac14 в сообщении #1037244 писал(а):

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

• Если теория противоречива, в ней всё подряд выводимо, и она полна — так что с этой причиной вы пролетели. [Хм, кажется, противоречивые теории полными не зовут, однако. Но всё равно это, можно сказать, дальше от неполноты, чем от полноты. В теоремах неполной не найдётся некоторых истинных формул; в теоремах противоречивой найдутся все истинные, как в полной, плюс ещё и все ложные.]
• Недостаточен алфавит — это вообще смешно. Можно закодировать строки в любом алфавите строками в алфавите из всего двух символов; а алфавит из одного символа, наоборот, тут совершенно неприменим, так что недостаточного алфавита случиться просто не может.
• Неверен алгоритм построения суждений, не верна аксиома — это просто по глупости написано (ещё раз, читайте про то, о чём собираетесь писать): проверить истинность аксиом и то, что правила вывода переводят истинные формулы в истинные — обычно не проблема. Потом, если здесь что-то не так, это светит опять же только противоречивостью, а не неполнотой.

Остаётся только «недостаточно аксиом», и про это уже писали: может быть так, что их всегда недостаточно, о чём 1-я теорема Гёделя и, кстати, говорит.