Связь булевых алгебр с исчислением высказываний

[Свободный Художник]

Каким образом можно наиболее просто и понятно описать связь булевых алгебр с исчислением высказываний?
(под “исчислением высказываний” понимается классическое исчисление высказываний).

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

[Профессор Снэйп]

Свободный Художник писал(а):

Каким образом можно наиболее просто и понятно описать связь булевых алгебр с исчислением высказываний?
(под “исчислением высказываний” понимается классическое исчисление высказываний).

"Связь" --- это слишком расплывчато. Вас конструкция алгебры Линденбаума интересует или что-то другое?

Свободный Художник писал(а):

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

Да ну какая разница, какое из дуальных понятий использовать?

Вероятно, какие-то исторические причины. Мне они неведомы.

[Свободный Художник]

Профессор Снэйп писал(а):

Свободный Художник писал(а):

Каким образом можно наиболее просто и понятно описать связь булевых алгебр с исчислением высказываний?
(под “исчислением высказываний” понимается классическое исчисление высказываний).

"Связь" --- это слишком расплывчато. Вас конструкция алгебры Линденбаума интересует или что-то другое?

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

[luitzen]

Профессор Снэйп писал(а):

Свободный Художник писал(а):

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

Да ну какая разница, какое из дуальных понятий использовать?

Вероятно, какие-то исторические причины. Мне они неведомы.

Наверное, это потому, что логики больше любят истину, чем ложь . А фильтр — он как-то поближе к понятию «истина», чем идеал: $1 \in F$.

[Свободный Художник]

Алгебра Линденбаума-Тарского имеет “синтаксический” смысл.
Но интересна также изоморфная ей “семантическая” булева алгебра.

Определить последнюю проще всего, наверное, если воспользоваться конструкцией Г. Биркгофа с “полярностями”, адаптировав ее для случая пропозициональной логики.
Биркгоф Г. Теория решеток.
Пер. с англ., М.: "Наука", 1984, сс. 163 — 165.
http://www.px-pict.com/9/4/4.html

Т. е. в качестве класса $J$ взять язык исчисления высказываний, в качестве класса $I$ взять множество всех интерпретаций этого языка, а в качестве “спаривающего” отношения $\rho$ взять отношение $\vDash$ из теории моделей.
Для любой формулы $\varphi$ языка $J$ и для любой интерпретации $i \in I$ обычным образом читаем выражение $i \vDash \varphi$ как “формула $\varphi$ истинна в интерпретации $i$” (т. е. интерпретация $i$ является моделью для $\varphi$).

Кто-нибудь знает, где найти информацию о подобной трактовке логических исчислений (через “полярности”). Кое-что я смог обнаружить здесь:
http://en.wikipedia.org/wiki/Galois_connection
(подраздел Syntax and semantics на этой странице).

[Свободный Художник]

Обычно высказывания определяют как предложения, о которых можно сказать, что они либо истинны, либо ложны.
Но это “семантическое” определение.

А как дать синтаксическое определение высказыванию? Нечто типа такого, которое дают Г. Дж. Кейслер, Ч. Ч. Чэн:
“Неважно, как представлять себе высказывания; существенно лишь, что доказывать любые свойства высказываний можно с помощью одной только индукции”.
http://www.px-pict.com/9/6/2/3/2/2/1.html

Ведь если разобраться, “исчисление высказываний” само по себе является чисто синтаксическим образованием.

[luitzen]

Т. е. Вы хотите придумать некую «семантику» для определения правильно построенной формулы? Ну, не знаю…

Или у Вас есть желание сделать понятие «высказывание» в каком-то смысле производным и частным? Насколько помню, кто-то из львовско-варшавской школы развивал нечто под названием «теория семантических категорий». Но это вроде бы тоже был голый синтаксический формализм начального уровня; какой-то либо «семантики» к нему (тем более, связанной с булевыми алгебрами) я не знаю.

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

[Свободный Художник]

luitzen писал(а):

Т. е. Вы хотите придумать некую «семантику» для определения правильно построенной формулы?

Нет, я вот что имею в виду.
Обычно под “исчислением” подразумевают формальный язык + правила вывода, а под формальным языком – алфавит + правила образования. Задание исчисления позволяет построить множество правильно построенных формул и определить на них отношение выводимости.
Все это -- чисто синтаксические вещи, сами по себе не требующие каких-то дополнительных семантических рассмотрений.

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

И алгебра Линденбаума-Тарского данного формального исчисления (не обязательно “исчисления высказываний”), о которой упоминал выше Профессор Снэйп, тоже при своем построении не требует апелляций к “истинности” или “ложности”.
Так что, по-видимому, чисто синтаксическое определение “высказываний” могло бы быть таким:
это правильно построенные формулы исчисления, алгебра Линденбаума-Тарского которого является булевой алгеброй.

Добавлено спустя 2 часа 3 минуты 21 секунду:

Придумал контрпример для своего определения.
Рассмотрим формальное исчисление с единственной связкой $\Rightarrow$, со схемами аксиом $(A_1) - (A_3)$:
$(A_1) \;\;\; (A \Rightarrow (B \Rightarrow A)),$
$(A_2) \;\;\; ((A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))),$
$(A_3) \;\;\; (((A \Rightarrow B) \Rightarrow A) \Rightarrow A),$

и с правилом “модус поненс”: (из пары формул $A \Rightarrow B$ и $A$ выводима формула $B$) в качестве единственного правила вывода.

(такое исчисление, как известно, формализует чисто импликативный фрагмент классического исчисления высказываний)

Это исчисление, конечно, имеет алгебру Линденбаума-Тарского, но эта алгебра не является булевой алгеброй.

[luitzen]

Вот какой полусонный вопрос про «семантику для правильно построенных формул» придумал.

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

Пример. Из формулы $b\to (a\lor \neg a)$ получается «структурная формула» $BpBpU\gamma$. Здесь $p$ — «обобщённая переменная», $\gamma$ — «хвост».

Будем воспринимать полученную строку как переменную («хвост») с последовательно навешанными на неё унарными операторами. Структурную формулу из рассмотренного примера можно было бы записать как $B(p(B(p(U(\gamma)))))$. Ясно, что есть и другие строки такого вида — не являющиеся структурными формулами каких-либо ППФ ИВ.

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

[Свободный Художник]

luitzen писал(а):

Для всякой формулы построим её запись в польской нотации ...

Вы поклонник польской школы логики?
http://en.wikipedia.org/wiki/Lwow-Warsaw_School_of_Logic

Я сам поклонник.
Но вот насчет “польской записи” логических формул… Не могли бы Вы пояснить, какие преимущества мы получим, если станем записывать формулы пропозиционального исчисления в польской нотации?

Эта нотация, вроде, не прижилась в логике. Хотя заняла свое место в Computer Science:
http://en.wikipedia.org/wiki/Jan_%C5%81ukasiewicz
http://en.wikipedia.org/wiki/Polish_notation

[luitzen]

Свободный художник писал(а):

Не могли бы Вы пояснить, какие преимущества мы получим, если станем записывать формулы пропозиционального исчисления в польской нотации?

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

[Свободный Художник]

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

Но мне нужно вспомнить подробности, поскольку занимался я этим уже давно. Завтра, если будет время, гляну в библиотеке. Ключевые работы здесь следующие:
Lambec J. The mathematics of sentence structure//Amer. Math. Monthly 65 (1958), 154 – 170;

Buszkowski W. Compatibility of a categorial grammar with an associated category system//Zeitschr. f. math. Logik und Grundlagen d. Math. Bd. 28. S. 229-237 (1982);

Zielonka W. Axiomatizability of Ajdukiewicz-Lambek calculus by means of cancellation schemes//Zeitschr. f. math. Logik und Grundlagen d. Math. Bd. 27. S. 215-224 (1981).

[Чудо-в-перьях]

Расеву и Сикорского можно почитать

[Чудо-в-перьях]

"Математика метаматематики" ))

[Свободный Художник]

Свободный Художник" в сообщении #213405 писал(а):

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

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

Чудо-в-перьях" в сообщении #213511 писал(а):

Расеву и Сикорского можно почитать

Мне еще больше нравится ее продолжение
Rasiowa H.
An Algebraic Approach to Non - Classical Logics.
Amsterdam, North - Holland publ. co, 1974.

Оно специально “заточено” на рассмотрение пропозициональных исчислений (в том числе и классических, рассматриваемых как предельные случаи).
-----------------------

Кстати говоря, определение формул языка пропозиционального исчисления с формальной точки зрения ничем не отличается от определения термов (в первопорядковой теории).
Но термы (согласно теории семантических категорий Лесневского) принадлежат категории “имен”, а не “предложений”:
http://www.px-pict.com/9/6/6/6/2.html

Чтобы рассматривать п.п.ф. исчисления высказываний как относящиеся к категории все же “предложений”, мы можем, наверное, без всякого ущерба видеть в них замаскированные тождества эквациональной теории для булевых алгебр специального вида $t = 1$, где $t$ -- терм в сигнатуре булевой алгебры, $1$ -- единичный элемент булевой алгебры.

Тождества эквациональной теории – они без проблем принадлежат к категории именно “предложений”.

-- Пт май 15, 2009 23:02:25 --

Свободный Художник в сообщении #200169 писал(а):

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

Нашел-таки в сети место о связи формул классического пропозиционального исчисления с тождествами эквациональной теории булевых алгебр:
http://en.wikipedia.org/wiki/Propositional_calculus
(раздел “Equivalence to equational logics” на этой странице)

О правилах дедукции в эквациональных теориях можно здесь посмотреть:
http://mathworld.wolfram.com/EquationalLogic.html