Modellen

De dubbele turnstile drukt waarheid in een model of semantische gevolgtrekking uit. Een model is een wiskundige interpretatie van logische symbolen. In A ⊧ φ maakt structuur A formule φ waar. In Γ ⊧ φ impliceren de premissen Γ semantisch φ: elk model dat Γ waar maakt, maakt ook φ waar. Zonder premissen links ervan betekent ⊧ φ dat φ in elk model geldt.

Simon Kochen gebruikte de dubbele turnstile in 1961 veelvuldig in de modeltheorie. Hij zei dat hij zich niet kon herinneren of hij de notatie zelf had bedacht of had overgenomen. Het gebruik voor logisch gevolg verscheen waarschijnlijk rond 1963 en was zeker bekend in 1967.

Wat is het verschil tussen ⊧ en ⊢?

⊧ drukt semantische waarheid uit; ⊢ staat voor formele afleiding. In Γ ⊢ φ leidt een bewijssysteem φ af uit de premissen Γ. In Γ ⊧ φ maakt elk model dat Γ waar maakt ook φ waar. De tekens beantwoorden verschillende vragen: wat volgt uit bewijsregels en wat geldt in alle interpretaties?

Wat betekent ⊧ als iemand het je stuurt?

Het wijst meestal op een logische of wiskundige context. Kijk in een bericht naar de formules eromheen: de plaatsing laat zien of ⊧ een model aan een formule koppelt of premissen aan een conclusie.