ไม่พิสูจน์

ไม่ใช่: เครื่องหมายนี้กล่าวถึงการอนุมาน ไม่ใช่ค่าความจริง

ใน P ⊬ Q นั้น P คือข้อสมมติและ Q คือข้อสรุป เครื่องหมายนี้ปฏิเสธผลตามทางไวยากรณ์ ส่วน P ⊭ Q หมายถึงมีแบบจำลอง (การตีความทางคณิตศาสตร์) ที่ทำให้ P เป็นจริงและ Q เป็นเท็จ

Begriffsschrift ของกอตล็อบ เฟรเกอ ซึ่งตีพิมพ์ในปี 1879 เป็นระบบเขียนตรรกะแบบสองมิติและมีเครื่องหมายต้นแบบทางประวัติศาสตร์ของเครื่องหมายอนุมาน ความหมายเปลี่ยนไปภายหลัง: ในระบบพิสูจน์จำนวนมาก ⊢ แสดงการอนุมานได้ ส่วน ⊬ ปฏิเสธความสัมพันธ์นั้น