Feferman–Vaught theorem
ماڈل تھیوری میں فیفرمین ووٹ تھیوریم سولومن فیفرمین اور رابرٹ لاسن ووٹ کا ایک تھیوریم ہے جو بتاتا ہے کہ کس طرح، الگورتھمک انداز میں، فرسٹ آرڈر ڈھانچے کے پروڈکٹ کے فرسٹ آرڈر تھیوری کو عناصر کے فرسٹ آرڈر تھیوری میں کم کیا جائے۔ ڈھانچہ نظریہ کو ماڈل تھیوری میں معیاری نتائج میں سے ایک سمجھا جاتا ہے۔ یہ نظریہ نظریات کی براہ راست مصنوعات پر آندریج موسٹوسکی کے پچھلے نتائج کی توسیع کرتا ہے۔ یہ عالمگیر الجبرا میں اس خاصیت کو عام کرتا ہے جو مساوات (شناخت) الجبرائی ڈھانچوں کے براہ راست پروڈکٹ پر لے جاتی ہے (جو برخوف کے نظریہ کی ایک سمت کا نتیجہ ہے)۔ ڈھانچوں کا براہ راست پروڈکٹ فرسٹ آرڈر منطق سگنیچر ایل پر غور کریں۔ پروڈکٹ ڈھانچوں کی تعریف کچھ انڈیکس سیٹ I کے لیے ایل-ڈھانچوں کے ایک خاندان کو لیتی ہے اور پروڈکٹ ڈھانچے کی وضاحت کرتی ہے، جو کہ ایک ایل-ڈھانچہ بھی ہے، جس میں تمام افعال اور تعلقات کو پوائنٹ وائز بیان کیا گیا ہے۔ یہ تعریف یونیورسل الجبرا میں براہ راست پروڈکٹ کو ریلیشنل فرسٹ آرڈر ڈھانچوں میں عام کرتی ہے، جس میں نہ صرف فنکشن کی علامتیں ہوتی ہیں بلکہ رشتہ کی علامتیں بھی ہوتی ہیں۔ اگر L میں دلائل کے ساتھ تعلق کی علامت ہے اور کارٹیشین پروڈکٹ کے عناصر ہیں، تو ہم کی تشریح کی وضاحت کرتے ہیں۔ جب ایک فعال تعلق ہے، تو یہ تعریف عالمگیر الجبرا میں براہ راست پروڈکٹ کی تعریف تک کم ہو جاتی ہے۔ براہ راست مصنوعات کے لیے تھیوریم کا بیان فری متغیرات کے ساتھ سگنیچر ایل میں فرسٹ آرڈر منطق فارمولے کے لیے، اور متغیرات کی تشریح کے لیے، ہم انڈیکس کے سیٹ کی وضاحت کرتے ہیں جس کے لیے فری متغیرات کے ساتھ فرسٹ آرڈر فارمولا دیا گیا ہے، اس کے مساوی گیم نارمل فارم کا حساب لگانے کے لیے ایک الگورتھم ہے، جو باہمی متضاد فارمولوں کا ایک محدود اختلاط ہے۔ فیفرمین ووٹ تھیوریم ایک الگورتھم دیتا ہے جو فرسٹ آرڈر فارمولا لیتا ہے اور ایک فارمولہ تشکیل دیتا ہے جو پروڈکٹ میں موجود حالت کو اس حالت تک کم کر دیتا ہے جو انڈیکس کے سیٹوں کی تشریح میں ہوتی ہے: فارمولہ اس طرح فری سیٹ متغیرات کے ساتھ ایک فارمولہ ہے، مثال کے طور پر، سیٹوں کے بولین الجبرا کے فرسٹ آرڈر تھیوری میں۔ پروف آئیڈیا فارمولا ابتدائی فارمولے کی ساخت کے مطابق بنایا جا سکتا ہے۔ کوانٹیفایر کب آزاد ہوتا ہے تو، اس کے اوپر براہ راست پروڈکٹ کی تعریف کے مطابق مندرجہ ذیل ہے۔ نتیجتا، ہم سیٹوں کے بولین الجبرا کی زبان میں مساوات کو لے سکتے ہیں (مساوی طور پر، سیٹوں کا میدان)۔ شرط کو مقداری فارمولوں تک بڑھانے کو مقداری خاتمے کی ایک شکل کے طور پر دیکھا جا سکتا ہے، جہاں پروڈکٹ کے عناصر پر مقداری کو ذیلی سیٹوں پر مقداری تک کم کر دیا جاتا ہے۔ عمومی مصنوعات براہ راست مصنوعات کے ڈھانچے کی ذیلی ساخت پر غور کرنا اکثر دلچسپی کا باعث ہوتا ہے۔ اگر سب اسٹرکچر سے تعلق رکھنے والے پروڈکٹ عناصر کی وضاحت کرنے والی پابندی کو انڈیکس عناصر کے سیٹوں پر ایک شرط کے طور پر ظاہر کیا جا سکتا ہے، تو نتائج کو عام کیا جا سکتا ہے۔ ایک مثال مصنوعات کے عناصر کی ذیلی ساخت ہے جو بالکل مستقل لیکن محدود طور پر بہت سے اشاریہ جات ہیں۔ فرض کریں کہ زبان L ایک مستقل علامت پر مشتمل ہے اور صرف ان پروڈکٹ عناصر پر مشتمل ذیلی ساخت پر غور کریں جس کے لیے سیٹ محدود ہے۔ تھیوریم پھر اس طرح کی ذیلی ساخت میں سچائی کی قدر کو سیٹوں کے بولین الجبرا میں ایک فارمولے میں کم کر دیتا ہے، جہاں کچھ سیٹس محدود ہونے تک محدود ہوتے ہیں۔ عمومی مصنوعات کی وضاحت کرنے کا ایک طریقہ ان ذیلی ڈھانچوں پر غور کرنا ہے جہاں سیٹ انڈیکس کے سیٹوں کے کچھ بولین الجبرا سے تعلق رکھتے ہیں (پاور سیٹ سیٹ الجبرا کا ایک ذیلی سیٹ)، اور جہاں پروڈکٹ سب اسٹرکچر گلوئنگ کو قبول کرتا ہے۔ یہاں گلوئنگ کو تسلیم کرنا مندرجہ ذیل اختتامی حالت سے مراد ہے: اگر دو پروڈکٹ عناصر ہیں اور یہ بولین الجبرا کا عنصر ہے، تو عنصر کی تعریف "گلوئنگ" سے ہوتی ہے اور اس کے مطابق: نتائج فیفرمین ووٹ تھیوریم ریاضی کے بنیادی تھیوریم کے ذریعے، ضرب کے ساتھ قدرتی اعداد کی ساخت کو پریسبرگر ریاضی کے ڈھانچے کے عمومی پروڈکٹ (طاقت) کے طور پر دیکھ کر اسکولیم ریاضی کی فیصلہ سازی کا اشارہ کرتا ہے۔ ماڈل تھیوری حوالہ جات