Моноидальная t-нормальная логика
В математической логике , моноидальная логика основанная на t-норме (или сокращенно MTL ), логика непрерывных слева t-норм , является одной из нечетких логик t-нормы . Она принадлежит к более широкому классу субструктурных логик или логик резидуальных решеток ; [1] Хёле он расширяет логику коммутативных ограниченных целочисленных резидуированных решеток (известную как моноидальная логика Оно , FL ew или интуиционистская логика без сжатия) с помощью аксиомы прелинейности.
Мотивация
[ редактировать ]В нечеткой логике вместо того, чтобы рассматривать утверждения как истинные или ложные, мы связываем каждое утверждение с числовой достоверностью этого утверждения. По соглашению доверительные интервалы варьируются в пределах единичного интервала. , где максимальная достоверность соответствует классическому понятию истинной и минимальной достоверности соответствует классическому понятию ложного.
Т-нормы — это двоичные функции на действительном единичном интервале [0, 1], которые в нечеткой логике часто используются для представления соединительной связки ; если это уверенность, которую мы приписываем утверждениям и соответственно, тогда используется t-норма рассчитать уверенность приписано составному высказыванию ' и '. Т-норма должен удовлетворять свойствам
- коммутативность ,
- ассоциативность ,
- монотонность — если и затем ,
- и имеющий 1 в качестве идентификационного элемента .
Примечательно, что в этом списке отсутствует свойство идемпотентности. ; самое близкое, что можно получить, это то, что . Быть менее уверенным в себе может показаться странным. и ', чем просто , но обычно мы хотим, чтобы уверенность в комбинированном ' и ' быть меньше, чем уверенность в и уверенность в , а затем порядок по монотонности требует . Другими словами, t-норма может учитывать только доверительные отношения как числа, а не причины, которые могут лежать в основе приписывания этих доверительных отношений; таким образом, он не может лечить ' и 'в отличие от' и , где мы одинаково уверены в обоих».
Потому что символ поскольку его использование в теории решеток очень тесно связано со свойством идемпотентности, может быть полезно переключиться на другой символ для соединения, который не обязательно является идемпотентным. В традиции нечеткой логики иногда используют для этого «сильного» союза, но эта статья следует традиции субструктурной логики использования для сильного союза; таким образом это уверенность, которую мы приписываем утверждению (все еще читаю ' и ', возможно, с «сильным» или «мультипликативным» в качестве уточнения «и»).
Формализовав союз , хочется продолжить с другими связками. Один из подходов к этому — представить отрицание как карту, меняющую порядок. , затем определяя оставшиеся связки, используя законы Де Моргана , материальную импликацию и тому подобное. Проблема при этом заключается в том, что результирующая логика может иметь нежелательные свойства: она может быть слишком близка к классической логике или, если не наоборот, не поддерживать ожидаемые правила вывода . Альтернативой, которая делает последствия различных выборов более предсказуемыми, является продолжение импликации. в качестве второй связки: в целом это наиболее распространенная связка в аксиоматизациях логики, и она имеет более тесную связь с дедуктивными аспектами логики, чем большинство других связок. Доверительный аналог импликационной связки фактически может быть определена непосредственно как остаток t-нормы.
Логическая связь между конъюнкцией и импликацией обеспечивается таким фундаментальным явлением, как правило вывода modus ponens. : от и следует . В случае нечеткой логики это более строго записывается как , потому что это ясно показывает, что наша уверенность в предпосылках здесь заключается в том, что в , а не те, что в и отдельно. Итак, если и наша уверенность в и соответственно, тогда это искомая уверенность в , и это совокупная уверенность в . Мы требуем, чтобы
поскольку наша уверенность для не должно быть меньше нашего доверия в заявлении откуда логически следует. Это ограничивает искомую уверенность , и один подход для поворота в бинарную операцию, например было бы сделать его как можно большим, соблюдая при этом эту границу:
- .
принимая дает , поэтому верхняя грань всегда принадлежит непустому ограниченному множеству и, следовательно, корректно определена. Для общей t-нормы остается возможность, что имеет скачок при , в этом случае может выйти строго больше, чем Несмотря на то определяется как наименьшая верхняя граница это удовлетворяет ; Чтобы предотвратить это и обеспечить ожидаемый результат строительных работ, мы требуем, чтобы t-норма является непрерывным слева . Таким образом, остаток непрерывной слева t-нормы можно охарактеризовать как самую слабую функцию, которая делает нечеткий modus ponens действительным, что делает его подходящей функцией истинности для применения в нечеткой логике.
Более алгебраически мы говорим, что операция является остатком t-нормы если для всех , , и это удовлетворяет
- тогда и только тогда, когда .
Эта эквивалентность числовых сравнений отражает эквивалентность следствий.
- тогда и только тогда, когда
существует, потому что любое доказательство из помещения можно превратить в доказательство из помещения делая дополнительный шаг введения импликации , и наоборот, любое доказательство из помещения можно превратить в доказательство из помещения выполнив дополнительный шаг устранения последствий . Непрерывность слева t-нормы является необходимым и достаточным условием для сохранения этой связи между соединением t-нормы и ее остаточной импликацией.
Функции истинности дальнейших пропозициональных связок могут быть определены с помощью t-нормы и ее остатка, например, остаточного отрицания. Таким образом, непрерывная слева t-норма, ее остаток и функции истинности дополнительных пропозициональных связок (см. раздел «Стандартная семантика» ниже) определяют значения истинности сложных пропозициональных формул в [0, 1]. Формулы, результат которых всегда равен 1, тогда называются тавтологиями относительно данной непрерывной слева t-нормы. или тавтологии. Набор всего тавтологии называется логикой t-нормы поскольку эти формулы представляют собой законы нечеткой логики (определяемые t-нормой), которые выполняются (до степени 1) независимо от степеней истинности атомарных формул . Некоторые формулы являются тавтологиями относительно всех непрерывных слева t-норм: они представляют собой общие законы пропозициональной нечеткой логики, которые не зависят от выбора конкретной непрерывных слева t-норм. Эти формулы образуют логику MTL, которую, таким образом, можно охарактеризовать как логику непрерывных слева t-норм. [2]
Синтаксис
[ редактировать ]Язык
[ редактировать ]Язык пропозициональной логики MTL состоит из счетного числа пропозициональных переменных и следующих примитивных логических связок :
- Импликация ( двоичный )
- Сильное соединение (двоичный). Знак & является более традиционным обозначением сильной связи в литературе по нечеткой логике, тогда как обозначение следует традиции субструктурной логики.
- Слабое соединение (двоичный), также называемый решеточной конъюнкцией (поскольку в алгебраической семантике он всегда реализуется решеточной операцией встречи ). В отличие от BL и более сильных нечетких логик, слабая конъюнкция не поддается определению в MTL и должна быть включена в число примитивных связок.
- Нижний ( нулевой — пропозициональная константа ; или являются общими альтернативными токенами, а ноль - общим альтернативным именем для пропозициональной константы (поскольку константы дно и ноль субструктурной логики совпадают в MTL).
Ниже приведены наиболее распространенные определяемые логические связки:
- Отрицание ( унарный ), определяемый как
- Эквивалентность (двоичный), определяемый как
- В MTL определение эквивалентно
- (Слабая) дизъюнкция (двоичный), также называемый решеточной дизъюнкцией (поскольку он всегда реализуется решеточной операцией соединения в алгебраической семантике), определяемый как
- Вершина (нулевой), также называемый единицей и обозначаемый или (поскольку константы top и ноль субструктурной логики совпадают в MTL), определяемые как
Правильно составленные формулы MTL определяются, как обычно, в логике высказываний . Чтобы сохранить круглые скобки, обычно используется следующий порядок приоритета:
- Унарные связки (связываются наиболее тесно)
- Бинарные связки, кроме импликации и эквивалентности
- Импликация и эквивалентность (наиболее слабая связь)
Аксиомы
[ редактировать ]Система вывода в стиле Гильберта для MTL была представлена Эстевой и Годо (2001). Его единственное правило вывода — modus ponens :
- от и вывести
Ниже приведены схемы его аксиом :
Традиционная нумерация аксиом, приведенная в левом столбце, получена из нумерации аксиом BL Гаека базовой нечеткой логики . [3] Аксиомы (MTL4a)–(MTL4c) заменяют аксиому делимости (BL4) BL. Аксиомы (MTL5a) и (MTL5b) выражают закон невязки , а аксиома (MTL6) соответствует условию предлинейности . Было показано, что аксиомы (MTL2) и (MTL3) исходной аксиоматической системы являются избыточными (Chvalovsky, 2012) и (Cintula, 2005). Показано, что все остальные аксиомы независимы (Хваловский, 2012).
Семантика
[ редактировать ]Как и в других пропозициональных нечетких логиках с t-нормой , алгебраическая семантика для MTL преимущественно используется с тремя основными классами алгебр , относительно которых логика является полной :
- Общая семантика , сформированная из всех MTL-алгебр — то есть всех алгебр, для которых логика верна.
- Линейная семантика , состоящая из всех линейных MTL-алгебр, то есть всех MTL-алгебр, решетки порядок которых линейный.
- Стандартная семантика , образованная из всех стандартных MTL-алгебр — то есть всех MTL-алгебр, редукцией решетки которых является действительный единичный интервал [0, 1] обычного порядка; они однозначно определяются функцией, интерпретирующей сильную конъюнкцию, которая может быть любой непрерывной слева t-нормой
Общая семантика
[ редактировать ]MTL-алгебры
[ редактировать ]Алгебры, для которых верна логика MTL, называются MTL-алгебрами. Их можно охарактеризовать как предлинейные коммутативные ограниченные целочисленные вычетные решетки. Более подробно, алгебраическая структура является MTL-алгеброй, если
- представляет собой ограниченную решетку с верхним элементом 0 и нижним элементом 1
- является коммутативным моноидом
- и образуют сопряженную пару , т. е. тогда и только тогда, когда где – порядок решетки для всех x , y и z в , ( условие невязки )
- выполняется для всех x и y в L ( условие предварительной линейности )
Важными примерами MTL-алгебр являются стандартные MTL-алгебры на вещественном единичном интервале [0, 1]. Дальнейшие примеры включают все булевы алгебры , все линейные алгебры Гейтинга (обе с ), все MV-алгебры , все BL -алгебры и т. д. Поскольку условие вычетности эквивалентно выражается тождествами, [4] MTL-алгебры образуют разновидность .
Интерпретация логики MTL в MTL-алгебрах
[ редактировать ]Связки MTL интерпретируются в MTL-алгебрах следующим образом:
- Сильная конъюнкция моноидальной операцией
- Последствия операции называется остатком ( который )
- Слабая конъюнкция и слабая дизъюнкция решеточными операциями. и соответственно (обычно обозначаются теми же символами, что и связки, если не может возникнуть путаницы)
- Константы истинности ноль (вверху) и единица (внизу) константами 0 и 1.
- Связка эквивалентности интерпретируется операцией определяется как
- В силу условия предлинейности это определение эквивалентно тому, которое использует вместо таким образом
- Отрицание интерпретируется определяемой операцией
При такой интерпретации связок любая оценка e v пропозициональных переменных в L однозначно распространяется на оценку e всех правильно построенных формул MTL согласно следующему индуктивному определению (которое обобщает условия истинности Тарского ) для любых формул A , B , и любая пропозициональная переменная p :
Неформально, значение истинности 1 представляет полную истину, а значение истинности 0 представляет полную ложность; промежуточные значения истинности представляют собой промежуточные степени истины. Таким образом, формула считается полностью истинной при вычислении e, если e ( A ) = 1. Формула A называется истинной в MTL-алгебре L, если она полностью истинна при всех оценках в L , то есть если e ( A ) = 1 для всех оценок e в L . Некоторые формулы (например, p → p ) справедливы в любой MTL-алгебре; они называются тавтологиями MTL.
Понятие глобального следствия (или: глобального следствия ) определяется для MTL следующим образом: набор формул Γ влечет за собой формулу A (или: A является глобальным следствием Γ) в символах если для любой оценки e в любой MTL-алгебре, когда e ( B ) = 1 для всех формул B в Γ, то также e ( A ) = 1. Неформально глобальное отношение следствий представляет собой передачу полной истины в любой MTL-алгебре. алгебра истинностных значений.
Общие теоремы о корректности и полноте
[ редактировать ]Логика MTL является корректной и полной по отношению к классу всех MTL-алгебр (Esteva & Godo, 2001):
- Формула доказуема в MTL тогда и только тогда, когда она справедлива во всех MTL-алгебрах.
Понятие MTL-алгебры фактически определено таким образом, что MTL-алгебры образуют класс всех алгебр, для которых логика MTL верна. Кроме того, справедлива сильная теорема полноты : [5]
- Формула A является глобальным следствием в MTL набора формул Γ тогда и только тогда, когда A выводима из Γ в MTL.
Линейная семантика
[ редактировать ]Подобно алгебрам для других нечетких логик, [6] MTL-алгебры обладают следующим свойством линейной подпрямой декомпозиции :
- Любая MTL-алгебра является подпрямым произведением линейно упорядоченных MTL-алгебр.
( Подпрямое произведение — это подалгебра прямого произведения, что все проекционные отображения сюръективны такая , . MTL-алгебра линейно упорядочена, порядок ее решетки линейный если .)
Вследствие свойства линейной подпрямой декомпозиции всех MTL-алгебр справедлива теорема о полноте в отношении линейных MTL-алгебр (Esteva & Godo, 2001):
- Формула доказуема в MTL тогда и только тогда, когда она справедлива во всех линейных MTL-алгебрах.
- Формула A выводится в MTL из множества формул Γ тогда и только тогда, когда A является глобальным следствием во всех линейных MTL-алгебрах Γ.
Стандартная семантика
[ редактировать ]Стандартными называются те MTL-алгебры, редукцией решетки которых является действительный единичный интервал [0, 1]. Они однозначно определяются вещественной функцией, интерпретирующей сильную конъюнкцию, которая может быть любой непрерывной слева t-нормой. . Стандартная MTL-алгебра, определяемая непрерывной слева t-нормой обычно обозначается В представлена остатком импликация слабая конъюнкция и дизъюнкция соответственно минимуму и максимуму, а константы истинности ноль и единица соответственно действительным числам 0 и 1.
Логика MTL полна относительно стандартных MTL-алгебр; этот факт выражается стандартной теоремой о полноте (Jenei & Montagna, 2002):
- Формула доказуема в MTL тогда и только тогда, когда она справедлива во всех стандартных MTL-алгебрах.
Поскольку MTL полна относительно стандартных MTL-алгебр, определяемых непрерывными слева t-нормами, MTL часто называют логикой непрерывных слева t-норм (аналогично тому, как BL — логика непрерывных t-норм ).
Библиография
[ редактировать ]- Хайек П., 1998, Метаматематика нечеткой логики . Дордрехт: Клювер.
- Эстева Ф. и Годо Л., 2001, «Логика, основанная на моноидальной t-норме: к логике непрерывных слева t-норм». Нечеткие множества и системы 124 : 271–288.
- Дженей С. и Монтанья Ф., 2002, «Доказательство стандартной полноты моноидальной логики Эстевы и Годо MTL». Студия Логика 70 : 184–192.
- Оно, Х., 2003, «Субструктурная логика и остаточные решетки — введение». В Ф. В. Хендриксе, Дж. Малиновском (ред.): Тенденции в логике: 50 лет Studia Logica, Тенденции в логике 20 : 177–212.
- Синтула П., 2005, «Краткая заметка: Об избыточности аксиомы (A3) в BL и MTL». Мягкие вычисления 9 : 942.
- Синтула П., 2006, «Слабо импликативная (нечеткая) логика I: основные свойства». Архив математической логики 45 : 673–704.
- Хваловский К., 2012, « О независимости аксиом в BL и MTL ». Нечеткие множества и системы 197 : 123–129, дои : 10.1016/j.fss.2011.10.018 .
Ссылки
[ редактировать ]- ^ Оно (2003).
- ^ Предположение Эстевы и Годо, представивших логику (2001), доказано Дженеем и Монтаньей (2002).
- ^ Хайек (1998), Определение 2.2.4.
- ^ Доказательство леммы 2.3.10 в Hájek (1998) для BL-алгебр можно легко адаптировать для работы и с MTL-алгебрами.
- ^ Общее доказательство сильной полноты по отношению ко всем L -алгебрам для любой слабо импликативной логики L (включая MTL) можно найти в Cintula (2006).
- ^ Цинтула (2006).