In this paper, we study a new Kripke-style semantics for classical modal logic, named as provability models. We study provability models for the propositional modal logics K, K4, S4 GL, GLP and the interpretability logic ILM. Provability models combine features of Kripke models with the assignment of logics to individual worlds. Originally introduced in [Mojtahedi, 2022], these models allowed the first author to establish arithmetical completeness for intuitionistic provability logic. Interestingly, we show that the ILM is complete for the same provability models of GL. We improve provability models to predicative and decidable provability models in the case of GL and ILM. Furthermore, we prove a soundness and completeness of GLP for provability models.
- পেপার আইডি: 2510.06696
- শিরোনাম: প্রমাণযোগ্যতা মডেল
- লেখক: মোজতাবা মোজতাহেদি (ঘেন্ট বিশ্ববিদ্যালয়), বোরহা সিয়েরা মিরান্ডা (বার্ন বিশ্ববিদ্যালয়)
- শ্রেণীবিভাগ: math.LO (গাণিতিক যুক্তিবিদ্যা)
- প্রকাশনার সময়: অক্টোবর ১৫, ২০২৫
- পেপার লিঙ্ক: https://arxiv.org/abs/2510.06696
এই পেপারটি একটি নতুন ক্রিপকে-সদৃশ শব্দার্থবিজ্ঞান অধ্যয়ন করে—প্রমাণযোগ্যতা মডেল (provability models), যা চিরন্তন মোডাল যুক্তির জন্য ব্যবহৃত হয়। গবেষণা প্রস্তাবনামূলক মোডাল যুক্তি K, K4, S4, GL, GLP এবং ব্যাখ্যাযোগ্যতা যুক্তি ILM-এর প্রমাণযোগ্যতা মডেল অন্তর্ভুক্ত করে। প্রমাণযোগ্যতা মডেল ক্রিপকে মডেলের বৈশিষ্ট্য এবং পৃথক বিশ্বের জন্য যুক্তি বরাদ্দ করার পদ্ধতি একত্রিত করে। এই মডেলটি প্রাথমিকভাবে মোজতাহেদি দ্বারা ২০২২ সালে প্রবর্তিত হয়েছিল, স্বজ্ঞাত প্রমাণযোগ্যতা যুক্তির পাটিগণিত সম্পূর্ণতা প্রতিষ্ঠার জন্য। আকর্ষণীয়ভাবে, এই পেপারটি প্রমাণ করে যে ILM GL-এর সমান প্রমাণযোগ্যতা মডেলের জন্য সম্পূর্ণ। GL এবং ILM-এর ক্ষেত্রে, এই পেপারটি প্রমাণযোগ্যতা মডেলকে পূর্বাভাসযোগ্য এবং সিদ্ধান্তযোগ্য প্রমাণযোগ্যতা মডেলে উন্নত করে, এবং GLP-এর প্রমাণযোগ্যতা মডেলের জন্য সুস্থতা এবং সম্পূর্ণতা প্রমাণ করে।
প্রথাগত প্রমাণযোগ্যতা যুক্তি গবেষণায়, মোডাল অপারেটর সাধারণত কিছু প্রথম-ক্রম পাটিগণিত বা সেট তত্ত্ব সিস্টেমে প্রমাণযোগ্যতা প্রবিধান হিসাবে ব্যাখ্যা করা হয়। তবে, □A কে L ⊢ A হিসাবে ব্যাখ্যা করা যায় (একটি প্রদত্ত প্রস্তাবনামূলক তত্ত্ব L-এর জন্য)। যদিও GL সমন্বিত যেকোনো যুক্তি L-এর জন্য, GL L-ব্যাখ্যার জন্য সুস্থ প্রমাণ করা যায়, কোনো L-ব্যাখ্যা GL-এর সম্পূর্ণতা প্রদান করতে পারে না।
এই ব্যর্থতা PA-ব্যাখ্যার সাথে বৈপরীত্য তৈরি করে, প্রধানত কারণ যুক্তি L ক্রিপকে মডেল অনুকরণ করতে পারে না, যখন পিয়ানো পাটিগণিত তার ক্রিপকে মডেল অনুকরণ করার ক্ষমতা ব্যবহার করতে পারে (যেমন সোলোভে প্রদর্শন করেছেন)। অতএব, GL কে একক প্রস্তাবনামূলক যুক্তির প্রমাণযোগ্যতা যুক্তি হিসাবে প্রত্যাশা করা যায় না।
- মান ক্রিপকে মডেলের সীমাবদ্ধতা: প্রমাণযোগ্যতা যুক্তির পাটিগণিত ব্যাখ্যা সরাসরি পরিচালনা করতে পারে না
- প্রস্তাবনামূলক প্রমাণযোগ্যতা ব্যাখ্যার অসম্পূর্ণতা: একক প্রস্তাবনামূলক যুক্তি GL-এর সম্পূর্ণতা প্রদান করতে পারে না
- জটিল কাঠামো বৈশিষ্ট্য: যেমন Iemhoff শব্দার্থবিজ্ঞানে জটিল কাঠামো বৈশিষ্ট্য পাটিগণিত সম্পূর্ণতা উপপাদ্য প্রতিষ্ঠা করা কঠিন করে তোলে
এই পেপারটি ক্রিপকে কাঠামোকে স্পষ্টভাবে প্রস্তাবনামূলক যুক্তিতে একীভূত করে এই সীমাবদ্ধতা দূর করে, মান ক্রিপকে মডেল বিবেচনা করে, যেখানে প্রতিটি বিশ্ব w একটি যুক্তি Lw দিয়ে সজ্জিত, এবং অন্তর্নিহিত অ্যাক্সেসযোগ্যতা সম্পর্কের উপর ভিত্তি করে এই তত্ত্বগুলির মধ্যে অ্যাক্সেসযোগ্যতা সম্পর্ক প্রয়োগ করে।
- প্রমাণযোগ্যতা মডেল কাঠামো প্রস্তাব: চিরন্তন মোডাল যুক্তির জন্য নতুন ক্রিপকে-শৈলী শব্দার্থবিজ্ঞান প্রবর্তন করা
- বিভিন্ন মোডাল যুক্তির সম্পূর্ণতা প্রতিষ্ঠা: K, K4, S4, GL-এর প্রমাণযোগ্যতা মডেলের জন্য সুস্থতা এবং সম্পূর্ণতা প্রমাণ করা
- স্বাধীন প্রমাণযোগ্যতা মডেল নির্মাণ: বিশেষত GL এবং ILM-এর জন্য, মান ক্রিপকে মডেল থেকে স্বাধীন প্রমাণযোগ্যতা মডেল কীভাবে নির্মাণ করতে হয় তা প্রদর্শন করা
- সিদ্ধান্তযোগ্যতা বাস্তবায়ন: GL এবং ILM-এর ক্ষেত্রে, সিদ্ধান্তযোগ্য প্রমাণযোগ্যতা মডেল নির্মাণ করা
- বহু-মোডাল যুক্তিতে সম্প্রসারণ: GLP (বহু-মোডাল প্রমাণযোগ্যতা যুক্তি) প্রমাণযোগ্যতা মডেলের জন্য সুস্থতা এবং সম্পূর্ণতা প্রমাণ করা
- ILM-এর সম্পূর্ণতা প্রতিষ্ঠা: ব্যাখ্যাযোগ্যতা যুক্তি ILM GL-এর সমান প্রমাণযোগ্যতা মডেলের জন্য সম্পূর্ণ প্রমাণ করা
প্রমাণযোগ্যতা মডেলকে মোডাল যুক্তির শব্দার্থবিজ্ঞান হিসাবে অধ্যয়ন করা, যেখানে:
- ইনপুট: মোডাল যুক্তি সূত্র এবং প্রমাণযোগ্যতা মডেল
- আউটপুট: মডেলে সূত্রের বৈধতা নির্ণয়
- সীমাবদ্ধতা: মডেল অবশ্যই নির্দিষ্ট যুক্তি বৈশিষ্ট্য এবং কাঠামো শর্ত পূরণ করবে
প্রমাণযোগ্যতা প্রাক-মডেল P = (W, <, {Lw}w∈W, V) অন্তর্ভুক্ত করে:
- W: অ-খালি বিশ্ব সেট
- <: W-এ দ্বিমুখী সম্পর্ক
- Lw: প্রতিটি <-অ্যাক্সেসযোগ্য বিশ্ব w-এর জন্য যুক্তি
- V: পারমাণবিক প্রস্তাবের জন্য মূল্যায়ন সম্পর্ক
সূত্র A-এর জন্য, P, w |= A সংজ্ঞায়িত করুন আবেগপূর্ণভাবে:
- বুলিয়ান সংযোগের সাথে বিনিময়যোগ্য
- P, w |= □A যখন এবং শুধুমাত্র যখন ∀u ⪯ w (⊢u A)
প্রমাণযোগ্যতা প্রাক-মডেল প্রমাণযোগ্যতা মডেল হয়ে ওঠে যখন সন্তুষ্ট হয়:
- মোডাল সম্পূর্ণতা: প্রতিটি বিশুদ্ধ মোডাল সূত্র A-এর জন্য, যদি P, w |=+ A তবে ⊢w A
প্রমাণযোগ্যতা মডেল কাঠামো শর্তকে পৃথক বিশ্বের জন্য বরাদ্দ করা যুক্তির অনুমান নিয়মে শোষণ করতে পারে:
- সংক্রমণশীলতা প্রয়োজনীয়করণ নিয়ম দ্বারা প্রতিস্থাপিত হতে পারে
- বিপরীত সুভিধা Löb নিয়ম দ্বারা প্রতিস্থাপিত হতে পারে
GL এবং ILM-এর জন্য, প্রমাণযোগ্যতা মডেল নির্মাণের জন্য গঠনমূলক পদ্ধতি প্রদান করা:
উপপাদ্য ৪.৪: প্রতিটি বিপরীত সুভিধা গাছ প্রমাণযোগ্যতা প্রাক-মডেল P-এর জন্য, প্রয়োজনীয়করণ সহ একটি প্রমাণযোগ্যতা মডেল P̄ বিদ্যমান, যেমন:
- P̄-এ প্রয়োজনীয়করণ রয়েছে
- P ⊆ P̄
- P̄ হল P সমন্বিত ন্যূনতম প্রমাণযোগ্যতা মডেল
যদি P দ্বি-সীমিত হয়, তবে P̄ সিদ্ধান্তযোগ্য, যেখানে দ্বি-সীমিত মানে W এবং প্রতিটি w∈W-এর জন্য Axiom(Lw) উভয়ই সীমিত।
এই পেপারটি প্রধানত তাত্ত্বিক প্রমাণ পরিচালনা করে, যাচাইকরণ কাঠামো অন্তর্ভুক্ত করে:
বিভিন্ন মোডাল যুক্তির জন্য, প্রমাণ করা যে যদি যুক্তি ⊢ A, তবে P |= A সমস্ত সংশ্লিষ্ট প্রমাণযোগ্যতা মডেল P-এর জন্য সত্য।
প্রমাণ করা যে যদি P |= A সমস্ত সংশ্লিষ্ট প্রমাণযোগ্যতা মডেল P-এর জন্য সত্য, তবে যুক্তি ⊢ A।
বিশেষত GL-এর জন্য, শক্তিশালী সম্পূর্ণতা প্রমাণ করা: Γ |=P A সূচিত করে Γ ⊢GL A।
নির্দিষ্ট নির্মাণের মাধ্যমে যাচাই করা:
- সীমিত প্রমাণযোগ্যতা মডেলের অস্তিত্ব
- সিদ্ধান্তযোগ্যতার বাস্তবায়ন
- স্বাধীনতা (মান ক্রিপকে মডেলের উপর নির্ভরশীল নয়)
- K: প্রমাণযোগ্যতা মডেলের জন্য সুস্থ এবং সম্পূর্ণ (উপপাদ্য ৩.৬, ৩.৭)
- K4: প্রয়োজনীয়করণ বা সংক্রমণশীলতা সহ প্রমাণযোগ্যতা মডেলের জন্য সুস্থ এবং সম্পূর্ণ (উপপাদ্য ৩.৮, ৩.৯)
- S4: প্রতিফলনশীল, সংক্রমণশীল, প্রয়োজনীয়করণ এবং স্থানীয় সম্পূর্ণতা সহ প্রমাণযোগ্যতা মডেলের জন্য সুস্থ এবং সম্পূর্ণ (উপপাদ্য ৩.১১, ৩.১२)
- সুস্থতা: GL বিপরীত সুভিধা প্রমাণযোগ্যতা মডেলের জন্য প্রয়োজনীয়করণ এবং Löb নিয়ম সহ সুস্থ (উপপাদ্য ৩.১४)
- সম্পূর্ণতা: GL সীমিত সংক্রমণশীল অ-প্রতিফলনশীল প্রমাণযোগ্যতা মডেলের জন্য সম্পূর্ণ (উপপাদ্য ৩.१७)
- শক্তিশালী সম্পূর্ণতা: GL প্রয়োজনীয়করণ এবং Löb নিয়ম সহ প্রমাণযোগ্যতা মডেলের জন্য শক্তিশালী সম্পূর্ণ (উপপাদ্য ৩.१८)
- সীমিততা সম্পূর্ণতা: GL সীমিত প্রমাণযোগ্যতা মডেলের জন্য সম্পূর্ণ (উপপাদ্য ४.६)
- সুস্থতা: ILM বিপরীত সুভিধা প্রমাণযোগ্যতা মডেলের জন্য প্রয়োজনীয়করণ সহ সুস্থ (উপপাদ্য ५.६)
- সম্পূর্ণতা: ILM সীমিত গাছ বিপরীত সুভিধা প্রমাণযোগ্যতা মডেলের জন্য প্রয়োজনীয়করণ সহ সম্পূর্ণ (উপপাদ্য ५.१०)
- সীমিততা সম্পূর্ণতা: ILM সীমিত প্রমাণযোগ্যতা মডেলের জন্য সম্পূর্ণ (উপপাদ্য ५.१३)
- সুস্থতা এবং সম্পূর্ণতা: GLP বহু-প্রমাণযোগ্যতা GLP-মডেলের জন্য সুস্থ এবং শক্তিশালী সম্পূর্ণ (উপপাদ্য ६.२, ६.३)
মান ক্রিপকে মডেল থেকে স্বাধীন প্রমাণযোগ্যতা মডেল সফলভাবে নির্মাণ করা, বিশেষত:
- যেকোনো বিপরীত সুভিধা গাছ কাঠামো এবং নোডে সূত্র সেটের যেকোনো বরাদ্দের জন্য, ন্যূনতম প্রমাণযোগ্যতা মডেল নির্মাণ করা যায়
- দ্বি-সীমিত ক্ষেত্রে, নির্মিত মডেল সিদ্ধান্তযোগ্য
- সোলোভে (१९७६): PA-এর প্রমাণযোগ্যতা যুক্তি প্রতিষ্ঠা করেছেন
- বুলোস (१९९५), স্মোরিনস্কি (१९८५): প্রমাণযোগ্যতা যুক্তির চিরন্তন পাঠ্যপুস্তক
- আর্টেমভ এবং বেকলেমিশেভ (२००४): ব্যাপক সমীক্ষা
- মান ক্রিপকে শব্দার্থবিজ্ঞান: বিভিন্ন মোডাল যুক্তির জন্য ব্যবহৃত
- ভেল্টম্যান মডেল: ব্যাখ্যাযোগ্যতা যুক্তি ILM-এর জন্য ব্যবহৃত
- স্থলাকৃতি শব্দার্থবিজ্ঞান: GLP-এর জন্য সম্পূর্ণতা প্রদান করে
- Iemhoff (२००१-२००३): Iemhoff শব্দার্থবিজ্ঞান প্রবর্তন করেছেন
- মোজতাহেদি (२०२२): প্রথমবার প্রমাণযোগ্যতা মডেল ব্যবহার করে স্বজ্ঞাত প্রমাণযোগ্যতা যুক্তির পাটিগণিত সম্পূর্ণতা প্রতিষ্ঠা করেছেন
- একীভূত কাঠামো: প্রমাণযোগ্যতা মডেল বিভিন্ন মোডাল যুক্তির জন্য একীভূত শব্দার্থবিজ্ঞান কাঠামো প্রদান করে
- গঠনমূলকতা: বিশেষত GL এবং ILM-এর জন্য, গঠনমূলকভাবে স্বাধীন প্রমাণযোগ্যতা মডেল প্রতিষ্ঠা করা যায়
- সিদ্ধান্তযোগ্যতা: উপযুক্ত শর্তে, প্রমাণযোগ্যতা মডেল সিদ্ধান্তযোগ্য
- নমনীয়তা: কাঠামো শর্ত যুক্তি বৈশিষ্ট্য দ্বারা প্রতিস্থাপিত হতে পারে, আরও নমনীয়তা প্রদান করে
- GLP-এর সীমাবদ্ধতা: GLP-এর জন্য, এখনও সিদ্ধান্তযোগ্য প্রমাণযোগ্যতা মডেল শ্রেণী খুঁজে পাওয়া যায়নি
- নির্মাণের জটিলতা: নির্দিষ্ট নির্মাণ (যেমন GLP-এর প্রামাণিক মডেল) গঠনমূলক নাও হতে পারে
- প্রয়োগের পরিধি: প্রধানত প্রমাণযোগ্যতা বৈশিষ্ট্যের যুক্তিতে প্রযোজ্য
পেপারটি স্পষ্টভাবে বেশ কয়েকটি খোলা প্রশ্ন উপস্থাপন করে:
- প্রমাণ যুক্তির সম্প্রসারণ: প্রমাণ যুক্তি LP এবং JGL-এর জন্য প্রমাণযোগ্যতা-শৈলী মডেল সংজ্ঞায়িত করা
- স্বজ্ঞাত মোডাল যুক্তি: দুটি মোডাল অপারেটর □ এবং ◇ সহ স্বজ্ঞাত মোডাল যুক্তির জন্য প্রমাণযোগ্যতা মডেল সংজ্ঞায়িত করা
- GLP-এর সিদ্ধান্তযোগ্য মডেল: GLP-এর সিদ্ধান্তযোগ্য প্রমাণযোগ্যতা মডেল শ্রেণী খুঁজে বের করা
- পাটিগণিত সম্পূর্ণতার সরলীকরণ: প্রমাণযোগ্যতা মডেলের মাধ্যমে ILM-এর পাটিগণিত সম্পূর্ণতা প্রমাণ সরলীকরণ করা যায় কিনা তা অন্বেষণ করা
- তাত্ত্বিক উদ্ভাবন: নতুন শব্দার্থবিজ্ঞান কাঠামো প্রস্তাব করা, বিভিন্ন মোডাল যুক্তির চিকিৎসা একীভূত করা
- প্রযুক্তিগত গভীরতা: বিস্তারিত গাণিতিক প্রমাণ এবং নির্মাণ পদ্ধতি প্রদান করা
- ব্যবহারিক মূল্য: বিশেষত সিদ্ধান্তযোগ্যতার ক্ষেত্রে উন্নতি উল্লেখযোগ্য তাৎপর্য রাখে
- সিস্টেমেটিকতা: মৌলিক মোডাল যুক্তি থেকে জটিল প্রমাণযোগ্যতা যুক্তি পর্যন্ত বিভিন্ন ক্ষেত্রে সিস্টেমেটিকভাবে চিকিৎসা করা
- জটিলতা: নির্দিষ্ট নির্মাণের জটিলতা (বিশেষত GLP) তার ব্যবহারিক প্রয়োগ সীমিত করতে পারে
- খোলা প্রশ্ন: এখনও গুরুত্বপূর্ণ খোলা প্রশ্ন অমীমাংসিত রয়েছে, যেমন GLP-এর সিদ্ধান্তযোগ্য মডেল
- প্রয়োগের পরিধি: প্রধানত তাত্ত্বিক গবেষণায় সীমাবদ্ধ, ব্যবহারিক প্রয়োগ মূল্য আরও অন্বেষণের জন্য অপেক্ষা করছে
- তাত্ত্বিক অবদান: মোডাল যুক্তি শব্দার্থবিজ্ঞানের জন্য নতুন গবেষণা দিকনির্দেশনা প্রদান করে
- পদ্ধতিগত মূল্য: কাঠামো শর্তের যুক্তিকরণ পদ্ধতি সর্বজনীন তাৎপর্য রাখে
- পরবর্তী গবেষণা: স্বজ্ঞাত যুক্তি, প্রমাণ যুক্তি ইত্যাদি ক্ষেত্রের গবেষণার জন্য নতুন সরঞ্জাম প্রদান করে
- প্রমাণযোগ্যতা যুক্তি গবেষণা: বিশেষত পাটিগণিত সম্পূর্ণতা প্রয়োজন এমন গবেষণার জন্য উপযুক্ত
- মোডাল যুক্তি শব্দার্থবিজ্ঞান: জটিল মোডাল যুক্তির জন্য নতুন শব্দার্থবিজ্ঞান পদ্ধতি প্রদান করে
- গণনামূলক যুক্তি: সিদ্ধান্তযোগ্যতা প্রয়োজন এমন প্রয়োগে সম্ভাব্য মূল্য রাখে
পেপারটি সমৃদ্ধ সম্পর্কিত সাহিত্য উদ্ধৃত করে, অন্তর্ভুক্ত করে:
- প্রমাণযোগ্যতা যুক্তির চিরন্তন সাহিত্য (বুলোস, স্মোরিনস্কি, সোলোভে ইত্যাদি)
- মোডাল যুক্তি শব্দার্থবিজ্ঞানের গুরুত্বপূর্ণ কাজ (ব্ল্যাকবার্ন ইত্যাদি)
- ব্যাখ্যাযোগ্যতা যুক্তির মূল গবেষণা (বেরার্ডুচি, শাভ্রুকভ ইত্যাদি)
- স্বজ্ঞাত প্রমাণযোগ্যতা যুক্তির সম্পর্কিত কাজ (Iemhoff ইত্যাদি)
এই পেপারটি মোডাল যুক্তি শব্দার্থবিজ্ঞান ক্ষেত্রে গুরুত্বপূর্ণ তাত্ত্বিক অবদান করেছে, বিভিন্ন প্রমাণযোগ্যতা যুক্তি পরিচালনার জন্য একটি নতুন একীভূত কাঠামো প্রদান করেছে, যখন গঠনমূলকতা এবং সিদ্ধান্তযোগ্যতার ক্ষেত্রে উল্লেখযোগ্য অগ্রগতি অর্জন করেছে। যদিও এখনও কিছু খোলা প্রশ্ন রয়েছে, তবে এই কাজ পরবর্তী গবেষণার জন্য একটি দৃঢ় ভিত্তি স্থাপন করেছে।