Введение
Расширение классической логики первого порядка. Независимость-дружественная логика (IF-логика; предложенная Яакко Хинтиккой и Габриэлем Санду в 1989 году) является расширением классической логики первого порядка (FOL) посредством кванторов со штрихом вида и , где – конечное множество переменных. Предполагаемое прочтение – «существует такое, что оно функционально независимо от переменных в ». IF-логика позволяет выражать более общие закономерности зависимости между переменными, чем те, что подразумеваются в логике первого порядка. Эта большая степень обобщенности приводит к фактическому увеличению выразительной силы; множество IF-предложений может характеризовать те же классы структур, что и экзистенциальная логика второго порядка. Например, она может выражать предложения с разветвленными кванторами, такие как формула , которая выражает бесконечность в пустой сигнатуре; это невозможно сделать в FOL. Следовательно, логика первого порядка в общем случае не может выразить эту закономерность зависимости, в которой зависит только от и , а зависит только от и . IF-логика более общая, чем разветвленные кванторы, например, тем, что она может выражать зависимости, которые не являются транзитивными, например, в префиксе кванторов , который выражает, что зависит от , а зависит от , но не зависит от . Введение IF-логики было частично мотивировано попыткой расширить игровую семантику логики первого порядка до игр с неполной информацией. Действительно, семантика для IF-предложений может быть задана в терминах таких игр (или, альтернативно, посредством процедуры перевода в экзистенциальную логику второго порядка). Семантику для открытых формул нельзя задать в форме тарскианской семантики; адекватная семантика должна уточнять, что означает, чтобы формула удовлетворялась набором назначений с общей областью переменных (командой), а не одним назначением. Такую командную семантику разработал Ходжес. Независимость-дружественная логика эквивалентна по выразительности на уровне предложений ряду других логических систем, основанных на командной семантике, таких как логика зависимости, зависимость-дружественная логика, логика исключения и логика независимости; за исключением последней, известно, что IF-логика также эквивалентна этим логикам на уровне открытых формул. Однако IF-логика отличается от всех вышеупомянутых систем тем, что ей не хватает локальности: значение открытой формулы нельзя описать только в терминах свободных переменных формулы; вместо этого оно зависит от контекста, в котором формула встречается. Независимость-дружественная логика разделяет ряд металлогических свойств с логикой первого порядка, но есть некоторые различия, включая отсутствие замкнутости относительно (классического, противоречивого) отрицания и более высокую сложность при определении истинности формул. Расширенная IF-логика решает проблему замкнутости, но ее игровая семантика более сложна, и эта логика соответствует большему фрагменту логики второго порядка, являющемуся собственным подмножеством . Хинтикка утверждал, что IF-логика и расширенная IF-логика должны использоваться в качестве основы для основ математики; это предложение в некоторых случаях встретило скептицизм.
Independence friendly logic (IF logic; proposed by Jaakko Hintikka and lt=Gabriel Sandu in 1989) is an extension of classical first order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second order logic
For example, it can express branching quantifier sentences, such as the formula which expresses infinity in the empty signature; this cannot be done in FOL. Therefore, first order logic cannot, in general, express this pattern of dependency, in which depends only on and , and depends only on and IF logic is more general than branching quantifiers, for example in that it can express dependencies that are not transitive, such as in the quantifier prefix , which expresses that depends on , and depends on , but does not depend on
The introduction of IF logic was partly motivated by the attempt of extending the game semantics of first order logic to games of imperfect information. Indeed, a semantics for IF sentences can be given in terms of these kinds of games (or, alternatively, by means of a translation procedure to existential second order logic). A semantics for open formulas cannot be given in the form of a Tarskian semantics; an adequate semantics must specify what it means for a formula to be satisfied by a set of assignments of common variable domain (a team) rather than satisfaction by a single assignment. Such a team semantics was developed by Hodges. Independence friendly logic is translation equivalent, at the level of sentences, with a number of other logical systems based on team semantics, such as dependence logic, dependence friendly logic, exclusion logic and independence logic; with the exception of the latter, IF logic is known to be equiexpressive to these logics also at the level of open formulas. However, IF logic differs from all the above mentioned systems in that it lacks locality: the meaning of an open formula cannot be described just in terms of the free variables of the formula; it is instead dependent on the context in which the formula occurs. Independence friendly logic shares a number of metalogical properties with first order logic, but there are some differences, including lack of closure under (classical, contradictory) negation and higher complexity for deciding the validity of formulas. Extended IF logic addresses the closure problem, but its game theoretical semantics is more complicated, and such logic corresponds to a larger fragment of second order logic, a proper subset of
Hintikka argued that IF and extended IF logic should be used as a basis for the foundations of mathematics; this proposal was met in some cases with skepticism.
Синтаксис
В литературе появилось несколько несколько различных вариантов представления логики, благоприятной независимости; здесь мы придерживаемся подхода Mann et al (2011).
Термины и атомные формулы
Для фиксированной сигнатуры σ термины и атомные формулы определяются точно так же, как в логике первого порядка с равенством.
IF-речения
Формула IF, которая представляет собой условную конструкцию (или предложение) IF.
Семантика
Для определения семантики логики IF предложено три основных подхода. Первые два, основанные соответственно на играх с неполной информацией и на сколемизации, используются главным образом для определения предложений IF. Первый из них обобщает аналогичный подход для логики первого порядка, который основывался на играх с полной информацией. Третий подход, семантика команд, является композиционной семантикой в духе тарскианской семантики. Однако эта семантика не определяет, что значит, чтобы формула была удовлетворена назначением (скорее, множеством назначений). Первые два подхода были разработаны в более ранних публикациях по логике IF, а третий – Ходжесом в 1997 году. В этом разделе мы будем различать эти три подхода, используя различные индексы, например, Далее, поскольку эти три подхода в принципе эквивалентны, в остальной части статьи будет использоваться только символ .
Семантика теории игр
Семантика теории игр присваивает значения истинности условным высказываниям (IF-высказываниям) в соответствии со свойствами некоторых двухместных игр с неполной информацией. Для удобства изложения целесообразно связывать игры не только с высказываниями, но и с формулами. Более точно, игры определяются для каждой тройки, состоящей из условной формулы, структуры и интерпретации.
Игроки
В семантической игре участвуют два игрока: Элоиза (или Верификатор) и Абелард (или Фальсификатор).
Правила игры
Допустимые ходы в семантической игре определяются синтаксической структурой рассматриваемой формулы. Для упрощения, мы сначала предположим, что формула приведена к отрицательной нормальной форме, где символы отрицания встречаются только перед атомарными подформулами. Если формула является литералом, игра заканчивается, и если она истинна (в смысле логики первого порядка), то Элоиза выигрывает; в противном случае выигрывает Абелард. Если , то Абелард выбирает одну из подформул , и запускается соответствующая игра . Если , то Элоиза выбирает одну из подформул , и запускается соответствующая игра . Если , то Абелард выбирает элемент из , и запускается игра . Если , то Элоиза выбирает элемент из , и запускается игра . В более общем случае, если формула не приведена к отрицательной нормальной форме, мы можем сформулировать правило для отрицания: когда игра достигает формулы с отрицанием, игроки начинают играть в двойную игру, в которой роли Проверяющего и Опровергателя меняются местами.
История
Неформально, последовательность ходов в игре – это история. В конце каждой истории разыгрывается некоторая подигра; мы называем присвоение, связанное с , и вхождение подформулы, связанное с . Игрок, связанный с , – Элоиза, если наиболее внешний логический оператор в является или , и Абелард, если это или . Множество допустимых ходов в истории равно , если наиболее внешний оператор в является или ; оно равно (где – любые два различных объекта, символизирующие ‘левый’ и ‘правый’), если наиболее внешний оператор в является или . Для двух присвоений с одинаковой областью определения, мы пишем , если для любой переменной. Неполная информация вводится в игры посредством условия, что определенные истории неразличимы для соответствующего игрока; неразличимые истории образуют ‘информационный набор’. Интуитивно, если история принадлежит информационному набору , то связанный с игрок не знает, находится ли он в или в какой-либо другой истории из . Рассмотрим две истории такие, что связанные с ними являются идентичными вхождениями подформулы вида (или ); если кроме того , мы пишем (в случае ) или (в случае ), чтобы указать, что эти две истории неразличимы для Элоизы, соответственно, для Абеляра. Мы также постулируем, в общем случае, рефлексивность этого отношения: если , то ; и если , то .
The set of allowed moves in a history is if the most external operator of is or ; it is ( being any two distinct objects, symbolizing 'left' and 'right') in case the most external operator of is or
Given two assignments of same domain, and we write if on any variable
Imperfect information is introduced in the games by stipulating that certain histories are indistinguishable for the associated player; indistinguishable histories are said to form an 'information set'. Intuitively, if the history is in the information set , the player associated to does not know whether he is in or in some other history of Consider two histories such that the associated are identical subformula occurrences of the form ( or ); if furthermore , we write (in case ) or (in case ), in order to specify that the two histories are indistinguishable for Eloise, resp. for Abelard. We also stipulate, in general, reflexivity of this relation: if , then ; and if , then .
Стратегии
Для фиксированной игры , обозначьте через множество историй, связанных с Элоизой, и аналогично через множество историй Абеляра. Стратегия для Элоизы в игре — это любое отображение, которое сопоставляет каждой возможной истории, в которой наступает ход Элоизы, допустимый ход; точнее, любое отображение , такое что для каждой истории можно двойственно определить стратегии Абеляра. Стратегия для Элоизы называется равномерной, если, когда , ; для Абеляра, если влечет за собой . Стратегия для Элоизы называется выигрышной, если Элоиза выигрывает в каждой терминальной истории, достижимой при игре в соответствии со стратегией. Аналогично для Абеляра.
A strategy for Eloise is winning if Eloise wins in each terminal history that can be reached by playing according to Similarly for Abelard.
Правда, ложь, неопределенность
Предложение IF истинно в структуре, если у Элоизы есть гарантированная выигрышная стратегия в игре. Оно ложно, если у Абеляра есть выигрышная стратегия. Если ни у Элоизы, ни у Абеляра нет выигрышной стратегии, то результат не определен.
It is false if Abelard has a winning strategy. It is undetermined if neither Eloise nor Abelard has a winning strategy.
Консервативность
Семантика логики IF, определенная таким образом, является консервативным расширением семантики первого порядка в следующем смысле. Если φ – предложение IF с пустыми множествами слэшей, сопоставим ему формулу первого порядка ψ, которая идентична φ, за исключением того, что каждый IF-квантор заменяется соответствующим квантором первого порядка. Тогда φ истинно (выполнимо) в смысле Тарского тогда и только тогда, когда ψ истинно (выполнимо) в смысле Тарского; и φ ложно (невыполнимо) в смысле Тарского тогда и только тогда, когда ψ ложно (невыполнимо) в смысле Тарского.
Семантика Skolem
Определение истины для условных предложений может быть дано, альтернативно, посредством перевода в экзистенциальную логику второго порядка. Этот перевод обобщает процедуру сколемизации логики первого порядка. Ложность определяется двойной процедурой, называемой крейселизацией.
Школемизация
При наличии формулы IF, мы сначала определяем её сколемизацию, релятивизированную к конечному множеству переменных. Для каждого экзистенциального квантора, встречающегося в формуле , вводим новый функциональный символ (так называемую "функцию Сколема"). Обозначим через формулу, полученную заменой в формуле всех свободных вхождений переменной термом . Сколемизация формулы относительно множества , обозначаемая , определяется следующими индуктивными правилами: если является литералом. , где является списком переменных в . Если является формулой IF, её (нерелятивизированная) сколемизация определяется как .
if is a literal. . , where is a list of the variables in
If is an IF sentence, its (unrelativized) Skolemization is defined as .
Крейселизация
При данной формуле IF, каждому универсальному квантору, встречающемуся в ней, сопоставьте новый символ функции ("функция Крейзеля"). Тогда, крейзелизация формулы относительно конечного множества переменных определяется следующими индуктивными правилами: если является литералом. , где – список переменных в . Если является IF-предложением, его (нерелятивизированная) крейзелизация определяется как .
if is a literal. . , where is a list of the variables in
If is an IF sentence, its (unrelativized) Kreiselization is defined as .
Правда, ложь, неопределенность
Если дано предложение IF с экзистенциальными кванторами, структура и список функций подходящей арности, мы обозначаем как расширение структуры , в котором функции интерпретируются как функции Сколема предложения. Предложение IF истинно на структуре , что записывается как , если существует кортеж функций, таких что . Аналогично, предложение ложно на структуре, если существует кортеж функций, таких что ; и неопределено, если ни одно из предыдущих условий не выполняется. Для любого предложения IF семантика Сколема возвращает те же значения, что и игросемантическая семантика.
An IF sentence is true on a structure , written , if there is a tuple of functions such that Similarly, if there is a tuple of functions such that ; and iff neither of the previous conditions holds. For any IF sentence, Skolem Semantics returns the same values as Game theoretical Semantics.
Семантика команды
С помощью командной семантики можно дать композиционное описание семантики логики IF. Истина и ложь обосновываются понятием "выполнимости формулы командой".
Команды
Пусть – структура и – конечное множество переменных. Тогда команда над с областью определения – это набор присваиваний над с областью определения , то есть набор функций из в .
Дублирование и дополнение команд
Дублирование и дополнение — это две операции над командами, связанные с семантикой всеобщей и существованияльной квантификации. Для команды над структурой и переменной, дублирующая команда — это команда. Для команды над структурой, функцией и переменной, дополняющая команда — это команда. Обычно повторяющиеся применения этих двух операций заменяют более компактными обозначениями, например, для .
It is customary to replace repeated applications of these two operation with more succinct notations, such as for .
Единые функции в группах
Как и выше, для двух назначений с одинаковой областью определения переменных, мы пишем, если для каждой переменной выполняется условие . Для команды на структуре и конечного множества переменных мы говорим, что функция является равномерной, если при .
Given a team on a structure and a finite set of variables, we say that a function is uniform if whenever .
Правда, ложь, неопределенность
Согласно командной семантике, предложение IF считается истинным на структуре, если оно выполняется на ней командой-одиночкой, что обозначается так: . Аналогично, считается ложным на , если ; считается неопределённым, если и .
Similarly, is said to be false on if ; it is said to be undetermined if and .
Понятия эквивалентности
Поскольку логика IF, в общепринятом понимании, является трехзначной, представляют интерес различные понятия эквивалентности формул.
Эквивалентность формул
Пусть и будут две формулы IF. (истина влечет) если для любой структуры и любой команды такое, что (истина эквивалентна) если и (ложь влечет) если для любой структуры и любой команды такое, что (ложь эквивалентна) если и (сильно влечет) если и (сильно эквивалентна) если и .
( is truth equivalent to ) if and
( falsity entails ) if for any structure and any team such that
( is falsity equivalent to ) if and
( strongly entails to ) if and
( is strongly equivalent to ) if and .
Равный смысл предложений
Вышеуказанные определения конкретизируются для предложений IF следующим образом. Два предложения IF истинно-эквивалентны, если они истинны в одних и тех же структурах; ложно-эквивалентны, если они ложны в одних и тех же структурах; сильно эквивалентны, если они одновременно истинно- и ложно-эквивалентны. Интуитивно, использование сильной эквивалентности равносильно рассмотрению логики IF как трёзначной (истина/неопределённость/ложь), в то время как истинная эквивалентность рассматривает предложения IF как двузначные (истина/ложь).
Эквивалентность в контексте
Многие логические правила логики ИФ могут быть адекватно выражены только с помощью более узких понятий эквивалентности, учитывающих контекст, в котором может встречаться формула. Например, если S – конечное множество переменных, а φ и ψ – формулы, можно утверждать, что φ истинно эквивалентна ψ относительно S, если для любой структуры M и любой интерпретации I из области определения M это условие выполняется.
Уровень предложения
Предложения IF могут быть переведены с сохранением истинности в предложения (функциональной) экзистенциальной логики второго порядка с помощью процедуры сколемизации (см. выше). И наоборот, любое предложение может быть переведено в предложение IF с помощью варианта процедуры перевода Walkoe-Enderton для частично упорядоченных кванторов. Другими словами, логика IF и экзистенциальная логика второго порядка эквивалентны по выразительной силе на уровне предложений. Эта эквивалентность может быть использована для доказательства многих следующих свойств; они наследуются от экзистенциальной логики второго порядка и во многих случаях аналогичны свойствам FOL. Мы обозначаем множество (возможно бесконечное) предложений IF как Γ. Свойство Лёвенгейма-Сколема: если Γ имеет бесконечную модель или произвольно большие конечные модели, то у него есть модели каждой бесконечной кардинальности. Экзистенциальная компактность: если каждое конечное подмножество Γ имеет модель, то и Γ имеет модель. Отсутствие дедуктивной компактности: существуют множества Γ такие, что Γ ⊢ φ, но для любого конечного подмножества Γ ⊬ φ. Это отличие от FOL. Теорема о разделении: если предложения IF Γ1 и Γ2 взаимно несовместимы, то существует предложение FOL φ такое, что Γ1 ⊢ φ и Γ2 ⊢ ¬φ. Это является следствием теоремы интерполяции Крейга для FOL. Теорема Берджесса: если предложения IF Γ1 и Γ2 взаимно несовместимы, то существует предложение IF φ такое, что Γ1 ⊢ φ и Γ2 ⊢ ¬φ (кроме, возможно, структур из одного элемента). В частности, эта теорема показывает, что отрицание в логике IF не является семантической операцией относительно эквивалентности по истинности (предложения, эквивалентные по истинности, могут иметь неэквивалентные отрицания). Определимость истины: существует предложение IF φ, на языке арифметики Пеано, такое, что для любого предложения IF ψ, φ ⊢ “ψ истинно” (где “ψ истинно” обозначает нумерацию Гёделя для ψ). Более слабое утверждение также справедливо для нестандартных моделей арифметики Пеано.
Расширенная логика IF
Логика IF не замкнута относительно классического отрицания. Булево замыкание логики IF известно как расширенная логика IF и эквивалентно собственному фрагменту (Figueira et al. 2011). Хинтикка (1996, с. 196) утверждал, что "практически вся классическая математика в принципе может быть построена в расширенной логике IF первого порядка".
Свойства и критика
Ряд свойств логики IF вытекают из её логической эквивалентности и приближают её к логике первого порядка, включая теорему о компактности, теорему Лёвенхайма — Сколема и теорему интерполяции Крейга (Väänänen, 2007, с. 86). Однако Väänänen (2001) доказал, что множество чисел Гёделя валидных предложений логики IF с хотя бы одним бинарным символом предиката (множество, обозначенное ValIF) рекурсивно изоморфно соответствующему множеству чисел Гёделя валидных (полных) предложений второго порядка в словаре, содержащем один бинарный символ предиката (множество, обозначенное Val2). Более того, Väänänen показал, что Val2 является полным Π2-определимым множеством целых чисел, и что Val2 не принадлежит для любых конечных m и n. Väänänen (2007, с. 136–139) суммирует результаты о сложности следующим образом:
predicate symbol (set denoted by ValIF) is recursively isomorphic with the corresponding set of Gödel numbers of valid (full) second order sentences in a vocabulary that contains one binary predicate symbol (set denoted by Val2). Furthermore, Väänänen showed that Val2 is the complete Π2 definable set of integers, and that it is Val2 not in for any finite m and n. Väänänen (2007, pp. 136–139) summarizes the complexity results as follows:
Проблема | Логика первого порядка | IF/dependence/ESO логика | Решение (r. e.) | Невалидность (co r. e.) | Состоятельность | Несостоятельность
Феферман (2006) ссылается на результат Väänänen 2001 года, чтобы утверждать (в противовес Hintikka), что, хотя выполнимость может быть вопросом первого порядка, вопрос о наличии выигрышной стратегии для Verifier над всеми структурами в целом «полностью переводит нас в логику второго порядка» (выделено Феферманом). Феферман также критиковал заявленную полезность расширенной логики IF, поскольку предложения в не допускают игротеоретической интерпретации.