Mô hình

Dấu turnstile kép biểu thị tính đúng trong mô hình hoặc hệ quả ngữ nghĩa. Mô hình là cách diễn giải các ký hiệu logic bằng toán học. Trong A ⊧ φ, cấu trúc A làm công thức φ đúng. Trong Γ ⊧ φ, các tiền đề Γ kéo theo φ về mặt ngữ nghĩa: mọi mô hình làm Γ đúng cũng làm φ đúng. Khi không có tiền đề bên trái, ⊧ φ có nghĩa là φ đúng trong mọi mô hình.

Simon Kochen dùng dấu turnstile kép rộng rãi trong lý thuyết mô hình vào năm 1961. Ông nói mình không nhớ đã tự tạo ra ký hiệu này hay mượn nó. Cách dùng để chỉ hệ quả logic có lẽ xuất hiện vào khoảng năm 1963 và chắc chắn đã có vào năm 1967.

⊧ khác ⊢ như thế nào?

⊧ biểu thị tính đúng về ngữ nghĩa; ⊢ ghi phép suy diễn hình thức. Trong Γ ⊢ φ, một hệ thống chứng minh suy ra φ từ các tiền đề Γ. Trong Γ ⊧ φ, mọi mô hình làm Γ đúng cũng làm φ đúng. Hai dấu này trả lời hai câu hỏi khác nhau: quy tắc chứng minh suy ra điều gì và điều gì đúng trong mọi cách diễn giải.

⊧ có nghĩa gì khi ai đó gửi cho bạn?

Thông thường, dấu này cho biết ngữ cảnh logic hoặc toán học. Hãy xem các công thức xung quanh trong tin nhắn: vị trí của nó cho biết ⊧ nối một mô hình với một công thức hay nối các tiền đề với một kết luận.