Natural deduction
منطق اور ثبوت کے نظریہ میں، قدرتی کٹوتی ایک قسم کا ثبوت کیلکولس ہے جس میں منطقی استدلال کا اظہار قیاس کے اصولوں کے ذریعے کیا جاتا ہے جو استدلال کے "قدرتی" طریقے سے قریب سے متعلق ہوتے ہیں۔ یہ ہلبرٹ طرز کے نظاموں سے متصادم ہے، جو اس کے بجائے کٹوتی استدلال کے منطقی قوانین کو ظاہر کرنے کے لیے زیادہ سے زیادہ محوریات کا استعمال کرتے ہیں۔ محرک قدرتی کٹوتی ہلبرٹ، فریج اور رسل کے نظاموں میں عام کٹوتی استدلال کے محوریات کے ساتھ عدم اطمینان کے تناظر سے پیدا ہوئی (دیکھیں، مثال کے طور پر، ہلبرٹ نظام)۔ اس طرح کے محوریات کو سب سے زیادہ مشہور طور پر رسل اور وائٹ ہیڈ نے اپنے ریاضیاتی مقالے پرنسپیا میتھمیٹکا میں استعمال کیا تھا۔ 1926 میں پولینڈ میں ہونے والے سیمیناروں کے ایک سلسلے سے حوصلہ افزائی کرتے ہوئے جس میں منطق کے زیادہ قدرتی علاج کی وکالت کی گئی تھی، جاکووسکی نے زیادہ قدرتی کٹوتی کی وضاحت کرنے کی ابتدائی کوششیں کیں، پہلے 1929 میں خاکہ کے اشارے کا استعمال کرتے ہوئے، اور بعد میں 1934 اور 1935 میں کاغذات کے سلسلے میں اپنی تجویز کو اپ ڈیٹ کیا۔ ان کی تجاویز کے نتیجے میں مختلف اشارے جیسے فچ طرز کے کیلکولس (یا فچ کے خاکے) یا سپس کا طریقہ جس کے لیے لیمون نے سسٹم ایل نامی ایک قسم دی۔ قدرتی کٹوتی کو اس کی جدید شکل میں جرمن ریاضی دان گیرہارڈ جینٹزن نے 1933 میں گوٹنگن یونیورسٹی کے ریاضیاتی علوم کی فیکلٹی کو فراہم کردہ ایک مقالے میں آزادانہ طور پر تجویز کیا تھا۔ قدرتی کٹوتی کی اصطلاح (یا اس کے بجائے، اس کے جرمن مساوی نیچرلیچس شلیسین) اس مقالے میں وضع کی گئی تھی: جینٹزن نمبر تھیوری کی مستقل مزاجی کو قائم کرنے کی خواہش سے متاثر تھا۔ وہ مستقل نتائج کے لیے درکار بنیادی نتیجہ، کٹ ایلیمینیشن تھیوریم-ہاپٹسٹز-کو براہ راست قدرتی کٹوتی کے لیے ثابت کرنے سے قاصر تھے۔ اس وجہ سے اس نے اپنا متبادل نظام، سیکوینٹ کیلکولس متعارف کرایا، جس کے لیے اس نے کلاسیکی اور بدیہی منطق دونوں کے لیے ہاپٹسٹز کو ثابت کیا۔ 1961 اور 1962 میں سیمیناروں کے ایک سلسلے میں پروٹز نے قدرتی کٹوتی کیلکولی کا ایک جامع خلاصہ دیا، اور جینٹزن کے زیادہ تر کام کو ترتیب وار کیلکولی کے ساتھ قدرتی کٹوتی کے فریم ورک میں منتقل کیا۔ ان کا 1965 کا مونوگراف نیچرل ڈیڈکشن: اے پروف تھیوریٹیکل اسٹڈی نیچرل ڈیڈکشن پر ایک حوالہ کام بننے والا تھا، اور اس میں موڈل اور سیکنڈ آرڈر منطق کے لیے ایپلی کیشنز شامل تھیں۔ قدرتی کٹوتی میں، تخمینہ کے اصولوں کو بار بار لاگو کرکے احاطے کے مجموعے سے ایک تجویز کا اندازہ لگایا جاتا ہے۔ اس مضمون میں پیش کیا گیا نظام جینٹزن یا پروٹز کی تشکیل کا ایک معمولی تغیر ہے، لیکن مارٹن لوف کی منطقی فیصلوں اور رابطوں کی تفصیل پر قریب سے عمل پیرا ہے۔ فیصلے اور تجاویز ایک فیصلہ ایسی چیز ہے جو قابل علم ہے، یعنی علم کا مقصد ہے۔ اگر حقیقت میں کوئی اسے جانتا ہے تو یہ واضح ہے۔ اس طرح "بارش ہو رہی ہے" ایک فیصلہ ہے، جو اس شخص کے لیے واضح ہے جو جانتا ہے کہ واقعی بارش ہو رہی ہے ؛ اس معاملے میں کوئی شخص کھڑکی سے باہر دیکھ کر یا گھر سے باہر نکل کر فیصلے کا ثبوت آسانی سے تلاش کر سکتا ہے۔ تاہم ریاضیاتی منطق میں، ثبوت اکثر اتنے براہ راست قابل مشاہدہ نہیں ہوتے، بلکہ زیادہ بنیادی واضح فیصلوں سے اخذ کیے جاتے ہیں۔ کٹوتی کا عمل وہ ہے جو ثبوت بناتا ہے ؛ دوسرے لفظوں میں، فیصلہ واضح ہوتا ہے اگر کسی کے پاس اس کا ثبوت ہو۔ منطق میں سب سے اہم فیصلے "اے سچ ہے" کی شکل کے ہوتے ہیں۔ حرف اے کسی بھی اظہار کے لیے کھڑا ہوتا ہے جو کسی تجویز کی نمائندگی کرتا ہے۔ اس طرح سچائی کے فیصلوں کے لیے زیادہ قدیم فیصلے کی ضرورت ہوتی ہے: "اے ایک تجویز ہے"۔ بہت سے دوسرے فیصلوں کا مطالعہ کیا گیا ہے ؛ مثال کے طور پر، "A غلط ہے" (کلاسیکی منطق دیکھیں)، "A وقت t پر درست ہے" (عارضی منطق دیکھیں)، "A لازمی طور پر درست ہے" یا "A ممکنہ طور پر درست ہے" (موڈل منطق دیکھیں)، "پروگرام M میں ٹائپ τ ہے" (پروگرامنگ زبانیں اور ٹائپ تھیوری دیکھیں)، "A دستیاب وسائل سے حاصل کیا جا سکتا ہے" (لکیری منطق دیکھیں)، اور بہت سے دوسرے۔ شروع کرنے کے لیے، ہم اپنے آپ کو آسان ترین دو فیصلوں سے متعلق سوچیں گے "A ایک تجویز ہے" اور "A سچ ہے"، مختصر طور پر بالترتیب "A پروپ" اور "A سچ"۔ فیصلہ "اے پروپ" اے کے درست ثبوتوں کے ڈھانچے کی وضاحت کرتا ہے، جو بدلے میں تجاویز کے ڈھانچے کی وضاحت کرتا ہے۔ اس وجہ سے، اس فیصلے کے قیاس کے قواعد کو بعض اوقات تشکیل کے قواعد کے نام سے جانا جاتا ہے۔ مثال کے طور پر، اگر ہمارے پاس دو تجاویز اے اور بی ہیں (یعنی فیصلے "اے پروپ" اور "بی پروپ" واضح ہیں)، تو ہم مرکب تجویز اے اور بی بناتے ہیں، جسے علامتی طور پر "" لکھا جاتا ہے۔ ہم اسے ایک انفریشن رول کی شکل میں لکھ سکتے ہیں: جہاں انفریشن رول کو مزید مختصر بنانے کے لیے قوسین کو چھوڑ دیا جاتا ہے: یہ انفریشن رول اسکیمیٹک ہے: A اور B کو کسی بھی اظہار کے ساتھ فوری کیا جا سکتا ہے۔ انفریشن رول کی عمومی شکل یہ ہے: جہاں ہر ایک فیصلہ ہوتا ہے اور انفریشن رول کو "نام" کا نام دیا جاتا ہے۔ لکیر کے اوپر کے فیصلوں کو احاطہ کہا جاتا ہے، اور لکیر کے نیچے والے فیصلے ہوتے ہیں۔ دیگر عام منطقی تجاویز اختلاط ()، نفی ()، امپلیکیشن ()، اور منطقی مستقلات سچائی () اور جھوٹ () ہیں۔ ان کی تشکیل کے اصول ذیل میں ہیں۔ تعارف اور خاتمہ اب ہم "ایک سچے" فیصلے پر بحث کرتے ہیں۔ قیاس کے وہ اصول جو نتیجہ میں منطقی ربط کو متعارف کراتے ہیں، تعارف کے قوانین کے نام سے جانے جاتے ہیں۔ امتزاج متعارف کرانے کے لیے، یعنی، تجاویز A اور B کے لیے "A اور B سچ" کا نتیجہ اخذ کرنے کے لیے، "A سچ" اور "B سچ" کے ثبوت کی ضرورت ہوتی ہے۔ ایک قیاس کے اصول کے طور پر: یہ سمجھنا ضروری ہے کہ اس طرح کے اصولوں میں اشیاء تجاویز ہیں۔ یعنی، مندرجہ بالا قاعدہ واقعی ایک مخفف ہے: یہ بھی لکھا جا سکتا ہے: اس شکل میں، پہلی بنیاد کو تشکیل کے اصول سے مطمئن کیا جا سکتا ہے، جس میں پچھلی شکل کے پہلے دو احاطے دیے گئے ہیں۔ اس مضمون میں ہم "پروپ" فیصلوں کو جہاں سمجھا جائے گا وہاں سے نکال لیں گے۔ کالعدم معاملے میں، کوئی بھی کسی بھی جگہ سے سچائی حاصل نہیں کر سکتا۔ اگر کسی تجویز کی سچائی کو ایک سے زیادہ طریقوں سے قائم کیا جا سکتا ہے، تو متعلقہ کنیکٹو میں متعدد تعارف کے اصول ہوتے ہیں۔ نوٹ کریں کہ کالعدم معاملے میں، یعنی جھوٹ کے لیے، تعارف کے کوئی اصول نہیں ہیں۔ اس طرح کوئی بھی آسان فیصلوں سے جھوٹ کا اندازہ نہیں لگا سکتا۔ دوہرے سے تعارف کے قواعد خاتمے کے قواعد ہیں جو یہ بیان کرتے ہیں کہ مرکب تجویز کے بارے میں معلومات کو اس کے اجزاء کے بارے میں معلومات میں کیسے تبدیل کیا جائے۔ اس طرح، "اے ڈبلیو بی ٹرو" سے، ہم یہ نتیجہ اخذ کر سکتے ہیں کہ "اے ٹرو" اور "بی ٹرو": تخمینہ کے اصولوں کے استعمال کی ایک مثال کے طور پر، کنجکشن کی تبادلہیت پر غور کریں۔ اگر اے ڈبلیو بی درست ہے، تو بی ڈبلیو اے درست ہے ؛ یہ مشتق اس انداز میں قیاس کے قواعد تشکیل دے کر تیار کیا جا سکتا ہے کہ کم تخمینہ کا احاطہ اگلے اعلی تخمینہ کے نتیجے سے میل کھاتا ہے۔ ہم نے اب تک جو تخمینے کے اعداد و شمار دیکھے ہیں وہ مضمرات کے تعارف یا اختلاط کے خاتمے کے اصولوں کو بیان کرنے کے لیے کافی نہیں ہیں۔ ان کے لیے، ہمیں فرضی مشتق کے زیادہ عمومی تصور کی ضرورت ہے۔ فرضی مشتقات ریاضیاتی منطق میں ایک وسیع عمل مفروضوں سے استدلال ہے۔ مثال کے طور پر، مندرجہ ذیل مشتق پر غور کریں: یہ مشتق B کی سچائی کو اس طرح قائم نہیں کرتا ہے ؛ بلکہ، یہ مندرجہ ذیل حقیقت کو قائم کرتا ہے: اگر A ′ (B ′C) سچ ہے تو B سچ ہے۔ منطق میں، ایک کہتا ہے کہ "یہ فرض کرتے ہوئے کہ اے ڈبلیو (بی ڈبلیو سی) سچ ہے، ہم دکھاتے ہیں کہ بی سچ ہے" ؛ دوسرے لفظوں میں، فیصلہ "بی سچ" فرض شدہ فیصلے "اے ڈبلیو (بی ڈبلیو سی) سچ" پر منحصر ہے۔ یہ ایک فرضی مشتق ہے، جسے ہم مندرجہ ذیل طور پر لکھتے ہیں: تشریح یہ ہے: "B سچ A ऱ् (B ऱ् C) سچ سے مشتق ہے"۔ یقینا، اس مخصوص مثال میں ہم اصل میں "بی ٹرو" کی مشتق "اے ڈبلیو (بی ڈبلیو سی) ٹرو" سے جانتے ہیں، لیکن عام طور پر ہم مشتق کو ترجیحی طور پر نہیں جانتے ہوں گے۔ فرضی مشتقات کی عمومی شکل یہ ہے: ہر فرضی مشتقات میں اوپری لائن پر لکھے گئے سابقہ مشتقات (دی) کا مجموعہ ہوتا ہے، اور نچلی لائن پر ایک کامیاب فیصلہ (جے) لکھا جاتا ہے۔ ہر ایک احاطہ خود ایک فرضی مشتق ہو سکتا ہے۔ (سادگی کے لیے، ہم کسی فیصلے کو بنیاد سے کم مشتق سمجھتے ہیں۔) فرضی فیصلے کے تصور کو مضمرات کے مربوط ہونے کے طور پر اندرونی بنایا گیا ہے۔ تعارف اور خاتمے کے اصول مندرجہ ذیل ہیں۔ تعارف کے اصول میں، یو نامی سابقہ نتیجہ میں خارج ہوتا ہے۔ یہ مفروضے کے دائرہ کار کو محدود کرنے کا ایک طریقہ کار ہے: اس کے وجود کی واحد وجہ "بی ٹرو" قائم کرنا ہے ؛ اسے کسی دوسرے مقصد کے لیے استعمال نہیں کیا جا سکتا، اور خاص طور پر، اسے تعارف کے نیچے استعمال نہیں کیا جا سکتا۔ مثال کے طور پر، "A′ (B′ (A′B)) کے مشتق کو درست سمجھیں: اس مکمل مشتق کا کوئی غیر مطمئن احاطہ نہیں ہے ؛ تاہم، ذیلی مشتقات فرضی ہیں۔ مثال کے طور پر، "B′ (A′B) سچ" کا مشتق سابقہ "A" سچ "(نام u) کے ساتھ فرضی ہے۔ فرضی مشتقات کے ساتھ، اب ہم اختلاط کے لیے خاتمے کا اصول لکھ سکتے ہیں: الفاظ میں، اگر A. B سچ ہے، اور ہم "A سچ" اور "B سچ" دونوں سے "C سچ" حاصل کر سکتے ہیں، تو C واقعی سچ ہے۔ نوٹ کریں کہ یہ قاعدہ "اے ٹرو" یا "بی ٹرو" کا پابند نہیں ہے۔ صفر کے معاملے میں، یعنی۔ جھوٹ کے لیے، ہم مندرجہ ذیل خاتمے کا اصول حاصل کرتے ہیں: اسے اس طرح پڑھا جاتا ہے: اگر جھوٹ سچ ہے، تو کوئی بھی تجویز C سچ ہے۔ منفی اثر سے ملتا جلتا ہے۔ تعارف کا قاعدہ مفروضے کے نام u دونوں کو خارج کرتا ہے، اور جانشین p، یعنی تجویز p کو نتیجہ A میں نہیں ہونا چاہیے۔ چونکہ یہ اصول منصوبہ بند ہیں، تو تعارف کے اصول کی تشریح یہ ہے: اگر "اے ٹرو" سے ہم ہر تجویز پی کے لیے اخذ کر سکتے ہیں کہ "پی ٹرو"، تو اے کو غلط ہونا چاہیے، یعنی "اے ٹرو نہیں"۔ خاتمے کے لیے، اگر A اور A دونوں کو درست دکھایا جائے، تو ایک تضاد ہے، اس صورت میں ہر تجویز C درست ہے۔ چونکہ امپلیکیشن اور نیگیشن کے قوانین اتنے ملتے جلتے ہیں، اس لیے یہ دیکھنا کافی آسان ہونا چاہیے کہ A اور A کے مساوی نہیں ہیں، یعنی ہر ایک دوسرے سے مشتق ہے۔ مستقل مزاجی، تکمیل، اور عام شکلیں ایک نظریہ کو مستقل کہا جاتا ہے اگر جھوٹ ثابت نہیں ہوتا ہے (بغیر کسی مفروضے کے) اور مکمل ہوتا ہے اگر ہر نظریہ یا اس کی نفی منطق کے قیاس کے اصولوں کا استعمال کرتے ہوئے ثابت ہو۔ یہ پوری منطق کے بارے میں بیانات ہیں، اور عام طور پر کسی ماڈل کے کسی تصور سے منسلک ہوتے ہیں۔ تاہم، مستقل مزاجی اور مکمل ہونے کے مقامی تصورات ہیں جو خالصتا قیاس کے اصولوں پر نحو چیک ہیں، اور ماڈلز کو اپیل کرنے کی ضرورت نہیں ہے۔ ان میں سے پہلا مقامی مستقل مزاجی ہے، جسے مقامی تخفیف کے نام سے بھی جانا جاتا ہے، جس میں کہا گیا ہے کہ کسی کنیکٹو کے تعارف پر مشتمل کسی بھی مشتق کے بعد اس کے فوری خاتمے کو اس چکر کے بغیر مساوی مشتق میں تبدیل کیا جا سکتا ہے۔ یہ خاتمے کے قوانین کی طاقت پر ایک چیک ہے: انہیں اتنا مضبوط نہیں ہونا چاہیے کہ ان میں وہ علم شامل ہو جو پہلے سے ہی ان کے احاطے میں موجود نہ ہو۔ مثال کے طور پر، امتزاج پر غور کریں۔ دو طرفہ طور پر، مقامی تکمیل کا کہنا ہے کہ خاتمے کے قوانین اتنے مضبوط ہیں کہ کسی کنیکٹو کو اس کے تعارف کے اصول کے لیے موزوں فارموں میں تحلیل کر سکتے ہیں۔ دوبارہ امتزاج کے لیے: یہ تصورات کری-ہاورڈ آئسومورفزم کا استعمال کرتے ہوئے لیمبڈا کیلکولس میں β-کمی (بیٹا کمی) اور η-تبدیلی (ایٹا تبدیلی) سے بالکل مطابقت رکھتے ہیں۔ مقامی تکمیل سے، ہم دیکھتے ہیں کہ ہر مشتق کو مساوی مشتق میں تبدیل کیا جا سکتا ہے جہاں اصل کنیکٹو متعارف کرایا جاتا ہے۔ درحقیقت، اگر پوری مشتق تعارف کے بعد خاتمے کے اس حکم کی پابندی کرتی ہے، تو اسے نارمل کہا جاتا ہے۔ ایک عام مشتق میں تمام خاتمے تعارف سے اوپر ہوتے ہیں۔ زیادہ تر منطقوں میں، ہر مشتق کا مساوی عام مشتق ہوتا ہے، جسے عام شکل کہا جاتا ہے۔ عام شکلوں کا وجود عام طور پر صرف قدرتی کٹوتی کا استعمال کرتے ہوئے ثابت کرنا مشکل ہے، حالانکہ اس طرح کے بیانات ادب میں موجود ہیں، خاص طور پر 1961 میں ڈاگ پروٹز کے ذریعے۔ اسے بالواسطہ طور پر کٹ فری سیکوینٹ کیلکولس پریزنٹیشن کے ذریعے دکھانا بہت آسان ہے۔ پہلے اور اعلی درجے کی توسیعات پہلے والے حصے کی منطق ایک ہی ترتیب شدہ منطق کی مثال ہے، یعنی ایک ہی قسم کے آبجیکٹ کے ساتھ منطق: تجاویز۔ اس سادہ ڈھانچے کی بہت سی توسیعات تجویز کی گئی ہیں ؛ اس حصے میں ہم اسے دوسری قسم کے افراد یا شرائط کے ساتھ بڑھائیں گے۔ مزید واضح طور پر، ہم ایک نئی قسم کا فیصلہ شامل کریں گے، "t ایک اصطلاح ہے" (یا "t اصطلاح") جہاں t اسکیمیٹک ہے۔ ہم متغیرات کا ایک قابل شمار سیٹ V، فنکشن علامتوں کا ایک اور قابل شمار سیٹ F طے کریں گے، اور مندرجہ ذیل تشکیل کے اصولوں کے ساتھ اصطلاحات کی تعمیر کریں گے: اور تجاویز کے لیے، ہم پیش گوئیوں کے تیسرے قابل شمار سیٹ P پر غور کرتے ہیں، اور مندرجہ ذیل تشکیل کے اصول کے ساتھ اصطلاحات پر جوہری پیش گوئیوں کی وضاحت کرتے ہیں: تشکیل کے پہلے دو اصول ایک ایسی اصطلاح کی تعریف فراہم کرتے ہیں جو مؤثر طریقے سے وہی ہے جو اصطلاح الجبرا اور ماڈل تھیوری میں بیان کی گئی ہے، حالانکہ مطالعہ کے ان شعبوں کا فوکس قدرتی کٹوتی سے بالکل مختلف ہے۔ تشکیل کا تیسرا قاعدہ مؤثر طریقے سے جوہری فارمولے کی وضاحت کرتا ہے، جیسا کہ فرسٹ آرڈر منطق میں، اور پھر ماڈل تھیوری میں۔ ان میں تشکیل کے اصولوں کا ایک جوڑا شامل کیا گیا ہے، جو مقداری تجاویز کے لیے اشارے کی وضاحت کرتا ہے۔ ایک عالمگیر (β) اور وجودی (HE) مقدار کے لیے: عالمگیر مقدار میں تعارف اور خاتمے کے اصول ہوتے ہیں: وجودی مقدار میں تعارف اور خاتمے کے اصول ہوتے ہیں: ان اصولوں میں، اشارے [t/x] A کا مطلب A میں x کی ہر (مرئی) مثال کے لیے t کے متبادل کے لیے ہوتا ہے، گرفتاری سے گریز کرتے ہوئے۔ جیسا کہ پہلے نام پر موجود سپر اسکرپٹس ان اجزاء کے لیے کھڑے ہوتے ہیں جو خارج کیے جاتے ہیں: اصطلاح a، I کے اختتام میں نہیں آسکتی (اس طرح کی اصطلاحات کو آئجین ویری ایبلز یا پیرامیٹرز کے نام سے جانا جاتا ہے)، اور HE میں u اور v نامی مفروضوں کو ایک فرضی مشتق میں دوسری بنیاد پر مقامی بنایا جاتا ہے۔ اگرچہ پہلے کے حصوں کی تجویز کردہ منطق فیصلہ کن تھی، لیکن کوانٹیفائرز کو شامل کرنے سے منطق ناقابل فیصلہ ہو جاتی ہے۔ اب تک، مقداری توسیعات پہلے درجے کی ہوتی ہیں: وہ تجاویز کو ان اشیاء کی اقسام سے ممتاز کرتی ہیں جن کی مقدار طے کی گئی ہے۔ اعلی درجے کی منطق ایک مختلف نقطہ نظر اختیار کرتی ہے اور اس میں صرف ایک ہی قسم کی تجاویز ہوتی ہیں۔ مقدار کے ڈومین کے طور پر مقدار میں ایک ہی قسم کی تجاویز ہوتی ہیں، جیسا کہ تشکیل کے قواعد میں ظاہر ہوتا ہے: اعلی ترتیب کی منطق کے لیے تعارف اور خاتمے کے فارموں کی بحث اس مضمون کے دائرہ کار سے باہر ہے۔ فرسٹ آرڈر اور ہائیر آرڈر منطق کے درمیان ہونا ممکن ہے۔ مثال کے طور پر، دوسرے درجے کی منطق میں دو قسم کی تجاویز ہوتی ہیں، ایک قسم اصطلاحات پر مقداری، اور دوسری قسم پہلی قسم کی تجاویز پر مقداری۔ قدرتی کٹوتی کی مختلف پریزنٹیشنز ٹری جیسی پریزنٹیشنز جنٹزن کی خارج ہونے والی تشریحات جو فرضی فیصلوں کو اندرونی بنانے کے لیے استعمال ہوتی ہیں ان سے ثبوتوں کو حقیقی فیصلوں کے درخت کے بجائے ترتیب کے درخت کے طور پر پیش کر کے بچا جا سکتا ہے۔ ترتیب وار پریزنٹیشنز جسکووسکی کی قدرتی کٹوتی کی نمائندگی مختلف اشارے کا باعث بنی جیسے فچ طرز کا کیلکولس (یا فچ کے خاکے) یا سپس کا طریقہ، جس میں سے لیمون نے سسٹم ایل نامی ایک قسم دی۔ اس طرح کے پریزنٹیشن سسٹم، جنہیں زیادہ درست طریقے سے ٹیبلر کے طور پر بیان کیا جاتا ہے، میں درج ذیل شامل ہیں۔ 1940: ایک نصابی کتاب میں، کوئین نے مربع بریکٹ میں لائن نمبروں کے ذریعے سابقہ انحصار کا اشارہ کیا، جس میں سپیس کے 1957 کے لائن نمبر کے اشارے کی توقع کی گئی تھی۔ 1950: ایک نصابی کتاب میں، انحصار کی نشاندہی کرنے کے لیے ثبوت کی ہر لائن کے بائیں طرف ایک یا زیادہ ستاروں کا استعمال کرنے کا طریقہ دکھایا گیا۔ یہ کلین کی عمودی سلاخوں کے برابر ہے۔ (یہ مکمل طور پر واضح نہیں ہے کہ آیا کوئین کا ستارے کا اشارہ اصل 1950 کے ایڈیشن میں شائع ہوا تھا یا بعد کے ایڈیشن میں شامل کیا گیا تھا۔) 1957: عملی منطق تھیوریم کا تعارف جو ایک نصابی کتاب میں ثابت ہوتا ہے۔ اس سے انحصار کی نشاندہی ہوتی ہے (یعنی۔ سابقہ تجاویز) ہر لائن کے بائیں طرف لائن نمبروں کے لحاظ سے۔ 1963: قدرتی کٹوتی کے تخمینے کے قواعد پر مبنی ترتیب وار منطقی دلائل کی لائنوں کے سابقہ انحصار کی نشاندہی کرنے کے لیے لائن نمبروں کے سیٹوں کا استعمال کرتا ہے۔ 1965: پوری نصابی کتاب میں قیاس پر مبنی طریقہ استعمال کرتے ہوئے منطق کے ثبوتوں کا تعارف ہے۔ 1967: ایک نصابی کتاب میں، مختصر طور پر دو قسم کے عملی منطق کے ثبوتوں کا مظاہرہ کیا گیا، ایک نظام جس میں ہر لائن کے بائیں طرف سابقہ تجاویز کے واضح حوالہ جات کا استعمال کیا گیا ہے، دوسرا نظام انحصار کی نشاندہی کرنے کے لیے بائیں طرف عمودی بار لائنوں کا استعمال کرتا ہے۔ ثبوت اور ٹائپ تھیوری قدرتی کٹوتی کی پیشکش نے اب تک ثبوت کی رسمی تعریف دیے بغیر تجاویز کی نوعیت پر توجہ مرکوز کی ہے۔ ثبوت کے تصور کو باقاعدہ بنانے کے لیے، ہم فرضی مشتقات کی پیشکش کو قدرے تبدیل کرتے ہیں۔ ہم ماضی کو ثبوت متغیرات (متغیرات کے کچھ قابل شمار سیٹ V سے) کے ساتھ لیبل لگاتے ہیں، اور اصل ثبوت کے ساتھ جانشین کو سجاتے ہیں۔ ماضی یا مفروضوں کو ٹرن اسٹائل کے ذریعے جانشین سے الگ کیا جاتا ہے۔ یہ ترمیم بعض اوقات مقامی مفروضوں کے نام سے کی جاتی ہے۔ مندرجہ ذیل خاکہ تبدیلی کا خلاصہ پیش کرتا ہے۔ مفروضوں کا مجموعہ اس وقت لکھا جائے گا جب ان کی صحیح ساخت متعلقہ نہ ہو۔ ثبوت کو واضح کرنے کے لیے، ہم بغیر ثبوت کے فیصلے "اے ٹرو" سے فیصلے کی طرف بڑھتے ہیں: "π (اے ٹرو) کا ثبوت ہے"، جسے علامتی طور پر "π: اے ٹرو" لکھا جاتا ہے۔ معیاری نقطہ نظر پر عمل کرتے ہوئے، فیصلے "π ثبوت" کے لیے ثبوتوں کو ان کے اپنے تشکیل کے اصولوں کے ساتھ متعین کیا جاتا ہے۔ سب سے آسان ممکنہ ثبوت لیبل شدہ مفروضے کا استعمال ہے۔ اس معاملے میں ثبوت خود لیبل ہے۔ مختصر ہونے کے لیے، ہم اس مضمون کے بقیہ حصے میں عدالتی لیبل کو درست چھوڑ دیں گے، یعنی، "καπ: A" لکھیں۔ آئیے واضح ثبوتوں کے ساتھ کچھ کنیکٹیوز کا دوبارہ جائزہ لیں۔ امتزاج کے لیے، ہم امتزاج کے ثبوت کی شکل کو دریافت کرنے کے لیے تعارف کے اصول کو دیکھتے ہیں: وہ دونوں امتزاج کے ثبوت کا ایک جوڑا ہونا چاہیے۔ اس طرح: خاتمے کے قواعد E1 اور E2 بائیں یا دائیں کنجکٹ کا انتخاب کرتے ہیں۔ اس طرح ثبوت پروجیکشنز کا ایک جوڑا ہے-پہلا (fst) اور دوسرا (snd)۔ مضمرات کے لیے، تعارف فارم مفروضے کو مقامی بناتا ہے یا باندھتا ہے، جسے λ کا استعمال کرتے ہوئے لکھا جاتا ہے ؛ یہ خارج شدہ لیبل سے مطابقت رکھتا ہے۔ قاعدے میں، "κ، u: A" کا مطلب ہے مفروضوں کا مجموعہ، اضافی مفروضے u کے ساتھ مل کر۔ واضح طور پر دستیاب ثبوتوں کے ساتھ، کوئی بھی ثبوت کے بارے میں ہیرا پھیری اور استدلال کر سکتا ہے۔ ثبوتوں پر کلیدی عمل دوسرے ثبوت میں استعمال ہونے والے مفروضے کے لیے ایک ثبوت کا متبادل ہے۔ یہ عام طور پر متبادل تھیوریم کے طور پر جانا جاتا ہے، اور دوسرے فیصلے کی گہرائی (یا ساخت) پر انڈکشن کے ذریعے ثابت کیا جا سکتا ہے۔ متبادل تھیوریم اگر κ′π1: A اور κ، u: A′π2: B، تو κ′ [π1/u] π2: B۔ اب تک کے فیصلے کی "κ′π: A" خالصتا منطقی تشریح رہی ہے۔ ٹائپ تھیوری میں، اشیاء کے زیادہ کمپیوٹیشنل نقطہ نظر کے لیے منطقی نقطہ نظر کا تبادلہ کیا جاتا ہے۔ منطقی تشریح میں تجاویز کو اب اقسام کے طور پر دیکھا جاتا ہے، اور ثبوت کو لیمبڈا کیلکولس میں پروگرام کے طور پر دیکھا جاتا ہے۔ اس طرح "π: A" کی تشریح یہ ہے کہ "پروگرام π کی قسم A ہے"۔ منطقی کنیکٹیوز کو بھی ایک مختلف ریڈنگ دی جاتی ہے: کنجکشن کو پروڈکٹ (×) کے طور پر دیکھا جاتا ہے، امپلیکیشن کو فنکشن تیر (→) وغیرہ کے طور پر دیکھا جاتا ہے۔ تاہم، فرق صرف کاسمیٹک ہیں۔ ٹائپ تھیوری میں تشکیل، تعارف اور خاتمے کے اصولوں کے لحاظ سے ایک قدرتی کٹوتی کی پیشکش ہوتی ہے ؛ درحقیقت، قاری آسانی سے پچھلے حصوں سے سادہ ٹائپ تھیوری کے طور پر جانا جاتا ہے جسے دوبارہ تشکیل دے سکتا ہے۔ منطق اور ٹائپ تھیوری کے درمیان فرق بنیادی طور پر اقسام (تجاویز) سے پروگراموں (ثبوت) کی طرف توجہ مرکوز کرنا ہے۔ ٹائپ تھیوری بنیادی طور پر پروگراموں کی تبدیلی یا تخفیف میں دلچسپی رکھتی ہے۔ ہر قسم کے لیے، اس قسم کے کینونکل پروگرام ہوتے ہیں جو ناقابل تلافی ہوتے ہیں ؛ انہیں کینونکل فارمز یا ویلیوز کے نام سے جانا جاتا ہے۔ اگر ہر پروگرام کو کینونکل شکل میں کم کیا جا سکتا ہے، تو ٹائپ تھیوری کو نارملائزنگ (یا کمزور نارملائزنگ) کہا جاتا ہے۔ اگر کینونکل شکل منفرد ہے، تو نظریہ کو مضبوطی سے معمول پر لانے والا کہا جاتا ہے۔ نارملسیبلٹی زیادہ تر غیر معمولی قسم کے نظریات کی ایک نایاب خصوصیت ہے، جو منطقی دنیا سے ایک بڑی روانگی ہے۔ (یاد رکھیں کہ تقریبا ہر منطقی مشتق کا مساوی عام مشتق ہوتا ہے۔) وجہ کا خاکہ بنانے کے لیے: ٹائپ تھیوریز میں جو تکراری تعریفوں کو تسلیم کرتے ہیں، ایسے پروگرام لکھنا ممکن ہے جو کبھی بھی قدر تک کم نہ ہوں۔ اس طرح کے لوپنگ پروگراموں کو عام طور پر کسی بھی قسم کا دیا جا سکتا ہے۔ خاص طور پر، لوپنگ پروگرام میں ٹائپ ڈی ڈی ہے، حالانکہ "ڈی ڈی سچ" کا کوئی منطقی ثبوت نہیں ہے۔ اس وجہ سے، تجاویز بطور اقسام ؛ ثبوت بطور پروگرام پیراڈائم صرف ایک سمت میں کام کرتے ہیں، اگر بالکل بھی: ٹائپ تھیوری کی منطق کے طور پر تشریح کرنا عام طور پر ایک متضاد منطق دیتا ہے۔ مثال: انحصار ٹائپ تھیوری منطق کی طرح، ٹائپ تھیوری میں بھی بہت سی توسیعات اور مختلف حالتیں ہیں، جن میں فرسٹ آرڈر اور ہائیر آرڈر ورژن شامل ہیں۔ ایک شاخ، جسے ڈیپینڈینٹ ٹائپ تھیوری کہا جاتا ہے، کمپیوٹر کے تعاون سے چلنے والے متعدد پروف سسٹمز میں استعمال ہوتی ہے۔ منحصر ٹائپ تھیوری کوانٹیفایئرز کو خود پروگراموں کی حد تک جانے کی اجازت دیتی ہے۔ ان مقداری اقسام کو β اور HE کے بجائے β اور β کے طور پر لکھا جاتا ہے، اور ان میں تشکیل کے درج ذیل اصول ہوتے ہیں: یہ اقسام بالترتیب تیر اور مصنوعات کی اقسام کی عمومی شکلیں ہیں، جیسا کہ ان کے تعارف اور خاتمے کے قوانین سے ظاہر ہوتا ہے۔ مکمل عام طور پر منحصر ٹائپ تھیوری بہت طاقتور ہے: یہ پروگراموں کی تقریبا کسی بھی قابل فہم خاصیت کو براہ راست پروگرام کی اقسام میں ظاہر کرنے کے قابل ہے۔ یہ عامیت ایک سخت قیمت پر آتی ہے-یا تو ٹائپ چیکنگ ناقابل فیصلہ ہے (ایکسٹینشنل ٹائپ تھیوری)، یا ایکسٹینشنل استدلال زیادہ مشکل ہے (انٹینشنل ٹائپ تھیوری)۔ اس وجہ سے، کچھ انحصار قسم کے نظریات صوابدیدی پروگراموں پر مقدار کی اجازت نہیں دیتے ہیں، بلکہ کسی دیئے گئے فیصلہ کن انڈیکس ڈومین کے پروگراموں تک محدود ہیں، مثال کے طور پر انٹیجرز، سٹرنگز، یا لکیری پروگرام۔ چونکہ انحصار قسم کے نظریات اقسام کو پروگراموں پر انحصار کرنے کی اجازت دیتے ہیں، اس لیے پوچھنا ایک فطری سوال ہے کہ کیا پروگراموں کے لیے اقسام، یا کسی دوسرے امتزاج پر انحصار کرنا ممکن ہے۔ اس طرح کے سوالات کے کئی قسم کے جوابات ہیں۔ ٹائپ تھیوری میں ایک مقبول نقطہ نظر یہ ہے کہ پروگراموں کو اقسام کے لحاظ سے مقداری بنانے کی اجازت دی جائے، جسے پیرامیٹرک پولیمورفزم بھی کہا جاتا ہے۔ اس کی دو اہم قسمیں ہیں: اگر اقسام اور پروگراموں کو الگ رکھا جائے تو کوئی کسی حد تک زیادہ اچھے رویے والا نظام حاصل کرتا ہے جسے پریڈیکیٹو پولیمورفزم کہا جاتا ہے۔ اگر پروگرام اور قسم کے درمیان فرق دھندلا ہوتا ہے، تو کوئی اعلی ترتیب کی منطق کا ٹائپ تھیوریٹک اینالاگ حاصل کرتا ہے، جسے امپریڈیکیٹو پولیمورفزم بھی کہا جاتا ہے۔ ادب میں انحصار اور پولیمرفزم کے مختلف امتزاج پر غور کیا گیا ہے، جن میں سب سے مشہور ہینک بیرینڈریگٹ کا لیمبڈا کیوب ہے۔ منطق اور ٹائپ تھیوری کا انٹرسیکشن ایک وسیع اور فعال تحقیقی شعبہ ہے۔ نئے منطقوں کو عام طور پر عام قسم کی نظریاتی ترتیب میں رسمی شکل دی جاتی ہے، جسے منطقی فریم ورک کہا جاتا ہے۔ مقبول جدید منطقی ڈھانچے جیسے کہ تعمیرات کا حساب اور ایل ایف اعلی ترتیب پر منحصر ٹائپ تھیوری پر مبنی ہیں، جس میں فیصلہ سازی اور اظہار کی طاقت کے لحاظ سے مختلف تجارت ہوتی ہے۔ یہ منطقی ڈھانچے خود ہمیشہ قدرتی کٹوتی کے نظام کے طور پر متعین کیے جاتے ہیں، جو قدرتی کٹوتی کے نقطہ نظر کی استعداد کا ثبوت ہے۔ کلاسیکی اور موڈل منطق سادگی کے لیے، اب تک پیش کردہ منطق بدیہی رہے ہیں۔ کلاسیکی منطق بدیہی منطق کو ایک اضافی محوری یا خارج شدہ وسط کے اصول کے ساتھ پھیلاتی ہے: کسی بھی تجویز p کے لیے، تجویز p ′p درست ہے۔ یہ بیان واضح طور پر کوئی تعارف یا خاتمہ نہیں ہے ؛ درحقیقت، اس میں دو الگ الگ ربط شامل ہیں۔ جینٹزن کا خارج شدہ مڈل کا اصل علاج درج ذیل تین (مساوی) فارمولیشنوں میں سے ایک تجویز کرتا ہے، جو پہلے ہی ہلبرٹ اور ہیٹنگ کے نظاموں میں مماثل شکلوں میں موجود تھے: (XM3 محض XM2 ہے جس کا اظہار E کے لحاظ سے کیا گیا ہے۔) خارج شدہ مڈل کا یہ علاج، پیورسٹ کے نقطہ نظر سے قابل اعتراض ہونے کے علاوہ، عام شکلوں کی تعریف میں اضافی پیچیدگیاں متعارف کراتا ہے۔ صرف تعارف اور خاتمے کے قوانین کے لحاظ سے کلاسیکی قدرتی کٹوتی کا نسبتا زیادہ تسلی بخش علاج پہلی بار 1992 میں پیریگوٹ نے کلاسیکی لیمبڈا کیلکولس کی شکل میں تجویز کیا تھا جسے λμ کہا جاتا ہے۔ ان کے نقطہ نظر کی کلیدی بصیرت سچائی پر مبنی فیصلے A کو زیادہ کلاسیکی تصور کے ساتھ تبدیل کرنا تھا، جو کہ ترتیب وار کیلکولس کی یاد دلاتا ہے: مقامی شکل میں، A کے بجائے، انہوں نے γ کا استعمال کیا۔ یہ ڈھانچہ بنیادی طور پر کلاسیکی سیکوینٹ کیلکولی سے براہ راست اٹھایا گیا ہے، لیکن ایل آئی ایس پی اور اس کی اولاد میں نظر آنے والے کال سی سی یا تھرو/کیچ میکانزم کے لحاظ سے کلاسیکی قدرتی کٹوتی کے ثبوتوں کو کمپیوٹیشنل معنی دینا تھا۔ (یہ بھی دیکھیں: فرسٹ کلاس کنٹرول۔) ایک اور اہم توسیع موڈل اور دیگر منطقوں کے لیے تھی جن کے لیے صرف سچائی کے بنیادی فیصلے سے زیادہ کی ضرورت ہوتی ہے۔ ان کو سب سے پہلے 1965 میں پروٹز کے ذریعہ قدرتی کٹوتی کے انداز میں الیتھک موڈل لاجکس ایس 4 اور ایس 5 کے لیے بیان کیا گیا تھا، اور اس کے بعد سے اس نے متعلقہ کام کا ایک بڑا حصہ جمع کیا ہے۔ ایک سادہ سی مثال دینے کے لیے، موڈل منطق S4 کے لیے ایک نئے فیصلے کی ضرورت ہوتی ہے، "A درست"، جو سچائی کے حوالے سے درجہ بند ہے: اگر "A سچ" "B سچ" کی شکل کے کسی مفروضے کے تحت نہیں ہے، تو "A درست"۔ اس واضح فیصلے کو مندرجہ ذیل تعارف اور خاتمے کے قواعد کے ساتھ ایک غیر متزلزل کنیکٹو اے ("لازمی طور پر اے" پڑھیں) کے طور پر اندرونی بنایا گیا ہے: نوٹ کریں کہ بنیاد "اے ویلڈ" کے کوئی وضاحتی اصول نہیں ہیں ؛ اس کے بجائے، صداقت کی واضح تعریف اس کی جگہ پر استعمال ہوتی ہے۔ یہ طریقہ مقامی شکل میں واضح ہو جاتا ہے جب مفروضے واضح ہوتے ہیں۔ ہم لکھتے ہیں "ω ؛ a سچ" جہاں ω پہلے کی طرح حقیقی مفروضوں پر مشتمل ہے، اور ω درست مفروضوں پر مشتمل ہے۔ دائیں طرف صرف ایک فیصلہ ہے "اے ٹرو" ؛ یہاں توثیق کی ضرورت نہیں ہے کیونکہ "اے ویلڈ" تعریف کے مطابق "اے ٹرو" کے برابر ہے۔ تعارف اور خاتمے کی شکلیں یہ ہیں: موڈل مفروضوں کا مفروضہ اصول اور متبادل تھیوریم کا اپنا ورژن ہوتا ہے۔ موڈل سبسٹیٹیوشن تھیوریم اگر ω ؛ ω: A سچ اور ω، u: (A درست) ؛ ω: C سچ، تو ω ؛ ω [π1/u] π2: C سچ۔ مفروضوں کے الگ الگ مجموعوں میں فیصلوں کو الگ کرنے کا یہ فریم ورک، جسے ملٹی زونڈ یا پولیڈیک سیاق و سباق بھی کہا جاتا ہے، بہت طاقتور اور قابل توسیع ہے۔ اس کا اطلاق بہت سے مختلف موڈل منطقوں کے لیے کیا گیا ہے، اور چند مثالیں دینے کے لیے لکیری اور دیگر ذیلی ساختی منطقوں کے لیے بھی۔ تاہم، موڈل منطق کے نسبتا کم نظاموں کو قدرتی کٹوتی میں براہ راست باقاعدہ بنایا جا سکتا ہے۔ ان نظاموں کی پروف تھیوریٹک خصوصیات دینے کے لیے، توسیع جیسے لیبلنگ یا گہرے تخمینے کے نظام۔ فارمولوں میں لیبلز کا اضافہ ان حالات پر بہت بہتر کنٹرول کی اجازت دیتا ہے جن کے تحت قواعد لاگو ہوتے ہیں، جس سے تجزیاتی جھانکیوں کی زیادہ لچکدار تکنیکوں کا اطلاق ہوتا ہے، جیسا کہ لیبل کٹوتی کے معاملے میں کیا گیا ہے۔ لیبلز کرپکے سیمنٹکس میں دنیاؤں کے ناموں کی بھی اجازت دیتے ہیں۔ ہائبرڈ منطق کی قدرتی کٹوتی کے رسمی شکل میں کرپکے سیمنٹکس میں موڈل لاجکس کے فریم کنڈیشنز کو انفریشن رولز میں تبدیل کرنے کے لیے ایک بااثر تکنیک پیش کرتے ہیں۔ بہت سے ثبوت کے نظریات کے اطلاق کا سروے کرتا ہے، جیسے کہ ایورن اور پوٹنگر کے ہائپرسیکوئنٹس اور بیلنیپ کی ڈسپلے منطق ایس 5 اور بی جیسے موڈل منطق کے لیے۔ دوسرے بنیادی طریقوں کے ساتھ موازنہ سیکوئنٹ کیلکولس سیکوئنٹ کیلکولس ریاضیاتی منطق کی بنیاد کے طور پر قدرتی کٹوتی کا بنیادی متبادل ہے۔ قدرتی کٹوتی میں معلومات کا بہاؤ دو طرفہ ہوتا ہے: خاتمے کے قواعد معلومات کو ڈی کنسٹرکشن کے ذریعے نیچے کی طرف بہاتے ہیں، اور تعارف کے قواعد اسمبلی کے ذریعے معلومات کو اوپر کی طرف بہاتے ہیں۔ اس طرح، قدرتی کٹوتی کے ثبوت میں خالص طور پر باٹم اپ یا ٹاپ ڈاؤن ریڈنگ نہیں ہوتی ہے، جس کی وجہ سے یہ ثبوت کی تلاش میں آٹومیشن کے لیے موزوں نہیں ہوتا ہے۔ اس حقیقت کو حل کرنے کے لیے، 1935 میں جینٹزن نے اپنے سیکوینٹ کیلکولس کی تجویز پیش کی، حالانکہ اس نے ابتدائی طور پر اسے پیش گوئی منطق کی مستقل مزاجی کو واضح کرنے کے لیے ایک تکنیکی آلہ کے طور پر ارادہ کیا تھا۔ کلین نے اپنی 1952 کی بنیادی کتاب انٹروڈکشن ٹو میٹامیتھمیٹکس میں جدید انداز میں ترتیب وار کیلکولس کی پہلی تشکیل دی۔ سیکوینٹ کیلکولس میں تمام انفریشن رولز میں خالصتا باٹم اپ ریڈنگ ہوتی ہے۔ تخمینہ کے قوانین ٹرن اسٹائل کے دونوں اطراف کے عناصر پر لاگو ہو سکتے ہیں۔ (قدرتی کٹوتی سے فرق کرنے کے لیے، یہ مضمون ترتیب کے لیے صحیح ٹاک کے بجائے ڈبل تیر کا استعمال کرتا ہے۔) قدرتی کٹوتی کے تعارف کے قوانین کو ترتیب وار حساب میں صحیح اصولوں کے طور پر دیکھا جاتا ہے، اور ساختی طور پر بہت ملتے جلتے ہیں۔ دوسری طرف ایلیمینیشن رولز سیکوینٹ کیلکولس میں لیفٹ رولز میں بدل جاتے ہیں۔ ایک مثال دینے کے لیے، اختلاط پر غور کریں ؛ دائیں قواعد واقف ہیں: بائیں طرف: مقامی شکل میں قدرتی کٹوتی کے اصول کو یاد کریں: تجویز اے۔ بی، جو کہ ای میں ایک بنیاد کا جانشین ہے، بائیں اصول ایل میں نتیجہ کے مفروضے میں بدل جاتا ہے۔ اس طرح، لیفٹ رولز کو ایک طرح کے الٹا خاتمے کے اصول کے طور پر دیکھا جا سکتا ہے۔ اس مشاہدے کو مندرجہ ذیل طور پر واضح کیا جا سکتا ہے: سیکوینٹ کیلکولس میں، بائیں اور دائیں قوانین کو لاک اسٹیپ میں انجام دیا جاتا ہے جب تک کہ کوئی ابتدائی سیکوینٹ تک نہ پہنچ جائے، جو قدرتی کٹوتی میں خاتمے اور تعارف کے اصولوں کے ملاپ کے مقام سے مطابقت رکھتا ہے۔ یہ ابتدائی اصول سطحی طور پر قدرتی کٹوتی کے مفروضے کے اصول سے ملتے جلتے ہیں، لیکن سیکوینٹ کیلکولس میں وہ بائیں اور دائیں تجویز کی منتقلی یا ہاتھ ملانے کو بیان کرتے ہیں: سیکوینٹ کیلکولس اور قدرتی کٹوتی کے درمیان خط و کتابت ساؤنڈنیس اور مکمل تھیوریمز کا ایک جوڑا ہے، جو دونوں ایک انڈکٹو دلیل کے ذریعے ثابت ہوتے ہیں۔ ڈبلیو آر ٹی کی ساؤنڈنیس۔ اگر γ-A، تو γ-A. کی مکملتا۔ اگر A، تو A۔ ان نظریات سے یہ واضح ہے کہ ترتیب وار حساب کتاب سچائی کے تصور کو تبدیل نہیں کرتا، کیونکہ تجاویز کا وہی مجموعہ درست رہتا ہے۔ اس طرح، کوئی بھی وہی پروف آبجیکٹ استعمال کر سکتا ہے جو پہلے سیکوینٹ کیلکولس مشتقات میں استعمال ہوتا تھا۔ مثال کے طور پر، امتزاج پر غور کریں۔ دائیں اصول عملی طور پر تعارف کے اصول سے ملتا جلتا ہے تاہم، بائیں اصول کچھ اضافی متبادل انجام دیتا ہے جو متعلقہ خاتمے کے قوانین میں انجام نہیں دیا جاتا ہے۔ اس لیے سیکوینٹ کیلکولس میں پیدا ہونے والے ثبوتوں کی اقسام قدرتی کٹوتی سے بالکل مختلف ہیں۔ سیکوینٹ کیلکولس ثبوت پیدا کرتا ہے جسے β-نارمل η-لانگ فارم کے نام سے جانا جاتا ہے، جو قدرتی کٹوتی ثبوت کی نارمل شکل کی کینونکل نمائندگی سے مطابقت رکھتا ہے۔ اگر کوئی قدرتی کٹوتی کا استعمال کرتے ہوئے ان ثبوتوں کو بیان کرنے کی کوشش کرتا ہے، تو وہ حاصل کرتا ہے جسے انٹرکلیشن کیلکولس کہا جاتا ہے (سب سے پہلے جان بیرنز نے بیان کیا تھا)، جسے قدرتی کٹوتی کے لیے عام شکل کے تصور کی باضابطہ وضاحت کے لیے استعمال کیا جا سکتا ہے۔ قدرتی کٹوتی کا متبادل تھیوریم ایک ساختی اصول یا ساختی تھیوریم کی شکل اختیار کرتا ہے جسے ترتیب وار کیلکولس میں کٹ کہا جاتا ہے۔ کٹ (متبادل) اگر जातک ν ν π1: A اور जातک، u: A ν π2: C، تو जातک ν [π1/u] π2: C۔ زیادہ تر اچھے برتاؤ والے منطق میں، کٹ ایک تخمینہ اصول کے طور پر غیر ضروری ہے، حالانکہ یہ میٹا تھیوریم کے طور پر ثابت ہوتا رہتا ہے۔ کٹ اصول کی ضرورت سے زیادہ کو عام طور پر ایک کمپیوٹیشنل عمل کے طور پر پیش کیا جاتا ہے، جسے کٹ ایلیمینیشن کہا جاتا ہے۔ قدرتی کٹوتی کے لیے اس کا ایک دلچسپ اطلاق ہے ؛ عام طور پر معاملات کی لامحدود تعداد کی وجہ سے قدرتی کٹوتی میں براہ راست کچھ خصوصیات کو ثابت کرنا انتہائی مشکل ہوتا ہے۔ مثال کے طور پر، یہ ظاہر کرنے پر غور کریں کہ دی گئی تجویز قدرتی کٹوتی میں قابل ثبوت نہیں ہے۔ ایک سادہ انڈکٹو دلیل اس وجہ سے ناکام ہو جاتی ہے کہ E یا E جیسے قواعد من مانی تجاویز پیش کر سکتے ہیں۔ تاہم، ہم جانتے ہیں کہ سیکوئنٹ کیلکولس قدرتی کٹوتی کے حوالے سے مکمل ہے، لہذا یہ سیکوئنٹ کیلکولس میں اس غیر تصدیق کو ظاہر کرنے کے لیے کافی ہے۔ اب، اگر کٹ ایک انفریشن رول کے طور پر دستیاب نہیں ہے، تو تمام سیکوئنٹ رولز یا تو دائیں یا بائیں طرف کنیکٹو متعارف کراتے ہیں، لہذا سیکوئنٹ مشتق کی گہرائی حتمی نتیجے میں کنیکٹو سے مکمل طور پر منسلک ہوتی ہے۔ اس طرح، غیر مصدقہ ظاہر کرنا بہت آسان ہے، کیونکہ غور کرنے کے لیے معاملات کی صرف ایک محدود تعداد موجود ہے، اور ہر معاملہ مکمل طور پر نتیجے کی ذیلی تجاویز پر مشتمل ہوتا ہے۔ اس کی ایک سادہ سی مثال عالمی مستقل مزاجی تھیوریم ہے: "سچ" قابل تصدیق نہیں ہے۔ سیکوینٹ کیلکولس ورژن میں، یہ واضح طور پر درست ہے کیونکہ ایسا کوئی قاعدہ نہیں ہے جس میں نتیجہ کے طور پر "ष्ण" ہو! پروف تھیوریسٹ اکثر اس طرح کی خصوصیات کی وجہ سے کٹ فری سیکوینٹ کیلکولس فارمولیشن پر کام کرنے کو ترجیح دیتے ہیں۔ نوٹ حوالہ جات (انگریزی ترجمہ ایم۔ ای۔ زابو میں منطقی کٹوتی کی تحقیقات) بھی دیکھیں۔ دی کلیکٹڈ ورکس آف گیرہارڈ جینٹزن۔ نارتھ ہالینڈ پبلشنگ کمپنی، 1969۔) ترجمہ اور پال ٹیلر اور یویس لافونٹ کے ضمیمہ کے ساتھ۔ پولینڈ کی منطق میں دوبارہ چھاپا گیا 1920-39، ایڈ۔ اسٹورس میک کال۔ اپریل 1983 میں یونیورسٹی ڈیگلی اسٹڈی دی سینا میں ایک مختصر کورس کے لیے لیکچر نوٹ۔ پی ایچ ڈی تھیسس۔ ایم ایس سی مقالہ۔ بیرونی روابط لیبوری، ڈینیل کلیمنٹ، "قدرتی کٹوتی کا تعارف"۔ ایسڈ پر ڈومینو۔ قدرتی کٹوتی ڈومینوز کے کھیل کے طور پر تصور کی گئی۔ پیلٹیئر، جیف، "قدرتی کٹوتی اور ابتدائی منطق کی نصابی کتابوں کی تاریخ"۔ لیوی، مشیل، ایک تجویز کردہ امثال۔ منطقی حساب کتاب تخفیف استدلال ثبوت نظریہ ثبوت کے طریقے