Есть ли синтаксис в математике?

[Xaositect]

errnough в сообщении #301331 писал(а):

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

Да.
Контраргументом к вашему "противоречию" является абзац про функциональную зависимость.

[venco]

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

[errnough]

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

где $P(x)$ - это некоторый предикат (пропозициональная функция).

Сейчас начался бы спор, является ли сам предикат таким высказыванием, что содержит опять же пропозициональную функцию по определению, в рамках теории Russell et al.. Если мы не остаемся в терминах определенной теории, то конструктива не будет. Из того, что я использую таблицы истинности в практике, и они доказали свою пригодность в конкретном применении (хорошо знаю, например, что переключение элемента "2И-НЕ" ничего не говорит о том, сколько еще до этого было переключений), никак не следует, что теория Рассела не ложна. Практика и теория сильно разные вещи. Теории в большинстве оказываются ложными. Будем считать, что это вопрос решен и рассуждения строятся в терминах одной теории.

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

$n$ и $k$ у нас вполне конкретные пропозициональные функции, зависящие от значения пропозиции "Цезарь мертв".
Мы не можем присваивать им значения произвольно!

Можем. Если при этом рассмотрим все возможные. А возможных-то всего два: {true,false}.
Можно --= ход рассуждений №2 =--- построить в уме, начав с false. Придем к тому же. Согласны, что этот довод, про произвольность, можно снять?

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

Я, наверное, зря Вас все-таки к Расселу-Уайтхеду отослал. Там терминология устаревшая, и перевода на русский нет.
Если хотите, почитайте "Введение в математическую логику" Черча, "Введение в метаматематику" Клини.

Лично меня устраивает. Чем запутаннее текст про математические объекты, тем лучше просматривается семантика и синтаксис.

[Xaositect]

errnough в сообщении #301367 писал(а):

Можем. Если при этом рассмотрим все возможные. А возможных-то всего два: {true,false}.
Можно --= ход рассуждений №2 =--- построить в уме, начав с false. Придем к тому же. Согласны, что этот довод, про произвольность, можно снять?

Не согласен.
Как только мы присвоили значение $m$, предложения $n$ и $k$ автоматически получают вполне определенное значение, основанное на значении $m$.

[errnough]

Цитата:

Согласны, что этот довод, про произвольность, можно снять?

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

Не согласен.

Возражение 1: Произвольность снимается указанием порядка выбора.

Произвольность означает: происходящее из воли человека. Не более того. Это вполне законный метод в математике и используется в методе подстановок из области допустимых значений аргумента. Если мы все допустимые варианты перебрали, то произвольность не является больше значимым в доказательстве. Так и пишут: для любого (для каждого) $x$ из области $Q$... А если мы укажем порядок выбора, т.е. вначала проверим true, а затем false, то и произвол в выборе снят, поскольку указан порядок выбора.

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

Как только мы присвоили значение $m$, предложения $n$ и $k$ автоматически получают вполне определенное значение, основанное на значении $m$.

Возражение 2: Возможно, Вы утверждаете, что мы вообще не можем присвоить конкретное значение из {true,false} для $m$, то есть, не можем сделать из $m$ asserted proposition, что вообще говоря, странно, поскольку фактически отвергается широко используемый метод проверки теорем, высказываний и алгоритмов с помощью подстановки. Тогда:
мы не можем сделать следующий после $m$ шаг, хотя раньше его делали, и не можем утверждать $n$, что очевидно абсурдно, и кроме того, противоречит Вашим прежним заключениям, в которых допускали этот шаг, и рассматривали его.

------------------------------------------------

• (цезарь мертв) суть высказывание $m$ (unasserted).
• $m$ может быть {true,false}. Пока неопределенность. Определим $m=true$ высказав $n$:
• «(цезарь мертв) это высказывание истинное» суть высказывание $n$.

------------------------------------------------

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

[Xaositect]

А вот теперь я действительно не понимаю, что Вы говорите.

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

[errnough]

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

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

Согласен. Теперь уточним это высказывание. Мое добавление — синим.

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

С этим добавлением согласны?

Кроме того, в терминах теории Russell et al. высказывание и есть пропозициональная функция. Ваше предложение можно сократить наполовину.

---------------
В обычной алгебре тоже так. Мы утверждаем что-то относительно функции в общем виде $f(x)=x^2$, а не конкретно $3^2$. Хотя это и возможно, при подстановке, но в алгебре область значений и область определения есть множество с бесконечным количеством элементов, и конкретное в числах утверждение обладает малой эвристической ценностью. В логике только два элемента, {ложь,истина}. Поэтому несложная функция в логике задается таблицей всех значений сразу, для обычной алгебры этот метод потребует бесконечной таблицы.

Алгебра логики работает реально. Компьютер, который перед нами, по сути не умеет ничего, кроме как сложить две единицы и позиционно сдвинуть. А всё программирование заключается в построении таблиц истинности. Результат перед нами. Это компьютер, который и точечку $1/3$ серым цветом нам на оси поставит в математическом пакете, и комплексные числа отобразит. Это всё симуляции. Симулякрон. Компьютер в самой основе даже не понимает, что такое отрицательное число. Помните такого Виету? Он умер, так и не признав существование отрицательных чисел.

А ошибки в программировании суть нежелание строить очень большую таблицу истинности до конца. По индукции, всё будет работать и так. Якобы. :)))

[Xaositect]

errnough в сообщении #301665 писал(а):

С этим добавлением согласны?

Согласен.
Но раз Вы тоже с ним согласны, то должны признать, что как только мы определяем $m$ как True, все остальные высказывания в Вашей цепочке автоматически получают некоторые значения, так как ни от чего, кроме истинностного значения $m$, не зависят. То есть произвольность заканчивается, как только мы фиксируем $m$.

-- Ср мар 24, 2010 14:54:44 --

errnough в сообщении #301665 писал(а):

Алгебра логики работает реально. Компьютер, который перед нами, по сути не умеет ничего, кроме как сложить две единицы и позиционно сдвинуть. А всё программирование заключается в построении таблиц истинности. Результат перед нами. Это компьютер, который и точечку серым цветом нам на оси поставит в математическом пакете, и комплексные числа отобразит. Это всё симуляции. Симулякрон. Компьютер в самой основе даже не понимает, что такое отрицательное число. Помните такого Виету? Он умер, так и не признав существование отрицательных чисел.

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

[errnough]

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

Но раз Вы тоже с ним согласны, то должны признать, что как только мы определяем $m$ как True, все остальные высказывания в Вашей цепочке автоматически получают некоторые значения, так как ни от чего, кроме истинностного значения $m$, не зависят. То есть произвольность заканчивается, как только мы фиксируем $m$.

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

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

• (цезарь мертв) суть высказывание $m$ (unasserted).
• $m$ может быть {true,false}. Пока неопределенность. Определим $m=true$ высказав $n$:
• «(цезарь мертв) это высказывание истинное» суть высказывание $n$.
• $n$ может быть {true,false}. Пока неопределенность. Определим $n=false$ высказав $k$:
• «(цезарь мертв) это высказывание истинное» это высказывание ложное» суть высказывание $k$.
• $k$ может быть {true,false}. Пока неопределенность. Определим $k$, высказав $k_1$...

Как же с этим можно не согласиться?

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

(Оффтоп)

Парадоксы не то, что думает про них абсолютное большинство людей.

На самом деле парадоксы это сущности, которые генерируются. Теория это алгоритм. Если вы ВИДИТЕ ошибку, то можете управлять процессом генерации парадоксов. Делается это через хитрый подбор данных, которые, будучи поданными на вход алгоритма, обязательно переключат управление на ошибочный кусок кода. Эти данные чаще всего даже проще тривиальных, на которые рассчитан алгоритм. Тот кто не видит ошибки, будет продолжать подавать на вход алгоритма тривиальные данные, проверяя этим, как он по наивности своей думает, правильность работы алгоритма. По найденной ошибке остается из генерирующихся парадоксов выбрать самый простой и убийственный. В этой теории, Principia mathematica, ошибка в самой основе. Ее уже ничто не спасет. IMHO.

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

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

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

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

Вы акцент поставили на процессоре. Но обратите внимание на файл. Именно файл есть доказательство, что в компьютере отрицательных чисел принципиально нет.

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

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

[Xaositect]

errnough в сообщении #302123 писал(а):

На самом деле парадоксы это сущности, которые генерируются. Теория это алгоритм.

Именно! Теория - это алгоритм. Обычно в логике рассматривают эффективно аксиоматизируемые теории, которые выглядят так:
1. Есть аксиомы, а именно, есть алгоритм, который позволяет распознать, является ли данная формула аксиомой. Обычно он представлен в виде семейства схем аксиом.
2. Есть правила вывода, т.е. алгоритм, который позволяет получать аксиом и из доказанных теорем новые доказанные теоремы.
Теория называется непротиворечивой, если не существует формулы $F$ такой, что $F$ и $\neg F$ доказуемы.

-- Чт мар 25, 2010 14:00:38 --

errnough в сообщении #302123 писал(а):

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

Но раз Вы тоже с ним согласны, то должны признать, что как только мы определяем $m$ как True, все остальные высказывания в Вашей цепочке автоматически получают некоторые значения, так как ни от чего, кроме истинностного значения $m$, не зависят. То есть произвольность заканчивается, как только мы фиксируем $m$.

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

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

• (цезарь мертв) суть высказывание $m$ (unasserted).
• $m$ может быть {true,false}. Пока неопределенность. Определим $m=true$ высказав $n$:
• «(цезарь мертв) это высказывание истинное» суть высказывание $n$.
• $n$ может быть {true,false}. Пока неопределенность. Определим $n=false$ [...]

Стоп.
Мы определили $m=true$? Если да, то $n$ не может быть $false$, ибо утверждает, что $m=true$.

[errnough]

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

Теория - это алгоритм.

Консенсус :)

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

1. Есть аксиомы, а именно, есть алгоритм, который позволяет распознать, является ли данная формула аксиомой. Обычно он представлен в виде семейства схем аксиом.

Что-то здесь не так... не чувствуете? Порочный круг просматривается.

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

Мы определили $m=true$? Если да, то $n$ не может быть $false$, ибо утверждает, что $m=true$.

Мы определили $m=true$ через высказывание(!). Нельзя по-другому в рамках этой теории.

1. $m$ (unasserted).
2. $n$ (unasserted) о том, что $m$ (asserted).
3. $k$ (unasserted) о том, что $n$ (asserted).
4. ...

Объяснение по-другому. Пропозициональная функция становится аргументом для другой пропозициональной функции, и далее, как матрешки. А первоначальная неопределенность аргумента остается. В точности аксиоматический метод.

И еще по-другому: утверждение об истинности высказывания является снова высказыванием, ложным или истинным, утверждение об истинности которого является снова...

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

PS__________

Парадокс лжеца, в этой интерпретации:
$m$= "всё что я говорю, ложь"
1. $m$ (unasserted).
2. $n$ (unasserted) о том, что $m$ (asserted).
3. $k$ (unasserted) о том, что $n$ (asserted).
4. ...

[Xaositect]

errnough в сообщении #302234 писал(а):

Что-то здесь не так... не чувствуете? Порочный круг просматривается.

Да нет, там все хорошо. Вы знаете, что такое Pattern matching? Ну так вот, формула признается аксиомой, если она подходит под одну из схем.
Например, есть схема аксиом индукции. $\varphi(0)\&(\forall n (\varphi(n)\to \varphi(n+1)))\to \forall n \varphi(n)$. Так вот, если формула совпадает с этой схемой при каком-то выборе подформулы $\varphi$, то это аксиома.

-- Чт мар 25, 2010 16:58:39 --

errnough в сообщении #302234 писал(а):

И еще по-другому: утверждение об истинности высказывания является снова высказыванием, ложным или истинным, утверждение об истинности которого является снова...

Утверждение об истинности высказывания тоже является высказыванием, ложным или истинным, но его ложность или истинность равна ложности или истинности исходного высказывания.

-- Чт мар 25, 2010 17:05:16 --

errnough в сообщении #302234 писал(а):

Объяснение по-другому. Пропозициональная функция становится аргументом для другой пропозициональной функции, и далее, как матрешки. А первоначальная неопределенность аргумента остается. В точности аксиоматический метод.

Замечательно. Но пока неопределенность остается, мы не можем ничего ни доказать, ни опровергнуть. Только если при любом возможном устранении неопределенности мы что-то получаем, мы можем это утверждать. Пока есть неопределенность, нет никаких выводов.
Так что это никак не мешает нам утверждать, что $p\ \text{i}\ \mathbf{False}$ равнозначно $\neg p$.
Ведь $\neg p$ - это тоже пропозициональная функция. Мы можем построить цепочки
$p$, $p\ \text{is}\ \mathbf{False}$, $(p\ \text{is}\ \mathbf{False})\ \text{is}\ \mathbf{False}$,...
$p$, $\neg p$, $\neg \neg p$,...
И как только мы устраним неопределенность в $p$(любым возможным образом - т.е. положим его True или False), эти цепочки сраз окажутся равными.
Именно это и есть смысл равенства $(p\ \text{is}\ \mathbf{False})\equiv \neg p$, именно это мы и доказали и ничего больше мы не утверждаем.

[errnough]

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

Утверждение об истинности высказывания тоже является высказыванием, ложным или истинным, но его ложность или истинность равна ложности или истинности исходного высказывания.

Кажется, по второму кругу поедем... не хотелось бы...

Утверждение об истинности высказывания тоже является высказыванием, 
      ^^^^^^^^^^^^^^^           |                           |
            |                   |                           |
            |                   |                           |
            |                  (m)                          |
            |         "всё что я говорю, ложь"              |
           (n)                                              |
       суть истина                                         (k)
                                                          /   \
                                                         /     \
                                                    ложным или истинным,
                                                            |
                                                            |
                                                            |
  1. (m)= "всё что я говорю, ложь" (unasserted)             |
  2. (n)= (unasserted) о том, что (m) (asserted, истина)"   |
  3. (k)= (unasserted) о том, что (n) (unasserted) <--------*
                 |
                / \
               /   \
              /     \
но его ложность или истинность 
равна ложности или истинности 
  исходного высказывания.

Правильнее будет сказать, что с высказыванием (k) полная неопределенность, а чему неопределенность может быть равна, не знаю... я о такой процедуре не слышал.

Цитата:

Пока есть неопределенность, нет никаких выводов.
Так что это никак не мешает нам утверждать, что $p\ \text{i}\ \mathbf{False}$ равнозначно $\neg p$.

Очень даже мешает. На каком основании можно утверждать, что одна неопределенность равнозначна другой неопределенности, да еще с отрицанием?

Цитата:

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

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

[Xaositect]

Парадокс лжеца? Как известно, он разрешается тем, что фразы типа "Это высказывание ложно", высказываниями не являются, поскольку не имеют истинностного значения.

-- Чт мар 25, 2010 20:19:01 --

errnough в сообщении #302382 писал(а):

Очень даже мешает. На каком основании можно утверждать, что одна неопределенность равнозначна другой неопределенности, да еще с отрицанием?

Одна неопределенность, зависящая от $p$, равна другой неопределенности, зависящей от $p$, потому что при любом устранении неопределенности в $p$ они становятся равными (и определенными) величинами.

Мы же обсуждали это на третьей странице:

Цитата:

This is done, for example, when the law of identity is asserted in the form "$A\ \text{is}\ A$". Here A is left undetermined, because, however A may be determined, the result will be true. Thus when we assert $A\ \text{is}\ A$ , leaving $A$ undetermined, we are asserting an ambiguous value of our function. This is only legitimate if, however the ambiguity may be determined, the result will be true.

Это абсолютно та же ситуация. Мы утверждаем $A\ \text{is}\ A$, поскольку любая возможная подстановка значения $A$ делает это утверждение истинным. Так и в случае $(p\ \text{is}\ \mathbf{False})\equiv \neg p$ мы утвеждаем это, поскольку любая возможная (True, False) подстановка вместо $p$ его значения делает эту формулы истинным утверждением.

[Xaositect]

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

1.Буквами $p$ c индексами будем обозначать атомарные высказывания. Атомарные высказывания являются высказываниями.
2. Буквой $\mathrm{t}$ будем обозначать тождественно истинное высказывание.
3.Знаком $\neg$ обозначаем отрицание. Если $\varphi$ - высказывание, то и $\neg \varphi$ будет высказыванием.
4.Введем еще символ: $\equiv$. Если $\varphi$ и $\psi$- высказывания, то $\varphi\equiv\psi$ будет высказываниями.
Никакие другие формулы высказываниями не являются.

Теперь придадим всему этому смысл. Введем понятие интерпретации.
Интерпретацией $I$ назовем отображение, приписывающее каждому высказыванию $\varphi$ его истинностное значение $\varphi_I$, которое может быть равным $\mathbf{True}$ или $\mathbf{False}$.
1. Атомарным высказываниям припишем истинностные значения произвольно. Содержательно, атомарные высказывания - это простые предложения языка, например "Идет дождь" или "Цезарь умер", которые являются истинными или ложными.
2. $I(\mathrm{t}) = \mathbf{True}$, т.е. $\mathrm{t}$ - это некоторое абсолютно истинное утверждение, например $0=0$.
3. Если $I(\varphi) = \mathbf{True}$, то $I(\neg\varphi) = \mathbf{False}$, если $I(\varphi) = \mathbf{False}$, то $I(\neg\varphi) = \mathbf{True}$. Это определяет смысл функции отрицания.
4. Если $I(\varphi) = I(\psi)$, то $I(\varphi\equiv\psi) = \mathbf{True}$, иначе $\mathbf{False}$. То есть, $\equiv$ выражает равенство истинностных значений.

Назовем высказывание $\varphi$ истинным в интерпретации $I$, если $I(\varphi) = \mathbf{True}$.
Назовем высказывание $\varphi$ общезначимым, если оно истинно в любой интерпретации. Это понятие соответствует понятию asserted proposition из Principia.
Назовем два высказывания $\varphi$ и $\psi$ синонимичными, если в любой интерпретации их истинностные значения совпадают.

Теперь попробуем перевести на язык этой теории нашу задачу. Заметим, что в любой интерпретации высказывание $\neg\mathrm{t}$ есть $\mathbf{False}$. Обозначим это высказывание $\mathrm{f}$. Далее, высказывание "$p$ есть ложное высказывание" переводится на язык нашей теории как $p\equiv \mathrm{f}$ - высказывание о том, что истинность $p$ совпадает истинностью лжи.
Таким образом, надо доказать синонимичность $p\equiv \mathrm{f}$ и $\neg p$. Это я уже проделывал немного в других терминах.

А теперь немного о том, как можно построить формальную теорию синонимов. Заметим следующую вещь: $\varphi$ синонимично $\psi$ тогда и только тогда, когда $\varphi\equiv\psi$ общезначимо.
Введем теперь аксиомы и правила:
Схемы аксиом.
I.$\varphi\equiv \varphi$
D.$\neg\neg \varphi\equiv \varphi$
T.$(\varphi\equiv\mathrm{t})\equiv\varphi$
N.$(\varphi\equiv\psi)\equiv(\neg\varphi\equiv\neg\psi)$
C.$(\varphi\equiv\psi)\equiv(\psi\equiv\varphi)$
T.$(\varphi\equiv\psi)\equiv((\varphi\equiv\xi)\equiv(\psi\equiv\xi))$
Правила:
E.$\dfrac{\varphi,\quad\varphi\equiv\psi}{\psi}$

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