Логики 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$ истинно

Цитата:

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

Цитата:

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

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