Podwójny kołowrót

W logice symbol nazywa się podwójnym kołowrotem ⊨, ⊧ lub $displaystyle \ modele}$ \ . Często odczytuje się go jako „ pociąga za sobą ”, „ modele ”, „jest semantyczną konsekwencją ” lub „jest silniejszy niż”. Jest blisko spokrewniony z $konsekwencję$ kołowrotu , który ma pojedynczą kreskę pośrodku i oznacza składniową (w przeciwieństwie do semantycznej ).

Oznaczający

Podwójny kołowrót jest relacją binarną. Ma kilka różnych znaczeń w różnych kontekstach:

Aby pokazać semantyczną konsekwencję , ze zbiorem zdań po lewej stronie i jednym zdaniem po prawej, aby zaznaczyć, że jeśli każde zdanie po lewej stronie jest prawdziwe, zdanie po prawej stronie musi być prawdziwe, np. Γ ⊨ φ $\ Gamma \vDash \varphi }$ . To użycie jest ściśle związane z symbolem kołowrotu z pojedynczą kreską, który oznacza konsekwencję składniową .
Aby pokazać satysfakcję , z modelem (lub strukturą prawdy) po lewej stronie i zbiorem zdań po prawej, aby zaznaczyć, że struktura jest modelem (lub spełnia) zbiór zdań, np. ZA ⊨ $Displaystyle {\mathcal {A}}\modele \Gamma}$ ${\mathcal {A}}\models \Gamma$ . Zwykle odbywa się to indukcyjnie wraz z ograniczeniem zakresu przypisania zmiennej , funkcją odwzorowującą każdy symbol zmiennej na wartość, którą może pomieścić. ${\ displaystyle {\ mathcal {A}}}$ ${\mathcal {A}}$
- W tym kontekście semantyczną konsekwencję na poprzedniej liście można określić jako „Dla danego modelu $mathcal {A}} \ modele \ Gamma}$ $\$ \ następnie ${\ Displaystyle {\ mathcal {A}} \ vDash \ varphi}$ ".
Aby oznaczyć tautologię , ${\ Displaystyle \ vDash \ varphi}$ . co oznacza, że wyrażenie $.$ semantyczną konsekwencją zbioru pustego

Możesz również użyć tego symbolu w następujący sposób: ⊭ dla oznaczenia stwierdzenia „nie pociąga za sobą”.

Typografia

W TeX symbole kołowrotu i ${\ displaystyle$ $modele} są uzyskiwane$ odpowiednio z poleceń \ vDash i \ modele .

W Unicode jest zakodowany w U+22A8 ⊨ TRUE ( &DoubleRightTee;, &vDash; ) , a jego przeciwieństwem jest U+22AD ⊭ NOT TRUE ( &nvDash; ).

W LaTeX- ie istnieje pakiet kołowrotu , który wystawia ten znak na wiele sposobów, w tym podwójny kołowrotek, i jest w stanie umieścić etykiety pod nim lub nad nim w odpowiednich miejscach. Artykuł A Tool for Logicians jest samouczkiem dotyczącym korzystania z tego pakietu.

Zobacz też

^ Nederpelt Rob (2004). „Rozdział 7: Wzmocnienie i osłabienie”. Rozumowanie logiczne: kurs pierwszy (wydanie trzecie poprawione). Publikacje King's College. P. 62. ISBN 0-9543006-7-X .
^ Projekt otwartej logiki, logika pierwszego rzędu (str. 7). Dostęp 4 stycznia 2022 r.

[1] Nederpelt Rob (2004). „Rozdział 7: Wzmocnienie i osłabienie”. Rozumowanie logiczne: kurs pierwszy (wydanie trzecie poprawione). Publikacje King's College. P. 62. ISBN 0-9543006-7-X .

[2] Projekt otwartej logiki, logika pierwszego rzędu (str. 7). Dostęp 4 stycznia 2022 r.