Modele

Podwójny turnstile wyraża prawdziwość w modelu lub wynikanie semantyczne. Model to matematyczna interpretacja symboli logicznych. W A ⊧ φ struktura A spełnia formułę φ. W Γ ⊧ φ przesłanki Γ semantycznie pociągają za sobą φ: każdy model, w którym Γ jest prawdziwe, spełnia też φ. Bez przesłanek po lewej stronie ⊧ φ oznacza, że φ jest prawdziwe w każdym modelu.

Simon Kochen szeroko używał podwójnego turnstile w teorii modeli w 1961 roku. Mówił, że nie pamięta, czy sam wymyślił tę notację, czy ją zapożyczył. Zastosowanie do wynikania logicznego pojawiło się prawdopodobnie około 1963 roku i na pewno do 1967 roku.

Czym ⊧ różni się od ⊢?

⊧ wyraża prawdę semantyczną; ⊢ oznacza formalne wyprowadzenie. W Γ ⊢ φ system dowodowy wyprowadza φ z przesłanek Γ. W Γ ⊧ φ każdy model spełniający Γ spełnia także φ. Znaki odpowiadają na różne pytania: co wynika z reguł dowodzenia, a co jest prawdziwe we wszystkich interpretacjach.

Co oznacza ⊧, gdy ktoś ci je wysyła?

Zwykle wskazuje na kontekst logiczny lub matematyczny. W wiadomości sprawdź sąsiednie formuły: położenie znaku pokazuje, czy ⊧ łączy model z formułą, czy przesłanki z wnioskiem.