Podpis (logika)

W logice , zwłaszcza w logice matematycznej , sygnatura wymienia i opisuje nielogiczne symbole języka formalnego . W algebrze uniwersalnej sygnatura zawiera listę operacji charakteryzujących strukturę algebraiczną . W teorii modeli sygnatury są używane do obu celów. Rzadko są one wyraźnie wyrażane w bardziej filozoficznych ujęciach logiki.

Definicja

$_ S _ {\ nazwa operatora {rel}}, S _ {\ nazwa operatora {stała}}, \ nazwa operatora {ar} \ po prawej),} gdzie S func {\ Displaystyle$ podpis pojedynczo można S $\ nazwa operatora {funkcja}}}$ i ${\ Displaystyle S_ {\operatorname {rel} }} to$ zbiory rozłączne nie zawierające żadnych innych podstawowych symboli logicznych, zwanych odpowiednio

• symbole funkcyjne (przykłady: ${\ Displaystyle +, \ razy, 0,1}$ ),
• symbol relacji s lub predykaty (przykłady: ${\ Displaystyle \, \ równoważnik, \, \ w}$ ),
• stałe symbole (przykłady: ${\ Displaystyle 0,1}$ ),

i funkcja ${\ Displaystyle \ nazwa operatora {ar}: S _ {\ nazwa operatora {func}} \ puchar S _ {\ nazwa operatora {rel}} \ do \ mathbb {N}}, która przypisuje$ a liczbę naturalną zwaną arity do każdego symbolu funkcji lub relacji. Symbol funkcji lub relacji nazywa się $wynosi$ , jeśli jego liczba ${\ displaystyle n.}$ Niektórzy autorzy definiują zerowy ( ${\ displaystyle 0}$ -ary) symbol funkcji jako symbol stały , w przeciwnym razie symbole stałe są definiowane oddzielnie.

Sygnatura bez symboli funkcji nazywana jest sygnaturą relacyjną , a sygnatura bez symboli relacji nazywana jest sygnaturą algebraiczną . Skończony podpis to podpis taki, że ${\ displaystyle S _ {\ operatorname {func}}}$ i ${\ displaystyle S _ {\ operatorname {rel}}}$ są skończone . Mówiąc bardziej ogólnie, liczność sygnatury ${\ Displaystyle \ sigma = \ lewo (S _ {\ nazwa operatora {funkcja}}, S _ {\ nazwa operatora {rel}}, S _ {\ nazwa operatora {stała}}, \ nazwa operatora {ar} \ po prawej)}$ jest zdefiniowany jako ${\ Displaystyle |\ sigma |= \ lewo | S _ {\ nazwa operatora {funkcja}} \ prawo | + \ lewo | S _ {\ nazwa operatora {rel}} \ prawo | + \ lewo | S_ {\ nazwa operatora {stała}} \ prawo|.}$

Język podpisu to zbiór wszystkich dobrze sformułowanych zdań zbudowanych z symboli w tym podpisie wraz z symbolami w systemie logicznym.

Inne konwencje

typ słowa lub typ podobieństwa jest często używany jako synonim „podpisu”. W teorii modeli sygnatura $dostarcza$ często nazywana słownictwem lub identyfikowana z $któremu$ (pierwszego rzędu), symbole nielogiczne . Jednak liczność języka zawsze będzie $;$ jeśli ${\ displaystyle \ sigma}$ jest wtedy skończony ${\ Displaystyle | L|}$ będzie ${\ Displaystyle \ aleph _ {0}.$ }

Ponieważ formalna definicja jest niewygodna w codziennym użyciu, definicja konkretnego podpisu jest często skracana w sposób nieformalny, jak w:

$_$ Standardowa grup to gdzie $_$ _

Czasami podpis algebraiczny jest traktowany tylko jako lista arities, jak w:

„Typ podobieństwa dla grup abelowych to ${\ Displaystyle \ sigma = (2,1,0).}$ "

Formalnie oznaczałoby to zdefiniowanie symboli funkcyjnych podpisu jako coś w rodzaju $($$displaystyle f_ {2}}$ jest binarne), co jest jednoargumentowe) i $fa$ (co jest nieważne), ale w rzeczywistości zwykłe nazwy są używane nawet w związku z tą konwencją.

W logice matematycznej bardzo często symbole nie mogą być zerowe, , więc symbole stałe muszą być traktowane oddzielnie, a nie jako symbole funkcji zerowych. Tworzą zbiór rozłączny z ${\ Displaystyle S _ {\ operatorname$$}}},$ którym funkcja arity ${\ displaystyle \ operatorname {ar} }$ nie jest zdefiniowany. Jednak służy to tylko skomplikowaniu sprawy, zwłaszcza w dowodach przez indukcję po strukturze formuły, gdzie należy wziąć pod uwagę dodatkowy przypadek. Każdy symbol relacji zerowej, który również nie jest dozwolony w takiej definicji, może być naśladowany przez symbol relacji jednoargumentowej wraz ze zdaniem wyrażającym, że jego wartość jest taka sama dla wszystkich elementów. To tłumaczenie nie działa tylko w przypadku pustych struktur (które często są wykluczane przez konwencję). Jeśli dozwolone są symbole zerowe, to każda formuła logiki zdań jest również formułą logiki pierwszego rzędu .

Przykład nieskończonej sygnatury używa ${\ Displaystyle S _ {\ operatorname {func}} = \ {+ \} \ cup \ lewo \ {f_ {a}: a \ in F \ right \}}$ i ${\ Displaystyle S _ {\ nazwa operatora {rel}} = \ {= \}}$ sformalizować wyrażenia i równania dotyczące przestrzeni wektorowej nad nieskończonym polem skalarnym ${\ Displaystyle F}$ gdzie każdy $jednoargumentową$ operację mnożenia przez skalar ${\ displaystyle a.}$ W ten sposób podpis i logika mogą być sortowane pojedynczo, przy czym jedynym sortowaniem są wektory.

Wykorzystanie sygnatur w logice i algebrze

W kontekście logiki pierwszego rzędu symbole w sygnaturze są również znane jako symbole nielogiczne , ponieważ wraz z symbolami logicznymi tworzą podstawowy alfabet, na podstawie którego indukcyjnie definiuje się dwa języki formalne : zbiór terminów nad podpis i zestaw (dobrze sformułowanych) formuł nad podpisem.

W strukturze interpretacja wiąże symbole funkcji i relacji z obiektami $}$$ich$ nazwy: Interpretacja -arnego funkcji w strukturze $A}}$${\ Displaystyle \ mathbf {$ z domeną ${\ Displaystyle A}$ jest funkcją ${\ Displaystyle f ^ {\ mathbf {A}}: A ^ {n} \ do A,}$ a interpretacją $relacji$ jest relacja ${\ Displaystyle R ^ {\ mathbf {A}} \ subseteq A ^ {n}.}$ Tutaj ${\ Displaystyle A ^ {n} = A \ razy A \ razy \ cdots \ razy A}$ oznacza -krotnie $displaystyle$ kartezjański domeny $A}$$sobą$ , $-ary$ więc $jest$ w rzeczywistości funkcją $-ary$ i

Wiele posortowanych podpisów

Dla logiki z wieloma sortowaniami i dla struktur z wieloma sortowaniami sygnatury muszą kodować informacje o sortowaniu. Najprostszym sposobem na to są typy symboli , które pełnią rolę uogólnionych liczb.

Typy symboli

Niech będzie zbiorem ( ${\ Displaystyle \ do.}$$)$$niezawierającym$ lub

Typy symboli nad to pewne słowa nad alfabetem $:$$\ Displaystyle S \ puchar \ {\ razy, \ do \}}$ : relacyjne typy symboli ${\ Displaystyle s_ {1} \ razy \ cdots \ razy s_ {n}}$ i funkcjonalne typy symboli ${\ Displaystyle s_ {1} \ razy \ cdots \ razy s_ {n} \ do s ^ {\ pierwsza},}$ dla nieujemnych liczb całkowitych ${\ Displaystyle n}$ i ${\ Displaystyle s_ {1}, s_ {2}, \ ldots, s_ {n}, s ^ ​​{\ pierwsza} \ w S.}$ (Dla ${\ Displaystyle n = 0,}$ wyrażenie ${\ Displaystyle s_ {1} \ razy \ cdots \ razy s_ {n}}$ oznacza puste słowo).

Podpis

Podpis (wielosortowany) to potrójny składający się z ${\ Displaystyle (S, P, \ operatorname {typ})}$

• zestaw rodzajów, ${\ displaystyle S}$
• zestaw symboli i. ${\ displaystyle P}$
• $,$ mapy $który$ kojarzy się z każdym symbolem w symbolu nad ${\ Displaystyle S.}$

Zobacz też

• Algebra terminów - Swobodnie generowana struktura algebraiczna nad danym podpisem

Notatki

•   Burris, Stanley N.; Sankappanavar, HP (1981). Kurs algebry uniwersalnej . Springera . ISBN 3-540-90578-2 . Bezpłatne wydanie internetowe .
•   Hodges, Wilfrid (1997). Krótsza teoria modelu . Wydawnictwo Uniwersytetu Cambridge . ISBN 0-521-58713-1 .

Linki zewnętrzne

• Stanford Encyclopedia of Philosophy : „ Teoria modeli ” - autorstwa Wilfreda Hodgesa .
• PlanetMath: Wpis „ Podpis ” opisuje koncepcję przypadku, gdy nie wprowadzono sortowania.
• Baillie, Jean , „ Wprowadzenie do algebraicznej specyfikacji abstrakcyjnych typów danych ” .