Дружественная к независимости логика - Independence-friendly logic

Дружественная к независимости логика (IF логика; предложено Яакко Хинтикка и Габриэль Санду в 1989 г.)^[1] является продолжением классической логика первого порядка (FOL) с помощью косых квантификаторов вида ${\displaystyle (\exists v/V)}$ и ${\displaystyle (\forall v/V)}$ (${\displaystyle V}$ конечный набор переменных). Предполагаемое чтение ${\displaystyle (\exists v/V)}$ есть "есть ${\displaystyle v}$ которая функционально не зависит от переменных в ${\displaystyle V}$". Логика ЕСЛИ позволяет выразить более общие закономерности зависимости между переменными, чем те, которые неявны в логике первого порядка. Этот более высокий уровень общности приводит к фактическому увеличению выразительной силы; набор предложений ЕСЛИ может характеризовать одни и те же классы структур как экзистенциальная логика второго порядка (${\displaystyle \Sigma _{1}^{1}}$). Например, он может выражать квантор ветвления предложения, такие как формула ${\displaystyle \exists c\forall x\exists y\forall z(\exists w/\{x,y\})((x=z\leftrightarrow y=w)\land y\neq c)}$ что выражает бесконечность в пустой подписи; это невозможно сделать в FOL. Следовательно, логика первого порядка, как правило, не может выразить эту модель зависимости, в которой ${\displaystyle y}$ зависит от Только на ${\displaystyle x}$ и ${\displaystyle c}$, и ${\displaystyle w}$ зависит от Только на ${\displaystyle z}$ и ${\displaystyle c}$. Если логика более общая, чем кванторы ветвления, например, в том, что он может выражать зависимости, которые не являются транзитивными, например, в префиксе квантификатора ${\displaystyle \forall x\exists y(\exists z/\{x\})}$ (${\displaystyle y}$ зависит от ${\displaystyle x}$, и ${\displaystyle z}$ зависит от ${\displaystyle y}$, но ${\displaystyle z}$ не зависит от ${\displaystyle x}$).

Введение логики IF отчасти было мотивировано попыткой расширить семантика игры логики первого порядка к играм несовершенная информация. В самом деле, семантика для предложений IF может быть задана в терминах таких игр (или, альтернативно, с помощью процедуры преобразования в экзистенциальную логику второго порядка). Семантика для открытых формул не может быть дана в виде тарской семантики (^[2]); адекватная семантика должна определять, что означает удовлетворение формулы набором назначений общей переменной домена ( команда), а не удовлетворение одним поручением. Такой командная семантика был разработан Ходжес (^[3]).

Логика IF является эквивалентом перевода на уровне предложений с рядом других логических систем, основанных на семантике команды, например логика зависимости, дружественная к зависимости логика, логика исключения и логика независимости; За исключением последнего, логика ЕСЛИ, как известно, эквивалентна этим логикам также на уровне открытых формул. Однако логика IF отличается от всех вышеупомянутых систем тем, что в ней отсутствует местонахождение (значение открытой формулы нельзя описать только в терминах свободных переменных формулы; вместо этого оно зависит от контекста, в котором встречается формула).

Логика ЕСЛИ разделяет ряд металогических свойств с логикой первого порядка, но есть некоторые отличия, в том числе отсутствие замыкания при (классическом, противоречивом) отрицании и более высокая сложность определения правильности формул. Расширенная логика IF решает проблему закрытия, но ее теоретико-игровая семантика более сложна, и такая логика соответствует большему фрагменту логики второго порядка, собственному подмножеству ${\displaystyle \Delta _{2}^{1}}$ (^[4]).

Хинтикка утверждал (например, в книге ^[5]), что IF и расширенная логика IF должны использоваться в качестве основы для основы математики; это предложение в некоторых случаях было встречено скептически (см., например,^[6]).

Синтаксис

В литературе появилось несколько несколько отличающихся друг от друга представлений логики IF; вот мы следуем.^[7]

Термины и атомарные формулы

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

Формулы IF

Для фиксированной сигнатуры σ формулы логики IF определяются следующим образом:

1. Любая атомная формула ${\displaystyle \varphi }$ является формулой ЕСЛИ.
2. Если ${\displaystyle \varphi }$ формула ЕСЛИ, то ${\displaystyle \lnot \varphi }$ является формулой ЕСЛИ.
3. Если ${\displaystyle \varphi }$ и ${\displaystyle \psi }$ являются формулами ЕСЛИ, то ${\displaystyle \phi \wedge \psi }$ и ${\displaystyle \phi \vee \psi }$ являются формулами ЕСЛИ.
4. Если ${\displaystyle \varphi }$ формула, ${\displaystyle v}$ переменная, а ${\displaystyle V}$ конечный набор переменных, то ${\displaystyle (\exists v/V)\varphi }$ и ${\displaystyle (\forall v/V)\varphi }$ также являются формулами ЕСЛИ.

Бесплатные переменные

Набор ${\displaystyle {\mbox{Free}}(\varphi )}$ свободных переменных формулы IF ${\displaystyle \varphi }$ индуктивно определяется следующим образом:

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

Последнее предложение - единственное, которое отличается от предложений для логики первого порядка, разница в том, что также переменные в наборе косой черты ${\displaystyle V}$ считаются свободными переменными.

IF предложения

Формула ЕСЛИ ${\displaystyle \varphi }$ такой, что ${\displaystyle {\mbox{Free}}(\phi )=\emptyset }$ является Если предложение.

Семантика

Были предложены три основных подхода к определению семантики логики IF. Первые два, основанные соответственно на играх с несовершенной информацией и на сколемизации, в основном используются только в определении предложений IF. Первый обобщает аналогичный подход для логики первого порядка, который был основан на играх идеально информация. Третий подход, командная семантика, является композиционной семантикой в ​​духе тарской семантики. Однако эта семантика не определяет, что означает, что формула удовлетворяется присваиванием (скорее, набор первых двух подходов были разработаны в более ранних публикациях по логике if (^[8][9]); третий Ходжес в 1997 г. (^[10][11]).

В этом разделе мы различаем три подхода, записывая разные педики, как в ${\displaystyle \models _{GTS},\models _{Sk},\models }$. Поскольку три подхода фундаментально эквивалентны, только символ ${\displaystyle \models }$ будет использоваться в оставшейся части статьи.

Теоретико-игровая семантика

Теоретико-игровая семантика присваивает значения истинности предложениям IF в соответствии со свойствами некоторых игр с несовершенной информацией для двух игроков. Для удобства изложения игры удобно связывать не только с предложениями, но и с формулами. Точнее, игры определяют ${\displaystyle G(\varphi ,{\mathcal {M}},s)}$ для каждой тройки, образованной формулой ЕСЛИ ${\displaystyle \varphi }$, структура ${\displaystyle {\mathcal {M}}}$, и задание ${\displaystyle s:U\supseteq {\mbox{Free}}(\varphi )\rightarrow {\mathcal {M}}}$.

Игроки

Семантическая игра ${\displaystyle G(\varphi ,{\mathcal {M}},s)}$ есть два игрока, которых зовут Элоиза (или Проверяющий) и Абеляр (или Фальсификатор).

Правила игры

Разрешенные ходы в смысловой игре ${\displaystyle G(\varphi ,{\mathcal {M}},s)}$ определяются синтаксической структурой рассматриваемой формулы. Для простоты сначала предположим, что ${\displaystyle \varphi }$ находится в нормальной форме отрицания, при этом символы отрицания встречаются только перед атомарными подформулами.

1. Если ${\displaystyle \varphi }$ является буквальным, игра заканчивается, и, если ${\displaystyle \varphi }$ верно в ${\displaystyle {\mathcal {M}}}$ (в смысле первого порядка), тогда побеждает Элоиза; в противном случае выигрывает Абеляр.
2. Если ${\displaystyle \varphi =\psi _{1}\land \psi _{2}}$, то Абеляр выбирает одну из подформул ${\displaystyle \psi _{i}}$, и соответствующая игра ${\displaystyle G(\psi _{i},{\mathcal {M}},s)}$ играет.
3. Если ${\displaystyle \varphi =\psi _{1}\lor \psi _{2}}$, то Элоиз выбирает одну из подформул ${\displaystyle \psi _{i}}$, и соответствующая игра ${\displaystyle G(\psi _{i},{\mathcal {M}},s)}$ играет.
4. Если ${\displaystyle \varphi =(\forall v/V)\psi }$, то Абеляр выбирает элемент ${\displaystyle a}$ из ${\displaystyle {\mathcal {M}}}$, и игра ${\displaystyle G(\psi ,{\mathcal {M}},s(a/v))}$ играет.
5. Если ${\displaystyle \varphi =(\exists v/V)\psi }$, то Элоиза выбирает элемент ${\displaystyle a}$ из ${\displaystyle {\mathcal {M}}}$, и игра ${\displaystyle G(\psi ,{\mathcal {M}},s(a/v))}$ играет.

В более общем смысле, если ${\displaystyle \varphi }$ не находится в нормальной форме отрицания, мы можем утверждать, как правило для отрицания, что когда игра ${\displaystyle G(\lnot \varphi ,{\mathcal {M}},s)}$ достигается, игроки начинают играть в двойную игру ${\displaystyle G^{*}(\varphi ,{\mathcal {M}},s)}$ в котором меняются роли Проверяющих и Фальсификаторов.

Истории

Неформально последовательность ходов в игре ${\displaystyle G(\varphi ,{\mathcal {M}},s)}$ это история. В конце каждой истории ${\displaystyle h}$, какая-то подигра ${\displaystyle G(\psi _{h},{\mathcal {M}},s_{h})}$ играет; мы называем ${\displaystyle s_{h}}$ то назначение, связанное с ${\displaystyle h}$, и ${\displaystyle \psi _{h}}$ то вхождение подформулы, связанное с ${\displaystyle h}$. В игрок, связанный с ${\displaystyle h}$ Элоиза в случае, если самый внешний логический оператор в ${\displaystyle \psi _{h}}$ является ${\displaystyle \lor }$ или же ${\displaystyle \exists }$, и Абеляр, если это ${\displaystyle \land }$ или же ${\displaystyle \forall }$.

Набор ${\displaystyle h}$ из разрешенные ходы в истории ${\displaystyle h}$ является ${\displaystyle {\mathcal {M}}}$ если самый внешний оператор ${\displaystyle \psi _{h}}$ является ${\displaystyle \exists }$ или же ${\displaystyle \forall }$; это ${\displaystyle \{L,R\}}$ (${\displaystyle L,R}$ быть любыми двумя отдельными объектами, символизирующими «левый» и «правый») в случае, если самый внешний оператор ${\displaystyle \psi _{h}}$ является ${\displaystyle \lor }$ или же ${\displaystyle \land }$.

Учитывая два задания ${\displaystyle s,t}$ того же домена и ${\displaystyle V\subseteq dom(s)}$ мы пишем ${\displaystyle s\sim _{V}t}$ если ${\displaystyle s(w)=t(w)}$ по любой переменной ${\displaystyle w\in dom(s)\setminus V}$.

Несовершенная информация вводится в игры, оговаривая, что определенные истории неразличимы для соответствующего игрока; Говорят, что неразличимые истории образуют «информационный набор». Интуитивно, если история ${\displaystyle h}$ находится в информационном наборе ${\displaystyle I}$, игрок, связанный с ${\displaystyle h}$ не знает, находится ли он в ${\displaystyle h}$ или в какой-то другой истории ${\displaystyle I}$.Рассмотрим две истории ${\displaystyle h,h'}$ так что связанный ${\displaystyle \psi _{h},\psi _{h'}}$ являются идентичными вхождениями подформул вида ${\displaystyle (Qv/V)\chi }$ (${\displaystyle Q=\exists }$ или же ${\displaystyle \forall }$); если к тому же ${\displaystyle s_{h}\sim _{V}s_{h'}}$, мы пишем ${\displaystyle h\sim _{\exists }h'}$ (в случае ${\displaystyle Q=\exists }$) или же ${\displaystyle h\sim _{\forall }h'}$ (в случае ${\displaystyle Q=\forall }$), чтобы указать, что эти две истории неразличимы для Элоизы, соответственно. для Абеляра. Мы также оговорим, вообще говоря, рефлексивность этого отношения: если ${\displaystyle \psi =\chi _{1}\lor \chi _{2}}$, тогда ${\displaystyle h\sim _{\exists }h'}$; и если ${\displaystyle \psi =\chi _{1}\land \chi _{2}}$, тогда ${\displaystyle h\sim _{\forall }h'}$.

Стратегии

Для фиксированной игры ${\displaystyle G(\varphi ,{\mathcal {M}},s)}$, записывать ${\displaystyle H_{\exists }}$ для набора историй, с которыми связана Элоиза, и аналогично ${\displaystyle H_{\forall }}$ для набора историй Абеляра.

А стратегия для Элоизы в игре ${\displaystyle G(\varphi ,{\mathcal {M}},s)}$ является ли любая функция, которая приписывает любой возможной истории, в которой настала очередь Элоизы играть, допустимый ход; точнее любая функция ${\displaystyle \sigma :H_{\exists }\rightarrow \prod _{h\in H_{\exists }}A(h)}$ такой, что ${\displaystyle \sigma (h)\in A(h)}$ для каждой истории ${\displaystyle h\in H_{\exists }}$. Можно определить двойственно стратегии Абеляра.

Стратегия Элоизы униформа если, когда ${\displaystyle h\sim _{\exists }h'}$, ${\displaystyle \sigma (h)=\sigma (h')}$; для Абеляра, если ${\displaystyle h\sim _{\forall }h'}$ подразумевает ${\displaystyle \sigma (h)=\sigma (h')}$.

Стратегия ${\displaystyle \sigma }$ для Элоизы победа если выиграет Элоиза в каждой истории терминала, до которой можно добраться, играя в соответствии с ${\displaystyle \sigma }$. Аналогично для Абеляра.

Правда, ложь, неопределенность

Предложение IF ${\displaystyle \varphi }$ является истинный в структуре ${\displaystyle {\mathcal {M}}}$ (${\displaystyle {\mathcal {M}}\models _{GTS}^{+}\varphi }$), если у Элоизы есть единая выигрышная стратегия в игре ${\displaystyle G(\varphi ,{\mathcal {M}},\emptyset )}$. это ложный (${\displaystyle {\mathcal {M}}\models _{GTS}^{-}\varphi }$), если у Абеляра есть выигрышная стратегия. неопределенный если ни у Элоизы, ни у Абеляра нет выигрышной стратегии.

Консервативность

Определенная таким образом семантика логики IF является консервативным расширением семантики первого порядка в следующем смысле. Если ${\displaystyle \varphi }$ предложение IF с пустыми наборами косой черты, свяжите с ним формулу первого порядка ${\displaystyle \varphi '}$ который идентичен ему, за исключением того, что каждый квантор IF ${\displaystyle (Qv/\emptyset )}$ заменяется соответствующим квантором первого порядка ${\displaystyle Qv}$. потом ${\displaystyle {\mathcal {M}}\models _{GTS}^{+}\varphi }$ если только ${\displaystyle {\mathcal {M}}\models \varphi '}$ в тарском смысле; и ${\displaystyle {\mathcal {M}}\models _{GTS}^{-}\varphi }$ если только ${\displaystyle {\mathcal {M}}\not \models \varphi '}$ в тарском смысле.

Открытые формулы

Для придания значения (возможно, открытым) формулам ЕСЛИ можно использовать более общие игры; более точно, можно определить, что это означает для формулы ЕСЛИ ${\displaystyle \varphi }$ быть удовлетворенным, на структуре ${\displaystyle {\mathcal {M}}}$, автор команда ${\displaystyle X}$ (набор присвоений общей переменной домена ${\displaystyle dom(X)}$ и codomain ${\displaystyle {\mathcal {M}}}$Связанные игры ${\displaystyle G(\varphi ,M,X)}$ начать со случайного выбора задания ${\displaystyle s\in X}$; после этого начального хода игра ${\displaystyle G(\varphi ,M,s)}$ играет. Существование выигрышной стратегии для Элоизы определяет положительное удовлетворение (${\displaystyle M,X\models _{GTS}^{+}\varphi }$), а наличие выигрышной стратегии для Абеляра определяет отрицательное удовлетворение (${\displaystyle M,X\models _{GTS}^{-}\varphi }$На этом уровне общности теоретико-игровая семантика может быть заменена алгебраическим подходом, командная семантика (определено ниже).

Сколемская семантика

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

Сколемизация

Учитывая формулу ЕСЛИ ${\displaystyle \varphi }$, сначала определим его сколемизацию, релятивизированную к конечному множеству ${\displaystyle U\supseteq {\mbox{Free}}(\varphi )}$ переменных. Для каждого экзистенциального квантора ${\displaystyle (\exists v/V)}$ происходящий в ${\displaystyle \varphi }$, позволять ${\displaystyle f_{v}}$ быть новым символом функции («функция Сколема»). Мы пишем ${\displaystyle Subst(\varphi ,v,t)}$ для формулы, которая получается заменой, в ${\displaystyle \varphi }$, все свободные вхождения переменной ${\displaystyle v}$ со сроком ${\displaystyle t}$. Сколемизация ${\displaystyle \varphi }$ относительно ${\displaystyle U}$, ${\displaystyle {\mbox{Sk}}_{U}(\varphi )}$, определяется следующими индуктивными предложениями:

1. ${\displaystyle \operatorname {Sk} _{U}(\varphi )=\varphi }$ если ${\displaystyle \varphi }$ буквально.
2. ${\displaystyle \operatorname {Sk} _{U}(\psi \circ \chi )=\operatorname {Sk} _{U}(\psi )\circ \operatorname {Sk} _{U}(\chi )}$ если ${\displaystyle \circ =\land ,\lor }$.
3. ${\displaystyle \operatorname {Sk} _{U}((\forall v/V)\psi )=\forall v\operatorname {Sk} _{U\cup \{v\}}(\psi )}$.
4. ${\displaystyle \operatorname {Sk} _{U}((\exists v/V)\psi )=Sub(\operatorname {Sk} _{U\cup \{v\}}(\psi ),v,f_{v}(y_{1},...,y_{n}))}$, куда ${\displaystyle y_{1},...,y_{n}}$ это список переменных в ${\displaystyle U\setminus V}$.

Если ${\displaystyle \varphi }$ является IF-предложением, его (нерелятивизированная) сколемизация определяется как ${\displaystyle {\mbox{Sk}}(\varphi )={\mbox{Sk}}_{\varnothing }(\varphi )}$.

Крейзелизация

Учитывая формулу ЕСЛИ ${\displaystyle \varphi }$ассоциировать с каждым универсальным квантором ${\displaystyle (\forall v/V)}$ в нем появляется новый функциональный символ ${\displaystyle g_{v}}$ («функция Крейзеля»). Затем кризелизация ${\displaystyle {\mbox{Kr}}_{U}(\varphi )}$ из ${\displaystyle \varphi }$ относительно конечного набора переменных ${\displaystyle U\supseteq {\mbox{Free}}(\varphi )}$, определяется следующими индуктивными предложениями:

1. ${\displaystyle \operatorname {Kr} _{U}(\varphi )=\lnot \varphi }$ если ${\displaystyle \varphi }$ буквально.
2. ${\displaystyle \operatorname {Kr} _{U}(\psi \land \chi )=\operatorname {Kr} _{U}(\psi )\lor \operatorname {Kr} _{U}(\chi )}$.
3. ${\displaystyle \operatorname {Kr} _{U}(\psi \lor \chi )=\operatorname {Kr} _{U}(\psi )\land \operatorname {Kr} _{U}(\chi )}$.
4. ${\displaystyle \operatorname {Kr} _{U}((\forall v/V)\psi )=Sub(\operatorname {Kr} _{U\cup \{v\}}(\psi ),v,g_{v}(y_{1},...,y_{n}))}$, куда ${\displaystyle y_{1},...,y_{n}}$это список переменных в ${\displaystyle U\setminus V}$.
5. ${\displaystyle \operatorname {Kr} _{U}((\exists v/V)\psi )=\forall v\operatorname {Kr} _{U\cup \{v\}}(\psi )}$

Если ${\displaystyle \varphi }$ является IF-предложением, его (нерелятивизированная) крейзелизация определяется как ${\displaystyle {\mbox{Kr}}(\varphi )={\mbox{Kr}}_{\varnothing }(\varphi )}$.

Правда, ложь, неопределенность

Учитывая предложение IF ${\displaystyle \varphi }$ с ${\displaystyle n}$ экзистенциальные кванторы, структура ${\displaystyle {\mathcal {M}}}$, и список ${\displaystyle {\vec {f}}}$из ${\displaystyle n}$ функции соответствующих арностей обозначим как ${\displaystyle ({\mathcal {M}},{\vec {f}})}$ расширение ${\displaystyle {\mathcal {M}}}$ который назначает функции ${\displaystyle {\vec {f}}}$ как интерпретации сколемских функций ${\displaystyle \varphi }$.

Предложение IF истинно для структуры ${\displaystyle {\mathcal {M}}}$ (${\displaystyle {\mathcal {M}}\models _{\mbox{Sk}}^{+}\varphi }$) тогда и только тогда, когда существует кортеж ${\displaystyle {\vec {f}}}$ таких функций, что ${\displaystyle ({\mathcal {M}},{\vec {f}})\models {\mbox{Sk}}(\varphi )}$.По аналогии, ${\displaystyle {\mathcal {M}}\models _{\mbox{Sk}}^{-}\varphi }$ если есть кортеж ${\displaystyle {\vec {f}}}$ таких функций, что ${\displaystyle ({\mathcal {M}},{\vec {f}})\models {\mbox{Kr}}(\varphi )}$; и ${\displaystyle {\mathcal {M}}\models _{\mbox{Sk}}^{0}\varphi }$ тогда и только тогда, когда не выполняется ни одно из предыдущих условий.

Для любого предложения IF Skolem Semantics возвращает те же значения, что и теоретико-игровая семантика.

Семантика команды

Посредством групповой семантики можно дать композиционное описание семантики логики IF. Истина и ложь основаны на понятии «выполнимость формулы командой».

Команды

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

Копирование и пополнение команд

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

1. Учитывая команду ${\displaystyle X}$ над структурой ${\displaystyle {\mathcal {M}}}$ и переменная ${\displaystyle v}$, дублирующая команда ${\displaystyle X[{\mathcal {M}}/v]}$ это команда ${\displaystyle \{s(a/v)|s\in X,a\in {\mathcal {M}}\}}$.

1. Учитывая команду ${\displaystyle X}$ над структурой ${\displaystyle {\mathcal {M}}}$, функция ${\displaystyle F:X\rightarrow {\mathcal {M}}}$ и переменная ${\displaystyle v}$, сопровождающая команда ${\displaystyle X[F/v]}$ это команда ${\displaystyle \{s(F(s)/v)|s\in X\}}$.

Принято заменять повторяющиеся применения этих двух операций более сжатыми обозначениями, такими как ${\displaystyle X[{\mathcal {M}}F/uv]}$ за ${\displaystyle (X[{\mathcal {M}}/u])[F/v]}$.

Единые функции в командах

Как и выше, с учетом двух заданий ${\displaystyle s,t}$ с той же переменной областью мы пишем ${\displaystyle s\sim _{V}t}$ если ${\displaystyle s(w)=t(w)}$ для каждой переменной ${\displaystyle w\in dom(s)\setminus V}$.

Учитывая команду ${\displaystyle X}$ на структуре ${\displaystyle {\mathcal {M}}}$ и конечное множество ${\displaystyle V}$ переменных, мы говорим, что функция ${\displaystyle F:X\rightarrow {\mathcal {M}}}$ является ${\displaystyle V}$-равномерно, если ${\displaystyle F(s)=F(t)}$ в любое время ${\displaystyle s\sim _{V}t}$.

Семантические предложения

Семантика команды трехзначна в том смысле, что формула может быть положительно удовлетворена командой в данной структуре или отрицательно ею удовлетворена, либо ни то, ни другое. Пункты семантики для положительного и отрицательного удовлетворения определяются путем одновременной индукции по синтаксической структуре формул IF.

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

1. ${\displaystyle \!{\mathcal {M}},X\models ^{+}Rt_{1}\ldots t_{n}}$ тогда и только тогда, когда для каждого задания ${\displaystyle s\in X}$, ${\displaystyle \!{\mathcal {M}},s\models Rt_{1}\ldots t_{n}}$ в смысле логики первого порядка (то есть кортеж ${\displaystyle \!(s(t_{1})\ldots s(t_{n}))}$ находится в интерпретации ${\displaystyle R^{\mathcal {M}}}$ из ${\displaystyle R}$).
2. ${\displaystyle \!{\mathcal {M}},X\models ^{+}t_{1}=t_{2}}$ тогда и только тогда, когда для каждого задания ${\displaystyle s\in X}$, ${\displaystyle \!{\mathcal {M}},s\models t_{1}=t_{2}}$ в смысле логики первого порядка (то есть ${\displaystyle s(t_{1})=s(t_{2})}$).
3. ${\displaystyle \!{\mathcal {M}},X\models ^{+}\lnot \phi }$ если и только если ${\displaystyle \!{\mathcal {M}},X\models ^{-}\phi }$.
4. ${\displaystyle \!{\mathcal {M}},X\models ^{+}\varphi \wedge \psi }$ если и только если ${\displaystyle \!{\mathcal {M}},X\models ^{+}\varphi }$ и ${\displaystyle \!{\mathcal {M}},X\models ^{+}\psi }$.
5. ${\displaystyle \!{\mathcal {M}},X\models ^{+}\varphi \vee \psi }$ если и только если есть команды ${\displaystyle \!Y}$ и ${\displaystyle \!Z}$ такой, что ${\displaystyle X=Y\cup Z}$ и ${\displaystyle \!{\mathcal {M}},Y\models ^{+}\varphi }$ и ${\displaystyle \!{\mathcal {M}},Z\models ^{+}\psi }$.
6. ${\displaystyle \!{\mathcal {M}},X\models ^{+}(\forall v/V)\varphi }$ если и только если ${\displaystyle \!{\mathcal {M}},X[M/v]\models ^{+}\varphi }$.
7. ${\displaystyle \!{\mathcal {M}},X\models ^{+}(\exists v/V)\varphi }$ тогда и только тогда, когда существует ${\displaystyle V}$-унифицированная функция ${\displaystyle F:X\rightarrow M}$такой, что ${\displaystyle \!{\mathcal {M}},X[F/v]\models ^{+}\phi }$.

Отрицательное удовлетворение:

1. ${\displaystyle \!{\mathcal {M}},X\models ^{-}Rt_{1}\ldots t_{n}}$ тогда и только тогда, когда для каждого задания ${\displaystyle s\in X}$, кортеж ${\displaystyle \!(s(t_{1})\ldots s(t_{n}))}$ не в интерпретации ${\displaystyle R^{\mathcal {M}}}$ из ${\displaystyle R}$.
2. ${\displaystyle \!{\mathcal {M}},X\models ^{-}t_{1}=t_{2}}$ тогда и только тогда, когда для каждого задания ${\displaystyle s\in X}$, ${\displaystyle s(t_{1})\neq s(t_{2})}$.
3. ${\displaystyle \!{\mathcal {M}},X\models ^{-}\lnot \phi }$ если и только если ${\displaystyle \!{\mathcal {M}},X\models ^{+}\phi }$.
4. ${\displaystyle \!{\mathcal {M}},X\models ^{-}\varphi \wedge \psi }$ если и только если есть команды ${\displaystyle \!Y}$ и ${\displaystyle \!Z}$ такой, что ${\displaystyle X=Y\cup Z}$ и ${\displaystyle \!{\mathcal {M}},Y\models ^{-}\varphi }$ и ${\displaystyle \!{\mathcal {M}},Z\models ^{-}\psi }$.
5. ${\displaystyle \!{\mathcal {M}},X\models ^{-}\varphi \vee \psi }$ если и только если ${\displaystyle \!{\mathcal {M}},X\models ^{-}\varphi }$ и ${\displaystyle \!{\mathcal {M}},X\models ^{-}\psi }$.
6. ${\displaystyle \!{\mathcal {M}},X\models ^{+}(\forall v/V)\varphi }$ тогда и только тогда, когда существует ${\displaystyle V}$-унифицированная функция ${\displaystyle F:X\rightarrow M}$такой, что ${\displaystyle \!{\mathcal {M}},X[F/v]\models ^{+}\phi }$.
7. ${\displaystyle \!{\mathcal {M}},X\models ^{+}(\exists v/V)\varphi }$ если и только если ${\displaystyle \!{\mathcal {M}},X[M/v]\models ^{+}\varphi }$.

Правда, ложь, неопределенность

Согласно семантике команды, предложение IF ${\displaystyle \varphi }$ говорят, что это правда (${\displaystyle {\mathcal {M}}\models ^{+}\varphi }$) на конструкции ${\displaystyle {\mathcal {M}}}$ если он удовлетворен ${\displaystyle {\mathcal {M}}}$ командой singleton ${\displaystyle \{\emptyset \}}$, в символах: ${\displaystyle {\mathcal {M}},\{\emptyset \}\models ^{+}\varphi }$. По аналогии, ${\displaystyle \varphi }$ считается ложным (${\displaystyle {\mathcal {M}}\models ^{-}\varphi }$) на ${\displaystyle {\mathcal {M}}}$ если ${\displaystyle {\mathcal {M}},\{\emptyset \}\models ^{-}\varphi }$; он считается неопределенным (${\displaystyle {\mathcal {M}}\models ^{0}\varphi }$) если ${\displaystyle {\mathcal {M}},\{\emptyset \}\not \models ^{+}\varphi }$ и ${\displaystyle {\mathcal {M}},\{\emptyset \}\not \models ^{-}\varphi }$.

Связь с теоретико-игровой семантикой

Для любой команды ${\displaystyle X}$ на структуре ${\displaystyle {\mathcal {M}}}$, и любая формула ЕСЛИ ${\displaystyle \varphi }$, у нас есть:${\displaystyle {\mathcal {M}},X\models ^{+}\varphi }$ если только ${\displaystyle {\mathcal {M}},X\models _{GTS}^{+}\varphi }$и${\displaystyle {\mathcal {M}},X\models ^{-}\varphi }$ если только ${\displaystyle {\mathcal {M}},X\models _{GTS}^{-}\varphi }$.

Отсюда сразу следует, что для предложений ${\displaystyle \varphi }$, ${\displaystyle {\mathcal {M}}\models ^{+}\varphi \Leftrightarrow {\mathcal {M}}\models _{GTS}^{+}\varphi }$, ${\displaystyle {\mathcal {M}}\models ^{-}\varphi \Leftrightarrow {\mathcal {M}}\models _{GTS}^{-}\varphi }$ и ${\displaystyle {\mathcal {M}}\models ^{0}\varphi \Leftrightarrow {\mathcal {M}}\models _{GTS}^{0}\varphi }$.

Понятия эквивалентности

Поскольку логика ЕСЛИ в ее обычном понимании является трехзначной, интерес представляют множественные понятия эквивалентности формул.

Эквивалентность формул

Позволять ${\displaystyle \varphi ,\psi }$ - две формулы IF.

${\displaystyle \varphi \models ^{+}\psi }$ (${\displaystyle \varphi }$ правда влечет за собой ${\displaystyle \psi }$) если ${\displaystyle {\mathcal {M}},X\models ^{+}\varphi \Rightarrow {\mathcal {M}},X\models ^{+}\psi }$ для любой конструкции ${\displaystyle {\mathcal {M}}}$ и любая команда ${\displaystyle X}$ такой, что ${\displaystyle dom(X)\supseteq {\mbox{Free}}(\varphi )\cup {\mbox{Free}}(\psi )}$.

${\displaystyle \varphi \equiv ^{+}\psi }$ (${\displaystyle \varphi }$ является эквивалент истины к ${\displaystyle \psi }$) если ${\displaystyle \varphi \models ^{+}\psi }$ и ${\displaystyle \psi \models ^{+}\varphi }$.

${\displaystyle \varphi \models ^{-}\psi }$ (${\displaystyle \varphi }$ ложь влечет за собой ${\displaystyle \psi }$) если ${\displaystyle {\mathcal {M}},X\models ^{-}\psi \Rightarrow {\mathcal {M}},X\models ^{-}\varphi }$ для любой конструкции ${\displaystyle {\mathcal {M}}}$ и любая команда ${\displaystyle X}$ такой, что ${\displaystyle dom(X)\supseteq {\mbox{Free}}(\varphi )\cup {\mbox{Free}}(\psi )}$.

${\displaystyle \varphi \equiv ^{-}\psi }$ (${\displaystyle \varphi }$ является эквивалент ложности к ${\displaystyle \psi }$) если ${\displaystyle \varphi \models ^{-}\psi }$ и ${\displaystyle \psi \models ^{-}\varphi }$.

${\displaystyle \varphi \models \psi }$ (${\displaystyle \varphi }$ сильно влечет к ${\displaystyle \psi }$) если ${\displaystyle \varphi \models ^{+}\psi }$ и ${\displaystyle \varphi \models ^{-}\psi }$.

${\displaystyle \varphi \equiv \psi }$ (${\displaystyle \varphi }$ является сильно эквивалентный к ${\displaystyle \psi }$) если ${\displaystyle \varphi \equiv ^{+}\psi }$ и ${\displaystyle \varphi \equiv ^{-}\psi }$.

Эквивалентность предложений

Приведенные выше определения предназначены для предложений IF следующим образом. ${\displaystyle \varphi ,\psi }$ находятся эквивалент истины если они верны в тех же структурах; они есть эквивалент ложности если они ложны в тех же структурах; они есть сильно эквивалентный если они эквивалентны истине и лжи.

Интуитивно, использование строгой эквивалентности равносильно рассмотрению логики ЕСЛИ как трехзначной (истина / неопределенность / ложь), в то время как эквивалентность истины рассматривает предложения ЕСЛИ как если бы они были двухзначными (истина / ложь).

Эквивалентность относительно контекста

Многие логические правила логики ЕСЛИ могут быть адекватно выражены только в терминах более ограниченных понятий эквивалентности, которые принимают во внимание контекст, в котором может появиться формула.

Например, если ${\displaystyle U}$ конечный набор переменных и ${\displaystyle U\supseteq {\mbox{Free}}(\varphi )\cup {\mbox{Free}}(\psi )}$, можно сказать, что ${\displaystyle \varphi }$ является истина эквивалентна ${\displaystyle \psi }$ относительно ${\displaystyle U}$ (${\displaystyle \varphi \equiv _{U}\psi }$) в случае ${\displaystyle {\mathcal {M}},X\models ^{+}\psi \Leftrightarrow {\mathcal {M}},X\models ^{+}\varphi }$ для любой конструкции ${\displaystyle {\mathcal {M}}}$ и любая команда ${\displaystyle X}$ домена ${\displaystyle U}$.

Теоретико-модельные свойства

Уровень приговора

Предложения ЕСЛИ могут быть переведены с сохранением истины в предложения (функциональные) экзистенциальная логика второго порядка (${\displaystyle \Sigma _{1}^{1}}$) посредством процедуры сколемизации (см. выше). И наоборот, каждый ${\displaystyle \Sigma _{1}^{1}}$ может быть переведено в предложение IF с помощью варианта процедуры перевода Walkoe-Enderton для частично упорядоченные кванторы (^[12][13]). Другими словами, логика ЕСЛИ и ${\displaystyle \Sigma _{1}^{1}}$ выразительно эквивалентны на уровне предложений. Эту эквивалентность можно использовать для доказательства многих следующих свойств; они унаследованы от ${\displaystyle \Sigma _{1}^{1}}$ и во многих случаях аналогичны свойствам ВОЛС.

Обозначим через ${\displaystyle T}$ (возможно, бесконечный) набор IF-предложений.

• Свойство Левенхайм-Сколема: если ${\displaystyle T}$ имеет бесконечную модель или сколь угодно большие конечные модели, чем модели любой бесконечной мощности.
• Экзистенциальная компактность: если каждое конечное ${\displaystyle T_{0}\subseteq T}$ есть модель, то также ${\displaystyle T}$ есть модель.
• Несостоятельность дедуктивной компактности: есть ${\displaystyle T,\varphi }$ такой, что ${\displaystyle T\models \varphi }$, но ${\displaystyle T_{0}\not \models \varphi }$ для любого конечного ${\displaystyle T_{0}\subset T}$. В этом отличие от ВОЛС.
• Теорема о разделении: если ${\displaystyle \varphi ,\psi }$ являются взаимно несовместимыми предложениями ЕСЛИ, то существует предложение FOL ${\displaystyle \theta }$ такой, что ${\displaystyle \varphi \models ^{+}\theta }$ и ${\displaystyle \psi \models ^{+}\lnot \theta }$. Это следствие Интерполяционная теорема Крейга для ВОЛС.
• Теорема Берджесса:^[14] если ${\displaystyle \varphi ,\psi }$ являются взаимно несовместимыми предложениями ЕСЛИ, то существует предложение ЕСЛИ ${\displaystyle \theta }$ такой, что ${\displaystyle \varphi \equiv ^{+}\theta }$ и ${\displaystyle \psi \equiv ^{+}\lnot \theta }$ (кроме, возможно, одноэлементных конструкций). В частности, эта теорема показывает, что отрицание логики IF не является семантической операцией относительно эквивалентности истинности (предложения, эквивалентные истинности, могут иметь неэквивалентные отрицания).
• Определимость истины:^[15] есть предложение ЕСЛИ ${\displaystyle TRUE(c)}$на языке арифметики Пеано, так что для любого предложения IF ${\displaystyle \varphi ,}$, ${\displaystyle \mathbb {N} \models \varphi \Leftrightarrow \mathbb {N} \models TRUE(\ulcorner \varphi \urcorner )}$ (куда ${\displaystyle \ulcorner \urcorner }$ обозначает гёделевскую нумерацию). Более слабое утверждение справедливо и для нестандартных моделей арифметики Пеано (^[16]).

Уровень формулы

Понятие выполнимости команды имеет следующие свойства:

• Закрытие вниз: если ${\displaystyle {\mathcal {M}},X\models ^{\pm }\varphi }$ и ${\displaystyle Y\subseteq X}$, тогда ${\displaystyle {\mathcal {M}},Y\models ^{\pm }\varphi }$.
• Последовательность: ${\displaystyle {\mathcal {M}},X\models ^{+}\varphi }$ и ${\displaystyle {\mathcal {M}},X\models ^{-}\varphi }$ если и только если ${\displaystyle X=\emptyset }$.
• Нелокация: есть ${\displaystyle {\mathcal {M}},X,\varphi }$ такой, что ${\displaystyle {\mathcal {M}},X\models \varphi \not \Leftrightarrow M,X_{\upharpoonright {\mbox{Free}}(\varphi )}\models \varphi }$.

Поскольку формулы IF удовлетворяются командами, а формулы классической логики удовлетворяются назначениями, нет очевидного взаимного перевода между формулами IF и формулами некоторой классической логической системы. Однако есть процедура перевода^[17] формул IF в фразы из реляционный ${\displaystyle \Sigma _{1}^{1}}$ (фактически, один отличный перевод ${\displaystyle \tau _{U,R}}$ для каждого конечного ${\displaystyle U\supseteq {\mbox{Free}}(\varphi )}$ и для каждого выбора предикатного символа ${\displaystyle R}$ арности ${\displaystyle card(U)}$). В этом виде перевода дополнительный n-арный предикатный символ ${\displaystyle R}$ используется для представления команды n переменных ${\displaystyle X}$. Это мотивировано тем, что при заказе ${\displaystyle v_{1}\dots v_{n}}$ переменных ${\displaystyle dom(X)}$ было исправлено, можно связать отношение ${\displaystyle Rel_{v_{1}\dots v_{n}}(X)=\{(s(v_{1}),\dots ,s(v_{n}))|s\in X\}}$ в команду ${\displaystyle X}$. Согласно этим соглашениям, формула ЕСЛИ связана со своим переводом следующим образом:

${\displaystyle {\mathcal {M}},X\models \varphi \Leftrightarrow ({\mathcal {M}},Rel_{v_{1}\dots v_{n}}(X))\models \tau _{dom(X),R}(\varphi )}$

куда ${\displaystyle (M,Rel_{v_{1}\dots v_{n}}(X))}$ расширение ${\displaystyle {\mathcal {M}}}$ что назначает ${\displaystyle Rel_{v_{1}\dots v_{n}}(X)}$ как интерпретация сказуемого ${\displaystyle R}$.

Благодаря этой корреляции можно сказать, что на конструкции ${\displaystyle {\mathcal {M}}}$, формула IF ${\displaystyle \varphi }$ из n свободных переменных определяет семья русских родственников закончилась ${\displaystyle {\mathcal {M}}}$ (семья родственников ${\displaystyle Rel_{v_{1}\dots v_{n}}(X)}$ такой, что ${\displaystyle {\mathcal {M}},X\models \varphi }$).

В 2009 году Континен и Вяэнянен,^[18] с помощью процедуры частичного обратного преобразования показал, что семейства отношений, определяемые логикой IF, - это в точности те, которые непусты, замкнуты вниз и определимы в реляционной логике. ${\displaystyle \Sigma _{1}^{1}}$ с дополнительным предикатом ${\displaystyle R}$ (или, что то же самое, непустое и определяемое ${\displaystyle \Sigma _{1}^{1}}$ предложение, в котором ${\displaystyle R}$ происходит только отрицательно).

Расширенная логика IF

Если логика не закрывается классическим отрицанием. Логическое закрытие логики IF известно как расширенная логика IF и он эквивалентен собственному фрагменту ${\displaystyle \Delta _{2}^{1}}$ (Фигейра и др. 2011). Хинтикка (1996, стр.196) утверждал, что «практически вся классическая математика в принципе может быть выполнена в расширенной логике первого порядка IF».

Свойства и критика

Ряд свойств логики IF вытекает из логической эквивалентности с ${\displaystyle \Sigma _{1}^{1}}$ и приблизить к логика первого порядка включая теорема компактности, а Теорема Левенгейма – Сколема, а Крейг интерполяция теорема. (Вяэнянен, 2007, с. 86). Однако Вяэнянен (2001) доказал, что множество Числа Гёделя допустимых предложений логики IF с хотя бы одним двоичным предикатным символом (множество, обозначенное Вал_ЕСЛИ) является рекурсивно изоморфный с соответствующим набором гёделевских чисел действительных (полных) предложений второго порядка в словаре, который содержит один двоичный символ предиката (набор обозначается Вал²). Кроме того, Вяэнянен показал, что Вал² это полный Π₂-определяемый набор целых чисел, и что это Вал² не в ${\displaystyle \Sigma _{n}^{m}}$ для любого конечного м и п. Вяэнянен (2007, стр. 136–139) резюмирует результаты по сложности следующим образом:

Проблема	логика первого порядка	IF / зависимость / логика ESO
Решение	${\displaystyle \Sigma _{1}^{0}}$ (r.e. )	${\displaystyle \Pi _{2}}$
Не-срок действия	${\displaystyle \Pi _{1}^{0}}$ (основной. )	${\displaystyle \Sigma _{2}}$
Последовательность	${\displaystyle \Pi _{1}^{0}}$	${\displaystyle \Pi _{1}^{0}}$
Непоследовательность	${\displaystyle \Sigma _{1}^{0}}$	${\displaystyle \Sigma _{1}^{0}}$

Феферман (2006) цитирует результат Вяэнянена 2001 года, чтобы доказать (вопреки Хинтикке), что, хотя выполнимость может быть вопросом первого порядка, вопрос о том, есть ли у Verifier выигрышная стратегия над всеми структурами в целом, «приводит нас прямо к полная логика второго порядка"(курсив Фефермана). Феферман также подверг критике заявленную полезность расширенной логики ЕСЛИ, поскольку предложения в ${\displaystyle \Pi _{1}^{1}}$ не допускают теоретико-игровой интерпретации.

Примечания

1. Хинтикка и Санду, 1989
2. Кэмерон и Ходжес 2001
3. Ходжес 1997
4. Фигейра, Горин и Гримсон 2011
5. Hintikka 1996
6. Феферман, 2006 г.
7. Манн, Санду и Севенстер 2011
8. Хинтикка и Санду 1989
9. Санду 1993
10. Ходжес 1997
11. Ходжес 1997b
12. Walkoe 1970
13. Эндертон 1970
14. Берджесс 2003
15. Санду 1998
16. Вяэнянен 2007
17. Ходжес 1997b
18. Континен и Вяэнянен, 2009 г.

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

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

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

• Берджесс, Джон П. "Замечание о предложениях Хенкина и их противоположностях ", Notre Dame Journal of Formal Logic 44 (3): 185-188 (2003).
• Кэмерон, Питер и Ходжес, Уилфрид (2001) "Некоторая комбинаторика несовершенной информации ". Journal of Symbolic Logic 66: 673-684.
• Эклунд, Матти и Колак, Даниэль "Является ли логика первоочередной задачей Hintikka? " Синтез, 131 (3): 371-388 июнь 2002 г., [1].
• Эндертон, Герберт Б. "Конечные частично упорядоченные кванторы ", Mathematical Logic Quarterly Volume 16, Issue 8, 1970, стр. 393–397.
• Феферман, Соломон, «Что это за логика,« дружественная к независимости »?», В Философия Яакко Хинтикка (Рэндалл Э. Осье и Льюис Эдвин Хан, ред.); Библиотека живых философов об. 30, Открытый суд (2006), 453-469, http://math.stanford.edu/~feferman/papers/hintikka_iia.pdf.
• Фигейра, Сантьяго, Горин, Даниэль и Гримсон, Рафаэль «О выразительной силе IF-логики с классическим отрицанием», протоколы WoLLIC 2011, стр. 135-145, ISBN  978-3-642-20919-2,[2].
• Хинтикка, Яакко (1996), «Возвращение к принципам математики», Cambridge University Press, ISBN  978-0-521-62498-5.
• Хинтикка, Яакко, «Гиперклассическая логика (также известная как логика IF) и ее применение в логической теории», Бюллетень символической логики 8, 2002, 404-423 http://www.math.ucla.edu/~asl/bsl/0803/0803-004.ps.
• Хинтикка, Яакко и Габриэль Санду (1989), «Информационная независимость как семантическое явление», в Логика, методология и философия науки VIII (J. E. Fenstad, et al., Eds.), Северная Голландия, Амстердам, Дои:10.1016 / S0049-237X (08) 70066-1.
• Хинтикка, Яакко и Санду, Габриэль, "Теоретико-игровая семантика ", в Справочник по логике и языку, изд. J. van Benthem и A. ter Meulen, Elsevier 1996 (1-е изд.) Обновлено во 2-м втором издании книги (2011 г.).
• Ходжес, Уилфрид (1997), "Композиционная семантика языка несовершенной информации Журнал IGPL 5: 539–563.
• Ходжес, Уилфрид, "Some Strange Quantifiers", в Lecture Notes in Computer Science 1261: 51-65, январь 1997 г.
• Янссен, Тео М. В., «Независимый выбор и интерпретация логики ЕСЛИ». Журнал логики, языка и информации, Volume 11 Issue 3, Summer 2002, pp. 367-387. Дои:10.1023 / А: 1015542413718[3].
• Колак Даниил, На Hintikka, Belmont: Wadsworth 2001. ISBN  0-534-58389-X.
• Колак, Дэниел и Саймонс, Джон, «Результаты в: Сфера и важность философии Hintikka» в Дэниеле Колаке и Джон Саймонс, ред., Кванторы, вопросы и квантовая физика. Очерки философии Яакко Хинтикки, Springer 2004, стр. 205-268. ISBN  1-4020-3210-2, Дои:10.1007/978-1-4020-32110-0_11.
• Континен, Юха и Вяэнянен, Йоуко, «Об определимости в логике зависимости» (2009), Журнал логики, языка и информации 18 (3), 317-332.
• Манн, Аллен Л., Санду, Габриэль и Севенстер, Мерлин (2011) Дружественная к независимости логика. Теоретико-игровой подход, Издательство Кембриджского университета, ISBN  0521149347.
• Санду, Габриэль, "Если-логика и истина-определение ", Journal of Philosophical Logic, апрель 1998 г., том 27, выпуск 2, стр. 143–164.
• Санду, Габриэль, "О логике информационной независимости и ее приложениях ", Journal of Philosophical Logic Vol. 22, No. 1 (февраль 1993 г.), стр. 29-60.
• Вяэнянен, Йоуко, 2007, «Логика зависимости - новый подход к независимой логике», Cambridge University Press, ISBN  978-0-521-87659-9, [4].
• Уолко, Уилбур Джон мл. "Конечная частично упорядоченная количественная оценка ", The Journal of Symbolic Logic Vol. 35, No. 4 (Dec., 1970), pp. 535-555.

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

• Теро Туленхеймо, 2009 год ».Дружественная к независимости логика '. Стэнфордская энциклопедия философии.
• Уилфрид Ходжес, 2009. 'Логика и игры '. Стэнфордская энциклопедия философии.
• IF логика на Планета Математика