Natural deduction
লজিক এবং প্রুফ থিওরিতে, ন্যাচারাল ডিডাকশন হল এক ধরনের প্রুফ ক্যালকুলাস যেখানে লজিক্যাল রিজনিং অনুমানের নিয়ম দ্বারা প্রকাশ করা হয় যা "প্রাকৃতিক" যুক্তির পদ্ধতির সাথে ঘনিষ্ঠভাবে সম্পর্কিত। এটি হিলবার্ট-শৈলীর পদ্ধতির সাথে বৈপরীত্যপূর্ণ, যা পরিবর্তে অনুমানমূলক যুক্তির যৌক্তিক আইনগুলি প্রকাশ করতে যতটা সম্ভব স্বতঃসিদ্ধ ব্যবহার করে। অনুপ্রেরণা হিলবার্ট, ফ্রেজ এবং রাসেলের সিস্টেমে প্রচলিত অনুমানমূলক যুক্তির স্বতঃসিদ্ধকরণের সাথে অসন্তোষের প্রেক্ষাপটে প্রাকৃতিক অনুমানের জন্ম হয় (দেখুন, উদাহরণস্বরূপ, হিলবার্ট সিস্টেম)। রাসেল এবং হোয়াইটহেড তাদের গাণিতিক গ্রন্থ প্রিন্সিপিয়া ম্যাথমেটিকা-তে এই ধরনের স্বতঃসিদ্ধকরণগুলি সবচেয়ে বিখ্যাতভাবে ব্যবহার করেছিলেন। 1926 সালে পোল্যান্ডে লুকাসিভিচ দ্বারা একাধিক সেমিনারের দ্বারা অনুপ্রাণিত হয়ে, যা যুক্তির আরও প্রাকৃতিক চিকিত্সার পক্ষে ছিল, জাস্কোভস্কি আরও প্রাকৃতিক অনুমানকে সংজ্ঞায়িত করার প্রথম প্রচেষ্টা করেছিলেন, প্রথমে 1929 সালে একটি চিত্রগত স্বরলিপি ব্যবহার করে এবং পরে 1934 এবং 1935 সালে গবেষণাপত্রের ক্রম অনুসারে তাঁর প্রস্তাবটি আপডেট করেছিলেন। তাঁর প্রস্তাবগুলি ফিচ-শৈলীর ক্যালকুলাস (বা ফিচের রেখাচিত্র) বা সাপেসের পদ্ধতির মতো বিভিন্ন স্বরলিপির দিকে পরিচালিত করেছিল যার জন্য লেমন সিস্টেম এল নামে একটি বৈকল্পিক দিয়েছিলেন। 1933 সালে জার্মান গণিতবিদ গেরহার্ড জেন্টজেন তার আধুনিক আকারে ন্যাচারাল ডিডাকশন স্বাধীনভাবে প্রস্তাব করেছিলেন, গটিঙেন বিশ্ববিদ্যালয়ের গাণিতিক বিজ্ঞান অনুষদের কাছে বিতরণ করা একটি গবেষণাপত্রে। ন্যাচারাল ডিডাকশন শব্দটি (বা এর জার্মান সমতুল্য ন্যাচারলিচেস শ্লেইসেন) সেই গবেষণাপত্রে তৈরি করা হয়েছিলঃ জেন্টজেন সংখ্যা তত্ত্বের সামঞ্জস্য প্রতিষ্ঠার আকাঙ্ক্ষা দ্বারা অনুপ্রাণিত হয়েছিল। তিনি ধারাবাহিকতার ফলাফলের জন্য প্রয়োজনীয় প্রধান ফলাফল, কাট এলিমিনেশন উপপাদ্য-হাউপটস্যাটজ-সরাসরি প্রাকৃতিক ডিডাকশনের জন্য প্রমাণ করতে পারেননি। এই কারণে তিনি তাঁর বিকল্প পদ্ধতি, ক্রমিক ক্যালকুলাস প্রবর্তন করেছিলেন, যার জন্য তিনি শাস্ত্রীয় এবং স্বজ্ঞাত যুক্তি উভয়ের জন্যই হাপ্সাতজকে প্রমাণ করেছিলেন। 1961 এবং 1962 সালে ধারাবাহিক সেমিনারে প্রাউইৎজ প্রাকৃতিক ডিডাকশন ক্যালকুলির একটি বিস্তৃত সারসংক্ষেপ দিয়েছিলেন এবং জেন্টজেনের ক্রমানুসারে ক্যালকুলির সাথে বেশিরভাগ কাজ প্রাকৃতিক ডিডাকশন কাঠামোর মধ্যে পরিবহন করেছিলেন। তাঁর 1965 সালের মনোগ্রাফ ন্যাচারাল ডিডাকশনঃ এ প্রুফ-থিওরিটিক্যাল স্টাডি ছিল ন্যাচারাল ডিডাকশনের উপর একটি রেফারেন্স কাজ, এবং মোডাল এবং সেকেন্ড অর্ডার লজিকের জন্য অ্যাপ্লিকেশন অন্তর্ভুক্ত করা হয়েছিল। প্রাকৃতিক ছাড়ের ক্ষেত্রে, অনুমানের নিয়মগুলি বারবার প্রয়োগ করে প্রাঙ্গণের সংগ্রহ থেকে একটি প্রস্তাব অনুমান করা হয়। এই নিবন্ধে উপস্থাপিত পদ্ধতিটি জেন্টজেন বা প্রাউইৎজের গঠনের একটি সামান্য বৈচিত্র্য, তবে মার্টিন-লোফের যৌক্তিক রায় এবং সংযোগগুলির বর্ণনার সাথে ঘনিষ্ঠভাবে মেনে চলা। বিচার ও প্রস্তাবনা একটি বিচার এমন কিছু যা জানা যায়, অর্থাৎ জ্ঞানের একটি বস্তু। যদি কেউ প্রকৃতপক্ষে এটি জানেন তবে এটি স্পষ্ট। সুতরাং "বৃষ্টি হচ্ছে" একটি রায়, যা যে জানে যে আসলে বৃষ্টি হচ্ছে তার পক্ষে স্পষ্ট; এই ক্ষেত্রে কেউ জানালার বাইরে তাকিয়ে বা বাড়ির বাইরে বেরিয়ে এসে সহজেই রায়ের প্রমাণ খুঁজে পেতে পারে। তবে গাণিতিক যুক্তিতে, প্রমাণ প্রায়শই সরাসরি পর্যবেক্ষণযোগ্য হয় না, বরং আরও মৌলিক স্পষ্ট রায় থেকে অনুমান করা হয়। ডিডাকশন প্রক্রিয়া হল যা একটি প্রমাণ গঠন করে; অন্য কথায়, একটি রায় স্পষ্ট হয় যদি একজনের কাছে এর প্রমাণ থাকে। যুক্তির ক্ষেত্রে সবচেয়ে গুরুত্বপূর্ণ বিচারগুলি হল "এ সত্য"। এ অক্ষরটি কোনও প্রস্তাবের প্রতিনিধিত্বকারী যে কোনও অভিব্যক্তি বোঝায়; সত্য বিচারের জন্য আরও আদিম বিচারের প্রয়োজনঃ "এ একটি প্রস্তাব"। অন্যান্য অনেক বিচার অধ্যয়ন করা হয়েছে; উদাহরণস্বরূপ, "এ মিথ্যা" (শাস্ত্রীয় যুক্তি দেখুন), "এ সময় টি-তে সত্য" (সাময়িক যুক্তি দেখুন), "এ অপরিহার্যভাবে সত্য" বা "এ সম্ভবত সত্য" (মডেল যুক্তি দেখুন), "এম প্রোগ্রামের টাইপ τ" (প্রোগ্রামিং ভাষা এবং টাইপ তত্ত্ব দেখুন), "এ উপলব্ধ সংস্থানগুলি থেকে অর্জনযোগ্য" (রৈখিক যুক্তি দেখুন), এবং আরও অনেক কিছু। প্রথমত, আমরা সহজতম দুটি রায় নিয়ে চিন্তা করব "এ হল একটি প্রস্তাব" এবং "এ হল সত্য", যা যথাক্রমে "এ প্রপ" এবং "এ ট্রু" হিসাবে সংক্ষিপ্ত। "এ প্রপ" রায়টি এ-এর বৈধ প্রমাণের কাঠামোকে সংজ্ঞায়িত করে, যা পরিবর্তে প্রস্তাবের কাঠামোকে সংজ্ঞায়িত করে। এই কারণে, এই রায়ের জন্য অনুমানের নিয়মগুলি কখনও কখনও গঠন নিয়ম হিসাবে পরিচিত হয়। উদাহরণস্বরূপ, যদি আমাদের দুটি প্রস্তাবনা এ এবং বি থাকে (অর্থাৎ, "এ প্রপ" এবং "বি প্রপ" রায়গুলি স্পষ্ট), তবে আমরা যৌগিক প্রস্তাবনা এ এবং বি গঠন করি, যা প্রতীকীভাবে "হিসাবে লেখা হয়। আমরা এটি একটি অনুমানের নিয়মের আকারে লিখতে পারিঃ যেখানে অনুমানের নিয়মটিকে আরও সংক্ষিপ্ত করার জন্য বন্ধনীগুলি বাদ দেওয়া হয়ঃ এই অনুমানের নিয়মটি পরিকল্পিতঃ এ এবং বি-কে যে কোনও অভিব্যক্তি দিয়ে তাত্ক্ষণিক করা যেতে পারে। একটি অনুমানের নিয়মের সাধারণ রূপটি হলঃ যেখানে প্রতিটি একটি রায় এবং অনুমানের নিয়মটিকে "নাম" বলা হয়। রেখার উপরের রায়গুলি প্রাঙ্গণ হিসাবে পরিচিত এবং রেখার নীচের রায়গুলি উপসংহার হিসাবে পরিচিত। অন্যান্য সাধারণ যৌক্তিক প্রস্তাবগুলি হল ডিসজাংশন (), নেগেশন (), ইম্প্লিকেশন (), এবং যৌক্তিক ধ্রুবক সত্য () এবং মিথ্যা ()। তাদের গঠনের নিয়মগুলি নীচে দেওয়া হল। ভূমিকা এবং অপসারণ এখন আমরা "একটি সত্য" রায় নিয়ে আলোচনা করি। উপসংহারের যে নিয়মগুলি উপসংহারের মধ্যে একটি যৌক্তিক সংযোগের প্রবর্তন করে সেগুলি ভূমিকা নিয়ম হিসাবে পরিচিত। সংমিশ্রণগুলি প্রবর্তন করতে, অর্থাৎ, এ এবং বি প্রস্তাবের জন্য "এ এবং বি সত্য" উপসংহারে আসার জন্য, "এ সত্য" এবং "বি সত্য"-এর প্রমাণ প্রয়োজন। একটি অনুমানের নিয়ম হিসাবেঃ এটি অবশ্যই বুঝতে হবে যে এই ধরনের নিয়মগুলিতে বস্তুগুলি প্রস্তাবনা। অর্থাৎ, উপরের নিয়মটি আসলে একটি সংক্ষিপ্ত রূপঃ এটিও লেখা যেতে পারেঃ এই রূপে, প্রথম ভিত্তিটি গঠন নিয়ম দ্বারা সন্তুষ্ট করা যেতে পারে, যা পূর্ববর্তী ফর্মের প্রথম দুটি প্রাঙ্গণ দেয়। এই প্রবন্ধে আমরা "প্রোপ" বিচারগুলি যেখানে বোঝা যায় সেখানে তুলে ধরব। শূন্য ক্ষেত্রে, কোনও ভিত্তি থেকে সত্য পাওয়া যায় না। যদি কোনও প্রস্তাবের সত্যতা একাধিক উপায়ে প্রতিষ্ঠিত করা যায়, তবে সংশ্লিষ্ট সংযোগকারীর একাধিক ভূমিকা নিয়ম রয়েছে। লক্ষ্য করুন যে নালারি ক্ষেত্রে, অর্থাৎ, মিথ্যার জন্য, কোনও ভূমিকা নিয়ম নেই। সুতরাং সহজ বিচার থেকে কেউ কখনও মিথ্যা অনুমান করতে পারে না। প্রবর্তনের নিয়মগুলির দ্বৈত হ 'ল একটি যৌগিক প্রস্তাব সম্পর্কে তথ্যকে তার উপাদানগুলি সম্পর্কে তথ্যের মধ্যে কীভাবে পুনর্নির্মাণ করা যায় তা বর্ণনা করার জন্য অপসারণের নিয়ম। সুতরাং, "এ বি সত্য" থেকে আমরা "এ সত্য" এবং "বি সত্য" উপসংহারে আসতে পারিঃ অনুমানের নিয়মের ব্যবহারের উদাহরণ হিসাবে, সংযোগের বিনিময়শীলতা বিবেচনা করুন। যদি এ বি সত্য হয়, তবে বি এ সত্য; এই ব্যুৎপত্তিটি এমনভাবে অনুমানের নিয়মগুলি রচনা করে আঁকা যেতে পারে যে একটি নিম্ন অনুমানের প্রাঙ্গণ পরবর্তী উচ্চতর অনুমানের উপসংহারের সাথে মেলে। আমরা এখন পর্যন্ত যে অনুমানের পরিসংখ্যান দেখেছি তা ইমপ্লিকেশন ভূমিকা বা বিচ্ছিন্নতা নির্মূলের নিয়মগুলি বর্ণনা করার জন্য যথেষ্ট নয়; এগুলির জন্য, আমাদের অনুমানমূলক ব্যুৎপত্তি সম্পর্কে আরও সাধারণ ধারণা প্রয়োজন। অনুমানমূলক ব্যুৎপত্তি গাণিতিক যুক্তিতে একটি বিস্তৃত ক্রিয়া হল অনুমান থেকে যুক্তি করা। উদাহরণস্বরূপ, নিম্নলিখিত ব্যুৎপত্তিটি বিবেচনা করুনঃ এই ব্যুৎপত্তিটি বি-এর সত্যকে প্রতিষ্ঠিত করে না; বরং, এটি নিম্নলিখিত সত্যটি প্রতিষ্ঠিত করেঃ যদি এ-ওয়াং (বি-ওয়াং-সি) সত্য হয় তবে বি সত্য। যুক্তিতে, একজন বলে "ধরে নেওয়া যায় যে এ. ওয়াই. (বি. ওয়াই. সি) সত্য, আমরা দেখাই যে বি সত্য"; অন্য কথায়, "বি সত্য" রায়টি "এ. ওয়াই. (বি. ওয়াই. সি) সত্য" অনুমিত রায়ের উপর নির্ভর করে। এটি একটি অনুমানমূলক ব্যুৎপত্তি, যা আমরা নিম্নরূপ লিখিঃ ব্যাখ্যাটি হ 'লঃ "বি সত্য সত্য থেকে উদ্ভূত"। অবশ্যই, এই নির্দিষ্ট উদাহরণে আমরা আসলে "বি সত্য" থেকে "এ ওয়াই (বি ওয়াই সি) সত্য" এর উৎপত্তি জানি, তবে সাধারণভাবে আমরা হয়তো পূর্বনির্ধারণটি জানি না। একটি অনুমানমূলক ব্যুৎপত্তির সাধারণ রূপটি হলঃ প্রতিটি অনুমানমূলক ব্যুৎপত্তির উপরের লাইনে পূর্ববর্তী ব্যুৎপত্তির (ডি) একটি সংগ্রহ রয়েছে এবং নীচের লাইনে একটি সফল রায় (জে) লেখা থাকে। প্রতিটি প্রাঙ্গণ নিজেই একটি অনুমানমূলক উৎপত্তি হতে পারে। (সরলতার জন্য, আমরা একটি রায়কে ভিত্তিহীন ব্যুৎপত্তি হিসাবে বিবেচনা করি।) অনুমানমূলক বিচারের ধারণাটি নিহিতার্থের সংযোগকারী হিসাবে অভ্যন্তরীণ করা হয়। ভূমিকা এবং অপসারণের নিয়মগুলি নিম্নরূপ। ভূমিকা নিয়মে, ইউ নামক পূর্বসূরী উপসংহারে মুক্তি পায়। এটি অনুমানের পরিধি সীমাবদ্ধ করার একটি প্রক্রিয়াঃ এর অস্তিত্বের একমাত্র কারণ হল "বি সত্য" প্রতিষ্ঠা করা; এটি অন্য কোনও উদ্দেশ্যে ব্যবহার করা যাবে না এবং বিশেষত, এটি ভূমিকার নীচে ব্যবহার করা যাবে না। উদাহরণস্বরূপ, "A′ (B′ (A′B))-এর উৎপত্তি সত্য" বিবেচনা করুনঃ এই সম্পূর্ণ ব্যুৎপত্তিটির কোনও অসন্তুষ্ট ভিত্তি নেই; তবে, উপ-ব্যুৎপত্তিগুলি অনুমানমূলক। উদাহরণস্বরূপ, "বি টু (এ টু বি) ট্রু"-এর উৎপত্তি পূর্ববর্তী "এ ট্রু" (ইউ নামে) সহ অনুমানমূলক। অনুমানমূলক ব্যুৎপত্তিগুলির সাথে, আমরা এখন বিচ্ছিন্নতার জন্য নির্মূলের নিয়মটি লিখতে পারিঃ শব্দের মধ্যে, যদি এ বি সত্য হয়, এবং আমরা "এ সত্য" এবং "বি সত্য" উভয় থেকে "সি সত্য" অর্জন করতে পারি, তবে সি প্রকৃতপক্ষে সত্য। মনে রাখবেন যে এই নিয়মটি "এ ট্রু" বা "বি ট্রু"-এর প্রতি প্রতিশ্রুতিবদ্ধ নয়। শূন্য-এরি ক্ষেত্রে, অর্থাৎ। মিথ্যার জন্য, আমরা নিম্নলিখিত নির্মূলের নিয়মটি পাইঃ এটি এইভাবে পড়া হয়ঃ যদি মিথ্যা সত্য হয়, তবে যে কোনও প্রস্তাব 'সি' সত্য। নেতিবাচকতা প্রভাবের অনুরূপ। ভূমিকা নিয়মটি অনুমানের নাম u, এবং সফল p, অর্থাৎ, প্রস্তাবনা p অবশ্যই উপসংহার এ-তে ঘটবে না। যেহেতু এই নিয়মগুলি পরিকল্পিত, তাই ভূমিকা নিয়মের ব্যাখ্যাটি হ 'লঃ যদি "এ সত্য" থেকে আমরা প্রতিটি প্রস্তাবের জন্য "পি সত্য" পেতে পারি, তবে এ অবশ্যই মিথ্যা হতে হবে, অর্থাৎ "এ সত্য নয়"। অপসারণের জন্য, যদি এ এবং এ নয় উভয়ই সত্য বলে দেখানো হয়, তবে একটি দ্বন্দ্ব রয়েছে, এই ক্ষেত্রে প্রতিটি প্রস্তাব সি সত্য। যেহেতু ইম্প্লিকেশন এবং নেগেটিভের নিয়মগুলি এতটাই একই রকম, তাই এটি দেখতে মোটামুটি সহজ হওয়া উচিত যে এ এবং এ সমতুল্য নয়, অর্থাৎ, প্রতিটি একে অপরের থেকে উদ্ভূত। সামঞ্জস্য, সম্পূর্ণতা এবং স্বাভাবিক রূপ একটি তত্ত্বকে সামঞ্জস্যপূর্ণ বলা হয় যদি মিথ্যা প্রমাণযোগ্য না হয় (কোনও অনুমান থেকে) এবং সম্পূর্ণ হয় যদি প্রতিটি উপপাদ্য বা এর নেতিবাচকতা যুক্তির অনুমান নিয়ম ব্যবহার করে প্রমাণযোগ্য হয়। এগুলি সম্পূর্ণ যুক্তি সম্পর্কে বিবৃতি এবং সাধারণত একটি মডেলের কিছু ধারণার সাথে আবদ্ধ থাকে। যাইহোক, ধারাবাহিকতা এবং সম্পূর্ণতার স্থানীয় ধারণাগুলি রয়েছে যা সম্পূর্ণরূপে অনুমানের নিয়মগুলির উপর বাক্যবিন্যাসগত পরীক্ষা এবং মডেলগুলির কাছে কোনও আবেদনের প্রয়োজন হয় না। এর মধ্যে প্রথমটি হল স্থানীয় সামঞ্জস্য, যা স্থানীয় হ্রাসযোগ্যতা নামেও পরিচিত, যা বলে যে কোনও সংযোগকারীর প্রবর্তন সহ যে কোনও ব্যুৎপত্তি যা অবিলম্বে তার অপসারণের পরে এই ঘোরাঘুরি ছাড়াই সমতুল্য ব্যুৎপত্তি রূপান্তরিত হতে পারে। এটি নির্মূলের নিয়মগুলির শক্তির উপর একটি নজরদারিঃ এগুলি এতটা শক্তিশালী হওয়া উচিত নয় যে এগুলিতে এমন জ্ঞান অন্তর্ভুক্ত থাকে যা ইতিমধ্যে তাদের প্রাঙ্গনে অন্তর্ভুক্ত ছিল না। উদাহরণস্বরূপ, সংযোগগুলি বিবেচনা করুন। দ্বৈতভাবে, স্থানীয় সম্পূর্ণতা বলে যে অপসারণের নিয়মগুলি একটি সংযোগকারীকে তার প্রবর্তন নিয়মের জন্য উপযুক্ত ফর্মগুলিতে বিভক্ত করার জন্য যথেষ্ট শক্তিশালী। আবার সংযোগের ক্ষেত্রেঃ এই ধারণাগুলি কারি-হাওয়ার্ড সমরূপতা ব্যবহার করে ল্যাম্বডা ক্যালকুলাসে β-হ্রাস (বিটা হ্রাস) এবং η-রূপান্তর (ইটা রূপান্তর) এর সাথে ঠিক মিলে যায়। স্থানীয় সম্পূর্ণতা দ্বারা, আমরা দেখতে পাই যে প্রতিটি ব্যুৎপত্তি একটি সমতুল্য ব্যুৎপত্তি রূপান্তরিত করা যেতে পারে যেখানে প্রধান সংযোগকারী চালু করা হয়। প্রকৃতপক্ষে, যদি পুরো ব্যুৎপত্তিটি অপসারণের এই ক্রম অনুসরণ করে প্রবর্তন অনুসরণ করে, তবে এটি স্বাভাবিক বলে মনে করা হয়। একটি স্বাভাবিক ব্যুৎপত্তির মধ্যে সমস্ত অপসারণ পরিচয়ের উপরে ঘটে। বেশিরভাগ যুক্তিতে, প্রতিটি ব্যুৎপত্তি একটি সমতুল্য স্বাভাবিক ব্যুৎপত্তি রয়েছে, যাকে স্বাভাবিক রূপ বলা হয়। সাধারণ রূপগুলির অস্তিত্ব সাধারণত শুধুমাত্র প্রাকৃতিক অনুমান ব্যবহার করে প্রমাণ করা কঠিন, যদিও এই ধরনের বিবরণ সাহিত্যে বিদ্যমান, বিশেষ করে 1961 সালে ডাগ প্রাউইৎজ দ্বারা। কাট-ফ্রি সিকোয়েন্ট ক্যালকুলাস উপস্থাপনার মাধ্যমে পরোক্ষভাবে এটি দেখানো অনেক সহজ। প্রথম এবং উচ্চতর ক্রমের সম্প্রসারণ পূর্ববর্তী বিভাগের যুক্তি একটি একক-সাজানো যুক্তির উদাহরণ, অর্থাৎ, একটি একক ধরনের বস্তু সহ একটি যুক্তিঃ প্রস্তাবনা। এই সহজ কাঠামোর অনেক সম্প্রসারণের প্রস্তাব দেওয়া হয়েছে; এই বিভাগে আমরা এটিকে দ্বিতীয় ধরণের ব্যক্তি বা শর্তাবলীর সাথে প্রসারিত করব। আরও সুনির্দিষ্টভাবে, আমরা একটি নতুন ধরনের রায় যোগ করব, "টি একটি শব্দ" (বা "টি শব্দ") যেখানে টি পরিকল্পিত। আমরা ভেরিয়েবলের একটি গণনাযোগ্য সেট V, ফাংশন প্রতীকগুলির আরেকটি গণনাযোগ্য সেট F স্থির করব এবং নিম্নলিখিত গঠন নিয়মগুলির সাথে পদগুলি তৈরি করবঃ এবং প্রস্তাবগুলির জন্য, আমরা ভবিষ্যদ্বাণীগুলির একটি তৃতীয় গণনাযোগ্য সেট P বিবেচনা করি এবং নিম্নলিখিত গঠন নিয়মের সাথে পদগুলির উপর পারমাণবিক ভবিষ্যদ্বাণীগুলি সংজ্ঞায়িত করিঃ গঠনের প্রথম দুটি নিয়ম এমন একটি শব্দের সংজ্ঞা প্রদান করে যা কার্যকরভাবে বীজগণিত এবং মডেল তত্ত্বের সংজ্ঞায়িত শব্দের মতোই, যদিও অধ্যয়নের সেই ক্ষেত্রগুলির ফোকাস প্রাকৃতিক অনুমান থেকে বেশ আলাদা। গঠনের তৃতীয় নিয়মটি কার্যকরভাবে একটি পারমাণবিক সূত্রকে সংজ্ঞায়িত করে, যেমন প্রথম-ক্রম যুক্তিতে এবং আবার মডেল তত্ত্বে। এগুলির সাথে এক জোড়া গঠন নিয়ম যুক্ত করা হয়েছে, যা পরিমাণগত প্রস্তাবের জন্য স্বরলিপি সংজ্ঞায়িত করে; সর্বজনীন (আ.) এবং অস্তিত্বগত (আ.) পরিমাণের জন্য একটিঃ সর্বজনীন পরিমাণকের ভূমিকা এবং নির্মূলের নিয়ম রয়েছেঃ অস্তিত্বগত পরিমাণকের ভূমিকা এবং নির্মূলের নিয়ম রয়েছেঃ এই নিয়মগুলিতে, স্বরলিপি [টি/এক্স] এ ক্যাপচার এড়াতে এ-তে এক্স-এর প্রতিটি (দৃশ্যমান) দৃষ্টান্তের জন্য টি-এর প্রতিস্থাপনকে বোঝায়। আগের মতোই নামের উপরের লিপিগুলি যে উপাদানগুলি নির্গত হয় সেগুলির জন্য দাঁড়ায়ঃ a শব্দটি I-এর উপসংহারে আসতে পারে না (এই ধরনের পদগুলি আইগেনভ্যারিয়েবল বা প্যারামিটার হিসাবে পরিচিত), এবং HE-তে u এবং v নামক অনুমানগুলি একটি অনুমানমূলক ব্যুৎপত্তির দ্বিতীয় ভিত্তির সাথে স্থানীয়করণ করা হয়। যদিও পূর্ববর্তী বিভাগগুলির প্রস্তাবমূলক যুক্তি নির্ণায়ক ছিল, তবে পরিমাপকারী যুক্ত করা যুক্তিটিকে অনিশ্চিত করে তোলে। এখন পর্যন্ত, পরিমাপ করা এক্সটেনশনগুলি প্রথম ক্রমেরঃ তারা প্রস্তাবগুলিকে পরিমাপ করা বস্তুর প্রকার থেকে আলাদা করে। উচ্চ-ক্রম যুক্তি একটি ভিন্ন পদ্ধতি গ্রহণ করে এবং শুধুমাত্র একটি একক ধরনের প্রস্তাবনা রয়েছে। কোয়ান্টিফায়ারের ক্ষেত্র হিসাবে কোয়ান্টিফিকেশনের ক্ষেত্রে একই ধরনের প্রস্তাব রয়েছে, যা গঠনের নিয়মগুলিতে প্রতিফলিত হয়ঃ উচ্চতর-ক্রম যুক্তির জন্য ভূমিকা এবং অপসারণ ফর্মগুলির আলোচনা এই নিবন্ধের আওতার বাইরে। ফার্স্ট-অর্ডার এবং হায়ার-অর্ডার লজিক্সের মধ্যে থাকা সম্ভব। উদাহরণস্বরূপ, দ্বিতীয়-ক্রম যুক্তিতে দুই ধরনের প্রস্তাব রয়েছে, এক ধরনের শব্দের পরিমাণ নির্ধারণ এবং দ্বিতীয় ধরনের প্রথম ধরনের প্রস্তাবের পরিমাণ নির্ধারণ। প্রাকৃতিক অনুমানের বিভিন্ন উপস্থাপনা বৃক্ষের মতো উপস্থাপনা অনুমানমূলক রায়গুলিকে অভ্যন্তরীণ করতে ব্যবহৃত জেন্টজেনের ডিসচার্জিং অ্যানোটেশনগুলি একটি সত্য বিচারের গাছের পরিবর্তে অনুক্রমের গাছ হিসাবে প্রমাণ উপস্থাপন করে এড়ানো যেতে পারে। ক্রমবর্ধমান উপস্থাপনা যাশকোভস্কির প্রাকৃতিক অনুমানের উপস্থাপনা ফিচ-স্টাইল ক্যালকুলাস (বা ফিচের রেখাচিত্র) বা সাপেসের পদ্ধতির মতো বিভিন্ন স্বরলিপির দিকে পরিচালিত করে, যার মধ্যে লেমন সিস্টেম এল নামে একটি বৈকল্পিক দিয়েছেন। এই ধরনের উপস্থাপনা ব্যবস্থা, যা আরও সঠিকভাবে ট্যাবুলার হিসাবে বর্ণনা করা হয়, নিম্নলিখিতগুলি অন্তর্ভুক্ত করে। 1940: একটি পাঠ্যপুস্তকে, কুইন বর্গাকার বন্ধনীতে লাইন নম্বর দ্বারা পূর্ববর্তী নির্ভরশীলতার ইঙ্গিত দিয়েছিলেন, সাপেসের 1957 লাইন-নম্বর স্বরলিপির পূর্বাভাস দিয়েছিলেন। 1950: একটি পাঠ্যপুস্তকে, নির্ভরতা নির্দেশ করার জন্য প্রমাণের প্রতিটি লাইনের বাম দিকে এক বা একাধিক তারকাচিহ্ন ব্যবহার করার একটি পদ্ধতি প্রদর্শন করা হয়েছে। এটি ক্লেইনের উল্লম্ব বারের সমতুল্য। (এটি সম্পূর্ণরূপে স্পষ্ট নয় যে কুইনের তারকাচিহ্নটি 1950 সালের মূল সংস্করণে প্রকাশিত হয়েছিল নাকি পরবর্তী সংস্করণে যোগ করা হয়েছিল।) 1957: একটি পাঠ্যপুস্তকে প্রমাণিত ব্যবহারিক যুক্তি উপপাদ্যের একটি ভূমিকা। এটি নির্ভরশীলতাকে নির্দেশ করে (অর্থাৎ। পূর্ববর্তী প্রস্তাবনা) প্রতিটি লাইনের বাম দিকে লাইন নম্বর দ্বারা। 1963: প্রাকৃতিক ডিডাকশন অনুমান নিয়মের উপর ভিত্তি করে ক্রমিক যৌক্তিক আর্গুমেন্টের লাইনের পূর্ববর্তী নির্ভরতা নির্দেশ করতে লাইন নম্বরের সেট ব্যবহার করে। 1965: সম্পূর্ণ পাঠ্যপুস্তকটি সাপেসের উপর ভিত্তি করে একটি পদ্ধতি ব্যবহার করে যুক্তি প্রমাণের একটি ভূমিকা। 1967: একটি পাঠ্যপুস্তকে সংক্ষেপে দুই ধরনের ব্যবহারিক যুক্তির প্রমাণ প্রদর্শন করা হয়েছে, একটি পদ্ধতি প্রতিটি লাইনের বাম দিকে পূর্ববর্তী প্রস্তাবগুলির স্পষ্ট উদ্ধৃতি ব্যবহার করে, অন্য পদ্ধতিটি নির্ভরশীলতা নির্দেশ করার জন্য বাম দিকে উল্লম্ব বার-লাইন ব্যবহার করে। প্রমাণ এবং প্রকার তত্ত্ব এখন পর্যন্ত প্রাকৃতিক অনুমানের উপস্থাপনা কোনও প্রমাণের আনুষ্ঠানিক সংজ্ঞা না দিয়ে প্রস্তাবের প্রকৃতির উপর মনোনিবেশ করেছে। প্রমাণের ধারণাকে আনুষ্ঠানিক করার জন্য, আমরা অনুমানমূলক ব্যুৎপত্তিগুলির উপস্থাপনাকে সামান্য পরিবর্তন করি। আমরা পূর্ববর্তীগুলিকে প্রুফ ভেরিয়েবল (ভেরিয়েবলের কিছু গণনাযোগ্য সেট ভি থেকে) দিয়ে লেবেল করি এবং প্রকৃত প্রুফ দিয়ে পরবর্তীটিকে সাজাই। পূর্ববর্তী বা অনুমানগুলি একটি টার্নস্টাইলের () মাধ্যমে পরবর্তী থেকে পৃথক করা হয়। এই পরিবর্তন কখনও কখনও স্থানীয় অনুমানের নামে হয়। নিম্নলিখিত চিত্রটি পরিবর্তনের সংক্ষিপ্তসার তুলে ধরেছে। যখন তাদের সঠিক গঠন প্রাসঙ্গিক না হয় তখন অনুমানের সংগ্রহকে জাত হিসাবে লেখা হবে। প্রমাণগুলি স্পষ্ট করার জন্য, আমরা প্রমাণহীন রায় "একটি সত্য" থেকে একটি রায়ে চলে যাইঃ "π হল (একটি সত্য) এর প্রমাণ", যা প্রতীকীভাবে "π: একটি সত্য" হিসাবে লেখা হয়। আদর্শ পদ্ধতি অনুসরণ করে, "π প্রমাণ" রায়ের জন্য প্রমাণগুলি তাদের নিজস্ব গঠনের নিয়মের সাথে নির্দিষ্ট করা হয়। সবচেয়ে সহজ সম্ভাব্য প্রমাণ হল একটি লেবেলযুক্ত অনুমানের ব্যবহার; এই ক্ষেত্রে প্রমাণ হল লেবেল নিজেই। সংক্ষিপ্ততার জন্য, আমরা এই নিবন্ধের বাকি অংশে বিচারমূলক লেবেলটি সত্য রেখে দেব, অর্থাৎ, "এঃ এ" লিখুন। আসুন স্পষ্ট প্রমাণ সহ কিছু সংযোগ পুনরায় পরীক্ষা করা যাক। সংযোগের জন্য, আমরা সংযোগের প্রমাণের রূপ আবিষ্কার করতে ভূমিকা নিয়মের দিকে তাকাইঃ সেগুলি অবশ্যই দুটি সংযোগের প্রমাণের একটি জোড়া হতে হবে। এইভাবেঃ অপসারণের নিয়ম ই1 এবং ই2 বাম বা ডান সংযোগস্থল নির্বাচন করে; এইভাবে প্রমাণগুলি হল অনুমানের একটি জোড়া-প্রথম (এফএসটি) এবং দ্বিতীয় (এসএনডি)। ইঙ্গিতের জন্য, ভূমিকা ফর্মটি একটি λ ব্যবহার করে লেখা অনুমানকে স্থানীয়করণ বা আবদ্ধ করে; এটি ডিসচার্জড লেবেলের সাথে মিলে যায়। নিয়মে, "γ, u: A" মানে হল অতিরিক্ত অনুমান u-এর সাথে একত্রে অনুমানের সংগ্রহ। স্পষ্টভাবে উপলব্ধ প্রমাণ সহ, কেউ প্রমাণ সম্পর্কে কারসাজি করতে এবং যুক্তি দিতে পারে। প্রমাণের মূল ক্রিয়াটি হল অন্য প্রমাণের জন্য ব্যবহৃত একটি অনুমানের জন্য একটি প্রমাণের প্রতিস্থাপন। এটি সাধারণত একটি প্রতিস্থাপন উপপাদ্য হিসাবে পরিচিত, এবং দ্বিতীয় রায়ের গভীরতার (বা কাঠামো) উপর আনয়ন দ্বারা প্রমাণিত হতে পারে। প্রতিস্থাপনের উপপাদ্য যদি A এবং γ, u: A′ π2: B, তাহলে γ′ [π1/u] π2: B। এখনও পর্যন্ত রায় "এ"-এর সম্পূর্ণ যৌক্তিক ব্যাখ্যা রয়েছে। টাইপ তত্ত্বে, বস্তুর আরও গণনামূলক দৃষ্টিভঙ্গির জন্য যৌক্তিক দৃষ্টিভঙ্গি বিনিময় করা হয়। যৌক্তিক ব্যাখ্যার প্রস্তাবগুলিকে এখন প্রকার হিসাবে দেখা হয়, এবং প্রমাণগুলিকে ল্যাম্বডা ক্যালকুলাসের প্রোগ্রাম হিসাবে দেখা হয়। সুতরাং "π: A"-এর ব্যাখ্যা হল "প্রোগ্রামের টাইপ A রয়েছে"। যৌক্তিক সংযোগগুলিকেও একটি ভিন্ন পাঠ দেওয়া হয়ঃ সংযোগকে গুণফল (×) হিসাবে দেখা হয়, প্রভাবকে ফাংশন তীর (→) হিসাবে দেখা হয় ইত্যাদি। তবে পার্থক্যগুলি কেবল প্রসাধনী। গঠন, ভূমিকা এবং অপসারণের নিয়মের পরিপ্রেক্ষিতে টাইপ তত্ত্বের একটি স্বাভাবিক অনুমান উপস্থাপনা রয়েছে; প্রকৃতপক্ষে, পাঠক সহজেই পূর্ববর্তী বিভাগগুলি থেকে সরল টাইপ তত্ত্ব হিসাবে পরিচিত পুনর্গঠন করতে পারেন। যুক্তি এবং প্রকার তত্ত্বের মধ্যে পার্থক্য প্রাথমিকভাবে প্রকার (প্রস্তাব) থেকে প্রোগ্রাম (প্রমাণ)-এ ফোকাসের স্থানান্তর। টাইপ তত্ত্ব মূলত প্রোগ্রামগুলির রূপান্তরযোগ্যতা বা হ্রাসযোগ্যতা সম্পর্কে আগ্রহী। প্রতিটি প্রকারের জন্য, সেই ধরনের ক্যানোনিকাল প্রোগ্রাম রয়েছে যা অপরিবর্তনীয়; এগুলি ক্যানোনিকাল ফর্ম বা মান হিসাবে পরিচিত। যদি প্রতিটি প্রোগ্রামকে ক্যানোনিকাল আকারে হ্রাস করা যায়, তবে টাইপ তত্ত্বটিকে স্বাভাবিককরণ (বা দুর্বলভাবে স্বাভাবিককরণ) বলা হয়। যদি ক্যানোনিকাল ফর্মটি অনন্য হয়, তবে তত্ত্বটি দৃঢ়ভাবে স্বাভাবিক বলে মনে করা হয়। স্বাভাবিকতা বেশিরভাগ অ-তুচ্ছ ধরনের তত্ত্বের একটি বিরল বৈশিষ্ট্য, যা যৌক্তিক জগত থেকে একটি বড় বিচ্যুতি। (মনে রাখবেন যে প্রায় প্রতিটি যৌক্তিক ব্যুৎপত্তি একটি সমতুল্য স্বাভাবিক ব্যুৎপত্তি রয়েছে।) কারণটি স্কেচ করার জন্যঃ পুনরাবৃত্তিমূলক সংজ্ঞাগুলি স্বীকার করে এমন ধরণের তত্ত্বগুলিতে, এমন প্রোগ্রাম লেখা সম্ভব যা কখনও কোনও মান হ্রাস করে না; এই ধরনের লুপিং প্রোগ্রামগুলি সাধারণত যে কোনও ধরণের দেওয়া যেতে পারে। বিশেষত, লুপিং প্রোগ্রামে টাইপ ডিডি রয়েছে, যদিও "ডিডি সত্য"-এর কোনও যৌক্তিক প্রমাণ নেই। এই কারণে, প্রস্তাবগুলি প্রকার হিসাবে; প্রমাণগুলি প্রোগ্রামের দৃষ্টান্ত হিসাবে শুধুমাত্র একটি দিকে কাজ করে, যদি মোটেওঃ একটি প্রকার তত্ত্বকে যুক্তি হিসাবে ব্যাখ্যা করা সাধারণত একটি অসঙ্গতিপূর্ণ যুক্তি দেয়। উদাহরণস্বরূপঃ নির্ভরশীল প্রকার তত্ত্ব যুক্তির মতো, প্রকার তত্ত্বের অনেক সম্প্রসারণ এবং রূপ রয়েছে, যার মধ্যে প্রথম ক্রম এবং উচ্চতর ক্রমের সংস্করণ রয়েছে। একটি শাখা, যা ডিপেন্ডেন্ট টাইপ থিওরি নামে পরিচিত, বেশ কয়েকটি কম্পিউটার-সমর্থিত প্রুফ সিস্টেমে ব্যবহৃত হয়। নির্ভরশীল প্রকার তত্ত্ব কোয়ান্টিফায়ারগুলিকে নিজেরাই প্রোগ্রামগুলির মধ্যে পরিসীমা তৈরি করতে দেয়। এই পরিমাপকৃত প্রকারগুলি β এবং HE এর পরিবর্তে β এবং β হিসাবে লেখা হয় এবং নিম্নলিখিত গঠনের নিয়মগুলি রয়েছেঃ এই প্রকারগুলি যথাক্রমে তীর এবং পণ্যের প্রকারের সাধারণীকরণ, যা তাদের প্রবর্তন এবং অপসারণের নিয়ম দ্বারা প্রমাণিত। সম্পূর্ণ সাধারণভাবে নির্ভরশীল ধরনের তত্ত্ব খুব শক্তিশালীঃ এটি প্রোগ্রামের প্রায় যে কোনও কল্পনাযোগ্য বৈশিষ্ট্য সরাসরি প্রোগ্রামের প্রকারগুলিতে প্রকাশ করতে সক্ষম। এই সাধারণতা একটি খাড়া মূল্যে আসে-হয় টাইপচেকিং অনিবার্য (এক্সটেনশনাল টাইপ তত্ত্ব), অথবা এক্সটেনশনাল যুক্তি আরও কঠিন (তীব্র টাইপ তত্ত্ব)। এই কারণে, কিছু নির্ভরশীল ধরনের তত্ত্ব নির্বিচারে প্রোগ্রামগুলির উপর পরিমাণ নির্ধারণের অনুমতি দেয় না, বরং একটি প্রদত্ত নির্ণায়ক সূচক ডোমেনের প্রোগ্রামগুলিতে সীমাবদ্ধ থাকে, উদাহরণস্বরূপ পূর্ণসংখ্যা, স্ট্রিং বা রৈখিক প্রোগ্রাম। যেহেতু ডিপেন্ডেন্ট টাইপ তত্ত্বগুলি প্রকারগুলিকে প্রোগ্রামের উপর নির্ভর করার অনুমতি দেয়, তাই একটি স্বাভাবিক প্রশ্ন জিজ্ঞাসা করা হয় যে প্রোগ্রামগুলির জন্য প্রকারের উপর নির্ভর করা সম্ভব কিনা, বা অন্য কোনও সংমিশ্রণ। এই ধরনের প্রশ্নের অনেক ধরনের উত্তর রয়েছে। টাইপ তত্ত্বের একটি জনপ্রিয় পদ্ধতি হল প্রোগ্রামগুলিকে প্রকারের উপর পরিমাপ করার অনুমতি দেওয়া, যা প্যারামেট্রিক পলিমরফিজম নামেও পরিচিত; এর মধ্যে দুটি প্রধান প্রকার রয়েছেঃ যদি প্রকার এবং প্রোগ্রামগুলিকে আলাদা রাখা হয়, তবে কেউ কিছুটা বেশি ভাল আচরণকারী সিস্টেম অর্জন করে যাকে বলা হয় প্রেডিকেটিভ পলিমরফিজম; যদি প্রোগ্রাম এবং প্রকারের মধ্যে পার্থক্য অস্পষ্ট হয়, তবে কেউ উচ্চতর-ক্রম যুক্তির টাইপ-তাত্ত্বিক এনালগ অর্জন করে, যা ইম্প্রেডেটিভ পলিমরফিজম নামেও পরিচিত। সাহিত্যে নির্ভরতা এবং বহুরূপতার বিভিন্ন সংমিশ্রণ বিবেচনা করা হয়েছে, যার মধ্যে সবচেয়ে বিখ্যাত হল হেঙ্ক বারেনড্রেগের ল্যাম্বডা কিউব। যুক্তি এবং প্রকার তত্ত্বের ছেদ একটি বিশাল এবং সক্রিয় গবেষণার ক্ষেত্র। নতুন যুক্তিগুলি সাধারণত একটি সাধারণ ধরনের তাত্ত্বিক বিন্যাসে আনুষ্ঠানিক করা হয়, যা যৌক্তিক কাঠামো হিসাবে পরিচিত। জনপ্রিয় আধুনিক যৌক্তিক কাঠামো যেমন নির্মাণের ক্যালকুলাস এবং এলএফ উচ্চ-ক্রম নির্ভরশীল প্রকার তত্ত্বের উপর ভিত্তি করে তৈরি, যার মধ্যে নির্ণয়যোগ্যতা এবং অভিব্যক্তিপূর্ণ শক্তির ক্ষেত্রে বিভিন্ন বিনিময় রয়েছে। এই যৌক্তিক কাঠামোগুলি সর্বদা প্রাকৃতিক ডিডাকশন সিস্টেম হিসাবে নির্দিষ্ট করা হয়, যা প্রাকৃতিক ডিডাকশন পদ্ধতির বহুমুখীতার একটি প্রমাণ। ধ্রুপদী এবং মোডাল লজিক্স সরলতার জন্য, এখনও পর্যন্ত উপস্থাপিত লজিক্স স্বজ্ঞাত হয়েছে। ধ্রুপদী যুক্তি একটি অতিরিক্ত স্বতঃসিদ্ধ বা বাদ দেওয়া মধ্যম নীতির সাথে স্বজ্ঞাত যুক্তিকে প্রসারিত করেঃ যে কোনও প্রস্তাবের জন্য p, প্রস্তাবটি সত্য। এই বিবৃতিটি স্পষ্টতই কোনও ভূমিকা বা নির্মূল নয়; প্রকৃতপক্ষে, এতে দুটি স্বতন্ত্র সংযোগ জড়িত। জেন্টজেনের বাদ দেওয়া মাঝখানে মূল চিকিত্সা নিম্নলিখিত তিনটি (সমতুল্য) সূত্রগুলির মধ্যে একটি নির্ধারণ করেছে, যা ইতিমধ্যে হিলবার্ট এবং হেইটিংয়ের সিস্টেমে অনুরূপ আকারে উপস্থিত ছিলঃ (এক্সএম 3 নিছক এক্সএম 2 ই এর পরিপ্রেক্ষিতে প্রকাশ করা হয়েছে।) বাদ দেওয়া মাঝখানে এই চিকিত্সা, একজন বিশুদ্ধবাদী দৃষ্টিকোণ থেকে আপত্তিকর হওয়ার পাশাপাশি, স্বাভাবিক রূপের সংজ্ঞায় অতিরিক্ত জটিলতা প্রবর্তন করে। শুধুমাত্র প্রবর্তন এবং নির্মূলের নিয়মের পরিপ্রেক্ষিতে ধ্রুপদী প্রাকৃতিক ছাড়ের তুলনামূলকভাবে আরও সন্তোষজনক চিকিত্সা 1992 সালে প্যারিগট দ্বারা λμ নামে একটি ধ্রুপদী ল্যাম্বডা ক্যালকুলাস আকারে প্রথম প্রস্তাব করা হয়েছিল। তাঁর পদ্ধতির মূল অন্তর্দৃষ্টি ছিল একটি সত্য-কেন্দ্রিক রায় 'এ' কে আরও শাস্ত্রীয় ধারণার সাথে প্রতিস্থাপন করা, যা ক্রমিক ক্যালকুলাসের স্মরণ করিয়ে দেয়ঃ স্থানীয় আকারে, 'এ'-এর পরিবর্তে, তিনি 'এ' ব্যবহার করেছিলেন, যার সাথে 'এ'-এর অনুরূপ প্রস্তাবনাগুলির একটি সংগ্রহ ছিল। এই কাঠামোটি মূলত ধ্রুপদী ক্রমিক গণনা থেকে সরাসরি উত্তোলন করা হয়, তবে λμ-এর উদ্ভাবনটি ছিল একটি কলসি বা এলআইএসপি এবং এর বংশধরদের মধ্যে দেখা একটি থ্রো/ক্যাচ পদ্ধতির পরিপ্রেক্ষিতে ধ্রুপদী প্রাকৃতিক ডিডাকশন প্রমাণগুলিকে একটি গণনামূলক অর্থ দেওয়া। (আরও দেখুনঃ প্রথম শ্রেণীর নিয়ন্ত্রণ।) আরেকটি গুরুত্বপূর্ণ সম্প্রসারণ ছিল মডেল এবং অন্যান্য যুক্তির জন্য যা সত্যের মৌলিক বিচারের চেয়ে বেশি প্রয়োজন। এগুলি প্রথম 1965 সালে প্রাউইৎজ দ্বারা একটি প্রাকৃতিক ডিডাকশন স্টাইলে আলেথিক মোডাল লজিক্স এস4 এবং এস5-এর জন্য বর্ণনা করা হয়েছিল এবং তারপর থেকে সম্পর্কিত কাজের একটি বড় অংশ জমা হয়েছে। একটি সহজ উদাহরণ দেওয়ার জন্য, মডেল লজিক এস4-এর জন্য একটি নতুন রায় প্রয়োজন, "এ বৈধ", যা সত্যের ক্ষেত্রে শ্রেণীবদ্ধঃ যদি "এ সত্য" "বি সত্য" ফর্মের কোনও অনুমানের অধীনে না হয়, তবে "এ বৈধ"। এই শ্রেণীবদ্ধ রায়টি নিম্নলিখিত ভূমিকা এবং অপসারণের নিয়মগুলির সাথে একটি একক সংযোগকারী হিসাবে অভ্যন্তরীণ করা হয়েছেঃ লক্ষ্য করুন যে "এ বৈধ" ভিত্তির কোনও সংজ্ঞায়িত নিয়ম নেই; পরিবর্তে, বৈধতার শ্রেণীবদ্ধ সংজ্ঞাটি তার জায়গায় ব্যবহার করা হয়। এই পদ্ধতিটি স্থানীয় আকারে আরও স্পষ্ট হয়ে ওঠে যখন অনুমানগুলি স্পষ্ট হয়। আমরা লিখি "ω; ω একটি সত্য" যেখানে ω আগের মতো সত্য অনুমান ধারণ করে এবং ω বৈধ অনুমান ধারণ করে। ডানদিকে কেবল একটি একক রায় রয়েছে "একটি সত্য"; এখানে বৈধতার প্রয়োজন নেই কারণ "একটি বৈধ" সংজ্ঞা অনুসারে "একটি সত্য"-এর সমান। ভূমিকা এবং অপসারণের রূপগুলি হ 'লঃ মোডাল হাইপোথিসিসগুলির হাইপোথিসিস নিয়ম এবং প্রতিস্থাপন উপপাদ্যের নিজস্ব সংস্করণ রয়েছে। মোডাল প্রতিস্থাপন উপপাদ্য যদি ω; ω: A সত্য এবং ω, u: (A বৈধ); ω: C সত্য, তাহলে ω; ω [π1/u] π2: C সত্য। বহু-জোন বা পলিঅ্যাডিক প্রসঙ্গ হিসাবেও পরিচিত অনুমানের স্বতন্ত্র সংগ্রহে রায়গুলিকে পৃথক করার এই কাঠামোটি অত্যন্ত শক্তিশালী এবং সম্প্রসারণযোগ্য; এটি কয়েকটি উদাহরণ দেওয়ার জন্য বিভিন্ন মোডাল লজিক্স এবং রৈখিক এবং অন্যান্য সাবস্ট্রাকচারাল লজিক্সের জন্যও প্রয়োগ করা হয়েছে। যাইহোক, মডেল লজিকের তুলনামূলকভাবে কয়েকটি পদ্ধতি সরাসরি প্রাকৃতিক ডিডাকশনে আনুষ্ঠানিক করা যেতে পারে। এই ব্যবস্থাগুলির প্রমাণ-তাত্ত্বিক বৈশিষ্ট্য প্রদান করার জন্য, লেবেলিং বা গভীর অনুমানের পদ্ধতির মতো সম্প্রসারণ। সূত্রগুলিতে লেবেল যুক্ত করার ফলে যে শর্তগুলির অধীনে নিয়মগুলি প্রযোজ্য হয় তার উপর আরও সূক্ষ্ম নিয়ন্ত্রণের অনুমতি দেয়, যা বিশ্লেষণাত্মক ট্যাবলো প্রয়োগের আরও নমনীয় কৌশলগুলিকে অনুমতি দেয়, যেমন লেবেলযুক্ত ছাড়ের ক্ষেত্রে করা হয়েছে। লেবেলগুলি ক্রিপকে শব্দার্থবিজ্ঞানে বিশ্বের নামকরণের অনুমতি দেয়; ক্রিপকে শব্দার্থবিজ্ঞানে মোডাল লজিক্সের ফ্রেম শর্তগুলিকে হাইব্রিড লজিকের প্রাকৃতিক ডিডাকশন ফর্মালাইজেশনে অনুমানের নিয়মে রূপান্তর করার জন্য একটি প্রভাবশালী কৌশল উপস্থাপন করে। অনেক প্রমাণ তত্ত্বের প্রয়োগ জরিপ করে, যেমন অ্যাভরন এবং পটিঞ্জারের হাইপারসিকোয়েন্টস এবং এস5 এবং বি-এর মতো মোডাল লজিক্সের বেলনাপের ডিসপ্লে লজিক। অন্যান্য মৌলিক পদ্ধতির সঙ্গে তুলনা ক্রমিক ক্যালকুলাস গাণিতিক যুক্তির ভিত্তি হিসাবে প্রাকৃতিক অনুমানের প্রধান বিকল্প হল ক্রমিক ক্যালকুলাস। প্রাকৃতিক অনুমানের ক্ষেত্রে তথ্যের প্রবাহ দ্বি-দিকনির্দেশক হয়ঃ অপসারণের নিয়মগুলি তথ্যকে বিন্যাসের মাধ্যমে নীচের দিকে প্রবাহিত করে এবং প্রবর্তনের নিয়মগুলি সমাবেশের মাধ্যমে তথ্যকে উপরের দিকে প্রবাহিত করে। সুতরাং, একটি প্রাকৃতিক ডিডাকশন প্রমাণের বিশুদ্ধভাবে বটম-আপ বা টপ-ডাউন রিডিং থাকে না, যা এটিকে প্রুফ সার্চে অটোমেশনের জন্য অনুপযুক্ত করে তোলে। এই সত্যটি সমাধান করার জন্য, 1935 সালে জেন্টজেন তাঁর ক্রমিক ক্যালকুলাস প্রস্তাব করেছিলেন, যদিও তিনি প্রাথমিকভাবে এটিকে প্রেডিকেট লজিকের সামঞ্জস্য স্পষ্ট করার জন্য একটি প্রযুক্তিগত যন্ত্র হিসাবে চেয়েছিলেন। ক্লেইন তাঁর 1952 সালের মৌলিক বই ইন্ট্রোডাকশন টু মেটামাথেম্যাটিক্স-এ আধুনিক শৈলীতে ক্রমিক ক্যালকুলাসের প্রথম সূত্র দিয়েছেন। সিকোয়েন্ট ক্যালকুলাসে সমস্ত অনুমানের নিয়মগুলির একটি বিশুদ্ধভাবে বটম-আপ রিডিং রয়েছে। টার্নস্টাইলের উভয় পাশের উপাদানগুলির ক্ষেত্রে অনুমানের নিয়মগুলি প্রযোজ্য হতে পারে। (প্রাকৃতিক অনুমান থেকে আলাদা করার জন্য, এই নিবন্ধটি ধারাবাহিকতার জন্য সঠিক ট্যাকের পরিবর্তে একটি ডাবল তীর ব্যবহার করে।) প্রাকৃতিক ডিডাকশনের প্রবর্তন নিয়মগুলি ক্রমিক গণনায় সঠিক নিয়ম হিসাবে দেখা হয় এবং কাঠামোগতভাবে খুব অনুরূপ। অন্যদিকে অপসারণের নিয়মগুলি ক্রমিক গণনায় বাম নিয়মে পরিণত হয়। একটি উদাহরণ দেওয়ার জন্য, বিচ্ছিন্নতা বিবেচনা করুন; ডান নিয়মগুলি পরিচিতঃ বাম দিকেঃ স্থানীয় আকারে প্রাকৃতিক ছাড়ের নিয়মটি স্মরণ করুনঃ প্রস্তাবনা এ বি, যা ই-তে একটি ভিত্তির উত্তরসূরি, বাম নিয়মের উপসংহারের একটি অনুমানের মধ্যে পরিণত হয়। সুতরাং, বাম নিয়মগুলিকে এক ধরনের উল্টানো নির্মূল নিয়ম হিসাবে দেখা যেতে পারে। এই পর্যবেক্ষণটি নিম্নরূপ চিত্রিত করা যেতে পারেঃ ক্রমিক গণনায়, বাম এবং ডান নিয়মগুলি লক-স্টেপে সঞ্চালিত হয় যতক্ষণ না কেউ প্রাথমিক ক্রমে পৌঁছায়, যা প্রাকৃতিক ছাড়ের ক্ষেত্রে নির্মূল এবং প্রবর্তনের নিয়মগুলির মিলন বিন্দুর সাথে মিলে যায়। এই প্রাথমিক নিয়মগুলি উপরিভাগে প্রাকৃতিক অনুমানের অনুমানের নিয়মের অনুরূপ, তবে ক্রমিক গণনায় তারা একটি বাম এবং ডান প্রস্তাবের স্থানান্তর বা হাত মেলানোর বর্ণনা দেয়ঃ ক্রমিক গণক এবং প্রাকৃতিক অনুমানের মধ্যে যোগাযোগ হল দৃঢ়তা এবং সম্পূর্ণতা উপপাদ্যের একটি জোড়া, যা উভয়ই একটি আবেগময় যুক্তির মাধ্যমে প্রমাণযোগ্য। রুটি-র সাউন্ডনেস। যদি এ হয়, তাহলে এ হবে। যদি এ হয়, তাহলে এ। এই উপপাদ্যগুলি থেকে এটা স্পষ্ট যে ক্রমিক ক্যালকুলাস সত্যের ধারণাকে পরিবর্তন করে না, কারণ প্রস্তাবগুলির একই সংগ্রহ সত্য থাকে। সুতরাং, ক্রমিক ক্যালকুলাস ব্যুৎপত্তিগুলিতে আগের মতো একই প্রমাণ বস্তু ব্যবহার করা যেতে পারে। উদাহরণস্বরূপ, সংযোগগুলি বিবেচনা করুন। ডান নিয়মটি প্রবর্তন নিয়মের সাথে কার্যত অভিন্ন বাম নিয়মটি, তবে, কিছু অতিরিক্ত প্রতিস্থাপন সম্পাদন করে যা সংশ্লিষ্ট অপসারণ নিয়মগুলিতে সঞ্চালিত হয় না। ক্রমবর্ধমান ক্যালকুলাসে উৎপন্ন প্রমাণের ধরন তাই প্রাকৃতিক অনুমানের প্রমাণের থেকে আলাদা। ক্রমিক ক্যালকুলাস β-স্বাভাবিক η-লং ফর্ম হিসাবে পরিচিত প্রমাণ তৈরি করে, যা প্রাকৃতিক ডিডাকশন প্রুফের স্বাভাবিক ফর্মের ক্যানোনিকাল উপস্থাপনার সাথে মিলে যায়। যদি কেউ প্রাকৃতিক ডিডাকশন ব্যবহার করে এই প্রমাণগুলি বর্ণনা করার চেষ্টা করে, তবে কেউ ইন্টারকেলেশন ক্যালকুলাস (জন বার্নস দ্বারা প্রথম বর্ণিত) অর্জন করে, যা প্রাকৃতিক ডিডাকশনের জন্য একটি স্বাভাবিক রূপের ধারণাকে আনুষ্ঠানিকভাবে সংজ্ঞায়িত করতে ব্যবহার করা যেতে পারে। প্রাকৃতিক অনুমানের প্রতিস্থাপন উপপাদ্যটি একটি কাঠামোগত নিয়ম বা কাঠামোগত উপপাদ্যের রূপ নেয় যা ক্রমিক ক্যালকুলাসে কাটা হিসাবে পরিচিত। কাটা (প্রতিস্থাপন) যদি  তাই হয়ঃ A: A: C, তাহলে γ: [π1/u] π2: C। বেশিরভাগ ভাল আচরণের যুক্তিতে, কাটা একটি অনুমানের নিয়ম হিসাবে অপ্রয়োজনীয়, যদিও এটি একটি মেটা-উপপাদ্য হিসাবে প্রমাণযোগ্য থাকে; কাটা নিয়মের অতিরিক্ততা সাধারণত একটি গণনামূলক প্রক্রিয়া হিসাবে উপস্থাপিত হয়, যা কাটা নির্মূল হিসাবে পরিচিত। প্রাকৃতিক ছাড়ের জন্য এর একটি আকর্ষণীয় প্রয়োগ রয়েছে; সাধারণত সীমাহীন সংখ্যক ক্ষেত্রে প্রাকৃতিক ছাড়ের ক্ষেত্রে নির্দিষ্ট বৈশিষ্ট্যগুলি সরাসরি প্রমাণ করা অত্যন্ত ক্লান্তিকর। উদাহরণস্বরূপ, একটি প্রদত্ত প্রস্তাব প্রাকৃতিক ছাড়ের ক্ষেত্রে প্রমাণযোগ্য নয় তা দেখানোর কথা বিবেচনা করুন। একটি সাধারণ ইন্ডাক্টিভ যুক্তি ব্যর্থ হয় কারণ ই বা ই-এর মতো নিয়মগুলি নির্বিচারে প্রস্তাবনা প্রবর্তন করতে পারে। যাইহোক, আমরা জানি যে প্রাকৃতিক ডিডাকশনের ক্ষেত্রে সিকোয়েন্ট ক্যালকুলাস সম্পূর্ণ, তাই সিকোয়েন্ট ক্যালকুলাসে এই অপ্রমাণিকতা দেখানোর জন্য এটি যথেষ্ট। এখন, যদি কাটা একটি অনুমানের নিয়ম হিসাবে উপলব্ধ না হয়, তবে সমস্ত ক্রমিক নিয়মগুলি ডান বা বাম দিকে একটি সংযোগকারী প্রবর্তন করে, তাই একটি ক্রমিক ব্যুৎপত্তির গভীরতা চূড়ান্ত উপসংহারে সংযোগকারী দ্বারা সম্পূর্ণরূপে আবদ্ধ হয়। সুতরাং, অপ্রমাণযোগ্যতা দেখানো অনেক সহজ, কারণ বিবেচনা করার জন্য কেবল সীমিত সংখ্যক মামলা রয়েছে এবং প্রতিটি মামলা সম্পূর্ণরূপে উপ-প্রস্তাবনা দ্বারা গঠিত। এর একটি সহজ উদাহরণ হল বৈশ্বিক সামঞ্জস্য উপপাদ্যঃ "সত্য" প্রমাণযোগ্য নয়। ক্রমবর্ধমান ক্যালকুলাস সংস্করণে, এটি স্পষ্টভাবে সত্য কারণ এমন কোনও নিয়ম নেই যার উপসংহার হিসাবে "ষ্ণন" থাকতে পারে! প্রুফ তাত্ত্বিকরা প্রায়শই এই ধরনের বৈশিষ্ট্যের কারণে কাট-ফ্রি সিকোয়েন্ট ক্যালকুলাস ফর্মুলেশনে কাজ করতে পছন্দ করেন। আরও দেখুন নোটস রেফারেন্স (ইংরেজি অনুবাদ ইনভেস্টিগেশন্স ইনটু লজিক্যাল ডিডাকশন ইন এম. ই. স্জাবো। দ্য কালেক্টেড ওয়ার্কস অফ গেরহার্ড জেন্টজেন। নর্থ-হল্যান্ড পাবলিশিং কোম্পানি, 1969।) অনুবাদ করেছেন পল টেলর এবং ইভস লাফন্ট। পোলিশ যুক্তিতে পুনঃমুদ্রিত 1920-39, সংস্করণ। স্টর্স ম্যাককল। 1983 সালের এপ্রিল মাসে সিয়েনা বিশ্ববিদ্যালয়ের একটি সংক্ষিপ্ত কোর্সে বক্তৃতার নোট। পিএইচডি থিসিস। এম. এসসি থিসিস। বাহ্যিক লিঙ্কগুলি ল্যাবোরিও, ড্যানিয়েল ক্লেমেন্ট, "প্রাকৃতিক অনুমানের পরিচিতি"। ডমিনো অন অ্যাসিড। প্রাকৃতিক ডিডাকশনকে ডোমিনোর খেলা হিসাবে কল্পনা করা হয়েছে। পেলেটিয়ার, জেফ, "এ হিস্ট্রি অফ ন্যাচারাল ডিডাকশন অ্যান্ড এলিমেন্টারি লজিক পাঠ্যপুস্তক"। লেভি, মিশেল, একটি প্রস্তাবনামূলক প্রবাদ। লজিক্যাল ক্যালকুলি ডিডাক্টিভ রিজনিং প্রুফ থিওরি পদ্ধতি