Theories of iterated inductive definitions
سیٹ تھیوری اور منطق میں، بوچولز کا آئی ڈی درجہ بندی فرسٹ آرڈر ریاضی کے ذیلی نظاموں کا درجہ بندی ہے۔ نظاموں/نظریات کو "ν-اوقات تکرار شدہ تعریفی تعریفوں کے رسمی نظریات" کے طور پر حوالہ دیا جاتا ہے۔ آئی ڈی این او مونوٹون آپریٹرز کے ν تکرار شدہ کم از کم فکسڈ پوائنٹس کے ذریعے پی اے کو بڑھاتا ہے۔ تعریف اصل تعریف رسمی نظریہ IDω (اور عام طور پر IDν) پیانو ریاضی کی ایک توسیع ہے، جسے زبان LID میں درج ذیل محوریوں کے ذریعے وضع کیا گیا ہے: ہر LID-فارمولا F (x) کے لیے نظریہ IDν کی تعریف اس طرح کی گئی ہے: ہر LID-فارمولا F (x) کے لیے اور ہر u <ν وضاحت/متبادل تعریف ID1 A سیٹ کو انڈکٹو طور پر بیان کیا جاتا ہے اگر کسی مونوٹونک آپریٹر کے لیے، جہاں سب سے کم فکسڈ پوائنٹ کی نشاندہی ہوتی ہے۔ آئی ڈی 1، کی زبان، فرسٹ آرڈر نمبر تھیوری سے حاصل کی جاتی ہے، ایل این [ایکس] میں ہر ایکس مثبت فارمولہ اے (ایکس، ایکس) کے لیے ایک سیٹ (یا پیش گوئی) مستقل آئی اے کے اضافے سے جس میں صرف ایکس (ایک نیا سیٹ متغیر) اور ایکس (ایک نمبر متغیر) آزاد متغیر کے طور پر ہوتا ہے۔ X-مثبت اصطلاح کا مطلب ہے کہ X صرف A میں مثبت ہوتا ہے (X کبھی بھی کسی مضمرات کے بائیں طرف نہیں ہوتا ہے)۔ ہم اپنے آپ کو تھوڑا سا سیٹ تھیوریٹک نوٹیشن دیتے ہیں: یعنی دو فارمولوں اور ذرائع کے لیے۔ پھر آئی ڈی 1 میں فرسٹ آرڈر نمبر تھیوری (پی اے) کے محوریات شامل ہیں جن میں انڈکشن اسکیم کو نئی زبان تک بڑھایا گیا ہے اور ساتھ ہی یہ محوریات: جہاں تمام فارمولوں کی حدود ہیں۔ نوٹ کریں کہ وہ اظہار جو ریاضی کے لحاظ سے قابل تعریف سیٹ آپریٹر کے تحت بند ہے، جبکہ اس کا اظہار کم از کم ایسا ہے (کم از کم قابل تعریف سیٹوں میں)۔ اس طرح، اس کا مطلب سب سے کم پہلے سے طے شدہ نقطہ ہے، اور اس لیے آپریٹر کا سب سے کم طے شدہ نقطہ ہے۔ آئی ڈی این ν-اوقات تکرار شدہ تعریفی تعریفوں کے نظام کی وضاحت کرنے کے لیے، جہاں ν ایک آرڈینل ہے، آئیے آرڈر ٹائپ ν کی ایک ابتدائی ریکرسو ویل آرڈرنگ ہو۔ ہم کے میدان کے عناصر کو ظاہر کرنے کے لیے یونانی حروف استعمال کرتے ہیں۔ آئی ڈی این کی زبان، ہر ایکس مثبت فارمولے کے لیے بائنری پیش گوئی مستقل جے اے کے اضافے سے حاصل کی جاتی ہے جس میں زیادہ سے زیادہ دکھائے گئے آزاد متغیرات ہوتے ہیں، جہاں ایکس دوبارہ ایک یونری (سیٹ) متغیر ہے، اور وائی ایک تازہ بائنری پیش گوئی متغیر ہے۔ ہم اس کے بجائے لکھتے ہیں، x کو مؤخر الذکر فارمولے میں ایک ممتاز متغیر کے طور پر سوچتے ہیں۔ نظام IDν اب فرسٹ آرڈر نمبر تھیوری (PA) کے نظام سے حاصل کیا جاتا ہے جس میں انڈکشن اسکیم کو نئی زبان میں بڑھایا جاتا ہے اور ایک صوابدیدی فارمولے کے ساتھ ساتھ محوریوں کے لیے ٹرانسفائنٹ انڈکشن کا اظہار کرنے والی اسکیم کو شامل کیا جاتا ہے: جہاں ایک صوابدیدی فارمولا ہے۔ میں اور ہم نے فارمولہ کا مخفف استعمال کیا، جہاں ممتاز متغیر ہے۔ ہم دیکھتے ہیں کہ یہ اس بات کا اظہار کرتے ہیں کہ آپریٹر کے لیے ہر ایک سب سے کم فکسڈ پوائنٹ (قابل تعریف سیٹوں میں) ہے۔ نوٹ کریں کہ کس طرح تمام پچھلے سیٹ، کے لیے، پیرامیٹرز کے طور پر استعمال ہوتے ہیں۔ اس کے بعد ہم وضاحت کرتے ہیں۔ متغیرات-کا ایک کمزور ورژن ہے۔ کے نظام میں، اس کے بجائے ایک سیٹ کو انڈکٹو طور پر بیان کیا جاتا ہے اگر کسی مونوٹونک آپریٹر کے لیے، سب سے کم فکسڈ پوائنٹ کے بجائے ایک فکسڈ پوائنٹ ہو۔ یہ ٹھیک ٹھیک فرق نظام کو نمایاں طور پر کمزور بنا دیتا ہے:، جبکہ۔ مزید کمزور ہو جاتا ہے۔ میں، یہ نہ صرف کم سے کم فکسڈ پوائنٹس کے بجائے فکسڈ پوائنٹس کا استعمال کرتا ہے، اور صرف مثبت فارمولوں کے لیے انڈکشن رکھتا ہے۔ یہ ایک بار پھر ٹھیک ٹھیک فرق نظام کو اور بھی کمزور بنا دیتا ہے:، جبکہ۔ W-اقسام پر مبنی تمام اقسام میں سب سے کمزور ہے۔ باقاعدہ تکرار شدہ انڈکٹو تعریفوں کے مقابلے میں کمزور ہونے کی مقدار دوسرے درجے کے ریاضی کے ایک مخصوص ذیلی نظام کو دیکھتے ہوئے بار انڈکشن کو ہٹانے کے مترادف ہے۔ ، جبکہ۔ یہ ایک "بے نقاب" مضبوطی ہے۔ یہ بالکل فرسٹ آرڈر ریاضی کا نظام نہیں ہے، لیکن ν-اوقات تکرار شدہ عمومی تعریفی تعریفوں کی بنیاد پر پیش گوئی استدلال سے جو کچھ حاصل کیا جا سکتا ہے اس پر قبضہ کرتا ہے۔ طاقت میں اضافے کی مقدار سے:، جبکہ میں اضافے کے برابر ہے۔ نتائج ν> 0 ہونے دیں۔ اگر a bul T0 میں ν <μ کے ساتھ کوئی علامت Dμ نہیں ہے، تو "a bul W0" IDν میں قابل ثبوت ہے۔ IDω میں موجود ہے۔ اگر IDν میں a-جملے کو ثابت کیا جا سکتا ہے، تو ایسا موجود ہے۔ اگر جملہ A تمام ν <ω کے لیے IDν میں قابل ثبوت ہے، تو k ω N اس طرح موجود ہے کہ۔ پروف تھیوریٹک آرڈینلز ID <ν کا پروف تھیوریٹک آرڈینل اس کے برابر ہے۔ IDν کا پروف تھیوریٹک آرڈینل اس کے برابر ہے۔ کا پروف تھیوریٹک آرڈینل برابر ہے۔ فار کا پروف تھیوریٹک آرڈینل اس کے برابر ہے۔ کا پروف تھیوریٹک آرڈینل برابر ہے۔ فار کا پروف تھیوریٹک آرڈینل اس کے برابر ہے۔ فار کا پروف تھیوریٹک آرڈینل اس کے برابر ہے۔ کا پروف تھیوریٹک آرڈینل برابر ہے۔ کا پروف تھیوریٹک آرڈینل برابر ہے۔ کا پروف تھیوریٹک آرڈینل برابر ہے۔ کا پروف تھیوریٹک آرڈینل برابر ہے۔ کا پروف تھیوریٹک آرڈینل برابر ہے۔ کا پروف تھیوریٹک آرڈینل برابر ہے۔ آئی ڈی 1 (باخمین-ہاورڈ آرڈینل) کا پروف تھیوریٹک آرڈینل بھی، اور کا پروف تھیوریٹک آرڈینل ہے۔ W-IDω () کا پروف تھیوریٹک آرڈینل بھی اس کا پروف تھیوریٹک آرڈینل ہے۔ IDω کا پروف تھیوریٹک آرڈینل (ٹیکوٹی-فیفرمین-بوچولز آرڈینل) بھی، اور کا پروف تھیوریٹک آرڈینل ہے۔ آئی ڈی <ω ^ ω () کا پروف تھیوریٹک آرڈینل بھی اس کا پروف تھیوریٹک آرڈینل ہے۔ آئی ڈی <ε0 () کا پروف تھیوریٹک آرڈینل بھی اور کا پروف تھیوریٹک آرڈینل ہے۔ حوالہ جات تکرار شدہ تعریفی تعریفیں اور تجزیہ کے ذیلی نظاموں کے لیے ایک آزاد نتیجہ: حالیہ ثبوت-نظریاتی مطالعات تکرار شدہ تعریفی تعریفوں کے بدیہی نظریہ کے لیے این لیب لیما میں تکرار شدہ تعریفی تعریفیں تکرار شدہ تعریفی تعریفیں اور اگڈا میں بڑے قابل گنتی آرڈینلز اور نمبر۔