Подпись (логика)

Описание нелогических символов

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

Определение

Формально подпись (одинарной сортировки) можно определить как кортеж из четырех чисел , где и представляют собой непересекающиеся множества , не содержащие каких-либо других основных логических символов, называемых соответственно ${\displaystyle \sigma =\left(S_{\operatorname {func} },S_{\operatorname {rel} },S_{\operatorname {const} },\operatorname {ar} \right),}$ ${\displaystyle S_{\operatorname {func} }}$ ${\displaystyle S_{\operatorname {rel} }}$

• функциональные символы (примеры:), ${\displaystyle +,\times }$
• символы отношения или предикаты (примеры:), ${\displaystyle \,\leq ,\,\in }$
• постоянные символы (примеры:), ${\displaystyle 0,1}$

и функция , которая присваивает натуральное число, называемое арностью , каждой функции или символу отношения. Символ функции или отношения называется -арным, если его арность равна. Некоторые авторы определяют нулевой ( -арный) символ функции как постоянный символ , в противном случае константные символы определяются отдельно. ${\displaystyle \operatorname {ar} :S_{\operatorname {func} }\cup S_{\operatorname {rel} }\to \mathbb {N} }$ ${\displaystyle n}$ ${\displaystyle n.}$ ${\displaystyle 0}$

Подпись, не содержащая функциональных символов, называетсяреляционная подпись , а подпись без символов отношения называетсяалгебраическая подпись . ^[1]Аконечная подпись — это подпись, такаячтоиконечны. В более общем смыслемощностьподписиопределяется как ${\displaystyle S_{\operatorname {func} }}$ ${\displaystyle S_{\operatorname {rel} }}$ ${\displaystyle \sigma =\left(S_{\operatorname {func} },S_{\operatorname {rel} },S_{\operatorname {const} },\operatorname {ar} \right)}$ ${\displaystyle |\sigma |=\left|S_{\operatorname {func} }\right|+\left|S_{\operatorname {rel} }\right|+\left|S_{\operatorname {const} }\right|.}$

The Язык подписи — это совокупность всех правильно построенных предложений, построенных из символов этой подписи вместе с символами логической системы.

Другие конвенции

В универсальной алгебре слововведите илиТип сходства часто используется как синоним слова «подпись». В теории моделей сигнатуручасто называют ${\displaystyle \sigma }$словарь или идентифицируется сязыком (первого порядка), которому он предоставляетнелогические символы. Однакомощностьязыкавсегда будет бесконечной; есликонечно, тобудет. ${\displaystyle L}$ ${\displaystyle L}$ ${\displaystyle \sigma }$ ${\displaystyle |L|}$ ${\displaystyle \aleph _{0}}$

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

«Стандартная подпись абелевых групп — это унарный оператор где ». ${\displaystyle \sigma =(+,-,0),}$ ${\displaystyle -}$

Иногда алгебраическая сигнатура рассматривается как просто список арностей, например:

«Тип подобия для абелевых групп есть » ${\displaystyle \sigma =(2,1,0).}$

Формально это определяло бы функциональные символы подписи как что-то вроде (что является двоичным), (что является унарным) и (что является нулевым), но на самом деле обычные имена используются даже в связи с этим соглашением. ${\displaystyle f_{0}}$ ${\displaystyle f_{1}}$ ${\displaystyle f_{2}}$

В математической логике очень часто символы не могут быть нулевыми, ^{[ нужна цитация ]} , поэтому константные символы следует рассматривать отдельно, а не как нулевые функциональные символы. Они образуют непересекающееся множество , на котором функция арности не определена. Однако это только усложняет дело, особенно при доказательствах индукцией по структуре формулы, где необходимо учитывать дополнительный случай. Любой символ нулевого отношения, который также не допускается согласно такому определению, может быть эмулирован символом унарного отношения вместе с предложением, выражающим, что его значение одинаково для всех элементов. Этот перевод не работает только для пустых структур (которые часто исключаются по соглашению). Если разрешены нулевые символы, то каждая формула логики высказываний является также формулой логики первого порядка . ${\displaystyle S_{\operatorname {const} }}$ ${\displaystyle S_{\operatorname {func} },}$ ${\displaystyle \operatorname {ar} }$

В примере бесконечной сигнатуры используются и для формализации выражений и уравнений о векторном пространстве над бесконечным скалярным полем , где каждое обозначает унарную операцию скалярного умножения на. Таким образом, сигнатура и логика могут сохраняться односортными, при этом векторы единственный сорт. ^[2] ${\displaystyle S_{\operatorname {func} }=\{+\}\cup \left\{f_{a}:a\in F\right\}}$ ${\displaystyle S_{\operatorname {rel} }=\{=\}}$ ${\displaystyle F,}$ ${\displaystyle f_{a}}$ ${\displaystyle a.}$

Использование подписей в логике и алгебре

В контексте логики первого порядка символы в сигнатуре также известны как нелогические символы , поскольку вместе с логическими символами они образуют базовый алфавит, в котором индуктивно определяются два формальных языка : подпись и набор (правильно сформированных) формул над подписью.

В структуре интерпретация связывает символы функции и отношения с математическими объектами, которые оправдывают их имена: Интерпретация символа -арной функции в структуре с областью определения является функцией , а интерпретация символа -арного отношения является отношением. Здесь обозначается -кратное декартово произведение области на саму себя, и поэтому на самом деле является -арной функцией и -арным отношением. ${\displaystyle n}$ ${\displaystyle f}$ ${\displaystyle \mathbf {A} }$ ${\displaystyle A}$ ${\displaystyle f^{\mathbf {A} }:A^{n}\to A,}$ ${\displaystyle n}$ ${\displaystyle R^{\mathbf {A} }\subseteq A^{n}.}$ ${\displaystyle A^{n}=A\times A\times \cdots \times A}$ ${\displaystyle n}$ ${\displaystyle A}$ ${\displaystyle f}$ ${\displaystyle n}$ ${\displaystyle R}$ ${\displaystyle n}$

Многосортные подписи

Для многосортной логики и многосортированных структур сигнатуры должны кодировать информацию о сортировках. Самый простой способ сделать это — черезтипы символов , играющие роль обобщенных арностей. ^[3]

Типы символов

Пусть это набор (своего рода), не содержащий символов или ${\displaystyle S}$ ${\displaystyle \times }$ ${\displaystyle \to .}$

Типы символов over — это определенные слова в алфавите : типы реляционных символов и типы функциональных символов для неотрицательных целых чисел и (ибо выражение обозначает пустое слово.) ${\displaystyle S}$ ${\displaystyle S\cup \{\times ,\to \}}$ ${\displaystyle s_{1}\times \cdots \times s_{n},}$ ${\displaystyle s_{1}\times \cdots \times s_{n}\to s^{\prime },}$ ${\displaystyle n}$ ${\displaystyle s_{1},s_{2},\ldots ,s_{n},s^{\prime }\in S.}$ ${\displaystyle n=0,}$ ${\displaystyle s_{1}\times \cdots \times s_{n}}$

Подпись

(Многосортированная) подпись — это тройка, состоящая из ${\displaystyle (S,P,\operatorname {type} )}$

• своего рода набор , ${\displaystyle S}$
• набор символов и ${\displaystyle P}$
• карта , которая связана с каждым символом в типе символа ${\displaystyle \operatorname {type} }$ ${\displaystyle P}$ ${\displaystyle S.}$

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

• Термическая алгебра  - свободно сгенерированная алгебраическая структура по заданной сигнатуре.

Примечания

1. Мокадем, Риад; Литвин, Витольд; Риго, Филипп; Шварц, Томас (сентябрь 2007 г.). «Быстрый поиск строк на основе nGram по данным, закодированным с использованием алгебраических сигнатур» (PDF) . 33-я Международная конференция по очень большим базам данных (VLDB) . Проверено 27 февраля 2019 г.
2. Джордж Гретцер (1967). «IV. Универсальная алгебра». В Джеймсе К. Эбботе (ред.). Тенденции в теории решеток . Принстон/Нью-Джерси: Ван Ностранд. стр. 173–210.Здесь: стр.173.
3. Многосортированная логика, первая глава в конспектах лекций по процедурам принятия решений, написанная Калоджеро Дж. Зарбой.

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

• Беррис, Стэнли Н.; Санкаппанавар, HP (1981). Курс универсальной алгебры . Спрингер . ISBN 3-540-90578-2.Бесплатное онлайн-издание.
• Ходжес, Уилфрид (1997). Теория более коротких моделей . Издательство Кембриджского университета . ISBN 0-521-58713-1.

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

• Стэнфордская энциклопедия философии: «Теория моделей» — Уилфред Ходжес .
• PlanetMath: Запись «Сигнатура» описывает концепцию для случая, когда сортировки не вводятся.
• Бэйли, Джин, «Введение в алгебраическую спецификацию абстрактных типов данных».