Логики 0, 1 и 2 порядков.

[tolstopuz]

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

В целом, если мы говорим чисто о выводимости, и в языке нет значков $\top$ и $\bot$, то я не понимаю, что вообще такое "таблица истинности".

У Верещагина-Шеня проблем с этим пониманием нет (ч.2, стр. 46):

Цитата:

Вообще каждой строке таблицы истинности для формулы $A$ соответствует утверждение о выводимости.

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

А это теорема о полноте

Да, это фактически часть доказательства теоремы о полноте. И эта часть полностью закрывает вопрос ТС.

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

причем тут импликация?

Доказываются четыре утверждения о выводимости, соответствующие таблице истинности для импликации.

[Vladimir Pliassov]

tolstopuz в сообщении #1727940 писал(а):

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

Я посмотрел: да, выводятся, и спасибо за то, что это прислали! Теперь мне легче будет с Вами (и не только с Вами) спорить!

Значит, есть такие высказывания, которые выводятся, и есть такие, которые не выводятся.

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

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

tolstopuz в сообщении #1727940 писал(а):

не требуется даже ни конъюнкция, ни дизъюнкция

Да, я вывожу эти формулы не так, как Гильберт. Я и аксиомы его доказываю своим методом. Например, $A\to (B\to A)$:

пусть $A$ истинно, тогда $\neg A$ ложно, и поэтому конъюнкция $B\wedge \neg A$ ложна. Отсюда следует, что если $B$ истинно, то $\neg A$ ложно, и, значит, $A$ истинно.

И, по-моему, формулы импликаций у меня доказываются проще (эти доказательства можно найти в первом сообщении темы).

Вообще, мне кажется, что для логики высказываний по-настоящему нужна только одна аксиома -- $A\vee \neg A$, остальные можно доказать. Или я ошибаюсь?

[mihaild]

tolstopuz в сообщении #1727949 писал(а):

У Верещагина-Шеня проблем с этим пониманием нет (ч.2, стр. 46):

Так у них там есть и семантика.
Ну и, кстати, для построения таблицы истинности формулы используются таблицы истиности для связок (стр. 9).

Vladimir Pliassov в сообщении #1727970 писал(а):

Так вот я предлагаю, называть те высказывания, которые выводятся, истинными, а те, которые не выводятся -- ложными

Предложение отклоняется. Уже есть стандартная терминология. Высказывания, которые выводятся, называются выводимыми, а те, которые не выводятся - не выводимыми.
А истинность и ложность высказывания определяется толькопри данной оценке, просто "истинных" высказываний не бывает. Как именно определяется - посмотрите в книге.

Vladimir Pliassov в сообщении #1727970 писал(а):

Я и аксиомы его доказываю своим методом

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

Vladimir Pliassov в сообщении #1727970 писал(а):

Вообще, мне кажется, что для логики высказываний по-настоящему нужна только одна аксиома -- $A\vee \neg A$, остальные можно доказать. Или я ошибаюсь?

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

[tolstopuz]

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

Так у них там есть и семантика.

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

[Vladimir Pliassov]

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

Предложение отклоняется. Уже есть стандартная терминология. Высказывания, которые выводятся, называются выводимыми, а те, которые не выводятся - не выводимыми.

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

(Что касается четвертой импликации -- ложной -- то он ее не вывел. Напротив,

оценка «Истина» (1) означает, что сама результирующая импликация выводима: $\vdash (A \to B)$.

оценка «Ложь» (0) означает, что выводима не сама импликация, а её отрицание: $\vdash \neg(A \to B)$.)

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

Зачем это надо?

Хотя бы в педагогическом плане: чтобы у изучающих логику "не ехала крыша" от импликации "из того, что сахар сладкий, следует, что $2\times 2=5$", чтобы они понимали, что эта импликация истинна не потому, что сладость сахара как-то (мистически) связана с тем, что $2\times 2=5$ (что само по себе уже трудно постичь, потому что это не так), а потому что она выводится, например, из пары условий "сахар не сладкий"$=\top$ и $(2\times 2\not=5)=\top$ (но не только из них, а и еще из двух пар условий).

(То есть, как я писал в предыдущем посте, "истинна" здесь это просто кодовое слово, оно означает "выводится".)

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

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

Ну а если посмотреть на формулу $A\to (B\to A)$ не как на аксиому, просто как на формулу, можно считать ее доказательством вот это:

Пусть $A$ истинно, тогда $\neg A$ ложно, и поэтому конъюнкция $B\wedge \neg A$ ложна. Отсюда следует, что если $B$ истинно, то $\neg A$ ложно, и, значит, $A$ истинно.

?

[mihaild]

Vladimir Pliassov в сообщении #1727993 писал(а):

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

Нет, не согласен.
Во-первых, в выводе выше нет никаких "разных выведенных импликаций". Там есть выводы вида $A, B \vdash A \rightarrow B$.
Во-вторых, в разговорах о формальных вещах - я вообще не согласен называть утверждения истинными без упоминания модели (в логике высказываний модель называется оценкой).
Я не согласен называть истинной, например, формулу $A \rightarrow A$. Я согласен называть её выводимой (в классическом исчислении высказываний). Я согласен называть её истинной при оценке $A = 0$ (и при оценка $A = 1$). Я согласен называть её тавтологией (истинной при любой оценке). Я не согласен называть её истинной, и я не согласен смешивать два разных фундаментальных понятия формальной логики.

Vladimir Pliassov в сообщении #1727993 писал(а):

Хотя бы в педагогическом плане: чтобы у изучающих логику "не ехала крыша"

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

Vladimir Pliassov в сообщении #1727993 писал(а):

можно считать ее доказательством вот это

Пока что нельзя. Просто "доказательств" не бывает, доказательства всегда в каком-то исчислении с какими-то аксиомами. Пока Вы не выписали аксиомы и правила вывода, о доказательствах говорить нельзя.
Конечно, можно легко выписать кучу разных систем аксиом, эквивалентных классической логике (с правилом вывода modus ponens). Но таки нужно выписать какую-то конкретную систему до того, как говорить о доказательствах.

[tolstopuz]

Vladimir Pliassov в сообщении #1727993 писал(а):

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

Они не "называются истинными". Этот вывод доказывает, что их выводимость согласуется с (не использованной в доказательстве!) таблицей истинности импликации. А из теоремы о корректности следует, что их отрицания невыводимы. Для четвертой импликации наоборот, выводимо отрицание.
Этот вывод - часть доказательства теоремы о том, что любая тавтология (формула, истинная при всех значениях переменных) выводима. Довольно глубокий факт, связывающий истинность и выводимость в одной конкретной логической системе - исчислении высказываний - и требующий доказательства. Вы же вместо этого занимаетесь игрой слов.

-- добавлено через 16 минут --

Vladimir Pliassov в сообщении #1727993 писал(а):

Ну а если посмотреть на формулу $A\to (B\to A)$ не как на аксиому, просто как на формулу, можно считать ее доказательством вот это:

Пусть $A$ истинно

Цитата:

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

Цитата:

Оказывается, что все тавтологии можно получить из некоторого набора «аксиом» с помощью «правил вывода», которые имеют чисто синтаксический характер и никак не апеллируют к смыслу формулы, её истинности и т.д. Эту задачу решает так называемое исчисление высказываний.

А при вашем подходе надо каждую формулу заново проверять при всех возможных значениях переменных.

[Vladimir Pliassov]

tolstopuz в сообщении #1727999 писал(а):

А при вашем подходе надо каждую формулу заново проверять при всех возможных значениях переменных.

А если посмотреть на формулу $A\to (B\to A)$ не как на формулу, а как на схему формул? Записать ее в виде $P\to (Q\to P)$ и потом подставлять вместо $P$ либо $A$, либо $\neg A$, а вместо $Q$ либо $B$, либо $\neg B$? Тогда не надо проверять каждую из получаемых формул, достаточно проверить, то есть доказать только схему $P\to (Q\to P)$. Правильно?

И этот способ радикально отличается от того способа, который дается в учебниках логики: подставлять вместо каждой переменной либо $t$, либо $f$ всевозможными способами, так что для двух переменных это будет 4 подстановки, для трех переменных 8 подстановок, для 4 переменных 16 подстановок и так далее -- просто ужас!

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

Это с точки зрения объема работы, но, по-моему, и само по себе интересно, что можно доказать схему формул, вместо того, чтобы подставлять $t$ и $f$ в отдельно взятые формулы.

Докажем схему $P\to (Q\to P)$. Пусть нам дана формула $P$ в качестве гипотезы. Из неё синтаксически выводима формула $\neg \neg P$, из которой, в свою очередь, выводима формула $\neg (Q\wedge \neg P)$. По правилам связи связок (по закону де Моргана и свойствам дизъюнкции), из отрицания этой конъюнкции выводится импликация $Q \to \neg\neg P$. Поскольку в классической логике из двойного отрицания $\neg\neg P$ выводимо $P$, мы получаем $Q \to P$. Таким образом, из гипотезы $P$ мы вывели $Q \to P$. Применяя теорему дедукции, мы окончательно выводим формулу $P\to (Q\to P)$ из пустого множества посылок.

Эта схема доказана синтаксически из неё самой, а не проверкой подстановками. Благодаря теореме о полноте классической логики, этот синтаксически выведенный закон гарантирует общезначимость (тавтологичность) получаемых формул для абсолютно любых конкретных высказываний, которые мы подставим вместо переменных $P$ и $Q$.

Теперь доказательство правильное?

[mihaild]

Vladimir Pliassov в сообщении #1728051 писал(а):

А если посмотреть на формулу $A\to (B\to A)$ не как на формулу, а как на схему формул?

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

Vladimir Pliassov в сообщении #1728051 писал(а):

Эта схема доказана синтаксически из неё самой

Нет, она доказана из каких-то аксиом. Которые можно явно выписать, но Вы пока этого не сделали.

(Оффтоп)

Vladimir Pliassov в сообщении #1728051 писал(а):

Но эту посылку (составной импликации) придется проверить. А что если она очень сложная?

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

[tolstopuz]

Vladimir Pliassov в сообщении #1728051 писал(а):

И этот способ радикально отличается от того способа, который дается в учебниках логики: подставлять вместо каждой переменной либо $t$, либо $f$ всевозможными способами

Похоже, вы не читаете не только учебники логики, но и то, что вам здесь пишут.

Верещагин и Шень писал(а):

Оказывается, что все тавтологии можно получить из некоторого набора «аксиом» с помощью «правил вывода», которые имеют чисто синтаксический характер и никак не апеллируют к смыслу формулы, её истинности и т.д. Эту задачу решает так называемое исчисление высказываний.

Vladimir Pliassov в сообщении #1728051 писал(а):

мы окончательно выводим формулу $P\to (Q\to P)$ из пустого множества посылок.

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

[waxtep]

Читал на днях об учениях стоиков в изложении Диогена Лаэртского, вспоминал этот тред, стиль рассуждений мне показался довольно похожим. Vladimir Pliassov, гляньте, может быть Вам зайдет; например, здесь. Строгости и систематичности там не найти, зато масса забавных историй и можно выбирать по вкусу:

VII, 74 писал(а):

... Утвердительно-условное суждение истинно, если исходит из истинного суждения и имеет вытекающее заключение, например: «Поскольку стоит день, то солнце стоит над землей»; ложно, если исходит из ложного суждения или имеет невытекающее заключение, например: «Поскольку стоит ночь, то Дион гуляет», когда на самом деле стоит день.

VII, 81 писал(а):

... Из ложного может следовать истинное, например, из того, что «земля летает», – то, что «земля существует»; но из истинного ложное следовать не может, например, из того, что земля существует, – то что земля летает.

[tolstopuz]

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

VII, 74 писал(а):

Условное суждение бывает истинно, если противоположность заключению противоречит началу; например, суждение «Если стоит день, то светло» истинно, потому что противоположность заключению «не светло» противоречит началу «стоит день». А ложно оно бывает, если противоположность заключению не противоречит началу, например: «Если стоит день, то Дион гуляет» – ложно, потому что «Дион не гуляет» не противоречит началу «стоит день».

[waxtep]

tolstopuz в сообщении #1728079 писал(а):

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

Тем более, раз там все аккуратно, можно брать на вооружение

[Vladimir Pliassov]

Мне сейчас пришла такая мысль.

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

Но если изменить определение:

Назовем те высказывания, формулы которых выводятся из данных синтаксических условий, истинными, а те высказывания, формулы которых не выводятся из этих условий, ложными ?

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

Откуда для высказываний возьмутся синтаксические условия? Семантическим условиям $A=\top, B=\top$ соответствуют синтаксические условия $A, B$. Правильно?

Между семантикой и синтаксисом ведь нет непроходимой пропасти:

tolstopuz в сообщении #1728053 писал(а):

Верещагин и Шень писал(а):

Оказывается, что все тавтологии можно получить из некоторого набора «аксиом» с помощью «правил вывода», которые имеют чисто синтаксический характер и никак не апеллируют к смыслу формулы, её истинности и т.д. Эту задачу решает так называемое исчисление высказываний.

иначе не было бы исчисления (синтаксическое понятие) высказываний (семантическое понятие).

И в выражении "формула высказывания" видна связь между синтаксисом ("формула") и семантикой ("высказывания").

Формулы (семантических) высказываний синтаксически выводятся друг из друга. При этом высказывание и его формула могут обозначаться одной и той же буквой.

(Высказывания все семантические или есть не семантические?)

waxtep в сообщении #1728076 писал(а):

Читал на днях об учениях стоиков в изложении Диогена Лаэртского, вспоминал этот тред, стиль рассуждений мне показался довольно похожим. Vladimir Pliassov, гляньте, может быть Вам зайдет; например, здесь
. Строгости и систематичности там не найти, зато масса забавных историй и можно выбирать по вкусу

Спасибо! Книга безусловно интересная, но объемная, всю ее просмотреть пока не успел, но исходя из тех цитат, что Вы прислали, вижу, что, как Вы и говорите, обоснование истинности/ложности импликаций в ней не строгое, на бытовом уровне, а я пытаюсь найти строгое.

На остальные комментарии надеюсь ответить чуть позже.

[mihaild]

Vladimir Pliassov в сообщении #1728103 писал(а):

Говорить "высказывание (семантический термин) выводится (синтаксический термин)" это и есть это смешение.

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