Modèles

Le double turnstile exprime la vérité dans un modèle ou la conséquence sémantique. Un modèle est une interprétation mathématique des symboles logiques. Dans A ⊧ φ, la structure A rend la formule φ vraie. Dans Γ ⊧ φ, les prémisses Γ impliquent sémantiquement φ : tout modèle qui rend Γ vraie rend aussi φ vraie. Sans prémisses à gauche, ⊧ φ signifie que φ est vraie dans tous les modèles.

Simon Kochen a largement employé le double turnstile en théorie des modèles en 1961. Il disait ne plus se souvenir s’il avait inventé cette notation ou l’avait empruntée. Son emploi pour la conséquence logique apparaît probablement vers 1963 et est attesté en 1967.

Quelle différence entre ⊧ et ⊢ ?

⊧ exprime une vérité sémantique ; ⊢ note une déduction formelle. Dans Γ ⊢ φ, un système de preuve déduit φ à partir des prémisses Γ. Dans Γ ⊧ φ, tout modèle qui rend Γ vraie rend aussi φ vraie. Les signes répondent à deux questions différentes : que permettent les règles de preuve, et qu’est-ce qui est vrai dans toutes les interprétations ?

Que signifie ⊧ quand quelqu’un vous l’envoie ?

Cela indique généralement un contexte de logique ou de mathématiques. Dans un message, regardez les formules qui l’entourent : sa position montre si ⊧ relie un modèle à une formule ou des prémisses à une conclusion.