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

[Someone]

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

Можем ли мы (по Генцену) сделать такой вывод:

$$\frac{\Gamma, P\vdash Q}{\Gamma \vdash P\rightarrow Q} \eqno (1)$$

Ведь для синтаксиса не важно, что значат буквы?

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

Кроме того, у Вас перепутаны в кучу теория и метатеория: $P\rightarrow Q$ — формула теории, а $\Gamma \vdash P\rightarrow Q$ — формула метатеории. Такая путаница — прямой путь к противоречиям.

[epros]

Someone в сообщении #1729714 писал(а):

Кроме того, у Вас перепутаны в кучу теория и метатеория: $P\rightarrow Q$ — формула теории, а $\Gamma \vdash P\rightarrow Q$ — формула метатеории. Такая путаница — прямой путь к противоречиям

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

[Vladimir Pliassov]

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

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

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

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

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

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

Что это вообще означает?

Я нашел такое Определение:

Цитата:

Семантическое следование — это логическое отношение между утверждениями, при котором истинность одного утверждения гарантирует истинность другого.

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

Что это за логика, в которой помимо обычных высказываний $A$ и $B$ есть ещё "оценочные"? По-моему, это масло масляное, говорить вместо "солнце село" что-нибудь вроде: "то, что солнце село, истина".

До позавчерашнего дня мне тоже казалось, что "солнце село" и "то, что солнце село, истина" это одно и то же, я думал, что высказывание $v(A)=\top\to v(B)=\top$ ("из истинности $A$ следует истинность $B$") это то же самое, что высказывание $A\to B$ (из $A$ следует $B$). Но оказалось, что это не так.

Разделение на формулы предметного языка и оценочные высказывания метаязыка — это, как я читал, фундаментальное требование теоремы Тарского о невыразимости истины.

Цитата:

Если мы откажемся от «оценочных» высказываний на метауровне и попытаемся засунуть предикат истинности v(A)=\top$ внутрь того же предметного языка, где живут обычные A и B, наша логическая система мгновенно взорвется парадоксом Лжеца («Данное высказывание ложно»).

Однако между предметным языком и метаязыком нет непроходимой пропасти, между высказыванием $A$ предметного языка и оценочным высказыванием $v(A)=\top$ метаязыка существует мостик в виде двух правил:

Правило спуска (Дерефлексия):

$$\frac{\vdash A}{A}$$

Читается: «Если на метаязыке утверждено, что $A$ имеет место, мы имеем право спуститься на нижний уровень и оперировать просто формулой $A$».

Правило подъема (Рефлексия):

$$\frac{A}{\vdash A}$$

Читается: «Если у нас на нижнем уровне есть формула $A$, мы имеем право подняться на метаязык и поставить перед ней знак утверждения».

Здесь, как я понимаю, в качестве "знака утверждения" может стоять знак $\top$, то есть вместо $\frac{\vdash A}{A}$ и $\frac{A}{\vdash A}$ можно писать $\frac{v(A)=\top}{A}$ и $\frac{A}{v(A)=\top}$.

Цитата:

Альфред Тарский (в своей знаменитой работе 1933 года о понятии истины в формализованных языках) доказал, что для любого корректного языка переход от «Высказывание $A$ истинно» к самому высказыванию $A$ синтаксически тождественен.

Уиллард Ван Орман Куайн (великий логик США). Он назвал этот процесс «децитацией» (disquotation) или «снятием кавычек». Он говорил: сказать «"Снег бел" — истинно» — это абсолютно то же самое, что просто сказать «Снег бел». Мы просто снимаем кавычки метаязыка и получаем чистую формулу предметного языка.

Но снятие кавычек здесь это операция (Дерефлексия), ее надо провести, сами собой они не снимаются.

Однако рефлексия/дерефлексия проводятся только с целыми формулами, но не с их частями, например, можно из высказывания $v(A\to B)=\top$ по правилу спуска вывести высказывание $A\to B$, но вывести по этому же правилу $A\to B$ непосредственно из $v(A)=\top\to v(B)=\top$ нельзя, тут нужна целая цепочка рассуждений.

Пусть нам дано, что $v(A)=\top\to v(B)=\top$. Возьмем гипотезу $A$. По правилу подъема выведем из нее формулу $v(A)=\top$. Возьмем ее в качестве посылки для modus ponens относительно формулы $v(A)=\top\to v(B)=\top$, получим формулу $v(B)=\top$, по правилу спуска выведем из нее формулу $B$. Таким образом, по транзитивности выводим $B$ из $A$, то есть импликацию $A\to B$, и по аналогии с теоремой о дедукции из импликации метаязыка $v(A)=\top\to v(B)=\top$ выводим импликацию предметного языка $A\to B$.

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

Эту цепочку мне предложил ИИ, когда я спросил его, может ли он вывести импликацию из одних только условий, не используя таблицу истинности. За что я ему чрезвычайно благодарен, так как она является ключевой в выведении импликации $A\to B$ из условий $\{A, B\}$, так что я отказываюсь от Определения. Те высказывания, которые семантически следуют из условий, назовем истинными и возвращаюсь к первоначальному определению Определения. Те высказывания, которые следуют из условий, назовем истинными.

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

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

[tolstopuz]

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

Я нашел такое Определение:

Почему "нашел"? Это вы употребили термин "семантическое следование", меня интересует, какой смысл вы в него вкладывали, а не то, что вы где-то потом "нашли".

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

Семантическое следование — это логическое отношение между утверждениями, при котором истинность одного утверждения гарантирует истинность другого.

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

[epros]

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

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

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

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

До позавчерашнего дня мне тоже казалось, что "солнце село" и "то, что солнце село, истина" это одно и то же, я думал, что высказывание $v(A)=\top\to v(B)=\top$ ("из истинности $A$ следует истинность $B$") это то же самое, что высказывание $A\to B$ (из $A$ следует $B$). Но оказалось, что это не так.

Видите ли какая штука, Ваши "оценочные" высказывания вообще не могут принадлежать исчислению высказываний по чисто синтаксическим причинам: там высказывания составляются только из пропозициональных переменных и логических связок. С его точки зрения символы $v$ и $=$ - просто непонятно что означают. Я, конечно, могу предположить, что $=$ следует трактовать как $\leftrightarrow$ (равносильность), но, знаете ли, $A \leftrightarrow \top$ сразу окажется эквивалентным $A$, а $A \leftrightarrow \bot$ сразу окажется эквивалентным $A \to \bot$ или $\neg A$.

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

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

Однако между предметным языком и метаязыком нет непроходимой пропасти, между высказыванием $A$ предметного языка и оценочным высказыванием $v(A)=\top$ метаязыка существует мостик в виде двух правил

По-моему, это какая-то ерунда. Метаязык для того и нужен, чтобы выражать что-то такое, что мы по каким-то причинам не можем выразить языком теории. Например, если мы хотим что-то сказать про доказуемость в теории, нам может для этого потребоваться метасимвол доказуемости $\vdash$. И утверждение о доказуемости $A$ не может быть эквивалентно самому $A$, как минимум, из-за существования истинных недоказуемых утверждений. Кстати, то, что из доказуемости $A$ должно следовать само $A$ - тоже нетривиальное следствие того, что метатеория признаёт аксиоматику предметной теории (а это может быть и не так).

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

то есть вместо $\frac{\vdash A}{A}$ и $\frac{A}{\vdash A}$ можно писать $\frac{v(A)=\top}{A}$ и $\frac{A}{v(A)=\top}$

А это-то откуда взято? Символ $\vdash$ вообще не про это - не про "оценку как истинное".

[Vladimir Pliassov]

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

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

Я нашел такое Определение:

Почему "нашел"? Это вы употребили термин "семантическое следование", меня интересует, какой смысл вы в него вкладывали, а не то, что вы где-то потом "нашли".

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

Семантическое следование — это логическое отношение между утверждениями, при котором истинность одного утверждения гарантирует истинность другого.

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

Выкладываю все формальное описание предлагаемой логической системы. В нем много пунктов, в том числе и пункт 16. Определение семантического следования. В нем тоже есть слово "гарантирует", но мне кажется, что в контексте оно приемлемо.

Хотя пунктов и много, подозреваю, что описание все же неполное. И к тому же я не уверен, что с ним все в порядке. Надеюсь получить критические замечания.

1. Существуют так называемые высказывания, которые будем обозначать буквами $A$, $B$, $C$ ... .

2. Существуют также высказывания $A'$, $B'$, $C'$ ... .

3. При этом $A\not=A', B\not=B', C\not=C', \dots$ .

4. Между множествами $\{A, B, C \dots\}$ и $\{A', B', C' \dots\}$ установлено взаимнооднозначное соответствие:

$A\leftrightarrow A', B\leftrightarrow B', C\leftrightarrow C' \dots$ .

5. Будем называть $A'$ отрицанием $A$ и писать $\neg A=A'$. Соответственно, $A$ будем называть отрицанием $A'$ и писать $\neg A'=A$.

6. Таким образом, $\neg (\neg A)=\neg A'=A$, то есть $\neg \neg A=A$ -- двойное отрицание.

7. Если $A$ и $B$ — произвольные высказывания, то выражение $(A \wedge B)$ также является высказыванием, называемым конъюнкцией, где в знак $\wedge$ интуитивно вкладывается тот же смысл, что и в союз "и" в бытовом языке.

8. Если $A$ и $B$ — произвольные высказывания, то выражение $(A \vee B)$ также является высказыванием, называемым дизъюнкцией, где в знак $\vee$ интуитивно вкладывается тот же смысл, что и в союз "или" в бытовом языке.

9. Если $A$ и $B$ — произвольные высказывания, то выражение $(A \to B)$ также является высказыванием, называемым импликацией, где в знак $\to$ интуитивно вкладывается тот же смысл, что и в союз "если ..., то ..." в бытовом языке.

10. Если $A$ и $B$ — произвольные высказывания, то выражение $(A \Leftrightarrow B)$ также является высказыванием, называемым эквиваленцией, где в знак $\Leftrightarrow $ интуитивно вкладывается тот же смысл, что и в союз "тогда и только тогда, когда ..." в бытовом языке.

11. Понятие истинности/ложности. Существует множество истинностных значений $\{\top, \bot\}$, где $\top$ означает "истинно", а $\bot$ означает "ложно". Каждому высказыванию $A$ мы сопоставляем его значение через функцию оценки $v(A)$. При этом, если $v(A) = \top$, то $v(\neg A) = \bot$, и наоборот, если $v(A) = \bot$, то $v(\neg A) = \top$.

12. Определение n-арной логической системы. n-арной логической системой назовем фиксированное множество, состоящее из n различных атомарных (простых) высказываний, а также всех сложных высказываний, которые могут быть построены из них по определениям пунктов 7–10.

13. Определение n-арной модели. n-арной логической моделью назовем n-арную логическую систему, в которой задано основное (определяющее) условие.

14. Определение основного (определяющего) условия. Основным (определяющим) условием n-арной модели назовем требование истинности всех n высказываний, составляющих одну из всех возможных в этой системе n-арных конъюнкций. (Примечание: это условие полностью убирает неопределенность в системе, однозначно задавая конкретный фиксированный «мир» рассуждения. Другими словами, задание такого условия превращает логическую систему в конкретную $n$-арную логическую модель.).

15. Определение. Те высказывания, которые следуют из основного условия модели, назовем истинными в этой модели, а те, которые не следуют из основного условия модели, назовем ложными в этой модели.

(Примечание: под словом «следуют» здесь понимается, что высказывания следуют семантически, синтаксически, дедуктивно или иными способами, строго подчиненными законам логики).

16. Определение семантического следования Высказывание $X$ семантически следует из фиксированных полных условий $W$, если в рамках этих условий невозможно, чтобы $X$ было ложным (не выполнялось). Иными словами, семантическое следование — это отношение, которое проверяется следующим правилом:

Высказывание $X$ семантически следует из условий $W$, если:

a) либо оно содержится в этих условиях ($X \in W$),

b) либо его истинность гарантирована истинностными значениями его частей, которые мы уже вычислили относительно этих условий.

(Примечание: в условиях W могут быть заявлены не только элементарные, но и сложные высказывания — например, что конъюнкция $A\wedge \neg B$ ложна).

Как это определение работает на практике?

Для конъюнкции $(A \wedge B)$: Следует ли она из условий $\{A, B\}$? Смотрим на правило b). Части конъюнкции — это $A$ и $B$. По правилу a): они обе содержатся в условиях ($A \in W, B \in W$), значит, обе следуют из них. А по определению конъюнкции (союз «И»), если обе части следуют, то и целое следует. Всё, семантическое следование доказано, конъюнкция истинна.

Для импликации $\neg A \to \neg B$ («из лжи ложь»): Как доказать, что она семантически следует из условий $\{A, B\}$? Мы берем ложную в наших условиях конъюнкцию $(\neg A \wedge B)$ — её ложность гарантирована тем, что $\neg A$ не содержится в условиях (правило a)). Ложность этой конъюнкции означает, что ситуация, где одновременно истинны $\neg A$ и $B$, семантически невозможна при условиях $\{A, B\}$. Следовательно, если мы гипотетически допускаем $\neg A$, то $B$ выполняться не может. А если $B$ не выполняется, то обязано выполняться $\neg B$. Получается, что при условиях $\{A, B\}$ гипотеза $\neg A$ жестко и без вариантов сопряжена с результатом $\neg B$. Этот переход гарантируется условиями $\{A, B\}$. Значит, импликация семантически следует из условий.

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

[epros]

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

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

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

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

4. Между множествами $\{A, B, C \dots\}$ и $\{A', B', C' \dots\}$ установлено взаимнооднозначное соответствие:

$A\leftrightarrow A', B\leftrightarrow B', C\leftrightarrow C' \dots$ .

5. Будем называть $A'$ отрицанием $A$ и писать $\neg A=A'$. Соответственно, $A$ будем называть отрицанием $A'$ и писать $\neg A'=A$.

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

[Vladimir Pliassov]

Someone в сообщении #1729714 писал(а):

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

Не могли бы Вы (или кто-нибудь еще) привести пример, когда подстановка вместо букв $\Gamma$, $P$ и $Q$ каких-то значений приводит к несоблюдению теоремы о дедукции

$$\frac{\Gamma, P\vdash Q}{\Gamma \vdash P\rightarrow Q} \eqno (1)$$

?

[Someone]

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

подстановка вместо букв $\Gamma$, $P$ и $Q$ каких-то значений

А у Вас вместо этих букв можно что угодно подставлять? А то я вот хочу вместо буквы $\Gamma$ подставить число $5$, вместо буквы $P$ — алгебру кватернионов над полем действительных чисел, а вместо $Q$ — строку букв "абракадабра". Да и вместо остальных символов можно что-нибудь подставить. Вы же спросили

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

Ведь для синтаксиса не важно, что значат буквы?

А я ответил:

Someone в сообщении #1729714 писал(а):

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

А теперь Вы демонстрируете сомнение в моих словах.

[Vladimir Pliassov]

1.

Someone в сообщении #1729811 писал(а):

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

подстановка вместо букв $\Gamma$, $P$ и $Q$ каких-то значений

А у Вас вместо этих букв можно что угодно подставлять? А то я вот хочу вместо буквы $\Gamma$ подставить число $5$, вместо буквы $P$ — алгебру кватернионов над полем действительных чисел, а вместо $Q$ — строку букв "абракадабра". Да и вместо остальных символов можно что-нибудь подставить.

Как я понимаю, если возможно вывести строку букв "абракадабра" из числа $5$ и алгебры кватернионов над полем действительных чисел, то

a) из числа $5$ выводится, что из алгебры кватернионов над полем действительных чисел следует строка букв "абракадабра",

b) из алгебры кватернионов над полем действительных чисел выводится, что из числа $5$ следует строка букв "абракадабра".

2.

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

Обозначим оценочное высказывание $v(A\wedge \neg B)=\bot$ через $R$, оценочное высказывание $v(A)=\top$ -- через $P$, оценочное высказывание $v(B)=\top$ -- через $Q$. Можем ли мы (по Генцену) сделать такой вывод:

$$\frac{\Gamma, P\vdash Q}{\Gamma \vdash P\rightarrow Q} \eqno (1)$$

где $\Gamma$ это множество посылок, включающее в себя $R$: $R\in \Gamma$ (точнее, в нашем случае $\Gamma$ это одноэлементное множество, оно состоит только из $R$)?

3.

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

Оценочные высказывания это тоже высказывания.

Что такое высказывание? Это предложение, которое можно оценить либо как истинное, либо как ложное. Но ведь и оценку можно оценить: является она истинной или ложной. И оценку оценки можно оценить и так далее до бесконечности. Это уровни языков Тарского .

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

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

Соответственно, второй уровень для первого является мета-уровнем, третий уровень для второго является мета-уровнем и так далее.

У меня высказывания $A, B, A\wedge \neg B$, $A\to B$ принадлежат первому уровню, оценочные высказывания $P=(v(A)=\top)$, $Q=(v(B)=\top)$, $R=\big ((A\wedge \neg B)=\bot\big )$ принадлежат второму уровню, выводы $\Gamma, P\vdash Q$ и $\Gamma \vdash P\rightarrow Q$ принадлежат третьему уровню, а теорема о дедукции

$$\frac{\Gamma, P\vdash Q}{\Gamma \vdash P\rightarrow Q} \eqno (1)$$

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

Поэтому я не совсем согласен (хотя не исключаю, что меня переубедят) со следующим комментарием:

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

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

То есть я согласен, что вся эта теорема находится на одном уровне, но не на втором -- метатеоретическом, а на третьем -- мета-метатеоретическом.

Если же вместо букв $\Gamma$, $P$ и $Q$ мы подставим соответствующие семантические высказывания, то получим теорему о дедукции в семантическом варианте (на втором уровне):

$$\frac{\{v(A\wedge \neg B)=\bot \}, v(A)=\top\Vdash v(B)=\top}{\{v(A\wedge \neg B)=\bot \} \Vdash v(A)=\top\rightarrow v(B)=\top} \eqno (2)$$

4.

Каждый уровень имеет свой синтаксис.

1). Синтаксис Уровня 1 (Предметный язык)

Алфавит: буквы $A, B$, связки $\wedge, \vee, \to, \neg$, скобки $(\quad)$.

Объекты: только формулы вида $A \wedge \neg B$ или $A \to B$. Никаких истин и оценок тут нет.

2). Синтаксис Уровня 2 (Семантический / Метаязык)

Чтобы построить метаязык, Тарский и Куайн расширяют исходный алфавит. Они создают новый, более богатый алфавит Метаязыка, в который официально добавляются:

Специальный функциональный символ оценки: $v$

Константы истинностных значений: $\top$ и $\bot$

Знак мета-равенства (или двоеточие): $=$

И вот по строгим синтаксическим правилам этого нового, второго уровня объект $v(A) = \top$ становится абсолютно законной, правильно построенной формулой! Для этого этажа выражения $P$, $Q$ и $R$ — это элементарные переменные-сокращения.

3). Синтаксис Уровня 3 (мета-метаязык)

Здесь мы берем буквы $P, Q, R$ (роль которых на Уровне 2 определена как равенства $P=(v(A)=\top)$, $Q=(v(B)=\top)$, $R=\big ((A\wedge \neg B)=\bot\big )$) и строим из них формулу Генцена (1).

5.

Вы говорите, что хотите вместо буквы $\Gamma$ подставить число $5$, вместо буквы $P$ — алгебру кватернионов над полем действительных чисел, а вместо $Q$ — строку букв "абракадабра". Но такие значения, исходя из описанного синтаксиса второго уровня, браться не могут.

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

[epros]

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

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

Оценочные
высказывания это тоже высказывания.

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

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

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

Вы неправильно оцениваете назначение уровней мета-, потому что неправильно оцениваете назначение логики.

Вы не поняли, что предназначение логики - быть общей частью всякого теоретического знания. Поэтому она должна строиться таким образом, чтобы её можно было применять на любом уровне мета-. Это значит, что хотя в метаязыке мы и вводим новый символ $\vdash$ (доказуемости, а никакой не "уровень оценки"), логика остаётся той же самой, мы не придумываем для этого никакой "логики следующего уровня". Если Вы думали, что логики 0, 1, 2 и т.д. порядка об этом, то Вы ошибаетесь.

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

То есть я согласен, что вся эта теорема находится на одном уровне, но не на втором -- метатеоретическом, а на третьем -- мета-метатеоретическом.

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

[Someone]

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

Как я понимаю, если возможно вывести строку букв "абракадабра" из числа $5$ и алгебры кватернионов над полем действительных чисел, то…

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

[Vladimir Pliassov]

Someone в сообщении #1729828 писал(а):

Вы бы посмотрели, как определяется алфавит теории.

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

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

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

1.

Вместо того, чтобы выводить импликацию $A\to B$ из ложности конъюнкции $A\wedge \neg B$, то есть из того, что $v(A\wedge \neg B)=\bot$, (что, как выяснилось, не так-то просто) и вовлекать при этом в рассуждение второй (семантический) уровень, можно выводить ее из отрицания конъюнкции $A\wedge \neg B$, то есть из дизъюнкции $\neg A\vee B$, и избежать тем самым этого второго (семантического) уровня:

Пусть формула $R$ — это $\neg A \vee B$. Пусть $\Gamma = \{R\}$. Тогда по правилам исчисления секвенций Генцена мы можем сделать следующий абсолютно легальный синтаксический вывод:

$$\frac{\Gamma ,A\vdash B}{\Gamma \vdash A\rightarrow B}$$

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

Первый уровень принадлежит логике 0 порядка, а второй уровень -- логике 1 порядка.

Это упрощение задачи, но я вывожу импликацию $A\to B$ не из дизъюнкции $\neg A\vee B$, а из ложности конъюнкции $A \wedge \neg B$.

2.

Для этого заменим $v(A\wedge \neg B)=\bot$ на $\neg T(A\wedge \neg B)$, $v(A)=\top$ на $T(A)$ и $v(B)=\top$ на $T(B)$, чтобы не выходить за рамки алфавита синтаксиса логики 1 порядка.

Здесь $T$ -- это унарный (одноместный) предикат истинности. Запись $T(X)$ читается как «Формула $X$ истинна».

Введем обозначения:

$P \triangleq T(A)$ (Формула Уровня 2: «А истинно»),

$Q \triangleq T(B)$ (Формула Уровня 2: «В истинно»),

$R \triangleq \neg T(A \wedge \neg B)$ (Формула Уровня 2: «Конъюнкция $A \wedge \neg B$ ложна»),

$\Gamma \triangleq \{R\}=\{\neg T(A \wedge \neg B)\}$.

И теперь можно написать и так:

$$\frac{\Gamma, P\vdash Q}{\Gamma \vdash P\rightarrow Q} \eqno (1)$$

и так:

$$\frac{\{\neg T(A \wedge \neg B)\}, T(A)\vdash T(B)}{\{\neg T(A \wedge \neg B)\} \vdash T(A)\rightarrow T(B)} \eqno (5)$$

3.

При этом выводы $\Gamma, P\vdash Q$ и $\Gamma \vdash P\rightarrow Q$ принадлежат уже не второму, а третьему уровню (мета-метатеории), так как это высказывания о формулах второго уровня (высказывания о том, что они выводятся друг из друга).

Но вся формула (1) принадлежит не четвертому уровню (как можно было бы предположить), а всего лишь третьему, так как
представляет собой мета-метаимпликацию: из вывода $\Gamma, P\vdash Q$ следует вывод $\Gamma \vdash P\rightarrow Q$ (если истинно высказывание над чертой, то отсюда следует истинность высказывания под чертой).

Правильно?

[epros]

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

Пусть формула $R$ — это $\neg A \vee B$. Пусть $\Gamma = \{R\}$. Тогда по правилам исчисления секвенций Генцена мы можем сделать следующий абсолютно легальный синтаксический вывод:

$$\frac{\Gamma ,A\vdash B}{\Gamma \vdash A\rightarrow B}$$

Не знаю, как именно Вы выводите теорему дедукции, но какие-то прелюдии про $\Gamma = \{R\}$ тут явно неуместны.

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

Первый уровень принадлежит логике 0 порядка, а второй уровень -- логике 1 порядка.

Ничего подобного.

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

Это упрощение задачи, но я вывожу импликацию $A\to B$ не из дизъюнкции $\neg A\vee B$, а из ложности конъюнкции $A \wedge \neg B$.

Импликацию не надо выводить ни из дизъюнкции, ни из отрицания конъюнкции. Впрочем, если очень хочется, то можно из гильбертовской аксиоматики исчисления высказываний вывести тавтологии $(\neg A\lor B) \to (A \to B)$ и $\neg (A \land \neg B) \to (A \to B)$.

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

Здесь $T$ -- это унарный (одноместный) предикат истинности. Запись $T(X)$ читается как «Формула $X$ истинна»

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

[mihaild]

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

я вывожу импликацию $A\to B$

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