S2S (mathematics)
ریاضی میں، S2S دو جانشینوں کے ساتھ موناڈک سیکنڈ آرڈر تھیوری ہے۔ یہ سب سے زیادہ اظہار خیال کرنے والے قدرتی فیصلہ کن نظریات میں سے ایک ہے، جس میں بہت سے فیصلہ کن نظریات ہیں جن کی S2S میں تشریح کی جا سکتی ہے۔ اس کی فیصلہ سازی رابن نے 1969 میں ثابت کی تھی۔ بنیادی خصوصیات S2S کے فرسٹ آرڈر آبجیکٹ محدود بائنری سٹرنگ ہیں۔ سیکنڈ آرڈر آبجیکٹ محدود بائنری سٹرنگ کے صوابدیدی سیٹ (یا یونری پیشن گوئی) ہوتے ہیں۔ S2S میں سٹرنگز پر فنکشن s → s0 اور s → s1 ہوتے ہیں، اور پیش گوئی کرتے ہیں s ω S (مساوی طور پر، S (s)) جس کا مطلب ہے سٹرنگ s سیٹ S سے تعلق رکھتا ہے۔ کچھ خصوصیات اور کنونشن: پہلے سے طے شدہ طور پر، چھوٹے حروف پہلے آرڈر کے آبجیکٹ کا حوالہ دیتے ہیں، اور بڑے حروف دوسرے آرڈر کے آبجیکٹ کا حوالہ دیتے ہیں۔ سیٹوں کی شمولیت S2S کو دوسرا آرڈر بناتی ہے، جس میں "موناڈک" k> 1 کے لیے k-ary پیش گوئی متغیرات کی عدم موجودگی کی نشاندہی کرتا ہے۔ سٹرنگز s اور t کے امتزاج کو سینٹ سے ظاہر کیا جاتا ہے، اور یہ عام طور پر S2S میں دستیاب نہیں ہے، یہاں تک کہ s → 0s بھی نہیں۔ تاروں کے درمیان سابقہ تعلق قابل تعریف ہے۔ مساوات ابتدائی ہے، یا اس کی تعریف اس طرح کی جا سکتی ہے کہ s = t′S (S (s) ′S (t) اور S = T′S (S (s) ′T (s)۔ تاروں کی جگہ، کوئی بھی (مثال کے طور پر) قدرتی اعداد استعمال کر سکتا ہے جن میں n → 2n + 1 اور n → 2n + 2 ہیں لیکن کوئی دوسری کارروائیاں نہیں ہیں۔ تمام بائنری تاروں کے سیٹ کو کلین اسٹار کا استعمال کرتے ہوئے {0,1} * سے ظاہر کیا جاتا ہے۔ {0,1} * کے صوابدیدی ذیلی مجموعوں کو بعض اوقات درختوں کے ساتھ شناخت کیا جاتا ہے، خاص طور پر {0,1}-لیبل والے درخت {0,1} * کے طور پر ؛ {0,1} * ایک مکمل لامحدود بائنری درخت بناتا ہے۔ فارمولہ کی پیچیدگی کے لیے، تاروں پر سابقہ تعلق کو عام طور پر فرسٹ آرڈر سمجھا جاتا ہے۔ اس کے بغیر، تمام فارمولے δ12 فارمولوں کے مساوی نہیں ہوں گے۔ S2S میں ظاہر ہونے والی خصوصیات کے لیے (تمام بائنری سٹرنگز کے سیٹ کو ٹری کے طور پر دیکھنا)، ہر نوڈ کے لیے، صرف O (1) بٹس کو بائیں ذیلی ٹری اور دائیں ذیلی ٹری اور باقی کے درمیان منتقل کیا جا سکتا ہے (مواصلاتی پیچیدگی دیکھیں)۔ ایک فکسڈ k کے لیے، سٹرنگ سے k تک ایک فنکشن (یعنی۔ k) سے نیچے قدرتی اعداد کو ایک سیٹ کے ذریعے انکوڈ کیا جا سکتا ہے۔ مزید برآں، ایس، ٹی این ڈی ایس01 ٹی جہاں ٹی ٹی کے ہر کردار کو دوگنا کرتا ہے وہ انجیکشن ہے، اور ایس این ڈی {ایس01 ٹی: ٹی bul {0,1} *} ایس 2 ایس قابل تعریف ہے۔ اس کے برعکس، مواصلاتی پیچیدگی کی دلیل سے، S1S (نیچے) میں سیٹوں کا ایک جوڑا کسی ایک سیٹ کے ذریعے انکوڈیبل نہیں ہوتا ہے۔ S2S کی کمزوریاں: کمزور S2S (WS2S) کے لیے تمام سیٹوں کو محدود ہونا ضروری ہے (نوٹ کریں کہ کنیگ کے لیما کا استعمال کرتے ہوئے S2S میں حد کا اظہار کیا جا سکتا ہے)۔ S1S کو اس ضرورت سے حاصل کیا جا سکتا ہے کہ '1' تاروں میں ظاہر نہ ہو، اور WS1S کو بھی حد کی ضرورت ہوتی ہے۔ یہاں تک کہ ڈبلیو ایس 1 ایس بھی پریس برگر ریاضی کی تشریح 2 کی طاقتوں کے لیے پیش گوئی کے ساتھ کر سکتا ہے، کیونکہ سیٹوں کو قابل تعریف اضافے کے ساتھ غیر محدود بائنری نمبروں کی نمائندگی کے لیے استعمال کیا جا سکتا ہے۔ فیصلہ سازی کی پیچیدگی S2S فیصلہ کن ہے، اور S2S، S1S، WS2S، WS1S میں سے ہر ایک میں غیر معمولی فیصلہ سازی کی پیچیدگی ہوتی ہے جو کہ متغیرات کے لکیری طور پر بڑھتے ہوئے اسٹیک سے مطابقت رکھتی ہے۔ نچلے باؤنڈ کے لیے، σ11 WS1S جملوں پر غور کرنا کافی ہے۔ سنگل سیکنڈ آرڈر کوانٹیفایر کو ریاضی (یا دیگر) کمپیوٹیشن کی تجویز کرنے کے لیے استعمال کیا جا سکتا ہے، جس کی تصدیق فرسٹ آرڈر کوانٹیفایرز کا استعمال کرتے ہوئے کی جا سکتی ہے اگر ہم جانچ کر سکیں کہ کون سے نمبر برابر ہیں۔ اس کے لیے، اگر ہم 1. m نمبروں کو مناسب طریقے سے انکوڈ کرتے ہیں، تو ہم بائنری نمائندگی i1i2.im کے ساتھ ایک نمبر کو i1 1 i2 2 کے طور پر انکوڈ کر سکتے ہیں۔ گارڈز کی جانچ کو ضم کرنے اور متغیر ناموں کو دوبارہ استعمال کرنے سے، بٹس کی تعداد متغیرات کی تعداد میں لکیری ہوتی ہے۔ اوپری باؤنڈ کے لیے، فیصلہ کے طریقہ کار (نیچے) کا استعمال کرتے ہوئے، k-fold مقداری متبادل کے ساتھ جملے جملے کی لمبائی کے k + O (1)-fold ایکسپونٹیشن (یکساں مستقلات کے ساتھ) کے مطابق وقت میں طے کیے جا سکتے ہیں۔ محوریت WS2S کو بعض بنیادی خصوصیات کے علاوہ انڈکشن اسکیما کے ذریعے محوریت کیا جا سکتا ہے۔ S2S کو جزوی طور پر اس طرح محوری بنایا جا سکتا ہے: (1) HE! s βt (t0  ऒत्त s βt1 βs) (خالی تار، جسے ε سے ظاہر کیا جاتا ہے ؛ HE! s کا مطلب ہے "منفرد s ہے") (2) βs، t βi βl {0,1} βj βl {0,1} (si = tj βs = t βi = j) (i اور j کا استعمال ایک مخفف ہے ؛ i = j کے لیے، 0 1 کے برابر نہیں ہے) (3) βS (S (ε) βs (S (s) βS (s0) βS ہمیشہ کی طرح، اگر φ میں آزاد متغیرات نہیں دکھائے گئے ہیں، تو ہم محوری کی عالمگیر بندش لیتے ہیں۔ اگر مساوات پیش گوئیوں کے لیے ابتدائی ہے، تو کوئی توسیع پسندی S = T ष्ण (s) ष्ण (s) کو بھی شامل کرتا ہے۔ چونکہ ہماری سمجھ ہے، انڈکشن اسکیما کے بجائے ایک بیان ہو سکتا ہے۔ S1S کی مماثل محوریت مکمل ہو چکی ہے۔ تاہم، S2S کے لیے، تکمیل کھلی ہے (2021 تک)۔ اگرچہ S1S میں یکسانیت ہے، لیکن کوئی S2S قابل تعریف (یہاں تک کہ پیرامیٹرز کی اجازت دینے والا) انتخاب فنکشن نہیں ہے جو ایک خالی سیٹ S کو S کا ایک عنصر واپس کرتا ہے، اور فہم اسکیما کو عام طور پر پسند کے محور کی مختلف شکلوں کے ساتھ بڑھایا جاتا ہے۔ تاہم، (1)-(4) اس وقت مکمل ہوتا ہے جب بعض برابری والے کھیلوں کے لیے ڈیٹرمینیسی اسکیما کے ساتھ توسیع کی جاتی ہے۔ S2S کو Π13 جملوں کے ذریعے بھی محوری بنایا جا سکتا ہے (تاروں پر سابقہ تعلق کو ابتدائی طور پر استعمال کرتے ہوئے)۔ تاہم، یہ حتمی طور پر محوریہ قابل نہیں ہے، اور نہ ہی اسے 13 جملوں کے ذریعے محوریہ بنایا جا سکتا ہے یہاں تک کہ اگر ہم انڈکشن اسکیما اور دیگر جملوں کا ایک محدود مجموعہ شامل کریں (یہ اس کے Π12-CA0 سے تعلق کی پیروی کرتا ہے)۔ S2S سے متعلق نظریات ہر محدود k کے لیے، تین چوڑائی ≤ k (اور ایک متعلقہ ٹری سڑنا) کے ساتھ قابل گنتی گراف کا موناڈک سیکنڈ آرڈر (MSO) نظریہ S2S میں قابل تشریح ہے (کورسل کا نظریہ دیکھیں)۔ مثال کے طور پر، درختوں کا ایم ایس او نظریہ (گراف کے طور پر) یا سیریز متوازی گراف فیصلہ کن ہے۔ یہاں (یعنی۔ باؤنڈڈ ٹری چوڑائی کے لیے)، ہم عمودی (یا کناروں) کے ایک سیٹ کے لیے فائنٹنیس کوانٹیفایر کی تشریح بھی کر سکتے ہیں، اور ایک مقررہ عدد میں سیٹ ماڈیولو میں عمودی (یا کناروں) کو بھی شمار کر سکتے ہیں۔ بے شمار گراف کی اجازت دینے سے نظریہ تبدیل نہیں ہوتا ہے۔ نیز، موازنہ کے لیے، S1S باؤنڈڈ پاتھ وڈتھ کے منسلک گراف کی تشریح کر سکتا ہے۔ اس کے برعکس، لامحدود تین چوڑائی کے گراف کے ہر سیٹ کے لیے، اس کا وجود (یعنی۔ 11) ایم ایس او تھیوری ناقابل فیصلہ ہے اگر ہم عمودی اور کناروں دونوں پر پیش گوئیوں کی اجازت دیتے ہیں۔ اس طرح، ایک لحاظ سے، S2S کی فیصلہ سازی بہترین ممکن ہے۔ غیر محدود تین چوڑائی والے گرافوں میں بڑے گرڈ نابالغ ہوتے ہیں، جنہیں ٹورنگ مشین کی تقلید کے لیے استعمال کیا جا سکتا ہے۔ ایس 2 ایس میں کمی سے، قابل گنتی آرڈرز کا ایم ایس او تھیوری فیصلہ کن ہے، جیسا کہ قابل گنتی درختوں کا ایم ایس او تھیوری ان کے کلین-بروور آرڈرز کے ساتھ ہے۔ تاہم، (، <) کا ایم ایس او نظریہ ناقابل فیصلہ ہے۔ آرڈینلز <ω2 کا ایم ایس او تھیوری فیصلہ کن ہے۔ ω2 کے لیے فیصلہ سازی ZFC سے آزاد ہے (فرض کریں کہ کون (ZFC + کمزور کمپیکٹ کارڈینل))۔ نیز، آرڈینلز پر موناڈک سیکنڈ آرڈر منطق کا استعمال کرتے ہوئے ایک آرڈینل کی تعریف کی جا سکتی ہے اگر اسے آرڈینل ایڈیشن اور ضرب کے ذریعے قابل تعریف باقاعدہ کارڈینلز سے حاصل کیا جا سکتا ہے۔ S2S بعض موڈل منطقوں کی فیصلہ سازی کے لیے مفید ہے، جس میں کرپکے سیمنٹکس قدرتی طور پر درختوں کی طرف لے جاتا ہے۔ S2S + U (یا صرف S1S + U) فیصلہ کن نہیں ہے اگر U غیر پابند مقداری ہے-UX φ (X) اگر f φ (X) کچھ من مانی طور پر بڑے محدود X کے لیے ہے۔ تاہم، WS2S + U، یہاں تک کہ لامحدود راستوں پر مقدار کے ساتھ، فیصلہ کن ہے، یہاں تک کہ S2S ذیلی فارمولوں کے ساتھ بھی جن میں U نہیں ہے۔ فارمولا پیچیدگی S2S میں بائنری تاروں کا ایک مجموعہ قابل تعریف ہے اگر یہ باقاعدہ ہے (یعنی۔ ایک باقاعدہ زبان کی تشکیل کرتا ہے)۔ S1S میں، سیٹوں پر ایک (یونیری) پیشن گوئی (پیرامیٹر فری) قابل تعریف ہے اگر یہ ایک ω-ریگولر زبان ہے۔ S2S کے لیے، ان فارمولوں کے لیے جو اپنے آزاد متغیرات کو صرف ان تاروں پر استعمال کرتے ہیں جن میں 1 نہیں ہوتا ہے، اظہار وہی ہے جو S1S کے لیے ہے۔ ہر S2S فارمولا φ (S1,., Sk)، (k فری متغیرات کے ساتھ) اور بائنری سٹرنگ T کے محدود ٹری کے لیے، φ (S1 θ T،., Sk θ T) کا حساب وقت لکیری میں |T | میں کیا جا سکتا ہے (کورسل کا نظریہ دیکھیں)، لیکن جیسا کہ اوپر ذکر کیا گیا ہے، اوور ہیڈ کو فارمولا سائز میں متغیر کیا جا سکتا ہے (زیادہ واضح طور پر، وقت ہے)۔ S1S کے لیے، ہر فارمولا δ11 فارمولے کے برابر ہے، اور Π02 ریاضی کے فارمولوں کے بولین امتزاج کے برابر ہے۔ مزید برآں، ہر S1S فارمولا فارمولے کے پیرامیٹرز کے متعلقہ ω-آٹومیٹن کے ذریعے قبولیت کے مساوی ہے۔ آٹومیٹن ایک تعیناتی برابری آٹومیٹن ہو سکتا ہے: ایک برابری آٹومیٹن میں ہر ریاست کے لیے ایک عدد ترجیح ہوتی ہے، اور یہ قبول کرتا ہے کہ آئی ایف ایف میں لامحدود طور پر دیکھی جانے والی اعلی ترین ترجیح اکثر عجیب (متبادل طور پر، یکساں) ہوتی ہے۔ S2S کے لیے، ٹری آٹومیٹا (نیچے) کا استعمال کرتے ہوئے، ہر فارمولا δ12 فارمولے کے مساوی ہے۔ مزید برآں، ہر S2S فارمولا ایک فارمولے کے مساوی ہوتا ہے جس میں صرف چار کوانٹیفایئر ہوتے ہیں، HE S β T β S β t. (یہ فرض کرتے ہوئے کہ ہماری رسمی شکل میں سابقہ تعلق اور جانشین افعال دونوں ہوتے ہیں)۔ S1S کے لیے، تین کوانٹیفایئرز (HE S® s HEt) کافی ہیں، اور WS2S اور WS1S کے لیے، دو کوانٹیفایئرز (HE S® t) کافی ہیں ؛ WS2S اور WS1S کے لیے یہاں پریفیکس ریلیشن کی ضرورت نہیں ہے۔ تاہم، فری سیکنڈ آرڈر متغیرات کے ساتھ، ہر S2S فارمولے کو صرف Π11 ٹرانسفائنٹ ریکرشن کے ذریعے سیکنڈ آرڈر ریاضی میں ظاہر نہیں کیا جا سکتا (ریورس ریاضی دیکھیں)۔ RCA0 + (اسکیما) {τ: τ ایک حقیقی S2S جملہ ہے} (اسکیما) کے مساوی ہے {τ: τ ایک Π13 جملہ ہے جو Π12-CA0} میں قابل ثبوت ہے۔ ایک بنیادی نظریہ کے مطابق، اسکیما (اسکیما اوور کے) کے مساوی ہوتے ہیں۔ محدود انضمام کی وجہ سے، Π12-CA0 یہ ثابت نہیں کرتا ہے کہ تمام سچ (معیاری فیصلہ کے طریقہ کار کے تحت) Π13 S2S بیانات اصل میں سچ ہیں حالانکہ اس طرح کا ہر جملہ ثابت Π12-CA0 ہے۔ مزید برآں، بائنری سٹرنگز S اور T کے سیٹ دیئے گئے ہیں، مندرجہ ذیل مساوی ہیں: (1) T S سے گنتی کے قابل بائنری سٹرنگز کثیر الجہتی وقت کے کچھ سیٹ سے S2S کی تعریف کی جا سکتی ہے۔ (2) T کا حساب کسی کھیل کے لیے جیتنے والی پوزیشنوں کے سیٹ سے لگایا جا سکتا ہے جس کی ادائیگی Π02 (S) سیٹوں کا ایک محدود بولین مجموعہ ہے۔ (3) ریاضی میں S سے T کی تعریف کی جا سکتی ہے (ریاضی کے فارمولے + کم سے کم فکسڈ پوائنٹ منطق) (4) T کم سے کم β ماڈل میں ہے (یعنی۔ ایک ω-ماڈل جس کا سیٹ تھیوریٹک ہم منصب ٹرانزیکٹو ہے) جس میں S ہوتا ہے اور Π12-CA0 کے تمام Π13 نتائج کو پورا کرتا ہے۔ ایس 1 ایس اور ایس 2 ایس کے ماڈل معیاری ماڈل کے علاوہ (جو ایس 1 ایس اور ایس 2 ایس کے لیے منفرد ایم ایس او ماڈل ہے)، ایس 1 ایس اور ایس 2 ایس کے لیے دوسرے ماڈل بھی ہیں، جو ڈومین کے تمام ذیلی سیٹوں کے بجائے کچھ استعمال کرتے ہیں (ہینکن سیمنٹکس دیکھیں)۔ ہر S ω کے لیے، S میں ریکرسو سیٹ معیاری S1S ماڈل کا ایک ابتدائی ذیلی ماڈل بناتے ہیں، اور ٹورنگ جوائن اور ٹورنگ ریڈکیوبلٹی کے تحت بند ω کے ذیلی سیٹوں کے ہر غیر خالی مجموعہ کے لیے یکساں ہوتے ہیں۔ یہ S1S کے قابل تعریف سیٹوں کے ساتھ ساتھ یکسانیت کے رشتہ دار تکرار سے ہوتا ہے:-φ (s) (s کے فنکشن کے طور پر) کا حساب φ کے پیرامیٹرز اور φ (s) کی اقدار سے s کے ایک محدود سیٹ کے لیے کیا جا سکتا ہے (اس کے سائز کے ساتھ جو φ کے لیے ایک متعین آٹومیٹن میں ریاستوں کی تعداد سے محدود ہے)۔ - HE Sφ (S) کے لیے ایک گواہ k اور S کا ایک محدود ٹکڑا منتخب کر کے حاصل کیا جا سکتا ہے، اور بار بار S کو اس طرح بڑھایا جا سکتا ہے کہ ہر توسیع کے دوران سب سے زیادہ ترجیح k ہو اور توسیع کو S میں مکمل کیا جا سکے جو k سے اوپر کی ترجیحات کو مارے بغیر φ کو مطمئن کرے (ان کی اجازت صرف ابتدائی S کے لیے ہے)۔ نیز، لغت کے لحاظ سے کم سے کم مختصر ترین انتخاب کا استعمال کرتے ہوئے، ایک S1S فارمولا φ 'ایسا ہے کہ φ' ν φ اور HE S φ (S) ν φ! S φ '(S) (یعنی۔ یکسانیت ؛ φ میں آزاد متغیرات نہیں دکھائے جا سکتے ہیں ؛ φ 'صرف فارمولا φ پر منحصر ہے)۔ S2S کا کم سے کم ماڈل بائنری سٹرنگ پر تمام باقاعدہ زبانوں پر مشتمل ہوتا ہے۔ یہ معیاری ماڈل کا ایک ابتدائی ذیلی ماڈل ہے، لہذا اگر S2S پیرامیٹر سے پاک قابل تعریف درختوں کا مجموعہ خالی نہیں ہے، تو اس میں ایک باقاعدہ درخت شامل ہے۔ ایک باقاعدہ زبان کو باقاعدہ {0,1}-لیبل شدہ مکمل لامحدود بائنری ٹری (تاروں پر پیش گوئیوں کے ساتھ شناخت شدہ) کے طور پر بھی سمجھا جا سکتا ہے۔ ایک لیبل شدہ ٹری باقاعدہ ہوتا ہے اگر اسے ابتدائی ورٹیکس کے ساتھ ورٹیکس لیبل والے محدود ڈائریکٹڈ گراف کو کھول کر حاصل کیا جا سکتا ہے۔ ابتدائی ورٹیکس سے قابل رسائی گراف میں ایک (ڈائریکٹڈ) سائیکل ایک لامحدود ٹری دیتا ہے۔ باقاعدہ درختوں کی اس تشریح اور انکوڈنگ کے ساتھ، ہر حقیقی S2S جملہ ابتدائی فنکشن ریاضی میں پہلے ہی ثابت ہو سکتا ہے۔ یہ غیر باقاعدہ درخت ہیں جن کے تعین کے لیے غیر متوقع فہم کی ضرورت پڑ سکتی ہے (نیچے)۔ غیر باقاعدہ ہیں (یعنی۔ غیر باقاعدہ زبانوں پر مشتمل) S1S کے ماڈل (اور ممکنہ طور پر S2S) (معیاری فرسٹ آرڈر پارٹ کے ساتھ اور اس کے بغیر) ایک کمپیوٹیبل اطمینان کے تعلق کے ساتھ۔ تاہم، تفہیم اور عزم کی ناکامی کی وجہ سے تاروں کے تکراری سیٹوں کا مجموعہ S2S کا نمونہ نہیں بناتا ہے۔ S2S کی فیصلہ سازی کا ثبوت یہ ظاہر کرنا ہے کہ ہر فارمولا غیر متعین ٹری آٹومیٹن کے ذریعہ قبولیت کے مساوی ہے (ٹری آٹومیٹن اور انفینٹ ٹری آٹومیٹن دیکھیں)۔ ایک لامحدود ٹری آٹومیٹن جڑ سے شروع ہوتا ہے اور درخت کو اوپر لے جاتا ہے، اور آئی ایف ایف کو قبول کرتا ہے جسے درخت کی ہر شاخ قبول کرتی ہے۔ ایک غیر متعین ٹری آٹومیٹن قبول کرتا ہے کہ آئی ایف ایف پلیئر 1 کی جیت کی حکمت عملی ہے، جہاں پلیئر 1 اجازت شدہ (موجودہ حالت اور ان پٹ کے لیے) نئی ریاستوں کی جوڑی (پی 0، پی 1) کا انتخاب کرتا ہے، جبکہ پلیئر 2 برانچ کا انتخاب کرتا ہے، پی 0 میں منتقلی کے ساتھ اگر 0 کا انتخاب کیا جاتا ہے اور پی 1 بصورت دیگر۔ شریک غیر تعیناتی آٹومیٹن کے لیے، تمام انتخاب کھلاڑی 2 کے ذریعے ہوتے ہیں، جبکہ تعیناتی کے لیے، (p0، p1) ریاست اور ان پٹ کے ذریعے طے کیا جاتا ہے ؛ اور گیم آٹومیٹن کے لیے، دونوں کھلاڑی برانچ اور ریاست کو ترتیب دینے کے لیے ایک محدود گیم کھیلتے ہیں۔ کسی شاخ پر قبولیت ان حالتوں پر مبنی ہوتی ہے جو شاخ پر لامحدود طور پر اکثر نظر آتی ہیں۔ یہاں پیریٹی آٹومیٹا کافی عام ہیں۔ فارمولوں کو آٹومیٹا میں تبدیل کرنے کے لیے، بیس کیس آسان ہے، اور غیر تعیناتی وجودی مقدار کے تحت بندش دیتا ہے، اس لیے ہمیں صرف تکمیل کے تحت بندش کی ضرورت ہے۔ برابری کے کھیلوں کی پوزیشن کے تعین کا استعمال کرتے ہوئے (جہاں ہمیں ناقابل فہم فہم کی ضرورت ہوتی ہے)، کھلاڑی 1 جیتنے کی حکمت عملی کا عدم وجود کھلاڑی کو 2 جیتنے کی حکمت عملی S دیتا ہے، جس میں شریک غیر متعین ٹری آٹومیٹن اس کی مضبوطی کی تصدیق کرتا ہے۔ اس کے بعد آٹومیٹن کو تعیناتی بنایا جا سکتا ہے (جہاں ہمیں حالتوں کی تعداد میں تیزی سے اضافہ ملتا ہے)، اور اس طرح S کا وجود غیر تعیناتی آٹومیٹن کی قبولیت سے مطابقت رکھتا ہے۔ عزم: ممکنہ طور پر زیڈ ایف سی میں، بوریل گیمز کا تعین کیا جاتا ہے، اور Π02 فارمولوں (من مانی حقیقی پیرامیٹرز کے ساتھ) کے بولین امتزاج کے لیے عزم کا ثبوت بھی یہاں ایک حکمت عملی دیتا ہے جو صرف موجودہ حالت اور درخت میں پوزیشن پر منحصر ہے۔ ثبوت ترجیحات کی تعداد کو شامل کرکے ہے۔ فرض کریں کہ k ترجیحات ہیں، جس میں سب سے زیادہ ترجیح k ہے، اور یہ کہ k کھلاڑی 2 کے لیے صحیح برابری رکھتا ہے۔ ہر پوزیشن (ٹری پوزیشن + اسٹیٹ) کے لیے کم از کم آرڈینل α (اگر کوئی ہو) اس طرح تفویض کریں کہ کھلاڑی 1 کے پاس جیتنے کی حکمت عملی ہو جس میں تمام داخل شدہ (ایک یا زیادہ مراحل کے بعد) ترجیحی k پوزیشن (اگر کوئی ہو) کے لیبل <α ہوں۔ اگر ابتدائی پوزیشن کا لیبل لگا دیا جائے تو کھلاڑی 1 جیت سکتا ہے: ہر بار جب ترجیحی k حالت تک پہنچ جاتا ہے، تو آرڈینل کم ہو جاتا ہے، اور اس کے علاوہ کمی کے درمیان، کھلاڑی 1 k-1 ترجیحات کے لیے حکمت عملی استعمال کر سکتا ہے۔ کھلاڑی 2 جیت سکتا ہے اگر پوزیشن کو غیر لیبل کیا گیا ہو: کے-1 ترجیحات کے تعین سے، کھلاڑی 2 کے پاس ایک حکمت عملی ہوتی ہے جو جیتتی ہے یا غیر لیبل شدہ ترجیحی کے ریاست میں داخل ہوتی ہے، ایسی صورت میں کھلاڑی 2 دوبارہ اس حکمت عملی کو استعمال کر سکتا ہے۔ حکمت عملی کو پوزیشنل بنانے کے لیے (کے پر انڈکشن کے ذریعے)، معاون گیم کھیلتے وقت، اگر دو منتخب پوزیشنل حکمت عملی ایک ہی پوزیشن کی طرف لے جاتی ہیں، تو نچلے α کے ساتھ، یا اسی α (یا کھلاڑی 2 کے لیے) نچلے ابتدائی پوزیشن کے ساتھ حکمت عملی جاری رکھیں (تاکہ ہم حکمت عملی کو محدود طور پر کئی بار تبدیل کر سکیں)۔ آٹومیٹا کا تعین: شریک غیر تعیناتی ٹری آٹومیٹا کے تعین کے لیے، ω-آٹومیٹا پر غور کرنا کافی ہے، برانچ کے انتخاب کو ان پٹ کے طور پر سمجھنا، آٹومیٹن کا تعین کرنا، اور اسے تعیناتی ٹری آٹومیٹن کے لیے استعمال کرنا۔ نوٹ کریں کہ یہ غیر متعین ٹری آٹومیٹا کے لیے بائیں جانے کے تعین کے طور پر کام نہیں کرتا (یعنی۔ s → s0) صحیح شاخ کے مندرجات پر منحصر ہو سکتا ہے ؛ غیر تعین پسندی کے برعکس، تعیناتی ٹری آٹومیٹا قطعی طور پر غیر خالی سیٹوں کو بھی قبول نہیں کر سکتا۔ ایک غیر تعیناتی ω-آٹومیٹن M کا تعین کرنے کے لیے (شریک غیر تعیناتی کے لیے، تکمیل لیں، یہ نوٹ کرتے ہوئے کہ تعیناتی برابری آٹومیٹا تکمیل کے تحت بند ہیں)، ہم ایک سفرا ٹری کا استعمال کر سکتے ہیں جس میں ہر نوڈ M کی ممکنہ حالتوں کے ایک سیٹ کو محفوظ کرتا ہے، اور اعلی ترجیحی حالتوں تک پہنچنے کی بنیاد پر نوڈ کی تخلیق اور حذف کرنا۔ تفصیلات کے لیے، دیکھیں یا۔ قبولیت کی فیصلہ سازی: خالی درخت کی غیر متعین برابری آٹومیٹن کی طرف سے قبولیت ایک محدود گراف G پر ایک برابری کے کھیل سے مطابقت رکھتی ہے۔ مندرجہ بالا پوزیشنل (جسے میموری لیس بھی کہا جاتا ہے) عزم کا استعمال کرتے ہوئے، اس کی تقلید ایک محدود کھیل کے ذریعے کی جا سکتی ہے جو اس وقت ختم ہوتا ہے جب ہم لوپ تک پہنچتے ہیں، جس میں جیتنے کی شرط لوپ میں سب سے زیادہ ترجیحی حالت پر مبنی ہوتی ہے۔ ایک ہوشیار اصلاح ایک کواسی پولینومیل ٹائم الگورتھم دیتی ہے، جو کہ کثیر الجہتی وقت ہوتا ہے جب ترجیحات کی تعداد کافی کم ہوتی ہے (جو عام طور پر عمل میں ہوتی ہے)۔ درختوں کا نظریہ: درختوں پر ایم ایس او منطق کی فیصلہ سازی کے لیے (یعنی۔ گراف جو درخت ہیں)، یہاں تک کہ فرسٹ آرڈر آبجیکٹ کے لیے فائنٹنیس اور ماڈیولر کاؤنٹنگ کوانٹیفایئرز کے ساتھ، ہم قابل گنتی درختوں کو مکمل بائنری ٹری میں سرایت کر سکتے ہیں اور S2S کی فیصلہ سازی کا استعمال کر سکتے ہیں۔ مثال کے طور پر، نوڈ s کے لیے، ہم اس کے بچوں کی نمائندگی s1، s01، s001 وغیرہ کے ذریعے کر سکتے ہیں۔ بے شمار درختوں کے لیے، ہم شیلاہ-اسٹپ تھیوریم (نیچے) استعمال کر سکتے ہیں۔ ہم کارڈینالیٹی ω1 والے سیٹ فرسٹ آرڈر آبجیکٹ کے لیے ایک پیشن گوئی بھی شامل کر سکتے ہیں، اور کارڈینالیٹی ω2 کے لیے پیشن گوئی، اور اسی طرح لامحدود باقاعدہ کارڈینلز کے لیے۔ باؤنڈڈ ٹری چوڑائی کے گرافز کی تشریح درختوں کا استعمال کرتے ہوئے کی جا سکتی ہے، اور کناروں پر پیش گوئیوں کے بغیر یہ باؤنڈڈ کلک چوڑائی کے گرافز پر بھی لاگو ہوتا ہے۔ S2S کو دیگر فیصلہ کن نظریات کے ساتھ جوڑنا موناڈک نظریات کی ٹری ایکسٹینشنز: شیلاہ اسٹپ تھیوریم کے مطابق، اگر موناڈک ریلیشنل ماڈل M فیصلہ کن ہے، تو اس کا ٹری ہم منصب بھی ایسا ہی ہے۔ مثال کے طور پر، (رسمی شکل کا ماڈیولو انتخاب) S2S {0,1} کا ٹری ہم منصب ہے۔ ٹری کے ہم منصب میں، فرسٹ آرڈر آبجیکٹ M کے عناصر کے محدود سلسلے ہوتے ہیں جو توسیع کے ذریعے ترتیب دیے جاتے ہیں، اور ایک M-رشتہ پائی کو Pi '(vd1,., vdk) ′Pi (d1,., dk) کے ساتھ نقشہ بنایا جاتا ہے جس میں Pi' غلط ہے بصورت دیگر (dj ωM، اور v M کے عناصر کا ایک (ممکنہ طور پر خالی) سلسلہ ہے۔ ثبوت S2S فیصلہ سازی ثبوت سے ملتا جلتا ہے۔ ہر مرحلے پر، ایک (غیر متعین) آٹومیٹن کو ان پٹ کے طور پر ایم آبجیکٹ (ممکنہ طور پر سیکنڈ آرڈر) کا ایک ٹپل ملتا ہے، اور ایک ایم فارمولا اس بات کا تعین کرتا ہے کہ کس حالت میں منتقلی کی اجازت ہے۔ پلیئر 1 (جیسا کہ اوپر بتایا گیا ہے) ایک نقشہ سازی چائلڈ کا انتخاب کرتا ہے جو فارمولے کے ذریعہ اجازت یافتہ ہے (موجودہ حالت کو دیکھتے ہوئے)، اور پلیئر 2 جاری رکھنے کے لیے چائلڈ (نوڈ کا) کا انتخاب کرتا ہے۔ غیر متعین آٹومیٹن کے ذریعے مسترد ہونے کا مشاہدہ کرنے کے لیے، ہر (نوڈ، اسٹیٹ) کے لیے (چائلڈ، اسٹیٹ) جوڑوں کا ایک مجموعہ اس طرح منتخب کریں کہ ہر انتخاب کے لیے، کم از کم ایک جوڑا مارا جائے، اور اس طرح کہ تمام نتیجے میں آنے والے راستے مسترد ہونے کا باعث بنیں۔ موناڈک تھیوری کو فرسٹ آرڈر تھیوری کے ساتھ جوڑنا: فیفرمین ووٹ تھیوریم کی توسیع/اطلاق مندرجہ ذیل ہے۔ اگر M ایک ایم ایس او ماڈل ہے اور N ایک فرسٹ آرڈر ماڈل ہے، تو M ایک (تھیوری (M)، تھیوری (N)) اوریکل سے متعلق فیصلہ کن رہتا ہے یہاں تک کہ اگر M کو تمام افعال M → N کے ساتھ بڑھایا جاتا ہے جہاں M کو اس کی پہلی اشیاء کے ساتھ شناخت کیا جاتا ہے، اور ہر s bul M کے لیے ہم N کی ایک جداگانہ کاپی استعمال کرتے ہیں، جس کے مطابق زبان میں ترمیم کی جاتی ہے۔ مثال کے طور پر، اگر N (، 0، +، ⋅) ہے، تو ہم بیان کر سکتے ہیں۔ اگر M S2S ہے (یا زیادہ عام طور پر، کچھ موناڈک ماڈل کا ٹری ہم منصب)، تو آٹومیٹا اب N-فارمولوں کا استعمال کر سکتا ہے، اور اس طرح f: M → Nk کو M سیٹوں کے ٹپل میں تبدیل کر سکتا ہے۔ اختلاف ضروری ہے کیونکہ بصورت دیگر مساوات کے ساتھ ہر لامحدود N کے لیے، توسیعی S2S یا صرف WS1S ناقابل فیصلہ ہے۔ نیز، ایک (ممکنہ طور پر نامکمل) تھیوری T کے لیے، T کے M-پروڈکٹس کا تھیوری TM ایک (تھیوری (M)، T) اوریکل سے متعلق فیصلہ کن ہے، جہاں TM کا ایک ماڈل ہر s bul M کے لیے T کے من مانی جداگانہ ماڈل Ns کا استعمال کرتا ہے (جیسا کہ اوپر، M ایک MSO ماڈل ہے ؛ تھیوری (Ns) کا انحصار s پر ہو سکتا ہے)۔ ثبوت فارمولا کی پیچیدگی پر انڈکشن کے ذریعے ہے۔ آئیے بمقابلہ مفت Ns متغیرات کی فہرست بنیں، بشمول f (s) اگر فنکشن f مفت ہے۔ انڈکشن کے ذریعے، یہ ظاہر ہوتا ہے کہ بمقابلہ صرف |vs | فری متغیرات کے ساتھ N-فارمولوں کے ایک محدود سیٹ کے ذریعے استعمال ہوتا ہے۔ اس طرح، ہم کیا ممکن ہے اس کا جواب دینے کے لیے N (یا T) کا استعمال کر کے تمام ممکنہ نتائج کی مقدار طے کر سکتے ہیں، اور فہرست کے امکانات (یا رکاوٹیں) کو دیکھتے ہوئے، M میں ایک متعلقہ جملے کی تشکیل کر سکتے ہیں۔ S2S کی توسیع میں کوڈنگ: سٹرنگز پر ہر فیصلہ کن پیش گوئی کو انکوڈ کیا جا سکتا ہے (لکیری ٹائم انکوڈنگ اور ڈیکوڈنگ کے ساتھ) S2S کی فیصلہ سازی کے لیے (یہاں تک کہ اوپر کی توسیع کے ساتھ بھی) انکوڈ شدہ پیش گوئی کے ساتھ۔ ثبوت: ایک غیر متعین لامحدود ٹری آٹومیٹن کو دیکھتے ہوئے، ہم محدود بائنری لیبل والے درختوں کے سیٹ کو (جن کے لیبل ہیں جن پر آٹومیٹن کام کر سکتا ہے) محدود طور پر بہت سی کلاسوں میں تقسیم کر سکتے ہیں جیسے کہ اگر ایک مکمل لامحدود بائنری ٹری ایک ہی طبقے کے درختوں پر مشتمل ہو سکتا ہے، تو قبولیت کا انحصار صرف کلاس اور ابتدائی حالت (یعنی۔ بتائیں کہ آٹومیٹن درخت میں داخل ہوتا ہے)۔ (پمپنگ لیما کے ساتھ کسی حد تک مماثلت کو نوٹ کریں۔) مثال کے طور پر (پیریٹی آٹومیٹن کے لیے)، درختوں کو ایک ہی کلاس میں تفویض کریں اگر ان کے پاس وہی پیش گوئی ہے جو ابتدائی _ ریاست دی گئی ہے اور (ریاست، سب سے زیادہ _ ترجیح _ پہنچ) جوڑوں کا سیٹ Q واپس کرتا ہے چاہے کھلاڑی 1 (یعنی۔ غیر تعین پسندی) بیک وقت تمام شاخوں کو ق کے عناصر کے مطابق ہونے پر مجبور کر سکتی ہے۔ اب، ہر k کے لیے، درختوں کا ایک محدود مجموعہ (کوڈنگ کے لیے موزوں) منتخب کریں جو آٹومیٹا 1-k کے لیے ایک ہی کلاس سے تعلق رکھتے ہیں، جس میں k کے پار مطابقت رکھنے والی کلاس کا انتخاب ہوتا ہے۔ پیش گوئی کو انکوڈ کرنے کے لیے، k = 1 کا استعمال کرتے ہوئے کچھ بٹس کو انکوڈ کریں، پھر k = 2 کا استعمال کرتے ہوئے مزید بٹس، اور اسی طرح۔ حوالہ جات اضافی حوالہ: ریاضیاتی منطق کمپیوٹیبلٹی تھیوری ثبوت پر مشتمل مضامین