Das Symbol ⊬ (Beweist nicht) verständlich erklärt
Das mathematische Symbol ⊬ (Unicode: U+22AC) steht für "beweist nicht" oder "lässt sich nicht ableiten". In der formalen Logik und Mathematik wird es verwendet, um auszudrücken, dass eine bestimmte Aussage nicht aus einer gegebenen Menge von Prämissen gefolgert werden kann. Es ist die verneinte Form des sogenannten "Turnstile"-Symbols (⊢), das für mathematische und logische Beweisbarkeit steht.
Das Zeichen ⊬ gehört zum Unicode-Block "Mathematische Operatoren" und trägt die offizielle Bezeichnung "DOES NOT PROVE". Es hat seinen Ursprung in der Prädikatenlogik und der Beweistheorie. Dort benötigen Mathematiker und Informatiker präzise Symbole, um logische Abhängigkeiten darzustellen. Der diagonale Strich durch das Zeichen ist das universelle mathematische Symbol für Negation – ganz ähnlich wie beim bekannten Ungleich-Zeichen (≠).
In der akademischen Welt, insbesondere in der theoretischen Informatik und Mathematik, triffst du ⊬ regelmäßig an. Wenn du zum Beispiel eine Formel wie "A ⊬ B" siehst, bedeutet das: Selbst wenn Aussage A wahr ist, reicht das syntaktisch nicht aus, um Aussage B zu beweisen. Außerhalb von Universitätsskripten und Fachbüchern taucht das Symbol im Alltag kaum auf. Auf Social Media oder in Chats wird es höchstens von Mathe-Nerds genutzt, um ironisch darauf hinzuweisen, dass ein Argument völlig unlogisch ist ("Deine Argumentation ⊬ Sinn"). In der Programmierung wird es selten direkt im Code abgetippt, spielt aber theoretisch bei der Entwicklung von Theorembeweisern eine große Rolle.
Wie bekommst du das "Beweist nicht"-Symbol nun auf deinen Bildschirm? Da es auf Standardtastaturen fehlt, helfen dir ein paar einfache Tricks. Unter Windows kannst du den Unicode direkt eingeben: Tippe 22AC und drücke danach Alt + C (funktioniert direkt in Microsoft Word). Auf dem Mac nutzt du die Zeichenübersicht (Ctrl + Cmd + Leertaste) und suchst einfach nach dem Begriff "does not prove". Auf Webseiten schreibst du im HTML-Code ⊬. Wenn du wissenschaftliche Dokumente in LaTeX verfasst, erzeugt der Befehl \nvdash das gewünschte Zeichen auf dem Papier.
Verwandte Zeichen helfen dabei, ⊬ besser einzuordnen. Das direkte Gegenstück ist das reguläre Turnstile-Symbol ⊢ (U+22A2, "Beweist"). Sehr ähnlich sieht auch das doppelte Turnstile ⊨ (U+22A8, "impliziert semantisch") aus, dessen verneinte Form ⊭ (U+22AD) lautet. Während ⊬ für die rein formale, syntaktische Ableitbarkeit von Formeln steht, geht es bei ⊭ um die inhaltliche, semantische Wahrheit. Ein kleiner, aber feiner Unterschied für echte Logik-Fans!