Разные вопросы математической логики

[realeugene]

Ende
Выделено из темы «Свобода воли - не есть физическая наблюдаемая...»

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

Какая теория? Аксиоматическая теория - это множество выводимых из заданного множества аксиом предложений языка. Если её аксиомы не все выполняются для данной модели, то нельзя говорить, что эта теория на этой модели "истинна".

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

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

-- 05.04.2025, 14:38 --

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

Вы полагаете, что метаматематика - это теория множеств?

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

[epros]

realeugene в сообщении #1681185 писал(а):

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

Я не перепутал. Аксиоматическая теория - про выводимость, а не следование.

realeugene в сообщении #1681185 писал(а):

Если вы "выводимостью" назвали доказуемость - то это просто неверно.

Кстати, выводимость и доказуемость - синонимы, а вот следование - увы нет (в классической логике).

realeugene в сообщении #1681185 писал(а):

В арифметике есть недоказуемые истинные утверждения.

Эта Гёделевская словесная формулировка - не совсем точная. На самом деле, речь про недоказуемые в арифметике Пеано утверждения, истинные в её стандартной модели. Ибо нет понятия "истинности вообще". А ещё правильнее (поскольку "стандартная модель" - недостаточно строго определённое понятие) было бы сказать, что речь про утверждения, доказуемые в метатеории, принимающей за аксиому непротиворечивость арифметики Пеано, но не в самой арифметике Пеано.

realeugene в сообщении #1681185 писал(а):

Кроме того, любое следование эквивалентно общезначимости соответствующей ему импликации.

Следование - и есть импликация. Причём тут общезначимость?

realeugene в сообщении #1681185 писал(а):

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

Я спросил это, потому что в моём понимании метаматематика - это в первую очередь reverse mathematics, а никак не теория множеств, о какой бы аксиоматике ни шла речь. Там исследуются разные системы математики с разной "доказательной силой". ZFC, например, это просто одна из таких систем - есть более слабые и есть более сильные.

[realeugene]

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

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

Теория содержит все следствия своей аксиоматики, и только их. Следование эквивалентно общезначимости именно импликации с аксиоматикой в антецеденте.

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

Я не перепутал. Аксиоматическая теория - про выводимость, а не следование.

Ваше утверждение противоречит определениям на стр. 145 и стр. 237 в Дж. Булос, Р. Джеффри, Вычислимость и логика, М., Мир, 1984

Там правда термин звучит "аксиоматизируемая", а не "аксиоматическая".

[epros]

realeugene в сообщении #1681191 писал(а):

Теория содержит все следствия своей аксиоматики, и только их.

К чему это было сказано? Вы (сославшись на определение слова "допускать" из словаря) сказали, что аксиомы должны скорее "предполагаться", чем "приниматься". Я ответил, что предположения - это то, что находится в антецеденте импликации, так что им не нужно быть аксиомами, ибо импликация может быть результатом условного вывода.

realeugene в сообщении #1681191 писал(а):

Следование эквивалентно общезначимости именно импликации с аксиоматикой в антецеденте.

Кстати, не всякую аксиоматику можно засунуть в антецедент импликации.

realeugene в сообщении #1681191 писал(а):

Ваше утверждение противоречит определениям на стр. 145 и стр. 237 в Дж. Булос, Р. Джеффри, Вычислимость и логика, М., Мир, 1984

Там правда термин звучит "аксиоматизируемая", а не "аксиоматическая".

На странице 145 - абстрактное определение теории "вообще", т.е. в некотором семантическом смысле. Большинство таких теорий абсолютно бесполезны, ибо не могут быть разумным образом аксиоматизированы. А это значит, что нет способа передать такую теорию от учителя к ученику - они никогда не договорятся о том, какие предложения языка принадлежат теории, а какие нет. Можете смело считать, что такие теории существуют только в воображении математиков, примерно как сферические кони в вакууме.

Реальное знание состоит из аксиоматических теорий. Булос говорит о них на стр. 237. Но он заходит со стороны семантики, а поэтому говорит об "аксиоматизируемых" теориях - как о таких теориях, которые состоят из следствий разрешимой аксиоматики. То, что он говорит о следовании (семантическом понятии), а не о выводимости (синтаксическом понятии), объясняется тем, что он в целом следует семантическому подходу. В данном случае разница не очень существенна, но всё же правильнее было бы говорить именно о выводимости, ибо могут быть такие следствия (импликации), которые в данной аксиоматике недоказуемы. Во всяком случае, вся Proof theory - именно про выводимость, а не про логическое следование.

[realeugene]

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

Кстати, не всякую аксиоматику можно засунуть в антецедент импликации.

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

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

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

Ну да, именно об этом первая теорема Гёделя о неполноте арифметики, если я правильно помню.

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

Во всяком случае, вся Proof theory
- именно про выводимость, а не про логическое следование.

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

[epros]

realeugene в сообщении #1681232 писал(а):

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

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

realeugene в сообщении #1681232 писал(а):

Ну да, именно об этом первая теорема Гёделя о неполноте арифметики, если я правильно помню.

Ну да. Вот в строгом соответствии с теоремой Гёделя есть утверждение, недоказуемое в арифметике Пеано, но которое становится доказуемым, если добавить к арифметике Пеано аксиому о непротиворечивости арифметики Пеано. Пример такового утверждения - теорема Гудстейна $G$. Это значит, что $G$ "следует", например, из $0=0$ - в том смысле, что в стандартной модели арифметики импликация $0=0 \to G$ истинна. Теперь скажите, принадлежит ли $G$ арифметике Пеано? Конечно нет, потому что это утверждение невыводимо из её аксиоматики. Так что определение "аксиоматизируемой теории" на стр. 237 в книжке Булоса к арифметике Пеано не очень подходит. Именно потому что в формулировке определения надо было сказать не "следует", а "выводится".

realeugene в сообщении #1681232 писал(а):

Тем не менее, механический вывод без семантики бесполезен.

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

[realeugene]

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

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

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

-- 06.04.2025, 09:46 --

(Оффтоп)

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

В целом что такое эти 2.4трлн. я не очень понимаю.

Вот, кстати, такое ощущение было, например, от популяризаторских постов Илларионова. "Такой-то индикатор здесь на 20% больше, чем там..." Ну и что? А считали-то этот индикатор как? Тишина. Но можно предположить, что даже если выложат детальный расчёт, всё равно там будет настолько сложный статистический анализ, что человеку со стороны в нём просто за пару часов не разобраться. В результате как в анекдота: "-- Петька, приборы! -- 13!". Из-за сложности пропал смысл.

[epros]

realeugene в сообщении #1681258 писал(а):

Не совсем я понял, но, насколько я помню, утверждение, что нельзя в любой достаточно сильной теории арифметики доказать непротиворечивость арифметики - это вторая теорема Гёделя о неполноте

Да, и она доказывается с использованием первой.

realeugene в сообщении #1681258 писал(а):

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

Нет, мы получим нормальную, т.е. предположительно непротиворечивую теорию. И она так же будет неполна в силу первой теоремы Гёделя о неполноте и в ней так же нельзя будет доказать её собственную непротиворечивость в силу второй теоремы Гёделя о неполноте.

[realeugene]

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

Нет, мы получим нормальную, т.е. предположительно непротиворечивую теорию. И она так же будет неполна в силу первой теоремы Гёделя о неполноте и в ней так же нельзя будет доказать её собственную непротиворечивость в силу второй теоремы Гёделя о неполноте.

Так в модели этой теории предикат доказуемости на номере этого утверждения про непротиворечивость расширенной арифметики будет истинным или ложным?

[epros]

realeugene в сообщении #1681260 писал(а):

Так в модели этой теории предикат доказуемости на номере этого утверждения про непротиворечивость расширенной арифметики будет истинным или ложным?

Смотря в какой модели.

[realeugene]

(Оффтоп)

Dedekind в сообщении #1681261 писал(а):

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

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

-- 06.04.2025, 11:01 --

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

Смотря в какой модели.

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

[realeugene]

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

Смотря в какой модели.

На самом деле, вторая теорема Гёделя утверждает, что какова бы ни была модель для самой арифметики, и какова бы ни была выбрана в ней (вычислимая) нумерация логических предложений, если попытаться определить предикат доказуемости $B(x)$ со стандартными свойствами правил вывода, окажется, что обязательно есть модель, в которой он будет принимать истинное значение на номере формулы $ \mathbf 0 = \mathbf 1$ в выбранной нами нумерации предложений. Так что как только мы добавляем в нашу аксиоматику в качестве аксиомы $\neg B\left(\ulcorner \mathbf 0 = \mathbf 1 \urcorner\right)$, или любую аналогичную, исключающее такие интерпретации (т. е. что все предложения, которые можно доказать нашей механической процедурой, истинны во всех моделях нашей теории), мы получаем противоречие со второй теоремой Гёделя.

[mihaild]

juna в сообщении #1681252 писал(а):

Причем здесь биномиальное распределение? Вы считаете, что вероятности ответить "доверяю", "не доверяю" в эксперименте одинаковы и равны $p, 1-p$ для всех людей?

Нет, я считаю, что переменные "ответ 1го случайного человека", "ответ 2го случайного человека" и т.д. - бернуливские, с одинаковым распределением, и, пока число людей невелико, почти независимы. Соответственно их сумма биномиальна.

realeugene в сообщении #1681266 писал(а):

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

Не нужно его задавать, он выражается через сложение и умножение.
Да, в стандартной модели PA выполнены как $\text{Cons}_{PA}$, так и $\text{Cons}_{PA + \text{Cons}_{PA}}$.

dsge в сообщении #1681271 писал(а):

Исследования - это R&D - Research and Development, а не инвестиции в datacenters

Как тут какое-то время назад обсуждали, затраты на R&D имеют, видимо, примерно столько же понятного смысла, как и затраты на астрологов которые 2,4 трлн. Т.е. посчитали что-то по каким-то критериям, понять, что они означают - без поллитры не получится.

realeugene в сообщении #1681278 писал(а):

и какова бы ни была выбрана в ней (вычислимая) нумерация логических предложений

Что такое "нумерация в модели"? В модели нет арифметических предложений (только числа), как их нумеровать?

realeugene в сообщении #1681278 писал(а):

Так что как только мы добавляем в нашу аксиоматику в качестве аксиомы $\neg B\left(\ulcorner \mathbf 0 = \mathbf 1 \urcorner\right)$,

Мы получаем другую аксиоматику, с другим предикатом доказуемости.

[realeugene]

dsge в сообщении #1681271 писал(а):

Исследования - это R&D - Research and Development, а не инвестиции в datacenters.

Это исследовательские датацентры. Оборудование для R&D .

-- 06.04.2025, 13:08 --

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

Мы получаем другую аксиоматику, с другим предикатом доказуемости.

Но вторая теорема Гёделя утверждает, что каким бы ни был предикат доказуемости, из любого расширения $Q$ не может следовать $\neg B\left(\ulcorner \mathbf 0 = \mathbf 1 \urcorner\right)$.

-- 06.04.2025, 13:16 --

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

Что такое "нумерация в модели"? В модели нет арифметических предложений (только числа), как их нумеровать?

У нас в арифметике есть функция $S(x)$, которая вместе с аксиоматикой арифметики даёт возможность складывать, вычитать, умножать и делить с остатком эти числа. Каждому предложению нашего языка соответствует его номер в этой нумерации. Не важно, в какой конкретно, важно, что возможно средствами этой арифметики вычислить номера подвыражений по номеру некоторого предложения.

[mihaild]

realeugene в сообщении #1681284 писал(а):

Но вторая теорема Гёделя утверждает, что каким бы ни был предикат доказуемости, из любого расширения $Q$ не может следовать $\neg B\left(\ulcorner \mathbf 0 = \mathbf 1 \urcorner\right)$.

Нет. Вы пишете $B$, это сбивает, надо обязательно указывать теорию.
Вторая теорема Гёделя утверждает, что если $T$ - эффективное непротиворечивое расширение $PA$, то $T \not \vdash \neg \Box_T\left(\ulcorner \bot \urcorner\right)$.
Собственно из теоремы о дедукции следует, что если в арифметике недоказуема противоречивость арифметики, то добавление в арифметику аксиомы о ее непротиворечивости оставляет ее непротиворечивой.