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

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

Определение [ править ]

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

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

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

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

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

Другие соглашения [ править ]

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

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

«Стандартной сигнатурой абелевых групп является

\sigma =(+,-,0),

где

-

является унарным оператором».

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

«Тип подобия для абелевых групп есть

\sigma =(2,1,0).

"

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

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

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

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

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

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

Многосортные подписи [ править ]

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

Типы символов [ править ]

Позволять $S$ быть набором (своего рода), не содержащим символы $\times$ или $\to .$

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

Подпись [ править ]

Подпись (многосортированная) представляет собой тройку $(S,P,\operatorname {type} )$ состоящий из

множество $S$ своего рода,
множество $P$ символов и
карта $\operatorname {type}$ который соответствует каждому символу в $P$ тип символа поверх $S.$

См. также [ править ]

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

Примечания [ править ]

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

Ссылки [ править ]

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

Внешние ссылки [ править ]

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

[FastN-Gram-BasedStringSearch-1] Мокадем, Риад; Литвин, Витольд; Риго, Филипп; Шварц, Томас (сентябрь 2007 г.). «Быстрый поиск строк на основе nGram по данным, закодированным с использованием алгебраических сигнатур» (PDF) . 33-я Международная конференция по очень большим базам данных (VLDB) . Проверено 27 февраля 2019 г.

[2] Джордж Гретцер (1967). «IV. Универсальная алгебра». В Джеймсе К. Эбботе (ред.). Тенденции в теории решеток . Принстон/Нью-Джерси: Ван Ностранд. стр. 173–210. Здесь: стр.173.

[3] Многосортированная логика , первая глава в конспектах лекций по процедурам принятия решений , написанная Калоджеро Дж. Зарбой .

[1]

[2]

[3]