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

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

Мотивация

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

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

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

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

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

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

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

• До тех пор, пока Дана Скотт не начал писать модельную теорию комбинаторной логики в конце 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, одна из двух, предложенных Куном (1983), кратка и проста для описания, но в ней широко используются свободные переменные , поэтому она не в полной мере отражает дух PFL. Кун дает еще одну аксиоматизацию, обходящуюся без свободных переменных, но ее труднее описать, и она требует широкого использования определенных функторов. Кун доказал, что обе его аксиоматизации ПФЛ верны и полны .

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

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

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

$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 ) и подчиняется свойству подстановки:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

$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 поворачивает переменные в списке аргументов вправо, так что последняя переменная становится первой.

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

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

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

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

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

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

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

$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.

Кун (1983) считает Большую инверсию и Малую инверсию примитивными. Обозначение p в Куне соответствует inv ; у него нет аналога перестановки и, следовательно, нет для нее аксиом. Если, следуя Куайну (1976), p считать примитивным, Inv и inv можно определить как нетривиальные комбинации + , ∃ и итерированного p .

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

Выражение	Степень
$p;\operatorname {Inv} ;\operatorname {inv} ;\ \lnot ;\ I$	без изменений
$+F^{n-1};\ \exists F^{n+1};\ SF^{n+1}$	н
$\alpha ^{m}\beta ^{n};\ F^{m}\times G^{n}$	Макс( м , п )

Правила

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

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

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

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

$\exists I$

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

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

+ и ∃ аннигилируют друг друга:

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

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

${\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 распределяет по соединению:

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

Идентичность имеет интересный смысл:

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

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

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

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

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

Бэкон также:

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

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

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

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

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

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

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

3. Замените союз декартовым произведением , ссылаясь на тот факт:
   $(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) до тех пор, пока все количественные переменные не будут исключены. Устраните любые дизъюнкции, попадающие в область действия квантора, призвав эквивалентность:
   $(\alpha \lor \beta \lor ...)\leftrightarrow \lnot (\lnot \alpha \land \lnot \beta \land ...).$

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

Канонической основой математики является аксиоматическая теория множеств , в которой базовая логика состоит из логики первого порядка с тождеством , а вселенная дискурса полностью состоит из множеств. Имеется единственная буква-предикат степени 2, интерпретируемая как членство во множестве. Перевод PFL канонической аксиоматической теории множеств ZFC не сложен, поскольку ни одна аксиома ZFC не требует более 6 количественных переменных.

См. также

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

Ссылки

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

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

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