البديهيات الدنيا للجبر البولياني

في المنطق الرياضي ، تُعرَّف البديهيات الدنيا للجبر البولياني بأنها افتراضات تُكافئ بديهيات الجبر البولياني (أو حساب القضايا )، ويتم اختيارها لتكون أقصر ما يمكن. على سبيل المثال، بديهية تتضمن ست عمليات NAND وثلاثة متغيرات تُكافئ الجبر البولياني: ^{[ 1 ]}

${\displaystyle ((a\mid b)\mid c)\mid (a\mid ((a\mid c)\mid a))=c}$

حيث يمثل الشريط العمودي عملية NAND المنطقية (المعروفة أيضًا باسم ضربة شيفر ).

يُعدّ هذا أحد 25 بديهية مرشحة لهذه الخاصية، حددها ستيفن وولفرام ، وذلك من خلال تعداد متطابقات شيفر التي لا يتجاوز طولها 15 عنصرًا (باستثناء الصور المرآوية) والتي لا تحتوي على نماذج غير تبادلية بأربعة متغيرات أو أقل، وقد أثبت تكافؤها لأول مرة ويليام ماكيون وبراندن فيتلسون ولاري ووس . ^{[ 2 ] [ 3 ]} أطلق موقع MathWorld ، المرتبط بوولفرام، على هذه البديهية اسم "بديهية وولفرام". ^{[ 4 ]} كما وجد ماكيون وآخرون بديهية واحدة أطول للجبر البولياني تعتمد على الفصل والنفي. ^{[ 3 ]}

في عام 1933، حدد إدوارد فيرميلي هنتنغتون البديهية

${\displaystyle {\neg ({\neg x}\lor {y})}\lor {\neg ({\neg x}\lor {\neg y})}=x}$

باعتبارها مكافئة للجبر البولياني، عند دمجها مع خاصية التبديل في عملية "أو" ،${\displaystyle x\lor y=y\lor x}$، الترابطية،${\displaystyle (x\lor y)\lor z=x\lor (y\lor z)}$، وافتراض التكرار،${\displaystyle (x\lor x)=x}$[5] [6] وقد ثبت في التصحيح أن هذا الأخير زائد عن الحاجة. ^{[ 5 ] [ 6 ]} افترض هربرت روبنز أنه يمكن استبدال بديهية هنتنغتون بـ

${\displaystyle \neg (\neg (x\lor y)\lor \neg (x\lor {\neg y}))=x,}$

مما يتطلب استخدامًا أقل لعامل النفي المنطقي${\displaystyle \neg }$لم يتمكن روبنز ولا هنتنغتون من إثبات هذه الفرضية، وكذلك لم يتمكن ألفريد تارسكي ، الذي أبدى اهتمامًا كبيرًا بها لاحقًا. وقد تم إثبات الفرضية في النهاية عام 1996 بمساعدة برامج إثبات النظريات . ^{[ 7 ] [ 8 ] [ 9 ] أثبت هذا البرهان أن بديهية روبنز، إلى جانب خاصيتي} التجميع والتبديل، تُشكل أساسًا ثلاثيًا للجبر البولياني. وقد أثبت كارو آرثر ميريديث وجود أساس ثنائي عام 1967. [ ^{10 ]}

${\displaystyle \neg ({\neg x}\lor y)\lor x=x,}$

${\displaystyle \neg ({\neg x}\lor y)\lor (z\lor y)=y\lor (z\lor x).}$

وفي العام التالي، وجد ميريديث أساسًا من الدرجة الثانية من حيث ضربة شيفر: ^{[ 11 ]}

${\displaystyle (x\mid x)\mid (y\mid x)=x,}$

${\displaystyle x|(y\mid (x\mid z))=((z\mid y)\mid y)\mid x.}$

في عام 1973، قدّم بادمانابهان وكواكنبوش طريقةً من شأنها، من حيث المبدأ، أن تُنتج أساسًا من الدرجة 1 للجبر البولياني. ^{[ 12 ]} وقد أدّى تطبيق هذه الطريقة بشكلٍ مباشر إلى ظهور "بديهيات طويلة جدًا"، ^{[ 3 ]} مما أثار التساؤل حول كيفية إيجاد بديهيات أقصر. وقد أسفر هذا البحث عن الأساس من الدرجة 1 بدلالة ضربة شيفر المذكورة أعلاه، بالإضافة إلى الأساس من الدرجة 1.

${\displaystyle \neg (\neg (\neg (x\lor y)\lor z)\lor \neg (x\lor \neg (\neg z\lor \neg (z\lor u))))=z,}$

والتي تُكتب باستخدام "أو" و "ليس" . ^{[ 3 ]}