Robbins cebiri - Robbins algebra

Gelen soyut cebir , bir Robbins cebir bir bir cebri tek ihtiva eden ikili işlem , genellikle ile gösterilen ve tek bir tekli işlemi genellikle ile gösterilmiştir . Bu işlemler aşağıdaki aksiyomları karşılar : ${\görüntüleme stili \lor }$${\görüntüleme stili \neg }$

a , b ve c tüm öğeleri için :

1. ilişkilendirme :${\displaystyle a\lor \sol(b\lor c\sağ)=\sol(a\lor b\sağ)\lor c}$
2. Değişebilirlik :${\displaystyle a\lor b=b\lor a}$
3. Robbins denklemi :${\displaystyle \neg \sol(\neg \sol(a\lor b\sağ)\lor \neg \sol(a\lor \neg b\sağ)\sağ)=a}$

Uzun yıllar boyunca, tüm Robbins cebirlerinin Boole cebiri olduğu varsayıldı, ancak kanıtlanmadı . Bu 1996'da kanıtlandı, bu nedenle "Robbins cebri" terimi artık "Boole cebri" ile eşanlamlı.

Tarih

1933'te Edward Huntington , Boole cebirleri için yukarıdaki (1) ve (2)'den oluşan yeni bir aksiyom seti önerdi, ayrıca:

• Huntington denklemi :${\displaystyle \neg (\neg a\lor b)\lor \neg (\neg a\lor \neg b)=a.}$

Bu aksiyomlardan Huntington, Boole cebrinin olağan aksiyomlarını türetmiştir.

Bundan çok kısa bir süre sonra Herbert Robbins , Huntington denkleminin Robbins denklemi olarak adlandırılan şeyle değiştirilebileceği ve sonucun yine Boole cebri olacağı şeklinde Robbins varsayımını ortaya koydu . Boolean birleşimini ve Boolean tamamlayıcısını yorumlar . Boolean buluşuyor ve 0 ve 1 sabitleri Robbins cebir ilkellerinden kolayca tanımlanabilir. Varsayımın doğrulanmasını bekleyen Robbins sistemine "Robbins cebiri" adı verildi. ${\görüntüleme stili \lor }$${\görüntüleme stili \neg }$

Robbins varsayımının doğrulanması, Huntington denkleminin veya bir Boole cebirinin başka bir aksiyomizasyonunun bir Robbins cebirinin teoremleri olarak kanıtlanmasını gerektiriyordu. Huntington, Robbins, Alfred Tarski ve diğerleri problem üzerinde çalıştılar, ancak bir kanıt veya karşı örnek bulamadılar.

William McCune kullanarak, 1996 yılında varsayım oldu otomatikleştirilmiş teoremi prover EQP . Tek bir tutarlı gösterimde ve McCune'u yakından takip ederek Robbins varsayımının tam bir kanıtı için bkz. Mann (2003). Dahn (1998), McCune'un makine kanıtını basitleştirdi.

Ayrıca bakınız

• cebirsel yapı
• Boole cebri için minimal aksiyomlar

Referanslar

• Dahn, BI (1998) Özeti " Robbins Cebirleri Booleandır: McCune'un Robbins Probleminin Bilgisayar Tarafından Oluşturulan Çözümünün Revizyonu ", Journal of Algebra 208(2): 526–32.
• Mann, Allen (2003) " Robbins Varsayımının Tam Bir Kanıtı. "
• William McCune , " Robbins Algebras Are Boolean ," Kanıtlara ve diğer belgelere bağlantılar ile.