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 =(S_{\mathrm{func}},S_{\mathrm{rel}},S_{\mathrm{const}},\mathrm{ar}),$ kde $S_{\mathrm{func}}$ a $S_{\mathrm{rel}}$ jsou disjunktní množiny neobsahující jiné základní logické symboly, nazývané po řadě

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

a funkce $\mathrm{ar}:S_{\mathrm{func}}\cup S_{\mathrm{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á Šablona:Kotvarelační signatura, signatura bez relačních symbolů se nazývá Šablona:Kotvaalgebraická signatura. Šablona:KotvaKonečná signatura je taková signatura, že množiny $S_{\mathrm{func}}$ a $S_{\mathrm{rel}}$ jsou konečné. Obecněji se kardinalita signatury $\sigma =(S_{\mathrm{func}},S_{\mathrm{rel}},S_{\mathrm{const}},\mathrm{ar})$ definuje jako $|\sigma |=\left|S_{\mathrm{func}}\right|+\left|S_{\mathrm{rel}}\right|+\left|S_{\mathrm{const}}\right|.$

Šablona:KotvaJazyk 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 Šablona:Kotvatyp nebo Šablona:Kotvatyp podobnosti často používá jako synonymum pro „signaturu“. V teorii modelů se signatura $\sigma$ často nazývá Šablona:Kotvaslovní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, ${\mathrm{\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,Šablona:Doplňte zdroj takže konstantní symboly se musí definovat zvlášť, ne jako nulární funkční symboly. Tvoří množinu $S_{\mathrm{const}}$ disjunktní s $S_{\mathrm{func}},$ na které aritní funkce $\mathrm{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_{\mathrm{func}}=\{+\}\cup \{f_a:a\in F\}$ a $S_{\mathrm{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 $𝐀$ s doménou $A$ je funkce $f^{𝐀}:A^n\to A,$ a interpretace $n$-árního relačního symbolu je relace $R^{𝐀}\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 Šablona:Kotvatypy 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,\dots ,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,\mathrm{type})$ tvořená

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

Odkazy

Reference

• Šablona:Citace monografie Free online edition.
• Šablona:Citace monografie

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 Šablona:Wayback, „An Introduction to the Algebraic Specification of Abstract Data Types. Šablona:Wayback“