Логика предикатного функтора

Алгебраизация логики первого порядка

В математической логике логика предикатных функторов ( PFL ) — один из нескольких способов выражения логики первого порядка (также известной как логика предикатов ) чисто алгебраическими средствами, т. е. без квантифицированных переменных . PFL использует небольшое количество алгебраических устройств, называемых предикатными функторами (или модификаторами предикатов ) ^[1] , которые оперируют терминами, чтобы получить термины. PFL в основном является изобретением логика и философа Уилларда Куайна .

Мотивация

Источником для этого раздела, как и для большей части этой записи, является Куайн (1976). Куайн предложил PFL как способ алгебраизации логики первого порядка способом, аналогичным тому, как булева алгебра алгебрирует пропозициональную логику . Он разработал PFL так, чтобы он имел в точности выразительную силу логики первого порядка с тождеством . Следовательно, метаматематика PFL в точности соответствует метаматематике логики первого порядка без интерпретируемых предикатных букв: обе логики являются обоснованными , полными и неразрешимыми . Большинство работ Куайна по логике и математике, опубликованных за последние 30 лет его жизни, так или иначе касались PFL. ^{[ требуется ссылка ]}

Куайн взял «функтор» из трудов своего друга Рудольфа Карнапа , первого, кто применил его в философии и математической логике , и определил его следующим образом:

«Слово функтор , грамматическое по смыслу, но логическое по месту обитания... — это знак, который присоединяется к одному или нескольким выражениям данного грамматического вида(ов) для создания выражения данного грамматического вида» (Куайн 1982: 129)

Другие способы алгебраизации логики первого порядка, помимо PFL, включают в себя:

• Цилиндрическая алгебра Альфреда Тарского и его американских студентов. Упрощенная цилиндрическая алгебра, предложенная в Бернайсе (1959), привела Куайна к написанию статьи, содержащей первое использование фразы «предикатный функтор»;
• Полиадическая алгебра Пола Халмоша . В силу своих экономичных примитивов и аксиом эта алгебра больше всего напоминает PFL;
• Реляционная алгебра алгебраизирует фрагмент логики первого порядка, состоящий из формул, не имеющих атомарной формулы, лежащей в области действия более трех кванторов . Однако этот фрагмент достаточен для арифметики Пеано и аксиоматической теории множеств ZFC ; следовательно, реляционная алгебра, в отличие от PFL, является незавершенной . Большая часть работ по реляционной алгебре с 1920 года была выполнена Тарским и его американскими учениками. Сила реляционной алгебры не стала очевидной до монографии Тарского и Живанта (1987), опубликованной после трех важных статей, касающихся PFL, а именно Бэкона (1985), Куна (1983) и Куайна (1976);
• Комбинаторная логика строится на комбинаторах , функциях высшего порядка , областью действия которых является другой комбинатор или функция, и областью действия которых является еще один комбинатор. Следовательно, комбинаторная логика выходит за рамки логики первого порядка, обладая выразительной силой теории множеств , что делает комбинаторную логику уязвимой для парадоксов . С другой стороны, функтор предикатов просто отображает предикаты (также называемые терминами ) в предикаты.

PFL, пожалуй, самый простой из этих формализмов, но при этом о нем написано меньше всего.

Куайн всю жизнь был очарован комбинаторной логикой , о чем свидетельствует его введение к переводу в Van Heijenoort (1967) статьи русского логика Моисея Шёнфинкеля, основавшего комбинаторную логику. Когда Куайн начал работать над PFL всерьез, в 1959 году, комбинаторная логика обычно считалась неудачей по следующим причинам:

• До тех пор, пока в конце 1960-х годов Дана Скотт не начал писать о модельной теории комбинаторной логики, над этой логикой работали почти только Хаскелл Карри , его ученики и Роберт Фейс в Бельгии;
• Удовлетворительные аксиоматические формулировки комбинаторной логики появлялись медленно. В 1930-х годах некоторые формулировки комбинаторной логики оказались противоречивыми . Карри также открыл парадокс Карри , свойственный комбинаторной логике;
• Лямбда -исчисление , обладающее той же выразительной силой, что и комбинаторная логика , рассматривалось как высший формализм.

Формализация Куна

Синтаксис PFL , примитивы и аксиомы, описанные в этом разделе, в основном принадлежат Стивену Куну (1983). Семантика функторов принадлежит Куайну (1982). Остальная часть этой записи включает некоторую терминологию из Бэкона (1985).

Синтаксис

Атомарный термин — это заглавная латинская буква, за исключением I и S , за которой следует числовой верхний индекс , называемый степенью , или соединенные строчные переменные, вместе известные как список аргументов . Степень термина передает ту же информацию, что и количество переменных, следующих за предикатной буквой. Атомарный термин степени 0 обозначает булеву переменную или значение истинности . Степень I всегда равна 2 и поэтому не указывается.

«Комбинаторные» (слово принадлежит Куайну) предикатные функторы, все монадические и специфичные для PFL, — это Inv , inv , ∃ , + и p . Терм является либо атомарным термином, либо сконструирован по следующему рекурсивному правилу. Если τ — терм, то Inv τ, inv τ, ∃ τ, + τ и p τ — термы. Функтор с верхним индексом n , n — натуральное число > 1, обозначает n последовательных применений (итераций) этого функтора.

Формула является либо термином, либо определяется рекурсивным правилом: если α и β являются формулами, то αβ и ~(α) также являются формулами. Следовательно, «~» является другим монадическим функтором, а конкатенация является единственным диадическим предикатным функтором. Куайн назвал эти функторы «алетическими». Естественной интерпретацией «~» является отрицание ; конкатенация — любая связка , которая в сочетании с отрицанием образует функционально полный набор связок. Предпочтительным функционально полным набором Куайна были конъюнкция и отрицание . Таким образом, конкатенированные термины рассматриваются как соединенные. Обозначение + принадлежит Бэкону (1985); все остальные обозначения принадлежат Куайну (1976; 1982). Алетическая часть PFL идентична схемам булевых терминов Куайна (1982).

Как известно, два алетических функтора можно заменить одним диадическим функтором со следующим синтаксисом и семантикой : если α и β являются формулами, то (αβ) является формулой, семантика которой «не (α и/или β)» (см. NAND и NOR ).

Аксиомы и семантика

Куайн не изложил ни аксиоматизацию, ни процедуру доказательства для PFL. Следующая аксиоматизация PFL, одна из двух, предложенных в Kuhn (1983), является краткой и простой для описания, но широко использует свободные переменные и поэтому не полностью соответствует духу PFL. Кун дает другую аксиоматизацию, обходящуюся без свободных переменных, но ее сложнее описать, и она широко использует определенные функторы. Кун доказал, что обе его аксиоматизации PFL обоснованы и полны .

Этот раздел построен вокруг примитивных предикатных функторов и нескольких определенных. Алетические функторы могут быть аксиоматизированы любым набором аксиом для сентенциальной логики, примитивами которой являются отрицание и один из ∧ или ∨. Эквивалентно, все тавтологии сентенциальной логики могут быть приняты в качестве аксиом.

Семантика Куайна (1982) для каждого предикатного функтора изложена ниже в терминах абстракции (нотация конструктора множеств), за которой следует либо соответствующая аксиома из Куна (1983), либо определение из Куайна (1976). Нотация обозначает множество n -кортежей, удовлетворяющих атомарной формуле ${\displaystyle \{x_{1}\cdots x_{n}:Fx_{1}\cdots x_{n}\}}$ ${\displaystyle Fx_{1}\cdots x_{n}.}$

• Идентичность , I , определяется как:

${\displaystyle IFx_{1}x_{2}\cdots x_{n}\leftrightarrow (Fx_{1}x_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{2}\cdots x_{n}){\text{.}}}$

Тождество рефлексивно ( Ixx ), симметрично ( Ixy → Iyx ), транзитивно ( ( Ixy ∧ Iyz ) → Ixz ) и подчиняется свойству подстановки:

${\displaystyle (Fx_{1}\cdots x_{n}\land Ix_{1}y)\rightarrow Fyx_{2}\cdots x_{n}.}$

• Заполнение , + , добавляет переменную слева от любого списка аргументов.

${\displaystyle \ +F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{0}x_{1}\cdots x_{n}:F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle +Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}\cdots x_{n}.}$

• Обрезка , ∃ , стирает самую левую переменную в любом списке аргументов.

${\displaystyle \exists F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:\exists x_{1}F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle Fx_{1}\cdots x_{n}\rightarrow \exists Fx_{2}\cdots x_{n}.}$

Обрезка позволяет использовать два полезных функтора:

• Отражение , S :

${\displaystyle SF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:F^{n}x_{2}x_{2}\cdots x_{n}\}.}$

${\displaystyle SF^{n}\leftrightarrow \exists IF^{n}.}$

S обобщает понятие рефлексивности на все термины любой конечной степени, большей 2. Примечание: S не следует путать с примитивным комбинатором S комбинаторной логики.

• Декартово произведение ,; ${\displaystyle \times }$

${\displaystyle F^{m}\times G^{n}\leftrightarrow F^{m}\exists ^{m}G^{n}.}$

Только здесь Куайн принял инфиксную запись, поскольку эта инфиксная запись для декартова произведения очень хорошо устоялась в математике. Декартово произведение позволяет переформулировать конъюнкцию следующим образом:

${\displaystyle F^{m}x_{1}\cdots x_{m}G^{n}x_{1}\cdots x_{n}\leftrightarrow (F^{m}\times G^{n})x_{1}\cdots x_{m}x_{1}\cdots x_{n}.}$

Переупорядочьте объединенный список аргументов так, чтобы сместить пару дублирующихся переменных в крайнее левое положение, затем вызовите S, чтобы устранить дублирование. Повторение этого столько раз, сколько требуется, приведет к списку аргументов длиной max( m , n ).

Следующие три функтора позволяют переупорядочивать списки аргументов по желанию.

• Основная инверсия , Inv , поворачивает переменные в списке аргументов вправо, так что последняя переменная становится первой.

${\displaystyle \operatorname {Inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{n}x_{1}\cdots x_{n-1}\}.}$

${\displaystyle \operatorname {Inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{n}x_{1}\cdots x_{n-1}.}$

• Незначительная инверсия , inv , меняет местами первые две переменные в списке аргументов.

${\displaystyle \operatorname {inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{2}x_{1}\cdots x_{n}\}.}$

${\displaystyle \operatorname {inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{1}\cdots x_{n}.}$

• Перестановка p сдвигает вторую и последнюю переменные в списке аргументов влево, так что вторая переменная становится последней.

${\displaystyle \ pF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{1}x_{3}\cdots x_{n}x_{2}\}.}$

${\displaystyle pFx_{1}\cdots x_{n}\leftrightarrow \operatorname {Inv} \operatorname {inv} Fx_{1}x_{3}\cdots x_{n}x_{2}.}$

При наличии списка аргументов, состоящего из n переменных, p неявно обрабатывает последние n −1 переменных как велосипедную цепь, где каждая переменная составляет звено в цепи. Одно применение p продвигает цепь на одно звено. k последовательных применений p к F ⁿ перемещают k +1 переменную на вторую позицию аргумента в F .

Когда n =2, Inv и inv просто меняют местами x ₁ и x ₂ . Когда n =1, они не оказывают никакого влияния. Следовательно, p не оказывает никакого влияния, когда n < 3.

Kuhn (1983) берет Major inversion и Minor inversion как примитивные. Обозначение p у Kuhn соответствует inv ; у него нет аналога Permutation и, следовательно, нет для него аксиом. Если, следуя Quine (1976), p берется как примитивный, Inv и inv можно определить как нетривиальные комбинации + , ∃ и итерированного p .

В следующей таблице показано, как функторы влияют на степени своих аргументов.

Правила

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

• Модус поненс ;
• Пусть α и β — формулы PFL, в которых не появляется. Тогда если — теорема PFL, то — также теорема PFL. ${\displaystyle x_{1}}$ ${\displaystyle (\alpha \land Fx_{1}...x_{n})\rightarrow \beta }$ ${\displaystyle (\alpha \land \exists Fx_{2}...x_{n})\rightarrow \beta }$

Некоторые полезные результаты

Вместо аксиоматизации PFL Куайн (1976) предложил следующие гипотезы в качестве кандидатов на аксиомы.

${\displaystyle \exists I}$

n −1 последовательных итераций p восстанавливает статус-кво ante :

${\displaystyle F^{n}\leftrightarrow p^{n-1}F^{n}}$

+ и ∃ уничтожают друг друга:

${\displaystyle {\begin{cases}F^{n}\rightarrow +\exists F^{n}\\F^{n}\leftrightarrow \exists +F^{n}\end{cases}}}$

Отрицание распространяется на + , ∃ и p :

${\displaystyle {\begin{cases}+\lnot F^{n}\leftrightarrow \lnot +F^{n}\\\lnot \exists F^{n}\rightarrow \exists \lnot F^{n}\\p\lnot F^{n}\leftrightarrow \lnot pF^{n}\end{cases}}}$

+ и p распределяются по конъюнкции:

${\displaystyle {\begin{cases}+(F^{n}G^{m})\leftrightarrow (+F^{n}+G^{m})\\p(F^{n}G^{m})\leftrightarrow (pF^{n}pG^{m})\end{cases}}}$

Идентичность имеет интересное последствие:

${\displaystyle IF^{n}\rightarrow p^{n-2}\exists p+F^{n}}$

Куайн также предположил правило: если α является теоремой PFL, то таковыми являются pα , +α и . ${\displaystyle \lnot \exists \lnot \alpha }$

Работа Бэкона

Бэкон (1985) берет условное выражение , отрицание , тождество , заполнение и основную и второстепенную инверсию как примитивные, а обрезку как определенную. Используя терминологию и обозначения, несколько отличающиеся от приведенных выше, Бэкон (1985) излагает две формулировки PFL:

• Формулировка естественной дедукции в стиле Фредерика Фитча. Бэкон доказывает, что эта формулировка верна и полна во всех подробностях.
• Аксиоматическая формулировка, которую Бэкон утверждает, но не доказывает, эквивалентна предыдущей. Некоторые из этих аксиом — просто гипотезы Куайна, переформулированные в обозначениях Бэкона.

Бэкон также:

• Обсуждает связь PFL с термином «логика» Соммерса (1982) и утверждает, что переработка PFL с использованием синтаксиса, предложенного в приложении Локвуда к Соммерсу, должна сделать PFL более простым для «чтения, использования и преподавания»;
• Затрагивает групповую теоретико-структурную структуру Inv и inv ;
• Упоминает, что пропозициональная логика , монадическая предикатная логика , модальная логика S5 и булева логика (не)переставляемых отношений являются фрагментами PFL.

От логики первого порядка к PFL

Следующий алгоритм адаптирован из Куайна (1976: 300–2). Имея замкнутую формулу логики первого порядка , сначала сделайте следующее:

• Прикрепите к каждой букве сказуемого числовой индекс, указывающий его степень;
• Перевести все универсальные квантификаторы в экзистенциальные квантификаторы и отрицание;
• Перепишите все атомарные формулы вида x = y как Ixy .

Теперь применим следующий алгоритм к предыдущему результату:

1. Переводим матрицы наиболее глубоко вложенных квантификаторов в дизъюнктивную нормальную форму , состоящую из дизъюнктов конъюнктов терминов, отрицая атомарные термины по мере необходимости. Полученная подформула содержит только отрицание, конъюнкцию, дизъюнкцию и экзистенциальную квантификацию .
2. Распределите квантификаторы существования по дизъюнктам в матрице, используя правило перехода (Куайн 1982: 119):

   ${\displaystyle \exists x[\alpha (x)\lor \gamma (x)]\leftrightarrow (\exists x\alpha (x)\lor \exists x\gamma (x)).}$

3. Заменим конъюнкцию декартовым произведением , ссылаясь на факт:
   ${\displaystyle (F^{m}\land G^{n})\leftrightarrow (F^{m}\times G^{n})\leftrightarrow (F^{m}\exists ^{m}G^{n});m<n.}$
4. Объедините списки аргументов всех атомарных терминов и переместите объединенный список в правую часть подформулы.
5. Используйте Inv и inv для перемещения всех экземпляров квантифицированной переменной (назовем ее y ) влево от списка аргументов.
6. Вызовите S столько раз, сколько потребуется, чтобы исключить все, кроме последнего экземпляра y . Исключите y , добавив к подформуле один экземпляр ∃ .
7. Повторяйте (1)-(6) до тех пор, пока все квантифицированные переменные не будут устранены. Устраните любые дизъюнкции, попадающие в область действия квантификатора, вызвав эквивалентность:
   ${\displaystyle (\alpha \lor \beta \lor ...)\leftrightarrow \lnot (\lnot \alpha \land \lnot \beta \land ...).}$

Обратный перевод, из PFL в логику первого порядка, обсуждается в работе Куайна (1976: 302–4).

Канонической основой математики является аксиоматическая теория множеств , с фоновой логикой, состоящей из логики первого порядка с тождеством , с вселенной дискурса, состоящей полностью из множеств. Существует одна предикатная буква степени 2, интерпретируемая как членство во множестве. Перевод канонической аксиоматической теории множеств ZFC на PFL не сложен, поскольку ни одна аксиома ZFC не требует более 6 квантифицированных переменных. ^[2]

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

• Алгебраическая логика

Сноски

1. Йоханнес Стерн, К предикатным подходам к модальности , Springer, 2015, стр. 11.
2. Аксиомы метаматематики.

Ссылки

• Бэкон, Джон, 1985, «Полнота логики предикат-функтор», Журнал символической логики 50 : 903–26.
• Пол Бернейс , 1959, «Uber eine naturliche Erweiterung des Relationenkalkuls» в издании Хейтинга А., « Конструктивность в математике» . Северная Голландия: 1–14.
• Кун, Стивен Т. , 1983, «Аксиоматизация логики предикатных функторов», Notre Dame Journal of Formal Logic 24 : 233–41.
• Уиллард Куайн , 1976, «Алгебраическая логика и предикатные функторы» в сборнике «Пути парадокса и другие эссе», переработанное и дополненное издание. Издательство Гарвардского университета: 283–307.
• Уиллард Куайн, 1982. Методы логики, 4-е изд. Издательство Гарвардского университета. Глава 45.
• Соммерс, Фред , 1982. Логика естественного языка . Oxford Univ. Press.
• Альфред Тарский и Дживант, Стивен, 1987. Формализация теории множеств без переменных . AMS .
• Жан Ван Хейеноорт , 1967. От Фреге до Гёделя: Справочник по математической логике . Издательство Гарвардского университета.

Внешние ссылки

• Введение в логику предикатов-функторов (загрузка в один клик, файл PS) Матса Даллёфа (Кафедра лингвистики, Уппсальский университет)