কারির কূটাভাস

কারির কূটাভাস হলো একটি কূটাভাস যেখানে একটি আরবিট্র্যারি দাবি F প্রমাণিত হয় শুধুমাত্র একটি বাক্য C এর অস্তিত্বের মাধ্যমে যা নিজেই বলে "যদি C, তবে F "। কূটাভাসটির জন্য কেবলমাত্র কয়েকটি আপাত-নিরীহ যৌক্তিক ডিডাকশন নিয়ম প্রয়োজন। যেহেতু F আরবিট্র্যারি,তাই এই নিয়মগুলি থাকা যে কোনো যুক্তি পদ্ধতি দিয়ে সবকিছুই প্রমাণ করা সম্ভব। কূটাভাসটি স্বাভাবিক ভাষায় এবং বিভিন্ন যুক্তিতে প্রকাশ করা যেতে পারে, যার মধ্যে সেট তত্ত্বের কিছু নির্দিষ্ট রূপ, ল্যাম্‌ডা ক্যালকুলাস এবং সংমিশ্রণমূলক যুক্তি অন্তর্ভুক্ত।

কূটাভাসটির নামকরণ করা হয়েছে যুক্তিবিদ হাসকেল কারির নামে, যিনি এই সম্পর্কে ১৯৪২ সালে লিখেছিলেন। লোবের উপপাদ্যের সাথে এর সম্পর্কের কারণে একে লোবের কূটাভাসও বলা হয়ে থাকে।

স্বাভাবিক ভাষায়

"যদি A, তবে B " ধরণের দাবিকে শর্তাধীন বা শর্তসাপেক্ষ দাবি বলা হয়। কারির কূটাভাস এক বিশেষ ধরনের স্ব-উল্লেখকারী শর্তসাপেক্ষ বাক্য ব্যবহার করে, যেমনটি এই উদাহরণে প্রদর্শিত হয়েছে:টেমপ্লেট:Block indentযদিও জার্মানি চীনের সীমান্তবর্তী নয়, উদাহরণ বাক্যটি অবশ্যই একটি প্রাকৃতিক-ভাষার বাক্য, এবং এই বাক্যটির সত্যতা বিশ্লেষণ করা সম্ভব। এই কূটাভাসের বিশ্লেষণ দুটি ধাপ নিয়ে গঠিত। প্রথমত, সাধারণ প্রাকৃতিক-ভাষা প্রমাণ কৌশলগুলি প্রমাণ করতে ব্যবহার করা যেতে পারে যে উদাহরণ বাক্যটি সত্য [ধাপ ১-৪] । দ্বিতীয়ত, বাক্যটির সত্যতা প্রমাণ করতে ব্যবহার করা যেতে পারে যে জার্মানি চীনের সীমান্তবর্তী [5-6] :

1. বাক্যটিতে লেখা "যদি এই বাক্যটি সত্য হয়, তবে জার্মানি চিনের সীমান্তবর্তী" [ প্রথাগত প্রমাণের সাথে সামঞ্জস্যপূর্ণ ধাপ নম্বর পেতে সংজ্ঞা পুনরাবৃত্তি করুন]
2. বাক্যটি সত্য হলে তা সত্য।
3. যদি বাক্যটি সত্য হয়, তাহলে: যদি বাক্যটি সত্য হয়, জার্মানি চিনের সীমান্তবর্তী।
4. যদি বাক্যটি সত্য হয়, তবে জার্মানি চীনের সীমান্তবর্তী।
5. কিন্তু ৪ হলো বাক্যটি যা বলে, তাই এটি প্রকৃতপক্ষে সত্য।
6. বাক্যটি সত্য [৫. দ্বারা], এবং [৪. দ্বারা] : যদি এটি সত্য হয়, তাহলে জার্মানি চীনের সীমান্তবর্তী।

সুতরাং, জার্মানি চীনের সীমান্তবর্তী।   [modus ponens]

যেহেতু জার্মানি চীনের সাথে সীমান্তবর্তী নয়, বোঝা যায় যে প্রমাণ পদক্ষেপগুলির একটিতে ত্রুটি হয়েছে৷ "জার্মানি চীনের সীমান্তবর্তী" দাবি অন্য যে কোনো দাবি দ্বারা প্রতিস্থাপিত হতে পারে, এবং বাক্যটি সেক্ষেত্রেও প্রমাণযোগ্য হবে। এইভাবে সকল বাক্য প্রমাণযোগ্য বলে মনে হয়। কারণ প্রমাণটি শুধুমাত্র ডিডাকশনের স্বীকৃত পদ্ধতি ব্যবহার করে, এবং যেহেতু এই পদ্ধতিগুলির কোনটিই ভুল বলে মনে হয় না, এই পরিস্থিতিটি বিরোধপূর্ণ।

অনানুষ্ঠানিক প্রমাণ

শর্তসাপেক্ষ বাক্য প্রমাণের জন্য আদর্শ পদ্ধতি ("যদি A, তবে B " ধরণের বাক্য) হলো " শর্তসাপেক্ষ প্রমাণ "। এই পদ্ধতিতে, "যদি A, তবে B " প্রমাণ করার জন্য, প্রথমে A ধরে নেওয়া হয় এবং তারপর সেই অনুমান সহ B কে সত্য দেখানো হয়।

কারির কূটাভাস তৈরি করতে, উপরের দুটি ধাপে বর্ণিত পদ্ধতি অনুসারে "যদি এই বাক্যটি সত্য হয়, তবে জার্মানি চীনের সাথে সীমান্তবর্তী" বাক্যের ক্ষেত্রে এই পদ্ধতি প্রয়োগ করুন। এখানে A, "এই বাক্যটি সত্য", সামগ্রিক বাক্যকে বোঝায়, যখন B হলো "জার্মানি চীনের সীমান্তবর্তী"। সুতরাং, A অনুমান করা "যদি A, তবে B " অনুমান করার সমান। অতএব, A কে সত্য ধরে নেওয়ার ক্ষেত্রে, আমরা A এবং "যদি A, তবে B " উভয়কেই সত্য ধরে নিয়েছি। অতএব, বি সত্য, মোডাস পোনেন্স দ্বারা, এবং আমরা প্রমাণ করেছি "যদি এই বাক্যটি সত্য হয়, তাহলে 'জার্মানি চীনের সীমান্তবর্তী' সত্য।" স্বাভাবিক উপায়ে, অনুমান অনুমান করে এবং উপসংহার বের করে।

এখন, যেহেতু আমরা প্রমাণ করেছি "যদি এই বাক্যটি সত্য হয়, তাহলে 'জার্মানি চিনের সীমান্তবর্তী' সত্য", তাহলে আমরা আবার মোডাস পোনেন্স প্রয়োগ করতে পারি, কারণ আমরা জানি যে "এই বাক্যটি সত্য" দাবিটি সঠিক। এইভাবে, আমরা দেখতে পারি যে জার্মানি চীনের সীমান্তবর্তী।

আনুষ্ঠানিক যুক্তিতে

বাক্যগত যুক্তি

পূর্ববর্তী অংশে দেওয়া উদাহরণটি আনুষ্ঠানিকভাবে অপ্রণীত, প্রাকৃতিক ভাষার যুক্তি ব্যবহার করেছিল। কারির কূটাভাস কিছু প্রকারের আনুষ্ঠানিক যুক্তিতেও ঘটে। এই প্রসঙ্গে, এটি দেখায় যে যদি আমরা ধরে নিই যে একটি আনুষ্ঠানিক বাক্য (X → Y) বিদ্যমান, যেখানে X নিজেই (X → Y)-এর সমতুল্য, তাহলে আমরা একটি আনুষ্ঠানিক প্রমাণ দ্বারা Y প্রমাণ করতে পারি। এমন একটি আনুষ্ঠানিক প্রমাণের একটি উদাহরণ নিম্নরূপ:

X := (X → Y)
টেমপ্লেট:Block indent

X → X
টেমপ্লেট:Block indent

X → (X → Y)
টেমপ্লেট:Block indent

X → Y
টেমপ্লেট:Block indent

X
টেমপ্লেট:Block indent

Y
টেমপ্লেট:Block indent

একটি বিকল্প প্রমাণ হল Peirce's law দ্বারা। যদি X = X → Y, তবে (X → Y) → X। এটি এবং Peirce-এর আইন ((X → Y) → X) → X এবং modus ponens একত্রে X এবং পরবর্তী Y প্রমাণ করে (উপরের প্রমাণের মতো)।

উপরের উদ্ভাবনটি দেখায় যে, যদি Y একটি আনুষ্ঠানিক ব্যবস্থায় একটি অপ্রমাণযোগ্য বিবৃতি হয়, তবে সেই ব্যবস্থায় এমন কোনো X বিবৃতি নেই যার জন্য X (X → Y)-এর সমতুল্য। অন্য কথায়, পূর্ববর্তী প্রমাণের ধাপ ১ ব্যর্থ হয়। অন্যদিকে, পূর্ববর্তী অংশটি দেখায় যে প্রাকৃতিক (অপ্রণীত) ভাষায়, প্রতিটি প্রাকৃতিক ভাষার বিবৃতি Y-এর জন্য এমন একটি প্রাকৃতিক ভাষার বিবৃতি Z বিদ্যমান, যেখানে Z প্রাকৃতিক ভাষায় (Z → Y)-এর সমতুল্য। যথা, Z হল "যদি এই বাক্যটি সত্য হয় তবে Y"।

নাইভ সেট তত্ত্ব

যদিও প্রাথমিক গাণিতিক যুক্তি কোনো স্ব-উল্লেখযোগ্য বাক্য গ্রহণ করে না, কিছু নির্দিষ্ট প্রকারের নাইভ সেট তত্ত্ব এখনও কারির কূটাভাসের জন্য দুর্বল। এমন সমষ্টি তত্ত্বে যা অসীমত সংজ্ঞাবদ্ধতা অনুমোদন করে, আমরা নিম্নলিখিত সমষ্টি বিবেচনা করে যেকোনো যৌক্তিক বিবৃতি Y প্রমাণ করতে পারি: পার্স করতে ব্যর্থ (সিনট্যাক্স ত্রুটি): {\displaystyle X \ \stackrel{\mathrm{def}}{=}\ \left{ x \mid (x \in x) \to Y \right}.} এরপর সহজেই দেখানো যায় যে $X\in X$ বিবৃতিটি $(X\in X)\to Y$-এর সমতুল্য। এখান থেকে, উপরে প্রদর্শিত প্রমাণগুলোর মতো করে, $Y$ সিদ্ধান্ত করা যায়। ("$X\in X$" দ্বারা "এই বাক্যটি" বোঝায়।)

অতএব, একটি সঙ্গতিপূর্ণ সমষ্টি তত্ত্বে, সমষ্টি পার্স করতে ব্যর্থ (সিনট্যাক্স ত্রুটি): {\displaystyle \left{ x \mid (x \in x) \to Y \right}} মিথ্যা Y-এর জন্য অস্তিত্বশীল নয়। একে রাসেলের কূটাভাসের একটি রূপ হিসাবে দেখা যেতে পারে, কিন্তু এটি অভিন্ন নয়। কিছু সমষ্টি তত্ত্বের প্রস্তাব রাসেলের কূটাভাসের মোকাবিলা করার চেষ্টা করেছে সংজ্ঞাবদ্ধতার নিয়ম সীমাবদ্ধ না করে বরং যুক্তির নিয়ম সীমাবদ্ধ করে, যাতে এটি এমন সব সমষ্টির স্ববিরোধী প্রকৃতিকে সহ্য করে যা নিজেদের সদস্য নয়। উপরের মতো প্রমাণের অস্তিত্ব দেখায় যে এমন কাজ সহজ নয়, কারণ উপরের প্রমাণে ব্যবহৃত অন্তত একটি সিদ্ধান্তের নিয়ম বাদ দিতে হবে বা সীমাবদ্ধ করতে হবে।

সীমিত সর্বনিম্ন যুক্তি সহ ল্যামডা ক্যালকুলাস

কারির কূটাভাস টাইপবিহীন ল্যাম্ডা ক্যালকুলাসে প্রকাশ করা যেতে পারে, যা ইমপ্লিকেশনাল প্রপোজিশনাল ক্যালকুলাস দ্বারা সমৃদ্ধ। ল্যামডা ক্যালকুলাসের বাক্যগঠনগত সীমাবদ্ধতার সাথে সামঞ্জস্য রাখতে, $m$ দুটি প্যারামিটার গ্রহণ করা একটি ইমপ্লিকেশন ফাংশন নির্দেশ করবে। অর্থাৎ, ল্যামডা টার্ম $((mA)B)$ সাধারণ ইনফিক্স নোটেশন $A\to B$-এর সমতুল্য হবে।

একটি ইচ্ছেমতো সূত্র $Z$ প্রমাণ করা যেতে পারে একটি ল্যামডা ফাংশন সংজ্ঞায়িত করে: $N:=\lambda p.((mp)Z)$, এবং $X:=(\mathsf{\text{Y}}N)$, যেখানে $\mathsf{\text{Y}}$ কারির স্থির-বিন্দু সমন্বয়কারী নির্দেশ করে। এরপর $X=(NX)=((mX)Z)$ হয় $\mathsf{\text{Y}}$ এবং $N$-এর সংজ্ঞা অনুযায়ী। ফলে উপরে প্রদর্শিত বাক্যগত যুক্তি প্রমাণটি ক্যালকুলাসেও পুনরায় করা যেতে পারে:

$$\begin{array}{ccc}⊢& ((mX)X)& \text{ সর্বনিম্ন যুক্তির স্বতঃসিদ্ধ }A\to A\text{ দ্বারা }\\ ⊢& ((mX)((mX)Z))& \text{ যেহেতু }X=((mX)Z)\\ ⊢& ((mX)Z)& \text{ সর্বনিম্ন যুক্তির উপপাদ্য দ্বারা }(A\to (A\to B))⊢(A\to B)\\ ⊢& X& \text{ যেহেতু }X=((mX)Z)\\ ⊢& Z& \text{ দ্বারা }modusponensA,(A\to B)⊢B\text{ থেকে }X\text{ এবং }((mX)Z)\end{array}$$ সিম্পলি টাইপড ল্যাম্ব্ডা ক্যালকুলাসে, স্থির-বিন্দু সমন্বয়কারী টাইপ করা যায় না এবং তাই অনুমোদিত নয়।

যৌগিক যুক্তি

কারির কূটাভাস যৌগিক যুক্তিতেও প্রকাশ করা যেতে পারে, যার ল্যামডা ক্যালকুলাসের সমান প্রকাশ ক্ষমতা রয়েছে। যেকোনো ল্যামডা অভিব্যক্তি যৌগিক যুক্তিতে অনুবাদ করা যায়, তাই ল্যামডা ক্যালকুলাসে কারির কূটাভাসের বাস্তবায়নের অনুবাদ যথেষ্ট হবে।

উপরে উল্লেখিত টার্ম $X$ যৌগিক যুক্তিতে $(rr)$ এ অনূদিত হয়, যেখানে $$r=\mathsf{\text{S}}(\mathsf{\text{S}}(\mathsf{\text{K}}m)(\mathsf{\text{S}}\mathsf{\text{I}}\mathsf{\text{I}}))(\mathsf{\text{K}}Z);$$ এবং তারপরে:

$$(rr)=((m(rr))Z).$$

আলোচনা

কারির কূটাভাস মৌলিক যৌক্তিক ক্রিয়াকলাপ সমর্থিত এবং একটি স্ব-আবৃত্তিমূলক ফাংশন একটি অভিব্যক্তি হিসেবে গঠন করার সুযোগ থাকে এমন যে কোনো ভাষায় প্রণীত হতে পারে। যে দুটি প্রক্রিয়া কূটাভাসটি নির্মাণে সহায়তা করে তা হলো স্ব-উল্লেখ (বাক্যের মধ্যেই "এই বাক্যটি" উল্লেখ করা) এবং অসীম সংকলন যা প্রাথমিক সেট তত্ত্বে বিদ্যমান। প্রাকৃতিক ভাষাগুলো প্রায়ই এমন অনেক বৈশিষ্ট্য ধারণ করে যা কূটাভাস তৈরিতে ব্যবহার করা যেতে পারে, এবং অন্যান্য অনেক ভাষাও তাই। সাধারণত, একটি ভাষায় মেটাপ্রোগ্রামিং ক্ষমতা যোগ করলে প্রয়োজনীয় বৈশিষ্ট্যগুলো যুক্ত হয়। গণিতের যুক্তি সাধারণত নিজ বাক্যের উপর সরাসরি উল্লেখ করার অনুমতি দেয় না; তবে, গ্যোডেলের অসম্পূর্ণতা তত্ত্ব-এর মর্মে রয়েছে যে স্ব-উল্লেখের একটি ভিন্ন রূপ যুক্ত করা যেতে পারে।

প্রমাণ নির্মাণে ব্যবহৃত নিয়মগুলো হলো শর্তমূলক প্রমাণের জন্য অনুমানের নিয়ম, সংকোচনের নিয়ম, এবং মোডাস পোনেন্স। এই নিয়মগুলো বেশিরভাগ সাধারণ যুক্তিতান্ত্রিক ব্যবস্থায় অন্তর্ভুক্ত, যেমন প্রথম-শ্রেণীর যুক্তি।

কিছু আনুষ্ঠানিক যুক্তির জন্য পরিণতি

১৯৩০-এর দশকে কারির কূটাভাস এবং সম্পর্কিত ক্লিন–রসর কূটাভাস, যেখান থেকে কারির কূটাভাস বিকশিত হয়, বিভিন্ন আনুষ্ঠানিক যুক্তিতান্ত্রিক ব্যবস্থাকে দেখিয়েছিল যে স্ব-আবৃত্তিমূলক অভিব্যক্তি অনুমোদন করলে তা অসঙ্গতিশীল হতে পারে।

অসীম সংকলনের স্বতঃপ্রমাণ আধুনিক সেট তত্ত্ব দ্বারা সমর্থিত নয়, এবং এ কারণে কারির কূটাভাস এড়ানো সম্ভব।