Drehkreuz (Symbol) - Turnstile (symbol)

In der mathematischen Logik und Informatik hat das Symbol den Namen Drehkreuz erhalten, weil es von oben betrachtet einem typischen Drehkreuz ähnelt. Es wird auch als Tee bezeichnet und wird oft als "erträgt", "bestätigt", "befriedigt" oder "beinhaltet" gelesen. ${\displaystyle \vdash}$

In TeX wird das Drehkreuzsymbol über den Befehl \vdash erhalten . In Unicode heißt das Drehkreuzsymbol ( ⊢ ) rechts und befindet sich am Codepunkt U+22A2. (Der Codepunkt U+22A6 wird als Behauptungszeichen ( ⊦ ) bezeichnet.) Auf einer Schreibmaschine kann ein Drehkreuz aus einem senkrechten Strich (|) und einem Bindestrich (–) bestehen. In LaTeX gibt es ein Drehkreuzpaket, das dieses Zeichen in vielerlei Hinsicht ausgibt und in der Lage ist, Etiketten an den richtigen Stellen darunter oder darüber zu platzieren. ${\displaystyle \vdash}$

Interpretationen

Das Drehkreuz stellt eine binäre Relation dar . Es hat verschiedene Interpretationen in verschiedenen Kontexten:

• In Epistemologie , Per Martin-Löf - Analysen (1996) , um das Symbol so:“... [D] ie Kombination von Freges Urteilsstrich , Urteil stroke [|], und Inhaltsstrich , Content - stroke [-], kam die Behauptungszeichen genannt werden ." Freges Notation für eine Beurteilung eines Inhalts A${\displaystyle \vdash}$

${\displaystyle \vdash A}$

kann dann gelesen werden

Ich weiß, dass A wahr ist .

Ebenso eine bedingte Behauptung

${\displaystyle P\vdash Q}$

kann gelesen werden als:

Aus P weiß ich, dass Q

• In der Metalogik das Studium formaler Sprachen ; das Drehkreuz stellt eine syntaktische Konsequenz (oder "Ableitbarkeit") dar. Das heißt, es zeigt, dass gemäß den Transformationsregeln (dh der Syntax ) eines gegebenen formalen Systems in einem einzigen Schritt ein String von einem anderen abgeleitet werden kann . Als solcher ist der Ausdruck

${\displaystyle P\vdash Q}$

bedeutet, dass Q im System von P ableitbar ist.

In Übereinstimmung mit seiner Verwendung für die Ableitbarkeit bezeichnet ein "⊢" gefolgt von einem Ausdruck ohne etwas davor einen Satz , das heißt, der Ausdruck kann aus den Regeln unter Verwendung einer leeren Menge von Axiomen abgeleitet werden . Als solcher ist der Ausdruck

${\displaystyle \vdash Q}$

bedeutet, dass Q ein Satz im System ist.

• In der Beweistheorie wird das Drehkreuz verwendet, um "Beweisbarkeit" oder "Ableitbarkeit" zu bezeichnen. Wenn beispielsweise T eine formale Theorie und S ein bestimmter Satz in der Sprache der Theorie ist, dann

${\displaystyle T\vdash S}$

bedeutet , dass S ist beweisbar von T . Diese Verwendung wird im Artikel über Aussagenkalkül demonstriert . Die syntaktische Folge der Beweisbarkeit sollte semantische Konsequenz gegenübergestellt werden, durch die bezeichneten Doppeldrehkreuz Symbol . Man sagt, das sei eine semantische Konsequenz von , oder , wenn alle möglichen Bewertungen, in denen wahr ist, auch wahr sind. Für die Aussagenlogik kann gezeigt werden, dass semantische Konsequenz und Ableitbarkeit einander äquivalent sind. Das heißt, Aussagenlogik ist solide ( impliziert ) und vollständig ( impliziert )${\displaystyle \models}$${\displaystyle S}$${\displaystyle T}$${\displaystyle T\models S}$${\displaystyle T}$${\displaystyle S}$${\displaystyle \models}$${\displaystyle \vdash}$${\displaystyle \vdash}$${\displaystyle \models}$${\displaystyle \models}$${\displaystyle \vdash}$

• Beim typisierten Lambda-Kalkül wird das Drehkreuz verwendet, um Tippannahmen von der Tippbewertung zu trennen.
• In der Kategorie Theorie , eine umgekehrte Drehkreuz ( ), wie in , verwendet wird , um anzuzeigen , dass der Funktor F ist adjoint links auf die Funktor G . Seltener, ein Drehkreuz ( ), wie in ist, dass der Funktor verwendet , um anzuzeigen G ist Recht adjoint zum functor F .${\displaystyle \dashv}$${\displaystyle F\dashv G}$ ${\displaystyle \vdash}$${\displaystyle G\vdash F}$
• In APL wird das Symbol „richtiger Tack“ und stellt die ambivalente richtige Identitätsfunktion , wo beide genannt X ⊢ Y und ⊢ Y ist Y . Das umgekehrte Symbol „⊣“ wird „links Tack“ genannt und stellt die analoge linke Identität wo X ⊣ Y ist X und ⊣ Y ist Y .
• In Kombinatorik , bedeutet , daß λ ist eine Trennwand der Ganzzahl n .${\displaystyle \lambda\vdash n}$
• In Hewlett-Packard ‚s HP-41C / CV / CX und HP-42S Reihe von Rechenmaschinen , das Symbol (im Codepunkt 127 in dem FOCAL Zeichensatz wird)‚Append Zeichen‘genannt und wird verwendet, um anzuzeigen , daß die folgenden Zeichen werden an das Alpha-Register angehängt werden, anstatt den bestehenden Inhalt des Registers zu ersetzen. Das Symbol wird auch (bei Codepunkt 148) in einer modifizierten Variante des HP Roman-8- Zeichensatzes unterstützt, der von anderen HP-Rechnern verwendet wird.
• Bei den Taschenrechnern Casio fx-92 Collège 2D und fx-92+ Spéciale Collège steht das Symbol für den Modulo- Operator; Die Eingabe ergibt eine Antwort von , wobei Q der Quotient und R der Rest ist . Bei anderen CASIO-Rechnern (wie bei den belgischen Varianten – den fx-92B Spéciale Collège- und fx-92B Collège 2D-Rechnern – bei denen das Dezimaltrennzeichen als Punkt anstelle eines Kommas dargestellt wird) wird der Modulo-Operator stattdessen durch ÷R . dargestellt .${\displaystyle 5\vdash 2}$${\displaystyle Q=2;R=1}$

Ähnliche Grapheme

• ꜔ (U+A714) Modifikatorbuchstabe Mittlerer linker Stiel- Tonbalken
• ├ (U+251C) Box-Zeichnungen Licht vertikal und rechts
• ㅏ (U+314F) Koreanisch Ah
• Ͱ (U+0370) Griechischer Großbuchstabe Heta
• ͱ (U+0371) Griechischer Kleinbuchstabe Heta
• Ⱶ (U+2C75) Lateinischer Großbuchstabe halbes H
• ⱶ (U+2C76) Lateinischer Kleinbuchstabe halbes H
• ⎬ (U+23AB) Rechte geschweifte Klammer

Siehe auch

• Doppeldrehkreuz ${\displaystyle \models}$
• Sequenz
• Sequenzrechnung
• Liste der Logiksymbole
• Liste der mathematischen Symbole

Anmerkungen

Verweise

• Frege, Gottlob (1879). "Begriffsschrift: Eine der arithmetischen nachgebildeten Formelsprache des reinen Denkens". Halle. Cite Journal erfordert |journal=( Hilfe )
• Iverson, Kenneth (1987). „Ein Wörterbuch der APL“. Cite Journal erfordert |journal=( Hilfe )
• Martin-Löf, Per (1996). "Über die Bedeutungen der logischen Konstanten und die Begründungen der logischen Gesetze" (PDF) . Nordische Zeitschrift für philosophische Logik . 1 (1): 11–60. (Vortragsnotizen zu einem Kurzkurs an der Università degli Studi di Siena, April 1983.)
• Schmidt, David (1994). „Die Struktur der typisierten Programmiersprachen“. MIT-Presse . ISBN 0-262-19349-3. Cite Journal erfordert |journal=( Hilfe )
• Troelstra, AS ; Schwichtenberg, H. (2000). "Grundlegende Beweistheorie" (2. Aufl.). Cambridge University Press . ISBN 978-0-521-77911-1. Cite Journal erfordert |journal=( Hilfe )