Signatura (logika)

Signatura v logice, především v matematické logice, udává a popisuje mimologické symboly formálního jazyka. V univerzální algebře signatura udává operace, které charakterizují algebraickou strukturu. V teorii modelů se signatury používají pro oba účely. Ve filozofičtějších pojednáních o logice se signatury zřídka uvádějí explicitně.

Definice

Formálně lze signaturu (s jednou sortou) definovat jako čtveřici $\sigma =\left(S_{\operatorname {func} },S_{\operatorname {rel} },S_{\operatorname {const} },\operatorname {ar} \right),$ kde $S_{\operatorname {func} }$ a $S_{\operatorname {rel} }$ jsou disjunktní množiny neobsahující jiné základní logické symboly, nazývané po řadě

• funkční symboly (příklady: $+,\times$),
• relační symboly neboli predikáty (příklady: $\,\leq ,\,\in$),
• konstantní symboly (příklady: $0,1$),

a funkce $\operatorname {ar} :S_{\operatorname {func} }\cup S_{\operatorname {rel} }\to \mathbb {N} ,$ která každému funkčnímu nebo relačnímu symbolu přiřazuje přirozené číslo nazývané arita operace. Funkční nebo relační symbol se nazývá $n$-ární, pokud jeho arita je $n.$ Někteří autoři definuje nulární ($0$-ární) funkční symboly jako konstantní symboly, jiní definují konstantní symboly odděleně.

Signatura bez funkčních symbolů se nazývá relační signatura, signatura bez relačních symbolů se nazývá algebraická signatura. Konečná signatura je taková signatura, že množiny $S_{\operatorname {func} }$ a $S_{\operatorname {rel} }$ jsou konečné. Obecněji se kardinalita signatury $\sigma =\left(S_{\operatorname {func} },S_{\operatorname {rel} },S_{\operatorname {const} },\operatorname {ar} \right)$ definuje jako $|\sigma |=\left|S_{\operatorname {func} }\right|+\left|S_{\operatorname {rel} }\right|+\left|S_{\operatorname {const} }\right|.$

Jazyk signatury je množina všech dobře utvořených vět vytvořených ze symbolů v této signatuře a symbolů logického systému.

Jiné konvence

V univerzální algebře se slovo typ nebo typ podobnosti často používá jako synonymum pro „signaturu“. V teorii modelů se signatura $\sigma$ často nazývá slovník nebo se identifikuje s jazykem (prvního řádu) $L,$ pro který poskytuje mimologické symboly. Mohutnost jazyka $L$ však bude vždy nekonečná; pokud $\sigma$ je konečná, pak $|L|$ bude mít kardinalitu nejmenší nekonečné množiny, $\aleph _{0}$ (alef-nula).

Protože formální definice je těžkopádná pro každodenní použití, definice určité signatury se často neformálně zkracuje, např.

„Standardní signatura abelovských grup je $\sigma =(+,-,0),$ kde $-$ je unární operátor.“

Někdy je algebraická signatura považována pouze za seznam arit:

„Typ podobnosti abelovských grup je $\sigma =(2,1,0).$“

Formálně by to znamenalo definovat funkční symboly v signatuře jako něco jako $f_{0}$ (binární), $f_{1}$ (unární) a $f_{2}$ (nulární), ale ve skutečnosti se používají obvyklá jména dokonce ve spojení s touto konvencí.

V matematické logice jsou velmi často zakázané nulární symboly,^[zdroj?] takže konstantní symboly se musí definovat zvlášť, ne jako nulární funkční symboly. Tvoří množinu $S_{\operatorname {const} }$ disjunktní s $S_{\operatorname {func} },$ na které aritní funkce $\operatorname {ar}$ není definována. Tím se však věci pouze zbytečně komplikují, zvláště v důkazech indukcí podle složitosti formule, kde se zbytečně musí probírat další případ. Libovolný nulární relační symbol, který takové definice nepovolují, lze napodobit unárním relačním symbolem a slovním vyjádřením, že jeho hodnota je pro všechny prvky stejná. To selhává pro prázdné struktury, které se však obvykle vynechávají. Výhodou je, že pokud nulární symboly nejsou povoleny, pak každá formule výrokové logiky je také formulí predikátové logiky prvního řádu.

Příklad použití nekonečné signatury je $S_{\operatorname {func} }=\{+\}\cup \left\{f_{a}:a\in F\right\}$ a $S_{\operatorname {rel} }=\{=\}$, která formalizuje výrazy a rovnice pro vektorový prostor nad nekonečným skalárním tělesem $F,$ kde každá $f_{a}$ označuje unární operaci násobení skalárem $a.$ Tímto způsobem lze signaturu a logiku omezit na jednosortovou, v níž jedinou sortou jsou vektory.

Použití signatur v logice a algebře

V predikátové logice prvního řádu se symboly signatury také nazývají mimologické symboly, protože spolu s logickými symboly tvoří podkladovou abecedu, nad kterou jsou induktivně definovány dva formální jazyky: Množina členů nad signaturou a množina (dobře utvořených) formulí nad signaturou.

V nějaké struktuře svazuje interpretace funkční a relační symboly s matematickými objekty, což ospravedlňuje jejich jména: Interpretace $n$-árního funkčního symbolu $f$ ve struktuře $\mathbf {A}$ s doménou $A$ je funkce $f^{\mathbf {A} }:A^{n}\to A,$ a interpretace $n$-árního relačního symbolu je relace $R^{\mathbf {A} }\subseteq A^{n}.$ Zde $A^{n}=A\times A\times \cdots \times A$ označuje $n$-násobný Kartézský součin definičního oboru $A$, takže $f$ je tak vlastně $n$-ární funkce a $R$ $n$-ární relace.

Signatury s mnoha sortami

Pro logiku s mnoha sortami a pro struktury s mnoha sortami musí signatury kódovat informace o sortách. Nejjednodušším způsobem, jak to udělat je použít typy symbolů, které hrají roli zobecněných arit.

Typy symbolů

Nechť $S$ je množina (sort) neobsahující symboly $\times$ ani $\to .$

Typy symbolů nad $S$ jsou určitá slova nad abecedou $S\cup \{\times ,\to \}$: symboly relačního typy $s_{1}\times \cdots \times s_{n},$ a symboly funkčního typu $s_{1}\times \cdots \times s_{n}\to s^{\prime },$ pro nezáporná celá čísla $n$ a $s_{1},s_{2},\ldots ,s_{n},s^{\prime }\in S.$ (Pro $n=0$ je výraz $s_{1}\times \cdots \times s_{n}$ prázdné slovo.)

Signatura

Signatura (s mnoha sortami) je trojice $(S,P,\operatorname {type} )$ tvořená

• množina $S$ sort,
• množina $P$ symbolů, a
• zobrazení $\operatorname {type} ,$ které přiřazuje každému symbolu z $P$ typ symbolu nad $S.$

Odkazy

Reference

V tomto článku byl použit překlad textu z článku Signature (logic) na anglické Wikipedii.

• BURRIS, Stanley N.; Sankappanavar, H.P., 1981. A Course in Universal Algebra. [s.l.]: Springer. ISBN 3-540-90578-2.  Free online edition.
• HODGES, Wilfrid, 1997. A Shorter Model Theory. [s.l.]: Cambridge University Press. ISBN 0-521-58713-1. 

Související články

• Algebra termů

Externí odkazy

• Stanford Encyclopedia of Philosophy: „Model theory“— autor Wilfred Hodges.
• PlanetMath: Položka „Signature“ popisuje pojem pro případ, kdy nejsou zavedeny žádné sorty.
• Baillie, Jean, „An Introduction to the Algebraic Specification of Abstract Data Types.“