แบบจำลอง

เครื่องหมายเทิร์นสไตล์คู่แสดงความจริงในแบบจำลองหรือผลตามเชิงอรรถศาสตร์ แบบจำลองคือการตีความสัญลักษณ์ตรรกะในเชิงคณิตศาสตร์ ใน A ⊧ φ โครงสร้าง A ทำให้สูตร φ เป็นจริง ส่วนใน Γ ⊧ φ ข้อสมมติ Γ นำไปสู่ φ ในเชิงอรรถศาสตร์ กล่าวคือ ทุกแบบจำลองที่ทำให้ Γ เป็นจริงก็ทำให้ φ เป็นจริงด้วย หากไม่มีข้อสมมติทางซ้าย ⊧ φ หมายถึง φ เป็นจริงในทุกแบบจำลอง

ไซมอน โคเชนใช้เครื่องหมายเทิร์นสไตล์คู่อย่างแพร่หลายในทฤษฎีแบบจำลองเมื่อปี 1961 เขากล่าวว่าจำไม่ได้ว่าเป็นผู้คิดสัญลักษณ์นี้ขึ้นเองหรือยืมมา การใช้เครื่องหมายนี้แทนผลตามทางตรรกะน่าจะเริ่มขึ้นราวปี 1963 และมีการใช้แน่นอนภายในปี 1967

⊧ ต่างจาก ⊢ อย่างไร?

⊧ แสดงความจริงเชิงอรรถศาสตร์ ส่วน ⊢ บันทึกการอนุมานอย่างเป็นทางการ ใน Γ ⊢ φ ระบบพิสูจน์อนุมาน φ จากข้อสมมติ Γ ใน Γ ⊧ φ ทุกแบบจำลองที่ทำให้ Γ เป็นจริงก็ทำให้ φ เป็นจริงด้วย สัญลักษณ์ทั้งสองตอบคำถามคนละข้อ: กฎการพิสูจน์อนุมานอะไรได้ และอะไรเป็นจริงในทุกการตีความ

ถ้ามีคนส่ง ⊧ มาให้ หมายความว่าอะไร?

โดยมากหมายถึงบริบททางตรรกศาสตร์หรือคณิตศาสตร์ ดูสูตรที่อยู่ใกล้กันในข้อความ ตำแหน่งของสัญลักษณ์บอกว่า ⊧ เชื่อมแบบจำลองกับสูตร หรือเชื่อมข้อสมมติกับข้อสรุป