Boole cebri için minimal aksiyomlar - Minimal axioms for Boolean algebra

Olarak matematiksel mantık , Boole cebri için en az aksiyomların aksiyomlarının eşdeğer varsayımlar, Boole cebri (veya önerme hesabı mümkün olduğu kadar kısa olacak şekilde seçilir). Örneğin, kişi değişmezlik kabul etmeyi seçerse, altı NAND işlemi ve üç değişkeni olan bir aksiyom Boole cebrine eşdeğerdir:

burada dikey çubuk NAND mantıksal işlemini temsil eder ( Sheffer vuruşu olarak da bilinir ).

Bu özellik için Stephen Wolfram tarafından, dört veya daha az değişkenli değişmeli olmayan modelleri olmayan 15 öğeye eşit veya daha az uzunluktaki Sheffer kimliklerini (ayna görüntüleri hariç) numaralandırarak tanımlanan bu özellik için 25 aday aksiyomdan biridir ve ilk olarak eşdeğer olduğu kanıtlanmıştır. William McCune , Branden Fitelson ve Larry Wos . Wolfram ile ilişkili bir site olan MathWorld , aksiyomu "Wolfram aksiyomu" olarak adlandırdı. McCun ve ark. ayrıca Boole cebri için ayrılma ve olumsuzlamaya dayalı daha uzun bir tek aksiyom buldu.

1933'te Edward Vermilye Huntington aksiyomu tanımladı.

OR işleminin değişmeliliği ile birleştirildiğinde, Boole cebrine eşdeğer olarak , ve ilişkisellik varsayımı, . Herbert Robbins , Huntington'ın aksiyomunun değiştirilebileceğini tahmin etti.

bu, mantıksal olumsuzlama operatörünün daha az kullanımını gerektirir . Ne Robbins ne de Huntington bu varsayımı kanıtlayamadı; ne de daha sonra büyük ilgi gördü Alfred Tarski . Bu varsayım, 1996 yılında teorem kanıtlayan bir yazılım yardımıyla sonunda kanıtlandı . Bu kanıt, Robbins aksiyomunun, çağrışımsallık ve değişebilirlik ile birlikte, Boole cebri için bir 3-temel oluşturduğunu ortaya koydu. 2 bazın varlığı 1967'de Carew Arthur Meredith tarafından kurulmuştur :

Ertesi yıl, Meredith Sheffer inme açısından 2 temel buldu:

1973'te Padmanabhan ve Quackenbush, prensipte Boole cebri için 1 temel verecek bir yöntem gösterdiler. Bu yöntemi basit bir şekilde uygulamak, "çok uzun aksiyomlar" verdi ve böylece daha kısa aksiyomların nasıl bulunabileceği sorusunu gündeme getirdi. Bu arama, yukarıda verilen Sheffer vuruşu açısından 1 tabanını ve ayrıca 1 tabanını verdi.

OR ve NOT cinsinden yazılır.

Referanslar