Zobrazení zdroje stránky Signatura (logika)

'''Signatura''' v [[Logika|logice]], především v [[Matematická logika|matematické logice]], udává a popisuje [[Mimologický symbol|mimologické symboly]] [[Formální jazyk|formálního jazyka]]. V [[Univerzální algebra|univerzální algebře]] signatura udává operace, které charakterizují [[Algebraická struktura|algebraickou strukturu]]. V [[Teorie modelů|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 <math>\sigma = \left(S_{\operatorname{func}}, S_{\operatorname{rel}}, S_{\operatorname{const}}, \operatorname{ar}\right),</math> kde <math>S_{\operatorname{func}}</math> a <math>S_{\operatorname{rel}}</math> jsou disjunktní [[Množina|množiny]] neobsahující jiné základní logické symboly, nazývané po řadě
* ''[[funkční symbol]]y'' (příklady: <math>+, \times</math>),
* ''{{Kotva|relační symbol}}relační symboly'' neboli ''[[Predikát (logika)|predikáty]]'' (příklady: <math>\,\leq, \, \in</math>),
* ''[[Konstantní symbol (logika)|konstantní symboly]]'' (příklady: <math>0, 1</math>),
a funkce <math>\operatorname{ar} : S_{\operatorname{func}} \cup S_{\operatorname{rel}} \to \N,</math> která každému funkčnímu nebo relačnímu symbolu přiřazuje [[přirozené číslo]] nazývané ''[[Operace (matematika)#Arita operace|arita operace]]''. Funkční nebo relační symbol se nazývá <math>n</math>-ární, pokud jeho arita je <math>n.</math> Někteří autoři definuje nulární (<math>0</math>-ární) funkční symboly jako ''konstantní symboly'', jiní definují konstantní symboly odděleně.

Signatura bez funkčních symbolů se nazývá '''{{Kotva|relační signatura}}relační signatura''', signatura bez relačních symbolů se nazývá '''{{Kotva|algebraická signatura}}algebraická signatura'''.<ref name="FastN-Gram-BasedStringSearch">{{Citace elektronické monografie
 | příjmení = Mokadem
 | jméno = Riad
 | autor2 = Litwin, Witold
 | autor3 = Rigaux, Philippe
 | autor4 = Schwarz, Thomas
 | titul = Fast nGram-Based String Search Over Data Encoded Using Algebraic Signatures
 | url = http://www.cse.scu.edu/~tschwarz/Papers/vldb07_final.pdf
 | vydavatel = 33rd International Conference on Very Large Data Bases (VLDB)
 | datum přístupu = 2019-02-27
 | format = PDF
 | datum = September 2007
 | ref = harv
 | datum archivace = 2017-08-09
 | url archivu = https://web.archive.org/web/20170809092717/http://www.cse.scu.edu/~tschwarz//Papers/vldb07_final.pdf
 | nedostupné = ano
 }}</ref>
''{{Kotva|Konečná signatura}}Konečná signatura'' je taková signatura, že množiny <math>S_{\operatorname{func}}</math> a <math>S_{\operatorname{rel}}</math> jsou [[Konečná množina|konečné]]. Obecněji se ''kardinalita'' signatury <math>\sigma = \left(S_{\operatorname{func}}, S_{\operatorname{rel}}, S_{\operatorname{const}}, \operatorname{ar}\right)</math> definuje jako <math>|\sigma| = \left|S_{\operatorname{func}}\right| + \left|S_{\operatorname{rel}}\right| + \left|S_{\operatorname{const}}\right|.</math>

''{{Kotva|jazyk signatury}}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 '''{{Kotva|typ}}typ''' nebo '''{{Kotva|typ podobnosti}}typ podobnosti''' často používá jako [[synonymum]] pro „signaturu“. V teorii modelů se signatura <math>\sigma</math> často nazývá '''{{Kotva|slovník}}slovník''' nebo se identifikuje s [[Predikátová logika prvního řádu|jazykem (prvního řádu)]] <math>L,</math> pro který poskytuje [[Mimologický symbol|mimologické symboly]]. [[Mohutnost]] jazyka <math>L</math> však bude vždy nekonečná; pokud <math>\sigma</math> je konečná, pak <math>|L|</math> bude mít [[Kardinalita|kardinalitu]] nejmenší nekonečné množiny, [[Funkce alef|<math>\aleph_0</math>]] (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 [[Abelova grupa|abelovských grup]] je <math>\sigma = (+, -, 0),</math> kde <math>-</math> je unární operátor.“

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

: „Typ podobnosti abelovských grup je <math>\sigma = (2, 1, 0).</math>“

Formálně by to znamenalo definovat funkční symboly v signatuře jako něco jako <math>f_0</math> (binární), <math>f_1</math> (unární) a <math>f_2</math> (nulární), ale ve skutečnosti se používají obvyklá jména dokonce ve spojení s touto konvencí.

V [[Matematická logika|matematické logice]] jsou velmi často zakázané nulární symboly,{{Doplňte zdroj|datum=leden 2017}} takže konstantní symboly se musí definovat zvlášť, ne jako nulární funkční symboly. Tvoří množinu <math>S_{\operatorname{const}}</math> disjunktní s <math>S_{\operatorname{func}},</math> na které aritní funkce <math>\operatorname{ar}</math> 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á logika|výrokové logiky]] je také formulí [[Predikátová logika prvního řádu|predikátové logiky prvního řádu]].

Příklad použití nekonečné signatury je <math>S_{\operatorname{func}} = \{+\} \cup \left\{f_a : a \in F\right\}</math> a <math>S_{\operatorname{rel}} = \{=\}</math>, která formalizuje výrazy a rovnice pro [[vektorový prostor]] nad nekonečným skalárním tělesem <math>F,</math> kde každá <math>f_a</math> označuje unární operaci násobení skalárem <math>a.</math> Tímto způsobem lze signaturu a logiku omezit na jednosortovou, v níž jedinou sortou jsou vektory.<ref>{{Citace monografie
 | editor = James C. Abbot
 | titul = Trends in Lattice Theory
 | místo = Princeton/NJ
 | vydavatel = Van Nostrand
 | rok = 1967
 | autor = George Grätzer
 | odkaz na autora = George Grätzer
 | contribution = IV. Universal Algebra
 | strany = 173–210
 | ref = harv
}} Here: p.173.</ref>

== Použití signatur v logice a algebře ==
V [[Predikátová logika prvního řádu|predikátové logice prvního řádu]] se symboly signatury také nazývají [[Mimologický symbol|mimologické symboly]], protože spolu s logickými symboly tvoří podkladovou abecedu, nad kterou jsou induktivně definovány dva [[formální jazyk]]y: Množina ''členů'' nad signaturou a množina (dobře utvořených) ''formulí'' nad signaturou.

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

== Signatury s mnoha sortami ==
Pro logiku s mnoha sortami a pro [[Struktura (logika)|struktury s mnoha sortami]] musí signatury kódovat informace o sortách. Nejjednodušším způsobem, jak to udělat je použít '''{{Kotva|typy symbolů}}typy symbolů''', které hrají roli zobecněných arit.<ref>[https://web.archive.org/web/20070929131504/http://react.cs.uni-sb.de/%7Ezarba/snow/ch01.pdf Many-Sorted Logic], první kapitola [https://web.archive.org/web/20081006212815/http://react.cs.uni-sb.de/~zarba/notes.html Lecture notes on Decision Procedures], kterou napsal [http://theory.stanford.edu/~zarba/ Calogero G. Zarba] {{Wayback|url=http://theory.stanford.edu/~zarba/ |date=20110927095649 }}.</ref>

=== Typy symbolů ===
Nechť <math>S</math> je množina (sort) neobsahující symboly <math>\times</math> ani <math>\to.</math>

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

=== Signatura ===
Signatura (s mnoha sortami) je trojice <math>(S, P, \operatorname{type})</math> tvořená
* množina <math>S</math> sort,
* množina <math>P</math> symbolů, a
* zobrazení <math>\operatorname{type},</math> které přiřazuje každému symbolu z <math>P</math> typ symbolu nad <math>S.</math>

== Odkazy ==

=== Poznámky ===
<references />

=== Reference ===
{{Překlad|en|Signature (logic)|1173025907}}
* {{Citace monografie
 | příjmení = Burris
 | jméno = Stanley N.
 | autor2 = Sankappanavar, H.P.
 | titul = A Course in Universal Algebra
 | rok = 1981
 | vydavatel = [[Springer Věda+Obchodní Media|Springer]]
 | isbn = 3-540-90578-2
 | ref = harv
}} [http://www.thoralf.uwaterloo.ca/htdocs/ualg.html Free online edition].
* {{Citace monografie
 | příjmení = Hodges
 | jméno = Wilfrid
 | titul = A Shorter Model Theory
 | url = https://archive.org/details/shortermodeltheo0000hodg
 | rok = 1997
 | vydavatel = [[Cambridge University Press]]
 | isbn = 0-521-58713-1
 | ref = harv
}}

=== Související články ===
* [[Algebra termů]]

=== Externí odkazy ===
* [http://plato.stanford.edu/entries/model-theory/ Stanford Encyclopedia of Philosophy]: „[http://plato.stanford.edu/entries/model-theory/ Model theory]“— autor [[Wilfred Hodges]].
* [http://planetmath.org/ PlanetMath:] Položka „[http://planetmath.org/signature Signature]“ popisuje pojem pro případ, kdy nejsou zavedeny žádné sorty.
* [http://homepages.feis.herts.ac.uk/~comqejb/algspec/pr.html Baillie, Jean] {{Wayback|url=http://homepages.feis.herts.ac.uk/~comqejb/algspec/pr.html |date=20040903183501 }}, „[http://homepages.feis.herts.ac.uk/~comqejb/algspec/pr.html An Introduction to the Algebraic Specification of Abstract Data Types.] {{Wayback|url=http://homepages.feis.herts.ac.uk/~comqejb/algspec/pr.html |date=20040903183501 }}“

{{Matematická logika}}
{{Autoritní data}}

[[Kategorie:Matematická logika]]
[[Kategorie:Teorie modelů]]
[[Kategorie:Univerzální algebra]]