Составляющие формальной системы. Язык формальной теории. Синтаксис формального языка, отношение между формулой и подформулой, сложные и атомарные формулы (стр. 12 )

Модальная логика — логика в которой кроме стандартных логических связок, переменных и/или предикатов есть модальности. Модальности бывают разные; наиболее распространены временны́е («когда-то в будущем», «всегда в прошлом», «всегда» и т. д.) и пространственные («здесь», «где-то», «близко» и т. д.). Например, модальная логика способна оперировать утверждениями типа «Москва всегда была столицей России», которые невозможно или сложно выразить в не модальном языке.

Кроме временных и пространственных модальностей есть и другие, например «известно, что» (логика знания) или «можно доказать, что» (логика доказуемости). Обычно для обозначения модального оператора используется и двойственный к нему : . Модальности: Алетические модальные понятия:

1) Логические: L — необходимо; M — возможно; С — случайно.

2) Фактические: — необходимо; — возможно; — случайно.

Формула А логики предикатов называется общезначимой, если она тождественна истинна на всякой области (на любой модели). Формулу А называют истинной в модели <G, K> этой формулы А в области D, если G сопоставляет А значение Т. А называют общезначимой в области D, если А истинна в каждой модели А в D. А называют выполнимой в D, если существует хотя бы одна модель А в D, в которой А истинна. А называют универсально общезначимой, если А общезначима в каждой непустой области.

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

Модальная система, которая обычно применяется при рассуждениях о знаниях, носит наз-нанис S5. Схемы ее аксиом выглядят следующим образом: l. La =) a 2.Lа=>р) =>(La->LP) 3.La => Lla 4.La=>L-1 La.

плюс привило вывода, позволяющее выводить La из a.

В первой аксиоме утверждается, что каждая известная формула также истинна. Вторая аксиома выражает логическое всезнание, тогда как третья и четвертая аксиомы вводят понятия соответственно позитивной и негативной интроспекции. Позитивная интроспекция означает, что агент точно представляет себе свои знания, т. е. ему известно, что он знает. Негативная интроспекция означает, что ему известна степень своего незнания, т. е, ему известно, чего он не знает. Если допустить возможность, что не все знания корректны, то первая из аксиом должна быть опущена, и результирующая система будет называться К4.

47.  Схема негативной интроспекции. Модальная система. Общезначимость в структурах.

Модальная логика — логика в которой кроме стандартных логических связок, переменных и/или предикатов есть модальности. Модальности бывают разные; наиболее распространены временны́е («когда-то в будущем», «всегда в прошлом», «всегда» и т. д.) и пространственные («здесь», «где-то», «близко» и т. д.). Например, модальная логика способна оперировать утверждениями типа «Москва всегда была столицей России», которые невозможно или сложно выразить в не модальном языке.

Формула А логики предикатов называется общезначимой, если она тождественна истинна на всякой области (на любой модели). Формулу А называют истинной в модели <G, K> этой формулы А в области D, если G сопоставляет А значение Т. А называют общезначимой в области D, если А истинна в каждой модели А в D. А называют выполнимой в D, если существует хотя бы одна модель А в D, в которой А истинна. А называют универсально общезначимой, если А общезначима в каждой непустой области.

Кванторы, которые выражают в том или ином виде временную (темпоральную) семантику, а именно: необходимость, возможность, будущность, прошлое, известность, допустимость, вера – получили название модальных. Эпистемическая логика или логика знания исследует модальности «знания» и «веры».

Каждая аксиомная схема для того или иного квантора при добавлении к аксиоматике исчисления предикатов порождает ту или иную модальную систему (исчисление). Модальная система 5 порождается аксиомной схемой негативной интроспекции.

Аксиома негативной интроспекции: . «Я вполне сознаю, что именно мне неизвестно». Негативная интроспекция означает, что агенту известна степень своего незнания, т. е, ему известно, чего он не знает. Эта аксиома является одной из основных аксиом эпистемической логики (остальные две: аксиома адекватности знания («Мои знания верны») и аксиома позитивной интроспекции («Я вполне представляю все, что мне известно»)). Здесь квадратом обозначается модальность «необходимо», ромбом – «возможно», причем .

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

48.  Язык временной логики с ветвящимся временем. Свойства темпорального отношения. Семантическая интерпретация кванторов временной логики с ветвящимся временем и для описания семантики возможных миров.

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

Введём следующие сокращения. Рассмотрим свойство отношение непосредственного следования интервалов. Запись (i;j) читается как: «интервал i непосредственно предшествует интервалу j». Ниже приведена зависимость некоторого предиката от значений переменной t. являющихся точечными интервалами.

Кванторы: Кванторы, которые выражают в том или ином виде временную (темпоральную) семантику, а именно: необходимость, возможность, будущность (будущее), прошлое, известность, допустимость, вера – получили называние модальных. Модальные кванторы могут обладать следующими свойствами. Модальные кванторы всегда двойственны, т. е. модальный квантор имеет всегда двойственный ему.

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

Модальная система T для модального квантора порождается «аксиомной схемой знания».

Модальная система 4 для модального квантора порождается «аксиомной схемой позитивной интроспекции».

Модальная система 5 для модального квантора порождается «аксиомной схемой позитивной интроспекции».

Можно рассматривать модальные системы, являющиеся комбинациями вышеперечисленных. Так, например, модальные системы 4KT и 45KT имеют обозначения S4 и S5 соответственно. Во всех этих системах наряду с правилами вывода исчисления предикатов используется следующее модальное правило вывода.

49.  Язык временной логики с ветвящимся временем. Аксиоматика.

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

Свойство отношения строгого порядка.

Свойство линейности в прошлое.

Свойство связности.

Семантика временных кванторов в логике ветвящегося времени определяется следующим образом. Вводится понятие формулы, общезначимой в модели, задаваемой тремя величинами σ,χ,T которые соответственно являются: временной моделью T, элементом множества всех ветвей T()BranchesT временной модели и микромоделью (состоянием) – элементом носителя модели T. Фактически эти три величины соответствуют неявным переменными в формуле α, обозначающей временной (зависящий от значений этих переменных) предикат.

Задана некоторая функция ϕ, которая позволяет вычислить общезначимость любой формулы α, принадлежащей множеству атомарных формул А, в микромодели Aχ.