Логика зависимости - Dependence logic

Логика зависимости логический формализм, созданный Йоуко Вяэнянен,^[1] что добавляет атомы зависимости на язык логика первого порядка. Атом зависимости - это выражение вида ${\displaystyle =\!\!(t_{1}\ldots t_{n})}$, куда ${\displaystyle t_{1}\ldots t_{n}}$ являются терминами, и соответствует утверждению, что значение ${\displaystyle t_{n}}$ является функционально зависимый о ценностях ${\displaystyle t_{1}\ldots t_{n-1}}$.

Логика зависимости - это логика несовершенной информации, подобно логика квантора ветвления или же независимая логика: другими словами, это теоретико-игровая семантика может быть получена из логики первого порядка путем ограничения доступности информации для игроков, что позволяет создавать нелинейно упорядоченные модели зависимости и независимости между переменными. Однако логика зависимости отличается от этой логики тем, что отделяет понятия зависимости и независимости от понятия количественной оценки.

Синтаксис

Синтаксис логики зависимости является расширением синтаксиса логики первого порядка. За фиксированный подпись σ = (S_func, S_rel, ar) множество всех логических формул правильно сформированной зависимости определяется по следующим правилам:

Условия

Определены термины в логике зависимости точно так же, как в логике первого порядка.

Атомарные формулы

В логике зависимости есть три типа атомарных формул:

1. А реляционный атом является выражением формы ${\displaystyle Rt_{1}\ldots t_{n}}$ для любого n-арного отношения ${\displaystyle \!R}$ в нашей подписи и на любое количество условий ${\displaystyle t_{1}\ldots t_{n}}$;
2. An атом равенства является выражением формы ${\displaystyle t_{1}=t_{2}}$, для любых двух условий ${\displaystyle t_{1}}$ и ${\displaystyle t_{2}}$;
3. А атом зависимости является выражением формы ${\displaystyle =\!\!(t_{1}\ldots t_{n})}$, для любого ${\displaystyle n\in \mathbb {N} }$ и для любого количества сроков ${\displaystyle t_{1}\ldots t_{n}}$.

Ничто иное не является атомарной формулой логики зависимости.

Атомы отношения и равенства также называют атомы первого порядка.

Сложные формулы и предложения

Для фиксированной сигнатуры σ множество всех формул ${\displaystyle \phi }$ логики зависимости и соответствующих им наборов свободных переменных ${\displaystyle {\mbox{Free}}(\phi )}$ определяются следующим образом:

1. Любая атомная формула ${\displaystyle \phi }$ формула, а ${\displaystyle {\mbox{Free}}(\phi )}$ - множество всех входящих в него переменных;
2. Если ${\displaystyle \phi }$ это формула, так это ${\displaystyle \lnot \phi }$ и ${\displaystyle {\mbox{Free}}(\lnot \phi )={\mbox{Free}}(\phi )}$;
3. Если ${\displaystyle \phi }$ и ${\displaystyle \psi }$ формулы, так же ${\displaystyle \phi \vee \psi }$ и ${\displaystyle {\mbox{Free}}(\phi \vee \psi )={\mbox{Free}}(\phi )\cup {\mbox{Free}}(\psi )}$;
4. Если ${\displaystyle \phi }$ это формула и ${\displaystyle x}$ переменная, ${\displaystyle \exists x\phi }$ также формула и ${\displaystyle {\mbox{Free}}(\exists v\phi )={\mbox{Free}}(\phi )\backslash \{v\}}$.

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

Формула ${\displaystyle \phi }$ такой, что ${\displaystyle {\mbox{Free}}(\phi )=\emptyset }$ это приговор логики зависимости.

Связь и универсальная количественная оценка

В приведенном выше представлении синтаксиса логики зависимости, конъюнкции и универсальная количественная оценка не рассматриваются как примитивные операторы; скорее, они определены в терминах дизъюнкции и отрицания и экзистенциальная количественная оценка соответственно, с помощью Законы Де Моргана.

Следовательно, ${\displaystyle \phi \wedge \psi }$ используется как сокращение для ${\displaystyle \lnot (\lnot \phi \vee \lnot \psi )}$, и ${\displaystyle \forall x\phi }$ используется как сокращение для ${\displaystyle \lnot (\exists x(\lnot \phi ))}$.

Семантика

В командная семантика для логики зависимости - это вариант Уилфрид Ходжес 'композиционная семантика для IF логика.^[2][3] Существует эквивалентная теоретико-игровая семантика для логики зависимости, как с точки зрения несовершенные информационные игры и с точки зрения идеальных информационных игр.

Команды

Позволять ${\displaystyle \!{\mathcal {A}}=(A,\sigma ,I)}$ быть структура первого порядка и разреши ${\displaystyle V=\{v_{1}\ldots v_{n}\}}$ - конечный набор переменных. Затем команда закончилась А с доменом V это набор заданий над А с доменом V, то есть набор функций μ из V к А.

Может быть полезно представить такую ​​команду как отношение к базе данных с атрибутами ${\displaystyle v_{1}\ldots v_{n}}$ и только с одним типом данных, соответствующим домену А структуры: например, если команда Икс состоит из четырех заданий ${\displaystyle \!\mu _{1}\ldots \mu _{4}}$ с доменом ${\displaystyle \!\{v_{1},v_{2},v_{3}\}}$ то можно представить его как отношение

${\displaystyle {\begin{array}{c|ccc}&v_{1}&v_{2}&v_{3}\\\hline \mu _{1}&\mu _{1}(v_{1})&\mu _{1}(v_{2})&\mu _{1}(v_{3})\\\mu _{2}&\mu _{2}(v_{1})&\mu _{2}(v_{2})&\mu _{2}(v_{3})\\\mu _{3}&\mu _{3}(v_{1})&\mu _{3}(v_{2})&\mu _{3}(v_{3})\\\mu _{4}&\mu _{4}(v_{1})&\mu _{4}(v_{2})&\mu _{4}(v_{3})\end{array}}}$

Положительное и отрицательное удовлетворение

Семантика команды может быть определена в терминах двух отношений ${\displaystyle {\mathcal {T}}}$ и ${\displaystyle {\mathcal {C}}}$ между структурами, командами и формулами.

Учитывая структуру ${\displaystyle {\mathcal {A}}}$, команда ${\displaystyle X}$ над ним и формулу логики зависимости ${\displaystyle \phi }$ чей свободные переменные содержатся в области ${\displaystyle X}$, если ${\displaystyle ({\mathcal {A}},X,\phi )\in {\mathcal {T}}}$ мы говорим, что ${\displaystyle X}$ это козырный за ${\displaystyle \phi }$ в ${\displaystyle {\mathcal {A}}}$, и мы пишем, что ${\displaystyle {\mathcal {A}}\models _{X}^{+}\phi }$; и аналогично, если ${\displaystyle ({\mathcal {A}},X,\phi )\in {\mathcal {C}}}$ мы говорим, что ${\displaystyle X}$ это шпажка за ${\displaystyle \phi }$ в ${\displaystyle {\mathcal {A}}}$, и мы пишем, что ${\displaystyle {\mathcal {A}}\models _{X}^{-}\phi }$.

Если ${\displaystyle {\mathcal {A}}\models _{X}^{+}\phi }$ можно также сказать, что ${\displaystyle \phi }$ является положительно доволен к ${\displaystyle X}$ в ${\displaystyle {\mathcal {A}}}$, а если вместо этого ${\displaystyle {\mathcal {A}}\models _{X}^{-}\phi }$ можно сказать что ${\displaystyle \phi }$ является отрицательно доволен к ${\displaystyle X}$ в ${\displaystyle {\mathcal {A}}}$.

Необходимость отдельно рассматривать положительное и отрицательное удовлетворение является следствием того факта, что в логике зависимости, как и в логике кванторы ветвления или в IF логика, закон исключенного третьего не выполняется; в качестве альтернативы, можно предположить, что все формулы находятся в отрицательной нормальной форме, используя отношения Де Моргана для определения универсальной количественной оценки и конъюнкции из экзистенциальной количественной оценки и дизъюнкции соответственно, и рассматривать только положительное удовлетворение.

Учитывая предложение ${\displaystyle \phi }$мы говорим, что ${\displaystyle \phi }$ является истинный в ${\displaystyle {\mathcal {A}}}$ если и только если ${\displaystyle {\mathcal {A}}\models _{\{\emptyset \}}^{+}\phi }$, и мы говорим, что ${\displaystyle \phi }$ является ложный в ${\displaystyle {\mathcal {A}}}$ если и только если ${\displaystyle {\mathcal {A}}\models _{\{\emptyset \}}^{-}\phi }$.

Семантические правила

Что касается случая Альфред Тарский отношения выполнимости для формул первого порядка, отношения положительной и отрицательной выполнимости семантики команды для логики зависимости определяются как структурная индукция над формулами языка. Поскольку оператор отрицания меняет местами положительную и отрицательную выполнимость, две индукции, соответствующие ${\displaystyle \!\models ^{+}}$ и ${\displaystyle \!\models ^{-}}$ необходимо выполнять одновременно:

Положительная выполнимость

1. ${\displaystyle \!{\mathcal {A}}\models _{X}^{+}Rt_{1}\ldots t_{n}}$ если и только если
   1. ${\displaystyle \!R}$ n-арный символ в подписи ${\displaystyle \!{\mathcal {A}}}$;
   2. Все переменные, встречающиеся в терминах ${\displaystyle \!t_{1}\ldots t_{n}}$ находятся в сфере ${\displaystyle \!X}$;
   3. Для каждого задания ${\displaystyle \!\mu \in X}$, оценка кортежа ${\displaystyle \!(t_{1}\ldots t_{n})}$ в соответствии с ${\displaystyle \!\mu }$ находится в интерпретации ${\displaystyle \!R}$ в ${\displaystyle \!{\mathcal {A}}}$;
2. ${\displaystyle \!{\mathcal {A}}\models _{X}^{+}t_{1}=t_{2}}$ если и только если
   1. Все переменные, встречающиеся в терминах ${\displaystyle \!t_{1}}$ и ${\displaystyle \!t_{2}}$ находятся в сфере ${\displaystyle \!X}$;
   2. Для каждого задания ${\displaystyle \!\mu \in X}$, оценки ${\displaystyle \!t_{1}}$ и ${\displaystyle \!t_{2}}$ в соответствии с ${\displaystyle \!{\mathcal {A}}}$ одинаковые;
3. ${\displaystyle \!{\mathcal {A}}\models _{X}^{+}=\!\!(t_{1}\ldots t_{n})}$ тогда и только тогда, когда любые два присваивания ${\displaystyle \!s,s'\in X}$ чьи оценки кортежа ${\displaystyle \!(t_{1}\ldots t_{n-1})}$ совпадают присвоить одно и то же значение ${\displaystyle \!t_{n}}$;
4. ${\displaystyle \!{\mathcal {A}}\models _{X}^{+}\lnot \phi }$ если и только если ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}\phi }$;
5. ${\displaystyle \!{\mathcal {A}}\models _{X}^{+}\phi \vee \psi }$ если и только если есть команды ${\displaystyle \!Y}$ и ${\displaystyle \!Z}$ такой, что
   1. ${\displaystyle X=Y\cup Z}$'
   2. ${\displaystyle \!{\mathcal {A}}\models _{Y}^{+}\phi }$;
   3. ${\displaystyle \!{\mathcal {A}}\models _{Z}^{+}\psi }$;
6. ${\displaystyle \!{\mathcal {A}}\models _{X}^{+}\exists x\phi }$ тогда и только тогда, когда существует функция ${\displaystyle \!F}$ из ${\displaystyle \!X}$ в область ${\displaystyle \!{\mathcal {A}}}$ такой, что ${\displaystyle \!{\mathcal {A}}\models _{X[F/x]}^{+}\phi }$, куда ${\displaystyle \!X[F/x]=\{s[F(s)/x]:s\in X\}}$.

Отрицательная выполнимость

1. ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}Rt_{1}\ldots t_{n}}$ если и только если
   1. ${\displaystyle \!R}$ n-арный символ в подписи ${\displaystyle \!{\mathcal {A}}}$;
   2. Все переменные, встречающиеся в терминах ${\displaystyle \!t_{1}\ldots t_{n}}$ находятся в сфере ${\displaystyle \!X}$;
   3. Для каждого задания ${\displaystyle \!\mu \in X}$, оценка кортежа ${\displaystyle \!(t_{1}\ldots t_{n})}$ в соответствии с ${\displaystyle \!\mu }$ не в интерпретации ${\displaystyle \!R}$ в ${\displaystyle \!{\mathcal {A}}}$;
2. ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}t_{1}=t_{2}}$ если и только если
   1. Все переменные, встречающиеся в терминах ${\displaystyle \!t_{1}}$ и ${\displaystyle \!t_{2}}$ находятся в сфере ${\displaystyle \!X}$;
   2. Для каждого задания ${\displaystyle \!\mu \in X}$, оценки ${\displaystyle \!t_{1}}$ и ${\displaystyle \!t_{2}}$ в соответствии с ${\displaystyle \!{\mathcal {A}}}$ разные;
3. ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}=\!\!(t_{1}\ldots t_{n})}$ если и только если ${\displaystyle \!X}$ это пустая команда;
4. ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}\lnot \phi }$ если и только если ${\displaystyle \!{\mathcal {A}}\models _{X}^{+}\phi }$;
5. ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}\phi \vee \psi }$ если и только если ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}\phi }$ и ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}\psi }$;
6. ${\displaystyle \!{\mathcal {A}}\models _{X}^{-}\exists x\phi }$ если и только если ${\displaystyle \!{\mathcal {A}}\models _{X[A/x]}^{-}\phi }$, куда ${\displaystyle \!X[A/x]=\{s[m/x]:s\in A\}}$ и ${\displaystyle \!A}$ это область ${\displaystyle \!{\mathcal {A}}}$.

Логика зависимости и другая логика

Логика зависимости и логика первого порядка

Логика зависимости - это консервативное расширение логики первого порядка:^[4] другими словами, для каждого предложения первого порядка ${\displaystyle \!\phi }$ и структура ${\displaystyle \!{\mathcal {A}}}$ у нас есть это ${\displaystyle \!{\mathcal {A}}\models _{\{\emptyset \}}^{+}\phi }$ если и только если ${\displaystyle \!\phi }$ верно в ${\displaystyle \!{\mathcal {A}}}$ согласно обычной семантике первого порядка. Кроме того, для любого первого заказа формула ${\displaystyle \!\phi }$, ${\displaystyle \!{\mathcal {A}}\models _{X}^{+}\phi }$ тогда и только тогда, когда все назначения ${\displaystyle \!\mu \in X}$ удовлетворить ${\displaystyle \!\phi }$ в ${\displaystyle \!{\mathcal {A}}}$ согласно обычной семантике первого порядка.

Однако логика зависимости более выразительна, чем логика первого порядка:^[5] например, предложение

${\displaystyle \!\exists z\forall x_{1}\forall x_{2}\exists y_{1}\exists y_{2}(=\!\!(x_{1},y_{1})\wedge =\!\!(x_{2},y_{2})\wedge (x_{1}=x_{2}\leftrightarrow y_{1}=y_{2})\wedge y_{1}\not =z)}$

верно в модели ${\displaystyle {\mathcal {A}}}$ тогда и только тогда, когда область этой модели бесконечна, даже если нет формулы первого порядка ${\displaystyle \!\phi }$ имеет это свойство.

Логика зависимости и логика второго порядка

Каждое предложение логики зависимости эквивалентно некоторому предложению в экзистенциальном фрагменте логики второго порядка,^[6] то есть к некоторому предложению второго порядка вида

${\displaystyle \!\exists R_{1}\ldots \exists R_{n}\psi (R_{1}\ldots R_{n})}$

куда ${\displaystyle \psi (R_{1}\ldots R_{n})}$ не содержит кванторов второго порядка. И наоборот, каждое предложение второго порядка в приведенной выше форме эквивалентно некоторому предложению логической зависимости.^[7]

Что касается открытых формул, логика зависимости соответствует монотонному вниз фрагменту экзистенциальной логики второго порядка в том смысле, что непустой класс команд определяется формулой логики зависимости тогда и только тогда, когда соответствующий класс отношений является монотонным вниз и определяемым. по экзистенциальной формуле второго порядка.^[8]

Логика зависимости и кванторы ветвления

Кванторы ветвления выражаются в терминах атомов зависимости: например, выражение

${\displaystyle (Q_{H}x_{1},x_{2},y_{1},y_{2})\phi (x_{1},x_{2},y_{1},y_{2})\equiv {\begin{pmatrix}\forall x_{1}\exists y_{1}\\\forall x_{2}\exists y_{2}\end{pmatrix}}\phi (x_{1},x_{2},y_{1},y_{2})}$

эквивалентно предложению логики зависимости ${\displaystyle \forall x_{1}\exists y_{1}\forall x_{2}\exists y_{2}(=\!\!(x_{1},y_{1})\wedge =\!\!(x_{2},y_{2})\wedge \phi )}$в том смысле, что первое выражение истинно в модели тогда и только тогда, когда истинно второе выражение.

И наоборот, любое предложение логики зависимости эквивалентно некоторому предложению в логике кванторов ветвления, поскольку все экзистенциальные предложения второго порядка выражаются в логике кванторов ветвления.^[9][10]

Логика зависимости и логика IF

Любое предложение логики зависимости логически эквивалентно некоторому предложению логики IF, и наоборот.^[11]

Однако, когда дело доходит до открытых формул, проблема более тонкая. Переводы между логикой IF и формулами логики зависимости, и наоборот, существуют до тех пор, пока область деятельности команды фиксирована: другими словами, для всех наборов переменных ${\displaystyle \!V=\{v_{1}\ldots v_{n}\}}$ и все формулы логики ЕСЛИ ${\displaystyle \!\phi }$ со свободными переменными в ${\displaystyle \!V}$ существует логическая формула зависимости ${\displaystyle \!\phi ^{D}}$ такой, что

${\displaystyle {\mathcal {A}}\models _{X}^{+}\phi \Leftrightarrow {\mathcal {A}}\models _{X}^{+}\phi ^{D}}$

для всех конструкций ${\displaystyle {\mathcal {A}}}$ и для всех команд ${\displaystyle \!X}$ с доменом ${\displaystyle \!V}$, и наоборот, для любой логической формулы зависимости ${\displaystyle \!\psi }$ со свободными переменными в ${\displaystyle \!V}$ существует формула логики ЕСЛИ ${\displaystyle \!\psi ^{I}}$ такой, что

${\displaystyle {\mathcal {A}}\models _{X}^{+}\psi \Leftrightarrow {\mathcal {A}}\models _{X}^{+}\psi ^{I}}$

для всех конструкций ${\displaystyle {\mathcal {A}}}$ и для всех команд ${\displaystyle \!X}$ с доменом ${\displaystyle \!V}$. Эти переводы не могут быть композиционными.^[12]

Характеристики

Формулы логики зависимости вниз закрыто: если ${\displaystyle {\mathcal {A}}\models _{X}\phi }$ и ${\displaystyle Y\subseteq X}$ тогда ${\displaystyle {\mathcal {A}}\models _{Y}\psi }$. Кроме того, пустая команда (но нет команда, содержащая пустое задание) удовлетворяет всем формулам логики зависимости, как положительно, так и отрицательно.

Закон исключенного третьего не работает в логике зависимости: например, формула ${\displaystyle \exists y(=\!\!(y)\wedge y=x)}$ не удовлетворен командой ни положительно, ни отрицательно ${\displaystyle X=\{(x:0),(x:1)\}}$. Более того, дизъюнкция не идемпотентна и не распространяется по конъюнкции.^[13]

Оба теорема компактности и Теорема Левенхайма-Сколема верны для логики зависимости. Интерполяционная теорема Крейга также имеет место, но из-за природы отрицания в логике зависимости, в несколько измененной формулировке: если две формулы логики зависимости ${\displaystyle \phi }$ и ${\displaystyle \psi }$ находятся противоречивый, то есть никогда не бывает, чтобы оба ${\displaystyle \phi }$ и ${\displaystyle \psi }$ в той же модели, то существует первый заказ приговор ${\displaystyle \theta }$ на общем языке двух предложений так, что ${\displaystyle \phi }$ подразумевает ${\displaystyle \theta }$ и ${\displaystyle \theta }$ противоречит ${\displaystyle \psi }$.^[14]

Как логика ЕСЛИ,^[15] Логика зависимости может определять свой собственный оператор истинности:^[16] точнее, существует формула ${\displaystyle \tau (x)}$ так что для каждого предложения ${\displaystyle \phi }$ логики зависимости и всех моделей ${\displaystyle {\mathcal {M}}_{\omega }}$ которые удовлетворяют Аксиомы Пеано, если ${\displaystyle '\phi '}$ это Число Гёделя из ${\displaystyle \phi }$ тогда

${\displaystyle {\mathcal {M}}_{\omega }\models _{\{\emptyset \}}^{+}\!\phi }$ если и только если ${\displaystyle {\mathcal {M}}_{\omega }\models _{\{\emptyset \}}^{+}\tau ('\phi ').}$

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

Сложность

Как следствие Теорема Феджина, свойства конечных структур, определяемых в логике зависимостей, в точности соответствуют свойствам NP. Более того, Дюран и Континен показали, что ограничение числа универсальных кванторов или арности атомов зависимости в предложениях порождает теоремы иерархии в отношении выразительной силы.^[17]

Проблема несогласованности логики зависимости состоит в следующем: полуразрешимый, и фактически эквивалентно проблеме несогласованности для логики первого порядка. Однако проблема решения для логики зависимости не являетсяарифметический, и фактически является полным относительно ${\displaystyle \Pi _{2}}$ класс Иерархия Леви.^[18]

Варианты и расширения

Логика команды

Логика команды^[19] расширяет логику зависимости с помощью противоречивое отрицание ${\displaystyle \sim \!\!\phi }$. Его выразительная сила эквивалентна полной логике второго порядка.^[20]

Логика модальной зависимости

Атом зависимости или его подходящий вариант может быть добавлен к языку модальная логика, таким образом получив логика модальной зависимости.^[21][22][23]

Интуиционистская логика зависимости

Как бы то ни было, логика зависимости не имеет смысла. В интуиционистский подтекст ${\displaystyle \phi \rightarrow \psi }$, название которого происходит от сходства между его определением и значением импликации интуиционистская логика, можно определить следующим образом:^[24]

${\displaystyle \!{\mathcal {A}}\models _{X}\phi \rightarrow \psi }$ если и только если для всех ${\displaystyle Y\subseteq X}$ такой, что ${\displaystyle {\mathcal {A}}\models _{Y}\phi }$ он считает, что ${\displaystyle {\mathcal {A}}\models _{Y}\psi }$.

Интуиционистская логика зависимости, то есть логика зависимости, дополненная интуиционистской импликацией, эквивалентна логике второго порядка.^[25]

Логика независимости

Вместо атомов зависимости логика независимости добавляет к языку логических атомов первого порядка независимость ${\displaystyle {\vec {t_{1}}}\bot _{\vec {t_{3}}}{\vec {t_{2}}}}$ куда ${\displaystyle {\vec {t_{1}}}}$, ${\displaystyle {\vec {t_{2}}}}$ и ${\displaystyle {\vec {t_{3}}}}$ кортежи терминов. Семантика этих атомов определяется следующим образом:

${\displaystyle {\mathcal {A}}\models _{X}{\vec {t_{1}}}\bot _{\vec {t_{3}}}{\vec {t_{2}}}}$ если и только если для всех ${\displaystyle s,s'\in X}$ с ${\displaystyle {\vec {t_{3}}}\langle s\rangle ={\vec {t_{3}}}\langle s'\rangle }$ Существует ${\displaystyle s''\in X}$ такой, что ${\displaystyle {\vec {t_{3}}}\langle s''\rangle ={\vec {t_{3}}}\langle s\rangle }$, ${\displaystyle {\vec {t_{1}}}\langle s''\rangle ={\vec {t_{1}}}\langle s\rangle }$ и ${\displaystyle {\vec {t_{2}}}\langle s''\rangle ={\vec {t_{2}}}\langle s'\rangle }$.

Логика независимости соответствует экзистенциальной логике второго порядка в том смысле, что непустой класс команд определяется формулой логики независимости тогда и только тогда, когда соответствующий класс отношений определяется экзистенциальной формулой второго порядка.^[26] Следовательно, на уровне открытых формул логика независимости имеет более сильную выразительную силу, чем логика зависимости. Однако на уровне предложений эти логики эквивалентны.^[27]

Логика включения / исключения

Логика включения / исключения расширяет логику первого порядка с помощью атомов включения ${\displaystyle {\vec {t_{1}}}\subseteq {\vec {t_{2}}}}$ и атомы исключения ${\displaystyle {\vec {t_{1}}}\mid {\vec {t_{2}}}}$ где в обеих формулах ${\displaystyle {\vec {t_{1}}}}$ и ${\displaystyle {\vec {t_{2}}}}$ являются кортежами одинаковой длины. Семантика этих атомов определяется следующим образом:

• ${\displaystyle {\mathcal {A}}\models _{X}{\vec {t_{1}}}\subseteq {\vec {t_{2}}}}$ если и только если для всех ${\displaystyle s\in X}$ Существует ${\displaystyle s'\in X}$ такой, что ${\displaystyle {\vec {t_{1}}}\langle s\rangle ={\vec {t_{2}}}\langle s'\rangle }$;
• ${\displaystyle {\mathcal {A}}\models _{X}{\vec {t_{1}}}\mid {\vec {t_{2}}}}$ если и только если для всех ${\displaystyle s,s'\in X}$ он считает, что ${\displaystyle {\vec {t_{1}}}\langle s\rangle \neq {\vec {t_{2}}}\langle s'\rangle }$.

Логика включения / исключения имеет такую ​​же выразительную силу, что и логика независимости, уже на уровне открытых формул.^[28] Логика включения и логика исключения получаются путем добавления только атомов включения или атомов исключения к логике первого порядка соответственно. Предложения логики включения соответствуют по выразительной силе предложениям с наибольшей логикой с фиксированной точкой; следовательно, логика включения захватывает (минимум) логику фиксированной точки на конечных моделях и PTIME для конечных упорядоченных моделей.^[29] Логика исключения в свою очередь соответствует логике зависимости по выразительной силе.^[30]

Обобщенные кванторы

Другой способ расширения логики зависимости - это добавление некоторых обобщенных кванторов к языку логики зависимости. Совсем недавно было проведено некоторое исследование логики зависимости с монотонными обобщенными кванторами.^[31] и логика зависимости с определенным мажоритарным квантификатором, последний приводит к новой описательной характеристике сложности подсчетной иерархии.^[32]

Смотрите также

• Семантика игры
• Квантификатор ветвления
• Дружественная к независимости логика

Примечания

1. Вяэнянен 2007
2. Ходжес 1997
3. Вяэнянен 2007, §3.2
4. Вяэнянен 2007, §3.2
5. Вяэнянен 2007, §4
6. Вяэнянен 2007, §6.1
7. Вяэнянен 2007, §6.3
8. Континен и Вяэнянен, 2009 г.
9. Эндертон 1970
10. Walkoe 1970
11. Вяэнянен 2007, §3.6
12. Континен и Вяэнянен 2009 бис
13. Вяэнянен 2007, §3
14. Вяэнянен 2007, §6.2
15. Hintikka 2002
16. Вяэнянен 2007, §6.4
17. Дюран и Континен
18. Вяэнянен 2007, §7
19. Вяэнянен 2007, §8
20. Континен и Нурми 2009
21. Севенстер 2009
22. Вяэнянен 2008
23. Ломанн и Фоллмер, 2010 г.
24. Абрамский и Вяэнянен, 2009 г.
25. Ян 2010
26. Галлиани 2012
27. Грэдель и Вяэнянен
28. Галлиани 2012
29. Галлиани и Хелла 2013
30. Галлиани 2012
31. Энгстрём
32. Дюран, Эббинг, Континен, Фоллмер 2011

Рекомендации

• Абрамский, Самсон и Вяэнянен, Йоуко (2009), «От IF к BI». Synthese 167 (2): 207–230.
• Дюран, Арно; Эббинг Йоханнес; Континен, Юха и Фоллмер Хериберт (2011), 'Логика зависимости с мажоритарным квантором '. FSTTCS 2011: 252-263.
• Дюран, Арно и Континен, Юха,Иерархии в логике зависимости^{[постоянная мертвая ссылка ]}'. ACM Transactions on Computational Logic, чтобы появиться.
• Эндертон, Герберт Б. (1970), «Конечные частично упорядоченные кванторы». Z. Math. Logik Grundlagen Math., 16: 393–397.
• Энгстрём, Фредрик,Обобщенные кванторы в логике зависимости '. Журнал логики, языка и информации, который должен появиться.
• Галлиани, Пьетро (2012), 'Включение и исключение в семантике команды - О некоторых логиках несовершенной информации '. Анналы чистой и прикладной логики 163 (1): 68-84.
• Галлиани, Пьетро и Хелла, Лаури (2013), 'Логика включения и логика с фиксированной точкой '. Proceedings of Computer Science Logic 2013 (CSL 2013), Leibniz International Proceedings in Informatics (LIPIcs) 23, 281-295.
• Гредель, Эрих и Вяэнянен, Йоуко,Зависимость и независимость '. Studia Logica, чтобы появиться.
• Хинтикка, Яакко (2002), 'Возвращение к принципам математики ', ISBN  978-0-521-62498-5.
• Ходжес, Уилфрид (1997), 'Композиционная семантика языка несовершенной информации '. Журнал IGPL 5: 539–563.
• Континен, Юха и Нурми, Вилле (2009), «Командная логика и логика второго порядка». В Логика, язык, информация и вычисления С. 230–241.
• Континен, Юха и Вяэнянен, Йоуко (2009), «Об определимости в логике зависимости». Журнал логики, языка и информации 18 (3): 317–332.
• Континен, Юха и Вяэнянен, Йоуко (2009), 'Замечание об отрицании логики зависимости '. Журнал Нотр-Дам по формальной логике, 52 (1): 55-65, 2011.
• Ломанн, Питер и Фоллмер, Хериберт (2010), «Результаты сложности для логики модальной зависимости». В Конспект лекций по информатике, стр. 411–425.
• Севенстер, Мерлин (2009), 'Теоретико-модельные и вычислительные свойства логики модальной зависимости '. Журнал логики и вычислений 19 (6): 1157–1173.
• Вяэнянен, Йоуко (2007), 'Логика зависимости - новый подход к независимой логике ', ISBN  978-0-521-87659-9.
• Вяэнянен, Йоуко (2008), 'Логика модальной зависимости '. Новые перспективы в логике и взаимодействии, стр. 237–254.
• Уолко, Уилбур Дж. (1970), 'Конечная частично упорядоченная количественная оценка '. Журнал символической логики, 35: 535–575.
• Ян, Фань (2010), «Выражение предложений второго порядка в интуиционистской логике зависимости». Зависимость и независимость в логике, стр. 118–132.

внешняя ссылка

• Галлиани, Пьетро. «Логика зависимости». В Залта, Эдуард Н. (ред.). Стэнфордская энциклопедия философии.
• Специальный выпуск Studia Logica «Зависимость и независимость в логике», содержащий ряд статей по логике зависимости.
• Презентации в Academy Colloquium Dependence Logic, Амстердам, 2014 г.