Бирешетки и логика аргументации

Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

Бирешетки и логика аргументации

В.К. Финном в статье [Финн, 1996] был предложен вариант логики аргументации, в настоящее время широко применяемый для оценки непротиворечивости мнений респондентов. В оригинальном изложении для логики JA₄ использовались 4 истинностных значения, восходящие к ДСМ-методу: +1 (фактическая истина), -1 (фактическая ложь), 0 (противоречие) и t (неопределенность). Однако в настоящей статье будут использоваться стандартные обозначения для истинностных значений в логике Белнапа: вместо +1 будем использовать t (как сокращение от true), вместо -1 используем f (как сокращение от false), вместо 0 используем ? и вместо t используем ?.

В логике аргументации [Финн, 1996] предполагается наличие (конечного) множества A аргументов. Задается пара функций «аргументации»: g⁺: Vars > Power(A) (аргументов pro) и g^-: Vars > Power(A) (аргументов contra), которые отображают множества всех пропозициональных переменных во множество подмножеств множества A.

С помощью функций g⁺ и g ^- вычисляется оценка переменных по правилам:

v[p] = t тогда и только тогда, когда g⁺(p)?? и g^-(p)=?;

v[p] = f тогда и только тогда, когда g⁺(p)=? и g^-(p)??

v[p] = ? тогда и только тогда, когда g⁺(p)?? и g^-(p)??;

v[p] = ? тогда и только тогда, когда g⁺(p)=? и g^-(p)=?.

После этого используются истинностные таблицы из [Финн, 1996] для связок &, ?, ? и ¬ для того, чтобы вычислить значение сложной пропозициональной формулы.

Единственным выделенным истинностным значением в логике аргументации [Финн, 1996] является t.

Новый вариант пропозициональной логики аргументации использует пару функций «аргументации» g⁺: Props > Power(A) и g^-: Props > Power(A), заданных на множестве всех пропозициональных формул, на которые накладываются дополнительные ограничения.

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

Эквивалентность формул в исходном языке

Несводимость к логике аргументации В.К. Финна

Теорема. Новый вариант логики аргументации не сводится к классическому подходу к логике аргументации ни для каких истинностных таблиц.

Доказательство. Достаточно найти такое множество A аргументов и такие функции аргументации g₁⁺: Vars > Power(A), g₁^-: Vars > Power(A), g₂⁺: Vars > Power(A), g₂^-: Vars > Power(A), что v₁[p] = v₁[q] = v₂[p] = v₂[q], но v₁[p ? q] ? v₂[p ? q]. Пусть A ={a₁, a₂}, g₁⁺(p) = {a₁}, g₁^-(p) = {a₂}, g₁⁺(q) = {a₂}, g₁^-(q) = {a₁}, g₂⁺(p) = {a₁}, g₁^-(p) = {a₂}, g₁⁺(q) = {a₁}, g₁^-(q) = {a₂}. Легко проверить, что v₁[p] = v₁[q] = v₂[p] = v₂[q] = ?. Но g₁⁺(p?q) = g₁⁺(p) ? g₁⁺(Ф₂) = ? и g₁^-(p?q) = g₁^-(p) ? g₁^-(q) = A, т.е. v₁[p ? q] = f. С другой стороны, g₁⁺(p?q) = g₁⁺(p) ? g₁⁺(Ф₂) = {a₁} и g₁^-(p?q) = g₁^-(p) ? g₁^-(q) = {a₂}, т.е. v₁[p ? q] = ?.

Квазибулевы алгебры и DM4-эквивалентность

Квазибулева алгебра - это алгебра D = бD; ?, ?, ¬, 0, 1с, удовлетворяющая условиям:

идемпотентность x?x = x; x?x = x;

коммутативность x?y = y?x; x?y = y?x;

ассоциативность x?(y?z) = (x?y)?z; x?(y?z) = (x?y)?z;

дистрибутивность x?(y?z) = (x?y)?(x?z); x?(y?z) = (x?y)?(x?z);

поглощение x?(x?y) = x; x?(x?y) = x;

грани 1?x = 1; 0?x = 0;

законы де Моргана ¬(x?y) = (¬x)?(¬y); ¬(x?y) = (¬x)?(?¬y);

элементы 0 и 1 ¬1 = 0; ¬0 = 1;

инволюция ¬(¬x) = x.

Примером квазибулевой алгебры является алгебра DM4 = б{t, ?, ?, f}; ?, ?, ¬, f, tс, где связки заданы таблицами:

Теорема Расевой и Балыницкого-Бирули [Biaіynicki-Birula, 1957]. Всякая квазибулева алгебра является подрешеткой прямого произведения (DM4)^A решеток DM4 для некоторого множества A.

Доказательство этой теоремы можно также найти в книге [Rasiowa, 1974].

Две пропозициональные формулы (в языке ?, ?, ¬) называются DM4-эквивалентными, если при любой оценке переменных q: Vars > DM4 они принимают одинаковое значение.

Следствие. Две формулы DM4-эквивалентны тогда и только тогда, когда их равенство доказуемо в эквациональной теории квазибулевых алгебр.

Две пропозициональные формулы (в языке ?, ?, ¬) называются аргументно-эквивалентными, если при любых функциях аргументации g⁺: Props > Power(A) и g^-: Props > Power(A) они принимают одинаковое значение оценки v, порожденное по этим функциям аргументации.

Теорема. Две формулы аргументно-эквивалентны тогда и только тогда, когда они DM4-эквивалентны.

Доказательство. Закодируем (взаимно-однозначно) обе функции «аргументации» g⁺: Props > Power(A) и g^-: Props > Power(A) одной функцией g: Props > (DM4)^A правилом:

для каждого высказывания ? и каждого аргумента a?A

g(?) (a)= ? тогда и только тогда, когда aОg⁺(?) и aОg^-(?);

g(?) (a)= t тогда и только тогда, когда aОg⁺(?) и aПg^-(?);

g(?) (a)= f тогда и только тогда, когда aПg⁺(?) и aОg^-(?);

g(?) (a)= ? тогда и только тогда, когда aПg⁺(?) и aПg^-(?);

Легко проверить, что истинностная оценка v[?] = ?{g(?) (a): a?A}, где ? задается таблицей:

бирешетка аргументация тавтология

Следствие. Две формулы аргументно-эквивалентны тогда и только тогда, когда их равенство доказуемо в эквациональной теории квазибулевых алгебр.

Тавтологий в исходном языке нет, так как связки сохраняют истинностные значения ? и ?.

Аналитические таблицы для расширенного языка

Зададим в алгебре DM4 = б{t, ¤, ?, f}; ?, ?, ¬, f, tс, связки ?, ? и ? таблицами:

Метод аналитических таблиц для логики Белнапа

Хотя в логике аргументации [Финн, 1996] выделенным значением будет только t, рассмотрим, следуя [Fitting, 1989], множество {t,¤} выделенных истинностных значений в логике Белнапа DM4.

Лемма 1. Для множества Хинтикки S найдется такая оценка g: Vars > DM4, что:

для всех T? ? ? верно g[?] ? {t,?};

для всех ¬T? ? ? верно g[?] ? {t,?};

для всех F? ? ? верно g[?] ? {f,?};

для всех ¬F? ? ? верно g[?] ? {f,?}.

Доказательство. Зададим оценку g для каждой переменной p правилом:

g(p) = ?, если и только если Tp ? ? и Fp ? ?,

g(p) = t, если и только если Tp ? ? и Fp ? ?,

g(p) = f, если и только если Tp ? ? и Fp ? ?,

g(p) = ?, если и только если Tp ? ? и Fp ? ?.

С помощью индукции легко проверить требуемые свойства.

Лемма 2. Для множества маркированных формул W и такой оценки g: Vars > DM4, что

для всех T? ? ? верно g[?] ? {t,?};

для всех ¬T? ? ? верно g[?] ? {t,?};

для всех F? ? ? верно g[?] ? {f,?};

для всех ¬F? ? ? верно g[?] ? {f,?}.

найдется множество Хинтикки S, содержащее W.

Доказательство. Искомое множество S образуют маркированные подформулы формул из W, отобранные по правилу:

T?, если g[?] ? {t,?},

¬T?, если g[?] ? {t,?},

F?, если g[?] ? {f,?},

¬F?, если g[?] ? {f,?}.

Легко проверить, что S является искомым множеством Хинтикки.

Теорема. ¬|=4 ­, если и только если множество {T?: ? ? ?} ? {¬T?: ? ? ?} не содержится ни в каком множестве Хинтикки.

Доказательство. Если {T?: ? ? ?} ? {¬T?: ? ? ?} ? ?, то по Лемме 1 найдется оценка g: Vars > DM4, для которой для всех ? ? ? верно g[?] ? {t,?} и для всех ? ? ? верно g[?] ? {t,¤}. Следовательно, ?|=₄ ? не имеет места. Наоборот, если неверно, что ?|=₄ ?, то найдется такая оценка g, что всех ? ? ? верно g[?] ? {t,?} и для всех ? ? ? верно g[?] ? {t,?}. Применим к W = {T?: ? ? ?} ? {¬T?: ? ? ?} Лемму 2. Тогда {T?: ? ? ?} ? {¬T?: ? ? ?} содержится во множестве Хинтикки.

Для систематического перечисления всех множеств Хинтикки, содержащих данное множество маркированных формул W используются семантические таблицы [Г. Метакидес, А. Нероуд, 1998]. Ветвь семантической таблицы называется запертой, если она содержит одновременно формулу и ее отрицание (T? и ¬T? или F? и ¬F?).

Метод аналитических таблиц для логики аргументации

Формула Н называется {t} - следствием множества формул ¬, если для всякой такой истинностной оценки g: Vars > DM4, что для всех ? ? ? верно g[?] = t, верно и g[?] = t. Обозначается это через ?|=_t ?.

Теорема. ?|=_t ?, если и только если ни одно из множеств {T?: ? ? ?} ? {¬F?: ? ? ?} ? {¬T?} и {T?: ? ? ?} ? {¬F?: ? ? ?} ? {F?} не содержится ни в каком множестве Хинтикки.

Доказательство. Заметим, что одновременное наличие формул T? и ¬F? в множестве Хинтикки означает для соответствующей оценки, что g[?] ? D\{f,?} = {t}, т.е. g[?] = t. Аналогично, наличие ¬T? или F? означает, что g[?] ? {f,?}?{f,?}, т.е. g[?] ? t. Осталось использовать Леммы 1 и 2.

Список литературы

1. O. Arieli, A. Avron, Reasoning with logical bilattices // Journal of Logic, Language and Information, Vol. 5, №1 (1996), pp. 25-63.

2. N.D. Belnap, A useful four-valued logic // Modern Uses of Multiple-Valued Logic (J.M. Dunn and G. Epstein, eds.), D. Reidel, 1977, pp. 8-37.

A. Biaіynicki-Birula, Remarks on quasi-Boolean algebras // Bull. Ac. Pol. Sc., Cl. III, 5 (1957), pp. 615-619.

3. М.С. Fitting, Negation as refutation // Proc. Fourth Annual Symp. Logic in Computer Science, IEEE Computer Society Press, (1989), pp. 63-70.

4. H. Rasiowa, An algebraic approach to non-classical logics. Studies in Logic and Found. Math. Vol. 78, Amsterdam: North-Holland, 1974.

5. В.К. Финн, Об одном варианте логики аргументации // НТИ, сер. 2, №5-6 (1996), стр. 3-19.

6. Г. Метакидес, А. Нероуд, Принципы логики и логического программирования. М.: Факториал, 1998.

Размещено на Allbest.ru