В математической логике , предикат функтор логика ( PFL ) является одним из нескольких способов выразить логику первого порядка (также известную как предикат логика ) чисто алгебраическими средствами, т.е. без количественных переменных . PFL использует небольшое количество алгебраических устройств, называемых функторами предикатов (или модификаторами предикатов ) [1], которые работают с терминами для получения терминов. PFL в основном изобретение логика и философа Уилларда Куайна .
Мотивация
Источником этого раздела, а также большей части этой статьи является Quine (1976). Куайн предложил 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).
Синтаксис
Атомный термин представляет собой верхний регистр латинской буквы, я и S освобожденный, с последующим числовым индексом называется ее степень , или сцепленных более низких переменных случая, известных под общим названием как список аргументов . Степень термина передает ту же информацию, что и количество переменных, следующих за предикатной буквой. Атомарный член степени 0 обозначает логическую переменную или значение истинности . Степень I всегда равна 2 и поэтому не указывается.
«Комбинаторными» (слово Куайна) предикатными функторами, монадическими и свойственными PFL, являются Inv , inv , ∃ , + и p . Термин является либо атомарным, либо построен по следующему рекурсивному правилу. Если τ - терм, то Inv τ, inv τ, ∃ τ, + τ и p τ - термы. Функтор с верхним индексом п , п натуральное число > 1, обозначает п последовательных приложений (итераций) этого функтора.
Формула - это либо термин, либо определяется рекурсивным правилом: если α и β являются формулами, то αβ и ~ (α) также являются формулами. Следовательно, «~» - еще один монадический функтор, а конкатенация - единственный диадический предикатный функтор. Куайн назвал эти функторы «алетическими». Естественная интерпретация «~» - отрицание ; Конкатенация - это любая связка, которая в сочетании с отрицанием образует функционально полный набор связок. Функционально полный набор Куайн предпочитал соединение и отрицание . Таким образом, сцепленные термины считаются соединенными. Обозначение + принадлежит Бэкону (1985); все остальные обозначения принадлежат Куайну (1976; 1982). Алетическая часть PFL идентична схемам логических терминов Куайна (1982).
Как хорошо известно, два алетических функтора могут быть заменены одним диадическим функтором со следующим синтаксисом и семантикой : если α и β - формулы, то (αβ) - это формула, семантика которой не (α и / или β) "(см. NAND и NOR ).
Аксиомы и семантика
Куайн не изложил ни процедуры аксиоматизации, ни процедуры доказательства для PFL. Следующая аксиоматизация PFL, одна из двух, предложенных Kuhn (1983), лаконична и легко описывается, но при этом широко использует свободные переменные и поэтому не полностью отражает дух PFL. Кун дает еще одну аксиоматизацию, обходящуюся без свободных переменных, но ее сложнее описать, и в ней широко используются определенные функторы. Кун доказал правильность и полноту обеих своих аксиоматизаций PFL .
Этот раздел построен на примитивных функторах предикатов и некоторых определенных. Алетические функторы могут быть аксиоматизированы с помощью любого набора аксиом сентенциальной логики , примитивы которой являются отрицанием и одним из или ∨. Точно так же все тавтологии сентенциальной логики могут быть приняты за аксиомы.
Семантика Куайна (1982) для каждого функтора предиката изложена ниже в терминах абстракции (нотация построителя множеств), за которой следует либо соответствующая аксиома из Куна (1983), либо определение из Куайна (1976). Обозначениеобозначает множество n -элементов, удовлетворяющих атомарной формуле
- Идентичность , I , определяется как:
Идентичность является рефлексивной ( Ixx ), симметричной ( Ixy → Iyx ), транзитивной (( Ixy ∧ Iyz ) → Ixz ) и подчиняется свойству подстановки:
- Padding , + , добавляет переменную слева от любого списка аргументов.
- Обрезка , ses , стирает крайнюю левую переменную в любом списке аргументов.
Обрезка позволяет использовать два полезных определенных функтора:
- Отражение , S :
S обобщает понятие рефлексивности на все члены любой конечной степени выше 2. NB: S не следует путать с примитивным комбинатором S комбинаторной логики.
- Декартово произведение ,;
Только здесь Куайн принял инфиксную нотацию, потому что эта инфиксная нотация для декартова произведения очень хорошо известна в математике. Декартово произведение позволяет переформулировать союз следующим образом:
Измените порядок составного списка аргументов, чтобы сдвинуть пару повторяющихся переменных в крайнее левое положение, затем вызовите S, чтобы исключить дублирование. Повторение этого столько раз, сколько требуется, приводит к списку аргументов длины max ( m , n ).
Следующие три функтора позволяют произвольно переупорядочивать списки аргументов.
- Основная инверсия , Inv , поворачивает переменные в списке аргументов вправо, так что последняя переменная становится первой.
- Незначительная инверсия , inv , меняет местами первые две переменные в списке аргументов.
- Перестановка , р , вращает второй через последние переменные в списке аргументов слева, так что вторая переменная становится последним.
Учитывая список аргументов, состоящий из n переменных, p неявно обрабатывает последние n - 1 переменную как велосипедную цепь, причем каждая переменная составляет звено в цепи. Одно применение p продвигает цепь на одно звено. K последовательных применений р к F п перемещает к переменной +1 ко второй позиции аргумента в F .
Когда n = 2, Inv и inv просто меняют местами x 1 и x 2 . Когда n = 1, они не действуют. Следовательно, p не действует, когда n <3.
Кун (1983) рассматривает основную инверсию и вспомогательную инверсию как примитивные. Обозначение p в Kuhn соответствует inv ; он не имеет аналога перестановки и, следовательно, не имеет для нее аксиом. Если, следуя Куайну (1976), p считается примитивным, Inv и inv могут быть определены как нетривиальные комбинации + , ∃ и повторного p .
В следующей таблице показано, как функторы влияют на степень своих аргументов.
Выражение | Степень |
---|---|
без изменений | |
п | |
макс ( м , п ) |
Правила
Все экземпляры предикатной буквы могут быть заменены другой предикатной буквой той же степени, не влияя на действительность. Эти правила являются:
- Modus ponens ;
- Пусть α и β - формулы ПФЛ, в которыхне появляются. Тогда если является теоремой ПФЛ, то также является теоремой ПФЛ.
Некоторые полезные результаты
Вместо аксиоматизации PFL Куайн (1976) предложил следующие гипотезы в качестве кандидатов в аксиомы.
n -1 последовательных итераций p восстанавливает status quo ante :
+ и ∃ уничтожают друг друга:
|
|
Отрицание распространяется на + , ∃ и p :
|
|
|
+ и p распределяются по соединению:
|
|
Идентичность имеет интересный смысл:
Куайн также предположил правило: если является теоремой PFL, то таковы а также .
Работа Бэкона
Бэкон (1985) рассматривает условное выражение , отрицание , идентичность , заполнение , а также инверсию Major и Minor как примитив, а обрезку - как определено. Используя терминологию и обозначения, несколько отличающиеся от приведенных выше, Бэкон (1985) предлагает две формулировки PFL:
- Естественный вычет формулировка в стиле Фредерика Fitch . Бэкон доказывает, что эта формулировка верна и полна во всех деталях.
- Аксиоматическая формулировка, которую Бэкон утверждает, но не доказывает, эквивалентную предыдущей. Некоторые из этих аксиом представляют собой просто гипотезы Куайна, переформулированные в обозначениях Бэкона.
Бэкон также:
- Обсуждает связь PFL с термином «логика» Соммерса (1982) и утверждает, что переработка PFL с использованием синтаксиса, предложенного в приложении Локвуда к Соммерсу, должна упростить «чтение, использование и обучение» PFL;
- Касания к теоретико-групповой структуре Inv и inv ;
- Упоминается, что сентенциальная логика , монадическая логика предикатов , модальная логика S5 и булева логика (не) перестановочных отношений - все это фрагменты PFL.
От логики первого порядка к PFL
Следующий алгоритм адаптирован из Quine (1976: 300-2). Учитывая замкнутую формулу из логики первого порядка , сначала сделать следующее:
- Прикрепите числовой индекс к каждой предикатной букве, указав ее степень;
- Перевести все универсальные кванторы в кванторы существования и отрицание;
- Переформулируйте все атомарные формулы вида x = y как Ixy .
Теперь примените следующий алгоритм к предыдущему результату:
1. Перевести матрицы наиболее глубоко вложенных кванторов в дизъюнктивной нормальной форме , состоящей из дизъюнктов из конъюнктов терминов, отрицающий атомные термины по мере необходимости. Результирующая подформула содержит только отрицание, соединение, дизъюнкцию и экзистенциальную количественную оценку.
2. Распределите кванторы существования по дизъюнктам в матрице, используя правило перехода (Quine 1982: 119):
3. Заменить союз декартовым произведением , указав на факт:
4. Объедините списки аргументов всех элементарных терминов и переместите объединенный список в крайнее правое положение от подформулы.
5. Используйте Inv и inv, чтобы переместить все экземпляры количественной переменной (назовите ее y ) в левую часть списка аргументов.
6. Вызовите S столько раз, сколько потребуется, чтобы удалить все, кроме последнего экземпляра y . Удалите y , поставив перед подформулой один экземпляр ∃ .
7. Повторяйте (1) - (6) до тех пор, пока все количественные переменные не будут исключены. Устраните любые дизъюнкции, попадающие в область действия квантификатора, применив эквивалентность:
Обратный перевод от PFL к логике первого порядка обсуждается в Quine (1976: 302-4).
Каноническая основа математики - это аксиоматическая теория множеств с базовой логикой, состоящей из логики первого порядка с идентичностью , с универсумом дискурса, полностью состоящим из множеств. Существует одна предикатная буква степени 2, интерпретируемая как принадлежность к множеству. PFL-перевод канонической аксиоматической теории множеств ZFC несложен , поскольку ни одна аксиома ZFC не требует более 6 количественных переменных. [2]
Смотрите также
- Алгебраическая логика
Сноски
- ^ Йоханнес Стерн, К подходам предикатов к модальности , Springer, 2015, стр. 11.
- ^ Аксиомы Metamath.
Рекомендации
- Бэкон, Джон, 1985, " Полнота логики предиката-функтора", Journal of Symbolic Logic 50 : 903–26.
- Пол Бернейс , 1959, "Uber eine naturliche Erweiterung des Relationenkalkuls" в Heyting, A., ed., Constructivity in Mathematics . Северная Голландия: 1–14.
- Кун, Стивен Т. , 1983, " Аксиоматизация логики предикатного функтора ", Нотр-Дам Журнал формальной логики 24 : 233–41.
- Уиллард Куайн , 1976, "Алгебраическая логика и функторы предикатов" в журналах " Пути парадокса и другие эссе" , доп. Ред. Harvard Univ. Пресс: 283–307.
- Уиллард Куайн, 1982. Методы логики , 4-е изд. Harvard Univ. Нажмите. Гл. 45.
- Соммерс, Фред, 1982. Логика естественного языка . Oxford Univ. Нажмите.
- Альфред Тарски и Гивант, Стивен, 1987. Формализация теории множеств без переменных . AMS .
- Жан Ван Хейенорт , 1967. От Фреге до Гёделя: Справочник по математической логике . Harvard Univ. Нажмите.
Внешние ссылки
- Введение в логику предикатов-функторов (загрузка в один клик, файл PS) Матса Даллёфа (факультет лингвистики, Уппсальский университет)