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

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

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

Определение

Формально (односортная) сигнатура может быть определена как 4-кортеж , где и являются непересекающимися множествами, не содержащими никаких других базовых логических символов, называемых соответственно ${\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]Aконечная сигнатура — это сигнатура, такая чтои конечны.Вболее общем смысле,мощностьсигнатурыопределяется как ${\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 .}$

Типы символов над представляют собой определенные слова в алфавите : реляционные типы символов и функциональные типы символов для неотрицательных целых чисел и (для выражения обозначает пустое слово.) ${\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. Универсальная алгебра». В Джеймсе С. Эбботе (ред.). Тенденции в теории решеток . Принстон/Нью-Джерси: Van Nostrand. стр. 173–210.Здесь: стр.173.
3. «Многосортная логика», первая глава в «Конспектах лекций по процедурам принятия решений», написанных Калоджеро Дж. Зарбой.

Ссылки

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

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

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