Q0 (mathematical logic)
کیو 0 پیٹر اینڈریوز کی سادہ ٹائپ شدہ لیمبڈا کیلکولس کی تشکیل ہے، اور ریاضی کے لیے ایک بنیاد فراہم کرتا ہے جس کا موازنہ فرسٹ آرڈر منطق پلس سیٹ تھیوری سے کیا جا سکتا ہے۔ یہ اعلی درجے کی منطق کی ایک شکل ہے اور HOL تھیوریم پروور فیملی کے منطق سے قریب سے متعلق ہے۔ تھیوریم ثابت کرنے والے نظام ٹی پی ایس اور ای ٹی پی ایس کیو 0 پر مبنی ہیں۔ اگست 2009 میں، ٹی پی ایس نے اعلی درجے کے نظریہ ثابت کرنے والے نظاموں کے درمیان پہلا مقابلہ جیتا۔ اس نظام میں صرف پانچ محوریات ہیں، جنہیں اس طرح بیان کیا جا سکتا ہے: (محوریات 2، 3، اور 4 محوری اسکیما ہیں-اسی طرح کے محوریات کے خاندان۔ محوریم 2 اور محوریم 3 کی مثالیں صرف متغیرات اور مستقلات کی اقسام کے لحاظ سے مختلف ہوتی ہیں، لیکن محوریم 4 کی مثالوں میں A اور B کی جگہ کوئی اظہار ہو سکتا ہے۔) سبسکرپٹڈ "او" بولین ویلیوز کے لیے ٹائپ علامت ہے، اور سبسکرپٹڈ "آئی" انفرادی (غیر بولین) ویلیوز کے لیے ٹائپ علامت ہے۔ ان کے سلسلے افعال کی اقسام کی نمائندگی کرتے ہیں، اور مختلف افعال کی اقسام میں فرق کرنے کے لیے قوسین شامل کر سکتے ہیں۔ سبسکرپٹ شدہ یونانی حروف جیسے α اور β قسم کی علامتوں کے لیے نحو متغیر ہیں۔ بولڈ بڑے حروف جیسے،، اور ڈبلیو ایف ایف کے لیے نحو متغیر ہیں، اور بولڈ چھوٹے حروف جیسے، متغیرات کے لیے نحو متغیر ہیں۔ تمام آزاد واقعات پر نحو متبادل کی نشاندہی کرتا ہے۔ صرف ابتدائی مستقلات ہیں، جو ہر قسم α کے ممبروں کی مساوات کی نشاندہی کرتے ہیں، اور، افراد کے لیے ایک تفصیل آپریٹر کی نشاندہی کرتے ہیں، بالکل ایک فرد پر مشتمل سیٹ کا منفرد عنصر۔ علامتیں λ اور بریکٹ ("[" اور "]") زبان کی نحو ہیں۔ دیگر تمام علامتیں ان پر مشتمل اصطلاحات کے لیے مخففات ہیں، بشمول کوانٹیفائرز۔ محور 4 میں، ان کے لیے آزاد ہونا چاہیے، مطلب یہ ہے کہ متبادل کے نتیجے میں آزاد متغیرات کے پابند ہونے کے کسی بھی واقعات کا سبب نہیں بنتا ہے۔ محوریات کے بارے میں محوری 1 اس خیال کا اظہار کرتا ہے کہ اور یہ واحد بولین اقدار ہیں۔ محوری اسکیما 2α اور 3αβ افعال کی بنیادی خصوصیات کا اظہار کرتے ہیں۔ محوری اسکیما 4 λ اشارے کی نوعیت کی وضاحت کرتا ہے۔ محور 5 کا کہنا ہے کہ سلیکشن آپریٹر افراد پر مساوات کے فعل کا الٹا ہے۔ (ایک دلیل کو دیکھتے ہوئے، اس فرد کو انفرادی پر مشتمل سیٹ/پیشن گوئی کے ساتھ نقشہ بنائیں۔ ق 0 میں، ایک مخفف ہے، جو اس کا مخفف ہے۔) اس آپریٹر کو ڈیفینیٹ ڈسکریشن آپریٹر کے نام سے بھی جانا جاتا ہے۔ میں، محور 4 کو پانچ ذیلی حصوں میں تیار کیا گیا ہے جو متبادل کے عمل کو توڑ دیتے ہیں۔ جیسا کہ یہاں دیا گیا محور ایک متبادل کے طور پر زیر بحث ہے اور ذیلی حصوں سے ثابت ہوتا ہے۔ منطقی کور اینڈریوز کی توسیعات اس منطق کو تمام اقسام کے مجموعوں کے لیے سلیکشن آپریٹرز کی تعریفوں کے ساتھ بڑھاتی ہیں، تاکہ ′ ایک تھیوریم (نمبر 5309) ہو۔ دوسرے لفظوں میں، تمام اقسام کا ایک قطعی تفصیل آپریٹر ہوتا ہے۔ یہ ایک قدامت پسند توسیع ہے، لہذا اگر کور مستقل ہے تو تو توسیعی نظام مستقل ہے۔ وہ ایک اضافی محوری 6 بھی پیش کرتا ہے، جس میں کہا گیا ہے کہ لامحدود کے مساوی متبادل محوریات کے ساتھ لامحدود افراد موجود ہیں۔ ٹائپ تھیوری اور ٹائپ تھیوری پر مبنی پروف اسسٹنٹ کی بہت سی دیگر فارمولیشنوں کے برعکس، کیو 0 او اور آئی کے علاوہ دیگر بنیادی اقسام کے لیے فراہم نہیں کرتا ہے، لہذا مثال کے طور پر محدود کارڈینل نمبروں کو افراد کے مجموعے کے طور پر بنایا جاتا ہے جو سادہ ٹائپ تھیوری کے معنی میں ایک قسم کے بجائے معمول کے پیانو مفروضوں کی پابندی کرتے ہیں۔ ق 0 ق 0 میں تخمینہ کا ایک واحد اصول ہے۔ قاعدہ R. سے اور ان کے ایک واقعہ کو ایک واقعہ سے تبدیل کرنے کے نتیجے کا اندازہ لگانا، بشرطیکہ ان کا واقعہ (متغیر کا واقعہ) فوری طور پر اس سے پہلے نہیں ہے۔ تخمینہ R′ کا اخذ شدہ قاعدہ مفروضوں کے ایک سیٹ سے استدلال کو قابل بناتا ہے۔ H. قاعدہ R′۔ اگر، اور، اور ایک واقعہ کی جگہ ایک واقعہ کی جگہ لے کر حاصل کیا جاتا ہے، تو، بشرطیکہ: ان کا واقعہ فوری طور پر اس سے پہلے آنے والے متغیر کا واقعہ نہیں ہے، اور کوئی متغیر آزاد نہیں ہے اور اس کا ممبر پابند نہیں ہے۔ نوٹ: بائی ان کے متبادل پر پابندی اس بات کو یقینی بناتی ہے کہ کوئی بھی متغیر دونوں مفروضوں میں آزاد ہے اور تبدیلی کے بعد دونوں میں ایک ہی قدر رکھنے کے لیے پابند رہتا ہے۔ ق 0 کے لیے کٹوتی تھیوریم سے پتہ چلتا ہے کہ قاعدہ R′ کا استعمال کرتے ہوئے مفروضوں کے ثبوتوں کو مفروضوں کے بغیر اور قاعدہ R کا استعمال کرتے ہوئے ثبوتوں میں تبدیل کیا جا سکتا ہے۔ کچھ اسی طرح کے نظاموں کے برعکس، ق 0 میں تخمینہ ڈبلیو ایف ایف کے اندر کسی بھی گہرائی میں ذیلی اظہار کی جگہ مساوی اظہار کے ساتھ لے لیتا ہے۔ تو مثال کے طور پر دیے گئے محوریات: 1. 2. اور حقیقت یہ ہے کہ، ہم مقداری کو ہٹائے بغیر آگے بڑھ سکتے ہیں: 3. A اور B 4 کے لیے فوری طور پر۔ قاعدہ R لائن 3 کا استعمال کرتے ہوئے لائن 1 میں تبدیل کر رہا ہے۔ نوٹ حوالہ جات مزید پڑھنا مزید گہرائی میں ق 0 کی تفصیل ؛ اسٹینفورڈ انسائیکلوپیڈیا آف فلاسفی میں چرچ کے ٹائپ تھیوری پر ایک مضمون کا حصہ۔ ریاضیاتی منطق پر ایک جائزہ (بشمول ق 0 کے مختلف جانشین): ریاضی کی بنیادیں۔ نسب اور جائزہ دوئی: 10.4444/100.111۔ کمپیوٹر سائنس میں منطق