Çift gerektirme, mantıkta iki önermenin birbirini gerektirdiği durumu ifade eden bileşik bir önermedir. "Ancak ve ancak" bağlacı ile oluşturulur ve sembolü ⇔ veya ≡'dir.
Matematiksel olarak, p ⇔ q ifadesi, (p ⇒ q) ∧ (q ⇒ p) bileşik önermesine denktir. Yani, "p ise q ve q ise p" demenin kısa yoludur.
p ve q önermelerinin tüm olası doğruluk değerleri için p ⇔ q'nun doğruluk değerleri aşağıdaki gibidir:
p | q | p ⇔ q
D | D | D
D | Y | Y
Y | D | Y
Y | Y | D
Görüldüğü gibi, çift gerektirme önermesi yalnızca her iki önerme aynı doğruluk değerine sahip olduğunda Doğru (D) olur.
Bu kavram, bir çift gerektirme önermesinin her zaman doğru olması durumunu ifade eder. Yani, p ⇔ q önermesinin doğruluk tablosundaki tüm değerleri "D" ise, bu bir totolojidir.
Başka bir deyişle, (p ⇒ q) ∧ (q ⇒ p) bileşik önermesinin totoloji olması, p ve q'nun mantıksal olarak eşdeğer olduğu anlamına gelir. Bu, matematikte ve programlamada iki ifadenin aynı şeyi ifade ettiğini kanıtlamak için kullanılır.
"Bir sayı çifttir ancak ve ancak 2'ye tam bölünür."
Burada p ⇔ q önermesi her zaman doğrudur. Çünkü bir sayı çiftse mutlaka 2'ye tam bölünür ve 2'ye tam bölünüyorsa mutlaka çifttir. Bu nedenle, bu çift gerektirme bir totolojidir.
