We combine the concepts of modal logics and many-valued logics in a general and comprehensive way. Namely, given any finite linearly ordered set of truth values and any set of propositional connectives defined by truth tables, we define the many-valued minimal normal modal logic, presented as a Gentzen-like sequent calculus, and prove its soundness and strong completeness with respect to many-valued Kripke models. The logic treats necessitation and possibility independently, i.e., they are not defined by each other, so that the duality between them is reflected in the proof system itself. We also prove the finite model property (that implies strong decidability) of this logic and consider some of its extensions. Moreover, we show that there is exactly one way to define negation such that De Morgan's duality between necessitation and possibility holds. In addition, we embed many-valued intuitionistic logic into one of the extensions of our many-valued modal logic.
- পত্র ID: 2501.00489
- শিরোনাম: Many-Valued Modal Logic
- লেখক: Amir Karniel (Technion), Michael Kaminski (Technion)
- শ্রেণীবিভাগ: cs.LO (কম্পিউটার বিজ্ঞানে যুক্তি)
- প্রকাশিত সম্মেলন: Non-Classical Logics Theory and Applications (NCL'24), EPTCS 415, 2024
- পত্র লিঙ্ক: https://arxiv.org/abs/2501.00489
এই পত্রটি একটি সাধারণ এবং সমন্বিত পদ্ধতিতে মডেল যুক্তি এবং বহু-মূল্যবান যুক্তির ধারণাগুলিকে একত্রিত করে। যেকোনো সীমিত রৈখিক ক্রম সত্য-মূল্য সেট এবং সত্য-সারণী দ্বারা সংজ্ঞায়িত যেকোনো প্রস্তাবনামূলক সংযোগকারী সেট দেওয়া হলে, লেখকরা বহু-মূল্যবান ন্যূনতম নিয়মিত মডেল যুক্তি সংজ্ঞায়িত করেন, যা জেনটজেন-শৈলীর ক্রম ক্যালকুলাসের আকারে উপস্থাপিত হয়, এবং বহু-মূল্যবান Kripke মডেলের সাথে সম্পর্কে এর সুস্থতা এবং শক্তিশালী সম্পূর্ণতা প্রমাণ করেন। এই যুক্তি প্রয়োজনীয়তা এবং সম্ভাবনা অপারেটরগুলি স্বাধীনভাবে পরিচালনা করে, অর্থাৎ তারা একে অপরের দ্বারা সংজ্ঞায়িত নয়, তাই তাদের মধ্যে দ্বৈততা প্রমাণ ব্যবস্থায় নিজেই প্রতিফলিত হয়। লেখকরা এই যুক্তির সীমিত মডেল সম্পত্তি (শক্তিশালী সিদ্ধান্তযোগ্যতা নিহিত) প্রমাণ করেন এবং এর কিছু সম্প্রসারণ বিবেচনা করেন। অতিরিক্তভাবে, নেতিবাচকতা সংজ্ঞায়িত করার একমাত্র উপায় প্রদর্শন করা হয়, যাতে প্রয়োজনীয়তা এবং সম্ভাবনার মধ্যে ডি মরগ্যান দ্বৈততা ধারণ করে, এবং বহু-মূল্যবান স্বজ্ঞাত যুক্তিকে বহু-মূল্যবান মডেল যুক্তির একটি সম্প্রসারণে এম্বেড করে।
এই গবেষণার মূল সমস্যা হল বহু-মূল্যবান যুক্তি কাঠামোর অধীনে একটি সর্বজনীন মডেল যুক্তি ব্যবস্থা কীভাবে প্রতিষ্ঠা করা যায়। ঐতিহ্যবাহী মডেল যুক্তি (যেমন K সিস্টেম) দ্বি-মূল্যবান যুক্তির উপর ভিত্তি করে, যখন বাস্তব বিশ্বের অনেক অনুমান পরিস্থিতি অনিশ্চয়তা বা সত্য-মূল্যের ক্রমান্বয়ে জড়িত, যা আরও ভাল মডেলিংয়ের জন্য বহু-মূল্যবান যুক্তির প্রয়োজন।
- তাত্ত্বিক তাৎপর্য: মডেল যুক্তিকে বহু-মূল্যবান সেটিংয়ে প্রসারিত করা, যুক্তি তত্ত্বের জন্য আরও সাধারণ কাঠামো প্রদান করে
- ব্যবহারিক প্রয়োগ: অস্পষ্ট যুক্তি ব্যবস্থা, বহু-এজেন্ট সিস্টেম ইত্যাদি অন্তর্নিহিত অনিশ্চয়তা বা সত্য-মূল্যের ক্রমান্বয় সহ পরিস্থিতিতে গুরুত্বপূর্ণ প্রয়োগ মূল্য রয়েছে
- একীভূত কাঠামো: আরও বিস্তৃত যুক্তি পরিস্থিতি পরিচালনা করতে সক্ষম একটি একীভূত কাঠামো প্রদান করে
বিদ্যমান বহু-মূল্যবান মডেল যুক্তি গবেষণায় নিম্নলিখিত সীমাবদ্ধতা রয়েছে:
- বেশিরভাগ সংযোগকারীর নির্দিষ্ট সেটের উপর ভিত্তি করে (যেমন Łukasiewicz সংযোগকারী)
- সাধারণত শুধুমাত্র প্রয়োজনীয়তা অপারেটর □ পরিচালনা করে, সম্ভাবনা অপারেটর ◇কে □-এর দ্বৈত হিসাবে সংজ্ঞায়িত করে
- যেকোনো সত্য-মূল্য সেট এবং সংযোগকারী পরিচালনা করার জন্য একটি একীভূত কাঠামোর অভাব
- শক্তিশালী সম্পূর্ণতা এবং শক্তিশালী সিদ্ধান্তযোগ্যতার ক্ষেত্রে সীমিত ফলাফল
লেখকদের গবেষণা প্রেরণা নিম্নলিখিতে নিহিত:
- একটি সম্পূর্ণ সর্বজনীন বহু-মূল্যবান মডেল যুক্তি কাঠামো প্রতিষ্ঠা করা
- □ এবং ◇ অপারেটরগুলি স্বাধীনভাবে পরিচালনা করা, তাদের পারস্পরিক সংজ্ঞাকে অনুমান না করে
- শক্তিশালী সম্পূর্ণতা এবং শক্তিশালী সিদ্ধান্তযোগ্যতার তাত্ত্বিক গ্যারান্টি প্রদান করা
- বহু-মূল্যবান মডেল যুক্তি এবং অন্যান্য যুক্তি ব্যবস্থার সম্পর্ক অন্বেষণ করা
- সর্বজনীন বহু-মূল্যবান মডেল যুক্তি mv-K প্রস্তাব করা: যেকোনো সীমিত রৈখিক ক্রম সত্য-মূল্য সেট এবং যেকোনো প্রস্তাবনামূলক সংযোগকারী সেটের জন্য প্রযোজ্য
- □ এবং ◇ পরিচালনার জন্য স্বাধীন প্রক্রিয়া প্রতিষ্ঠা করা: দুটির পারস্পরিক সংজ্ঞাকে অনুমান না করে, প্রমাণ ব্যবস্থায় সরাসরি দ্বৈততা প্রতিফলিত করা
- শক্তিশালী সম্পূর্ণতা এবং শক্তিশালী সিদ্ধান্তযোগ্যতা প্রমাণ করা: নিয়মিত মডেল উপপাদ্য এবং সীমিত মডেল সম্পত্তির মাধ্যমে
- সম্পূর্ণ সম্প্রসারণ ব্যবস্থা নির্মাণ করা: mv-D, mv-T, mv-K4, mv-S4, mv-B, mv-S5 ইত্যাদি সম্প্রসারণ সহ
- নেতিবাচকতার অনন্য সংজ্ঞা চিহ্নিত করা: যাতে □ এবং ◇ ডি মরগ্যান দ্বৈততা সন্তুষ্ট করে
- বহু-মূল্যবান স্বজ্ঞাত যুক্তির এম্বেডিং বাস্তবায়ন করা: বহু-মূল্যবান স্বজ্ঞাত যুক্তিকে mv-S4-এ এম্বেড করা
এই পত্রের কাজ হল প্রদত্ত সত্য-মূল্য সেট V = {v₁, v₂, ..., vₙ} (যেখানে v₁ < v₂ < ... < vₙ) এবং যেকোনো প্রস্তাবনামূলক সংযোগকারী সেটের জন্য একটি বহু-মূল্যবান মডেল যুক্তি ব্যবস্থা mv-K সংজ্ঞায়িত করা, যাতে এটি:
- শব্দার্থগতভাবে বহু-মূল্যবান Kripke মডেলের উপর ভিত্তি করে
- বাক্যগতভাবে চিহ্নিত সূত্রের ক্রম ক্যালকুলাস গ্রহণ করে
- সুস্থতা এবং শক্তিশালী সম্পূর্ণতা রয়েছে
- সীমিত মডেল সম্পত্তি সন্তুষ্ট করে
বহু-মূল্যবান Kripke মডেল তিন-গুণ M = ⟨W,R,I⟩ হিসাবে সংজ্ঞায়িত, যেখানে:
- W সম্ভাব্য বিশ্বের অ-খালি সেট
- R হল W-এর উপর অ্যাক্সেসযোগ্যতা সম্পর্ক
- I: W × P → V হল মূল্যায়ন ফাংশন
মডেল অপারেটরের শব্দার্থ:
- I(u,□φ) = inf({I(v,φ) : v ∈ S(u)})، যেখানে inf(∅) = vₙ
- I(u,◇φ) = sup({I(v,φ) : v ∈ S(u)})، যেখানে sup(∅) = v₁
চিহ্নিত সূত্র: (φ,k) ফর্মের জোড়া, যা সূত্র φ-এর সত্য-মূল্য vₖ হওয়া নির্দেশ করে
ক্রম: Γ → Δ ফর্মের অভিব্যক্তি, যেখানে Γ এবং Δ চিহ্নিত সূত্রের সীমিত সেট
স্বতঃসিদ্ধ ব্যবস্থা অন্তর্ভুক্ত করে:
- পরিচয় স্বতঃসিদ্ধ: (φ,k) → (φ,k)
- সংযোগকারী স্বতঃসিদ্ধ: সত্য-সারণী দ্বারা সংজ্ঞায়িত স্বতঃসিদ্ধ
- মডেল নিয়ম:
- □ নিয়ম: (φ,k) → Γ× / (□φ,k),Γ → (k ≠ n)
- ◇ নিয়ম: (φ,k) → Γ× / (◇φ,k),Γ → (k ≠ 1)
যেখানে Γ×-এর সংজ্ঞা মডেল অপারেটরের শব্দার্থিক সীমাবদ্ধতা প্রতিফলিত করে।
- চিহ্নিত সূত্র পদ্ধতি: চিহ্নিত সূত্র (φ,k) ব্যবহার করে সরাসরি সত্য-মূল্য তথ্য প্রকাশ করা, নির্দিষ্ট মূল্যের সীমাবদ্ধতা এড়ানো
- স্বাধীন মডেল পরিচালনা: □ এবং ◇ স্বাধীন আদিম অপারেটর হিসাবে, নেতিবাচকতার মাধ্যমে পারস্পরিক সংজ্ঞা নয়
- সর্বজনীন সংযোগকারী পরিচালনা: সত্য-সারণীর মাধ্যমে যেকোনো প্রস্তাবনামূলক সংযোগকারী একীভূতভাবে পরিচালনা করা
- শক্তিশালী সম্পূর্ণতা প্রমাণ: নিয়মিত মডেল নির্মাণের মাধ্যমে শক্তিশালী সম্পূর্ণতা বাস্তবায়ন করা
এই পত্রটি প্রধানত তাত্ত্বিক বিশ্লেষণ এবং প্রমাণ যাচাইকরণ পরিচালনা করে, যার মধ্যে রয়েছে:
- সুস্থতা প্রমাণ: প্রাপ্তির দৈর্ঘ্যের উপর আবেগপ্রবণ প্রমাণের মাধ্যমে সমস্ত নিয়ম শব্দার্থগতভাবে বৈধ প্রমাণ করা
- শক্তিশালী সম্পূর্ণতা প্রমাণ: নিয়মিত মডেল উপপাদ্যের মাধ্যমে শব্দার্থিক অনুমানের সম্পূর্ণতা প্রমাণ করা
- সীমিত মডেল সম্পত্তি প্রমাণ: ফিল্টারিং কৌশলের মাধ্যমে প্রতিটি যুক্তির সীমিত মডেল সম্পত্তি প্রমাণ করা
পত্রটি তাত্ত্বিক ফলাফল যাচাই করার জন্য একাধিক নির্দিষ্ট উদাহরণ ব্যবহার করে:
উদাহরণ 2: ক্রম (□φ,k) → (◇φ,k)⁺ mv-K-তে প্রাপ্য প্রমাণ করা (k ≠ n)
উদাহরণ 5: তিন-মূল্যবান Łukasiewicz যুক্তির মডেল সম্প্রসারণে প্রমাণ করা:
(□(p ⊃ q),3),(□p,3) → (□q,3)
এই উদাহরণগুলি ব্যবস্থার প্রকাশনীয় ক্ষমতা এবং অনুমান ক্ষমতা প্রদর্শন করে।
উপপাদ্য 6 (সুস্থতা এবং শক্তিশালী সম্পূর্ণতা):
ক্রম সেট Σ এবং ক্রম Γ → Δ-এর জন্য, Σ ⊢ Γ → Δ যদি এবং শুধুমাত্র যদি Σ ⊨ Γ → Δ
উপপাদ্য 21 (সম্প্রসারণের সম্পূর্ণতা):
- mv-D সিরিয়াল Kripke মডেলের সাথে সম্পর্কে সুস্থ এবং শক্তিশালী সম্পূর্ণ
- mv-T স্বতঃসম্পর্কিত Kripke মডেলের সাথে সম্পর্কে সুস্থ এবং শক্তিশালী সম্পূর্ণ
- mv-K4 ট্রানজিটিভ Kripke মডেলের সাথে সম্পর্কে সুস্থ এবং শক্তিশালী সম্পূর্ণ
- mv-S4 প্রি-অর্ডার Kripke মডেলের সাথে সম্পর্কে সুস্থ এবং শক্তিশালী সম্পূর্ণ
- mv-B সমতাপূর্ণ Kripke মডেলের সাথে সম্পর্কে সুস্থ এবং শক্তিশালী সম্পূর্ণ
- mv-S5 সমতুল্য সম্পর্ক Kripke মডেলের সাথে সম্পর্কে সুস্থ এবং শক্তিশালী সম্পূর্ণ
উপপাদ্য 24 (সীমিত মডেল সম্পত্তি):
বিবেচিত সমস্ত যুক্তির সীমিত মডেল সম্পত্তি রয়েছে
অনুসিদ্ধান্ত 25 (শক্তিশালী সিদ্ধান্তযোগ্যতা):
বিবেচিত সমস্ত যুক্তি শক্তিশালী সিদ্ধান্তযোগ্য
উপপাদ্য 28:
¬ একটি একক-স্থান সংযোগকারী হোক, তাহলে ক্রম (◇φ,k) → (¬□¬φ,k) এবং (□φ,k) → (¬◇¬φ,k) mv-K-তে প্রাপ্য যদি এবং শুধুমাত্র যদি সমস্ত k = 1,2,...,n-এর জন্য, ¬(vₖ) = vₙ₋ₖ₊₁
এটি ডি মরগ্যান দ্বৈততা ধারণের নেতিবাচকতা সংজ্ঞার অনন্যতা প্রমাণ করে।
উপপাদ্য 32:
Σ ⊨ₘᵥᵢₗ Γ → Δ যদি এবং শুধুমাত্র যদি Σᵗ ⊨_C Γᵗ → Δᵗ, যেখানে C প্রি-অর্ডার Kripke মডেলের শ্রেণী
এটি বহু-মূল্যবান স্বজ্ঞাত যুক্তি থেকে mv-S4-এ সম্পূর্ণ এম্বেডিং প্রতিষ্ঠা করে।
পত্রটি বহু-মূল্যবান মডেল যুক্তির সম্পর্কিত গবেষণা বিস্তারিতভাবে পর্যালোচনা করে:
- নির্দিষ্ট সংযোগকারীর উপর ভিত্তি করে পদ্ধতি: যেমন Ostermann-এর n-মূল্যবান Łukasiewicz মডেল যুক্তি
- ম্যাট্রিক্স পদ্ধতি: যেমন Morikawa-এর তিন-মূল্যবান যুক্তির উপর ভিত্তি করে মডেল যুক্তি
- সাধারণ পদ্ধতি: যেমন Fitting-এর সীমিত জালির উপর ভিত্তি করে পদ্ধতি, Takano-এর ম্যাট্রিক্স চিহ্নিত সূত্র পদ্ধতি
বিদ্যমান কাজের তুলনায়, এই পত্রের সুবিধা হল:
- বৃহত্তর সর্বজনীনতা: যেকোনো সত্য-মূল্য সেট এবং সংযোগকারীর জন্য প্রযোজ্য
- স্বাধীন মডেল পরিচালনা: □ এবং ◇ একসাথে পরিচালনা করা যখন পারস্পরিক সংজ্ঞাকে অনুমান না করে
- শক্তিশালী তাত্ত্বিক গ্যারান্টি: শক্তিশালী সম্পূর্ণতা এবং শক্তিশালী সিদ্ধান্তযোগ্যতা
- একীভূত কাঠামো: সমস্ত মৌলিক যুক্তি সম্প্রসারণ অন্তর্ভুক্ত করে
- সফলভাবে সর্বজনীন বহু-মূল্যবান মডেল যুক্তি কাঠামো mv-K এবং এর সম্প্রসারণ প্রতিষ্ঠা করা
- সমস্ত ব্যবস্থার শক্তিশালী সম্পূর্ণতা এবং শক্তিশালী সিদ্ধান্তযোগ্যতা প্রমাণ করা
- ডি মরগ্যান দ্বৈততা ধারণের অনন্য নেতিবাচকতা সংজ্ঞা চিহ্নিত করা
- বহু-মূল্যবান স্বজ্ঞাত যুক্তির সম্পূর্ণ এম্বেডিং বাস্তবায়ন করা
- রৈখিক ক্রম সীমাবদ্ধতা: বর্তমান কাঠামো সত্য-মূল্য সেটকে রৈখিক ক্রম হতে প্রয়োজন করে, আংশিক ক্রম কাঠামো সরাসরি পরিচালনা করতে পারে না
- সীমিততা প্রয়োজনীয়তা: শুধুমাত্র সীমিত সত্য-মূল্য সেট বিবেচনা করা
- প্রমাণ বিস্তারিত অপর্যাপ্ত: পৃষ্ঠা সীমাবদ্ধতার কারণে, অনেক গুরুত্বপূর্ণ প্রমাণ বাদ দেওয়া হয়েছে
- আংশিক ক্রম সত্য-মূল্য কাঠামোতে প্রসারিত করা
- অসীম সত্য-মূল্য সেট বিবেচনা করা
- গণনামূলক জটিলতা অধ্যয়ন করা
- আরও যুক্তি ব্যবস্থার এম্বেডিং অন্বেষণ করা
- উল্লেখযোগ্য তাত্ত্বিক অবদান: সবচেয়ে সর্বজনীন বহু-মূল্যবান মডেল যুক্তি কাঠামো প্রতিষ্ঠা করা
- প্রযুক্তিগত পদ্ধতি উদ্ভাবন: মডেল অপারেটর স্বাধীনভাবে পরিচালনা করা, চিহ্নিত সূত্র প্রযুক্তি ব্যবহার করা
- শক্তিশালী ফলাফল সম্পূর্ণতা: সুস্থতা, শক্তিশালী সম্পূর্ণতা, সিদ্ধান্তযোগ্যতা ইত্যাদি মূল বৈশিষ্ট্য অন্তর্ভুক্ত করে
- শক্তিশালী সিস্টেমেটিকতা: সমস্ত প্রধান মডেল যুক্তি সম্প্রসারণ একীভূতভাবে পরিচালনা করা
- সীমিত ব্যবহারিক প্রয়োগ: প্রধানত তাত্ত্বিক অবদান, নির্দিষ্ট প্রয়োগ পরিস্থিতির যাচাইকরণের অভাব
- অপর্যাপ্ত প্রমাণ বিস্তারিত: পৃষ্ঠা সীমাবদ্ধতার কারণে, অনেক গুরুত্বপূর্ণ প্রমাণ বাদ দেওয়া হয়েছে
- অনুপস্থিত গণনামূলক জটিলতা বিশ্লেষণ: সিদ্ধান্ত সমস্যার নির্দিষ্ট জটিলতা বিশ্লেষণ করা হয়নি
- তাত্ত্বিক প্রভাব: বহু-মূল্যবান মডেল যুক্তি গবেষণার জন্য একটি একীভূত তাত্ত্বিক ভিত্তি প্রদান করা
- পদ্ধতি প্রভাব: চিহ্নিত সূত্র এবং স্বাধীন মডেল পরিচালনার পদ্ধতি প্রচারের মূল্য রয়েছে
- প্রয়োগ সম্ভাবনা: অস্পষ্ট অনুমান, অনিশ্চয়তা মডেলিং ইত্যাদি ক্ষেত্রে প্রয়োগ সম্ভাবনা রয়েছে
- অস্পষ্ট যুক্তি ব্যবস্থা: অনিশ্চয়তা সহ অনুমান পরিচালনা করা
- বহু-এজেন্ট সিস্টেম: এজেন্টের বিশ্বাস এবং জ্ঞান মডেলিং করা
- অসম্পূর্ণ তথ্য অনুমান: আংশিক তথ্যের অধীনে মডেল অনুমান পরিচালনা করা
- তাত্ত্বিক যুক্তি গবেষণা: বহু-মূল্যবান যুক্তি এবং মডেল যুক্তির সমন্বয় অধ্যয়নের ভিত্তি কাঠামো হিসাবে
পত্রটি 24টি সম্পর্কিত তথ্যসূত্র উদ্ধৃত করে, যা বহু-মূল্যবান যুক্তি, মডেল যুক্তি, স্বজ্ঞাত যুক্তি ইত্যাদি একাধিক ক্ষেত্রের গুরুত্বপূর্ণ কাজ অন্তর্ভুক্ত করে, যার মধ্যে রয়েছে:
- Kripke-এর ক্লাসিক্যাল মডেল যুক্তি শব্দার্থ কাজ
- Fitting-এর বহু-মূল্যবান মডেল যুক্তির যুগান্তকারী গবেষণা
- Takano-এর বহু-মূল্যবান স্বজ্ঞাত যুক্তির কাজ
- বিভিন্ন বহু-মূল্যবান যুক্তি ব্যবস্থার গবেষণা
সামগ্রিক মূল্যায়ন: এটি বহু-মূল্যবান মডেল যুক্তি ক্ষেত্রে একটি উচ্চ-মানের তাত্ত্বিক যুক্তি বিজ্ঞান পত্র, যা গুরুত্বপূর্ণ তাত্ত্বিক অবদান করেছে। পত্রটি দ্বারা প্রতিষ্ঠিত সর্বজনীন কাঠামো শক্তিশালী তাত্ত্বিক মূল্য এবং সম্ভাব্য প্রয়োগ সম্ভাবনা রয়েছে, এবং এই ক্ষেত্রের একটি গুরুত্বপূর্ণ অগ্রগতি।