১৯৩৪ সালে জার্মান গণিতবিদ গেরহার্ড জেনটজেন গণিত চিন্তার কেন্দ্রবিন্দুকে কী প্রমাণিত হচ্ছে তা থেকে সরিয়ে নিয়ে যান প্রমাণের নিজস্ব জ্যামিতিক কাঠামোর দিকে। ন্যাচারাল ডিডাকশন এবং সিকোয়েন্ট ক্যালকুলাস ($mathbf{LK}$ ও $mathbf{LJ}$) উদ্ভাবন করে জেনটজেন প্রমাণ করেন আধুনিক প্রুফ থিওরির সর্বশ্রেষ্ঠ উপপাদ্য: কাট এলিমিনেশন থিওরেম (Gentzen’s Hauptsatz)। আনুষ্ঠানিক গণিত থেকে সমস্ত উপপাদ্য বা মধ্যবর্তী লেমা (Lemmas) ছেঁটে ফেলে কীভাবে একটি প্রমাণকে তার বিশুদ্ধতম রূপ দেওয়া যায়, তা দেখিয়ে জেনটজেন $varepsilon_0$ অর্ডিনাল আরোহ পদ্ধতির মাধ্যমে পিয়ানো পাটিগণিতের অবিরোধিতা প্রমাণ করেন।
১. জেনটজেনের সিকোয়েন্ট ক্যালকুলাস $mathbf{LK}$
হিলবার্টের প্রমাণ ব্যবস্থায় সূত্রগুলো স্রেফ সরলরেখায় সাজানো থাকত। জেনটজেন উদ্ভাবন করলেন সিকোয়েন্ট (Sequent):
[
Gamma vdash Delta
]
যেখানে $Gamma = langle A_1, dots, A_k rangle$ হলো পূর্বশর্ত এবং $Delta = langle B_1, dots, B_m rangle$ হলো সিদ্ধান্ত। এর অর্থ: “যদি $Gamma$-এর সমস্ত সূত্র একসাথে সত্য হয়, তবে $Delta$-এর অন্তত একটি সূত্র অবশ্যই সত্য হবে।”
[
bigwedge A_i implies bigvee B_j
]
উভয় পাশ ফাঁকা হলে তৈরি হয় ফাঁকা সিকোয়েন্ট $vdash$, যা বিশুদ্ধ স্ব-বিরোধিতা বা অসম্ভবতাকে ($bot$) নির্দেশ করে।
২. কাট রুল (The Cut Rule): লেমার ইঞ্জিন
সিকোয়েন্ট ক্যালকুলাসে সমস্ত যৌক্তিক সংযোজকের জন্য প্রবেশ নিয়ম রয়েছে। কিন্তু সবার ওপরে অবস্থান করে প্রধান চালিকাশক্তি: কাট রুল (The Cut Rule):
কাট রুল
[
frac{Gamma vdash Delta, A quad A, Sigma vdash Pi}{Gamma, Sigma vdash Delta, Pi} quad (text{Cut})
]
কাট রুল হলো গণিতের লেমা বা মধ্যবর্তী সিদ্ধান্তের আনুষ্ঠানিক রূপ। বাম দিকের প্রমাণে আমরা একটি মধ্যবর্তী সত্য $A$ প্রমাণ করি। ডান দিকের প্রমাণে সেই $A$-কে শর্ত হিসেবে ব্যবহার করে মূল সিদ্ধান্তে পৌঁছানো হয়। কাট রুল মাঝখান থেকে $A$-কে কেটে বাদ দিয়ে সরাসরি সিদ্ধান্ত উপস্থাপন করে। মানুষের তৈরি প্রায় সমস্ত গাণিতিক প্রমাণ এই কাট রুলের ওপর নির্ভরশীল।
৩. জেনটজেনের হাউপ্টসাৎস (Cut Elimination Theorem)
১৯৩৪ সালে জেনটজেন প্রমাণ করেন তাঁর মহাকাব্যিক উপপাদ্য:
জেনটজেনের কাট এলিমিনেশন উপপাদ্য (Hauptsatz)
সিকোয়েন্ট ক্যালকুলাসের যেকোনো প্রমাণকে একটি সুনির্দিষ্ট অ্যালগরিদমিক নিয়মে রূপান্তর করে এমন একটি কাট-মুক্ত প্রমাণে (Cut-Free Proof) রূপান্তর করা সম্ভব যার চূড়ান্ত সিদ্ধান্ত সম্পূর্ণ একই থাকবে!
অর্থাৎ গণিতের যেকোনো প্রমাণ থেকে সমস্ত মধ্যবর্তী অনুমান বা লেমাকে পদ্ধতিগতভাবে অপসারণ করা সম্ভব।
৪. সাব-ফর্মুলা ধর্ম: খাঁটি যুক্তির অ্যানাটমি
কাট রুল অপসারণের ফলে জন্ম নেয় এক অপার বিস্ময়:
সাব-ফর্মুলা ধর্ম (Subformula Property)
একটি কাট-মুক্ত প্রমাণে ব্যবহৃত প্রতিটি সূত্রই চূড়ান্ত সিদ্ধান্তের কোনো না কোনো উপ-সূত্র (Subformula) হতে বাধ্য!
লেমা ব্যবহার করলে $2 + 2 = 4$ প্রমাণের ভেতরেও হঠাৎ করে কমপ্লেক্স নম্বর বা টপোলজির সূত্র ঢুকে পড়তে পারে। কিন্তু কাট-মুক্ত প্রমাণে কোনো অচেনা, বহিরাগত সূত্রের প্রবেশাধিকার নেই! প্রমাণটি কেবল সিদ্ধান্তের অভ্যন্তরীণ উপাদানগুলোকে ভেঙে জোড়া লাগিয়ে তৈরি হয়।
প্রত্যক্ষ ফল: পরম অবিরোধিতা প্রমাণ
একটি তত্ত্বে কি কোনো স্ব-বিরোধ প্রমাণ করা সম্ভব? স্ব-বিরোধ মানে ফাঁকা সিকোয়েন্ট $vdash$। যদি তার কোনো প্রমাণ থাকে, তবে তার একটি কাট-মুক্ত প্রমাণ থাকতে হবে। কিন্তু সাব-ফর্মুলা ধর্ম অনুসারে কাট-মুক্ত প্রমাণের প্রতিটি উপাদান সিদ্ধান্তের ভেতর থাকতে হয়। যেহেতু $vdash$-এর ভেতর কোনো সূত্রই নেই, তাই কোনো নিয়ম দিয়েই তা তৈরি করা অসম্ভব! অর্থাৎ স্ব-বিরোধিতার উৎপত্তি সম্পূর্ণ অসম্ভব।
৫. এপসাইলন-জিরো ($varepsilon_0$) আরোহে পাটিগণিতের অবিরোধিতা প্রমাণ
গোডেল প্রমাণ করেছিলেন যে পাটিগণিত নিজের সাধারণ নিয়মে নিজের অবিরোধিতা প্রমাণ করতে পারে না। তবে জেনটজেন ১৯৩৬ সালে পাটিগণিতের অবিরোধিতা কীভাবে প্রমাণ করলেন?
জেনটজেন দেখালেন যে পাটিগণিতের গাণিতিক আরোহ বিধির কাট এলিমিনেশন সাধারণ সংখ্যা দিয়ে শেষ হয় না; এটি শেষ করতে প্রয়োজন হয় ক্যান্টর অর্ডিনাল $varepsilon_0$ পর্যন্ত ট্রান্সফাইনাইট আরোহ (Transfinite Induction):
[
varepsilon_0 = omega^{omega^{omega^{cdot^{cdot^omega}}}}
]
জেনটজেন প্রমাণ করেন যে প্রতিটি প্রমাণ হ্রাসের সাথে সাথে অর্ডিনাল সংখ্যাটি কমতে থাকে। যেহেতু $varepsilon_0$-এর নিচে অর্ডিনালের কোনো অসীম নিম্নমুখী ধারা থাকা অসম্ভব, তাই সসীম পদক্ষেপে কাট এলিমিনেশন সম্পন্ন হতে বাধ্য!
গোডেলের সাথে এখানে কোনো বিরোধ নেই: পাটিগণিত নিজে $varepsilon_0$-এর আরোহ বিধি প্রমাণ করতে পারে না। জেনটজেন নিখুঁতভাবে পরিমাপ করলেন গণিতের আত্মবিশ্বাসের পরিধি: পাটিগণিতের সঙ্গতি এবং $varepsilon_0$ অর্ডিনালের সুশৃঙ্খলতা পরস্পর গাণিতিকভাবে সম্পূর্ণ অভিন্ন। এখান থেকেই জন্ম নিল আধুনিক অর্ডিনাল অ্যানালাইসিস।
