Unterschrift (Logik) - Signature (logic)

In der Logik , insbesondere der mathematischen Logik , listet und beschreibt eine Signatur die nicht logischen Symbole einer formalen Sprache . In der universellen Algebra listet eine Signatur die Operationen auf, die eine algebraische Struktur charakterisieren . In der Modelltheorie werden Signaturen für beide Zwecke verwendet. Sie werden selten in philosophischeren Behandlungen der Logik explizit gemacht.

Definition

Formal kann eine (einfach sortierte) Signatur als ein Dreifach σ = ( S func , S rel , ar) definiert werden, wobei S func und S rel disjunkte Mengen sind , die keine anderen logischen Grundsymbole enthalten, die jeweils aufgerufen werden

  • Funktionssymbole (Beispiele: +, ×, 0, 1) und
  • Beziehungssymbole oder Prädikate (Beispiele: ≤, ∈),

und eine Funktion ar: S func  S rel →, die jeder Funktion oder jedem Beziehungssymbol eine natürliche Zahl namens arity zuweist . Ein Funktions- oder Beziehungssymbol heißt n -ary, wenn seine Arität n ist . Ein Nullfunktionssymbol ( 0 -ary) wird als konstantes Symbol bezeichnet .  

Eine Signatur ohne Funktionssymbole wird als relationale Signatur bezeichnet , und eine Signatur ohne Beziehungssymbole wird als algebraische Signatur bezeichnet . Eine finite Signatur ist eine Signatur , so dass S func und S rel sind finite . Allgemeiner ist die Kardinalität einer Signatur σ = ( S func , S rel , ar) definiert als | σ | = | S func | + | S rel |.

Die Sprache einer Signatur ist die Menge aller wohlgeformten Sätze, die aus den Symbolen in dieser Signatur zusammen mit den Symbolen im logischen System aufgebaut sind.

Andere Konventionen

In Universal-Algebra des Worttyp oder Ähnlichkeit Typ wird oft als Synonym für „Signatur“ verwendet. In der Modelltheorie wird eine Signatur σ oft als Vokabular bezeichnet oder mit der Sprache L (erster Ordnung) identifiziert, für die sie die nicht logischen Symbole bereitstellt . Die Kardinalität der Sprache L wird jedoch immer unendlich sein; wenn σ endlich ist, dann | L | wird ℵ 0 sein .

Da die formale Definition für den täglichen Gebrauch unpraktisch ist, wird die Definition einer bestimmten Signatur häufig informell abgekürzt, wie in:

"Die Standardsignatur für abelsche Gruppen ist σ = (+, -, 0), wobei - ein unärer Operator ist."

Manchmal wird eine algebraische Signatur nur als eine Liste von Aritäten angesehen, wie in:

"Der Ähnlichkeitstyp für abelsche Gruppen ist σ = (2,1,0)."

Formal würde dies die Funktionssymbole der Signatur als etwas wie f 0  (nullär), f 1  (unär) und f 2  (binär) definieren, aber in Wirklichkeit werden die üblichen Namen auch in Verbindung mit dieser Konvention verwendet.

In der mathematischen Logik dürfen Symbole sehr oft nicht null sein, so dass konstante Symbole separat und nicht als Nullfunktionssymbole behandelt werden müssen. Sie bilden einen Satz S const disjunkt S func , auf dem die Funktion arity ar ist nicht definiert. Dies dient jedoch nur dazu, die Angelegenheit zu komplizieren, insbesondere bei Beweisen durch Induktion über die Struktur einer Formel, bei denen ein zusätzlicher Fall berücksichtigt werden muss. Jedes Nullrelationssymbol, das unter einer solchen Definition ebenfalls nicht zulässig ist, kann durch ein Unärrelationssymbol zusammen mit einem Satz emuliert werden, der ausdrückt, dass sein Wert für alle Elemente gleich ist. Diese Übersetzung schlägt nur für leere Strukturen fehl (die häufig durch Konventionen ausgeschlossen werden). Wenn Nullsymbole zulässig sind, ist jede Formel der Aussagenlogik auch eine Formel der Logik erster Ordnung .

Ein Beispiel für eine unendliche Signatur verwendet S func = {+} ∪ {f a : a ∈ F } und S rel = {=}, um Ausdrücke und Gleichungen über einen Vektorraum über einem unendlichen Skalarfeld F zu formalisieren , wobei jedes f a bezeichnet die unäre Operation der Skalarmultiplikation mit a . Auf diese Weise können die Signatur und die Logik einfach sortiert gehalten werden, wobei Vektoren die einzige Sortierung sind.

Verwendung von Signaturen in Logik und Algebra

Im Kontext der Logik erster Ordnung werden die Symbole in einer Signatur auch als nicht logische Symbole bezeichnet , da sie zusammen mit den logischen Symbolen das zugrunde liegende Alphabet bilden, über das zwei formale Sprachen induktiv definiert werden: Die Menge der Begriffe über der Signatur und die Menge der (wohlgeformten) Formeln über der Signatur.

In einer Struktur bindet eine Interpretation die Funktions- und Beziehungssymbole an mathematische Objekte, die ihre Namen rechtfertigen: Die Interpretation eines n- fachen Funktionssymbols f in einer Struktur A mit Domäne A ist eine Funktion f A :  A n  →  A und die Die Interpretation eines n -ary-Beziehungssymbols ist eine Beziehung R A  ⊆  A n . Hier bezeichnet A n = A × A × ... × A das n- fache kartesische Produkt der Domäne A mit sich selbst, und so ist f tatsächlich eine n -ary-Funktion und R eine n -ary-Beziehung.

Vielsortierte Unterschriften

Für vielfach sortierte Logik und für vielfach sortierte Strukturen müssen Signaturen Informationen über die Sortierungen codieren. Der einfachste Weg , dies zu tun , ist über Symboltypen , die die Rolle der verallgemeinerten arities spielen.

Symboltypen

Sei S eine Menge (von Art), die die Symbole × oder → nicht enthält.

Die Symboltypen über S sind bestimmte Wörter über dem Alphabet : die relationalen Symboltypen s 1 ×… × s n und die funktionalen Symboltypen s 1 ×… × s n → s ' für nicht negative ganze Zahlen n und . (Für n = 0 bezeichnet der Ausdruck s 1 ×… × s n das leere Wort.)

Unterschrift

Eine (vielfach sortierte) Signatur ist ein Tripel ( S , P , Typ) bestehend aus

  • eine Art S ,
  • eine Menge P von Symbolen und
  • ein Kartentyp, der jedem Symbol in P einen Symboltyp über S zuordnet .

Anmerkungen

  1. ^ Mokadem, Riad; Litwin, Witold; Rigaux, Philippe; Schwarz, Thomas (September 2007). "Schnelle nGram-basierte Zeichenfolgensuche über Daten, die mithilfe algebraischer Signaturen codiert wurden" (PDF) . 33. Internationale Konferenz über sehr große Datenbanken (VLDB) . Abgerufen am 27. Februar 2019 . CS1-Wartung: entmutigter Parameter ( Link )
  2. ^ George Grätzer (1967). "IV. Universelle Algebra". In James C. Abbot (Hrsg.). Trends in der Gittertheorie . Princeton / NJ: Van Nostrand. S. 173–210. CS1-Wartung: entmutigter Parameter ( Link ) Hier: S.173.
  3. ^ Vielseitige Logik , das erste Kapitel in den Vorlesungsunterlagen zu Entscheidungsverfahren , geschrieben von Calogero G. Zarba .

Verweise

Externe Links