📐 Lean 4 का उपयोग करके प्रपोज़िशनल लॉजिक प्रमाण: एक व्यावहारिक मार्गदर्शिका 🔗

यह पोस्ट Lean 4 प्रोग्रामिंग भाषा और प्रमेय प्रदर्शक (theorem prover) का उपयोग करके मौलिक प्रपोज़िशनल लॉजिक (propositional logic) अवधारणाओं और उनके औपचारिक कार्यान्वयन का एक तकनीकी विवरण प्रदान करती है।

चाहे आप एक गणितज्ञ हों जो प्रमाणों को औपचारिक रूप देना चाहते हैं या एक प्रोग्रामर जो टाइप थ्योरी (type theory) में गहराई से उतर रहे हैं, यह मार्गदर्शिका प्रथम सिद्धांतों से तर्कशास्त्र (logic) का पुनर्निर्माण करती है। हम बुनियादी तार्किक स्थिरांकों से शुरुआत करेंगे और पता लगाएंगे कि Lean 4 किस प्रकार करी-हावर्ड आइसोमोर्फिज्म (Curry-Howard Isomorphism)—यह सिद्धांत कि प्रपोज़िशन (कथन) टाइप हैं और प्रमाण प्रोग्राम हैं—का उपयोग करके तार्किक संरचनाओं को सुंदरता से मॉडल करता है।

📑 विषय-सूची 🔗

⚙️ प्रस्तावना: आधार तैयार करना 🔗

अपने तार्किक संयोजकों (logical connectives) को परिभाषित करने से पहले, हमें एक आधारभूत वातावरण तैयार करने की आवश्यकता है। Lean 4 में, यह आम तौर पर स्कोप और कम्प्यूटेशनल व्यवहार को नियंत्रित करने के लिए दो विशिष्ट कमांड का उपयोग करके किया जाता है।

namespace Basic

noncomputable section

• namespace Basic: यह कमांड हमारी परिभाषाओं को समूहित करता है, जिससे Lean की अंतर्निहित लाइब्रेरी (Prelude) के साथ नामकरण के टकराव को रोका जा सके। यह हमें शैक्षिक उद्देश्यों के लिए True, False, और And जैसी मौलिक संरचनाओं को शून्य से फिर से परिभाषित करने की अनुमति देता है।
• noncomputable section: Lean 4 एक प्रमेय प्रदर्शक और एक फंक्शनल प्रोग्रामिंग भाषा दोनों है। डिफ़ॉल्ट रूप से, यह प्रत्येक परिभाषा के लिए निष्पादन योग्य बाइटकोड जनरेट करने का प्रयास करता है। किसी अनुभाग को noncomputable के रूप में चिह्नित करना कंपाइलर को इस चरण को छोड़ने के लिए कहता है, जो औपचारिक तर्कशास्त्र में आम है जहाँ हम रनटाइम निष्पादन के बजाय गणितीय गुणों की परवाह करते हैं।

🧩 मुख्य तार्किक संयोजक (Core Logical Connectives) 🔗

इस अनुभाग में, हम मानक गणितीय संकेतन को Lean 4 कोड से मैप करते हुए, तर्कशास्त्र के आधारभूत तत्वों को परिभाषित करेंगे।

✅ 1. सत्य / True (⊤) 🔗

सबसे सरल कथन (proposition) वह है जो सार्वभौमिक रूप से तार्किक रूप से मान्य है। प्रोग्रामिंग के संदर्भ में, $\top$ एक Unit टाइप की तरह व्यवहार करता है—इसकी ठीक एक स्थिति होती है और यह कोई अतिरिक्त डेटा नहीं रखता है।

परिभाषा:

inductive True : Prop where
  | intro : True

चूँकि इसे एक एकल कंस्ट्रक्टर (intro) के साथ परिभाषित किया गया है, इसलिए True को “सिद्ध” करने का एकमात्र तरीका यही सटीक कंस्ट्रक्टर प्रदान करना है।

उदाहरण:

-- Proving True unconditionally
example : True := True.intro

-- Any proposition 'a' trivially implies True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. असत्य / False (⊥) 🔗

जहाँ True को प्रमाण के सहज अस्तित्व द्वारा परिभाषित किया जाता है, वहीं False को प्रमाण की पूर्ण अनुपस्थिति द्वारा परिभाषित किया जाता है। यह एक Empty टाइप (या Void टाइप) है।

परिभाषा:

inductive False : Prop

चूँकि False का कोई कंस्ट्रक्टर नहीं है, आप इसे कभी भी शून्य से इंस्टेंशिएट नहीं कर सकते। यह एक तार्किक विरोधाभास का प्रतिनिधित्व करता है।

विस्फोट का सिद्धांत (Ex Falso Quodlibet): यदि आप कभी भी अपने पास False का प्रमाण पाते हैं, तो तर्क टूट जाता है, और आप कुछ भी सिद्ध कर सकते हैं। Lean रिकर्सर False.elim का उपयोग करके इसे संभालता है।

-- From a falsehood, any proposition 'a' follows (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. निषेध / Negation (¬) 🔗

Lean 4 में, निषेध (negation) कोई आदिम, अंतर्निहित अवधारणा नहीं है। इसके बजाय, इसे निहितार्थ (implication) और False का उपयोग करके कार्यात्मक रूप से परिभाषित किया गया है। यह सिद्ध करने के लिए कि कथन $a$ असत्य है (जिसे $\neg a$ द्वारा दर्शाया गया है), आपको एक ऐसा फ़ंक्शन प्रदर्शित करना होगा जहाँ $a$ को मान लेने से सीधे विरोधाभास ($\bot$) उत्पन्न होता है।

परिभाषा:

def Not (a : Prop) : Prop := a → False

मुख्य प्रमेय:

-- Proving Negation: If assuming 'a' proves False, then Not 'a' is true.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- Double Negation Introduction (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' has type (a → False), so passing 'ha' yields False.

-- Modus Tollens: If (a → b) and (¬b), then (¬a)
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. निहितार्थ / Implication (→) 🔗

चूँकि Lean टाइप थ्योरी पर निर्भर करता है, इसलिए तार्किक निहितार्थ ($a \to b$) को शाब्दिक रूप से एक फ़ंक्शन के रूप में माना जाता है। यह सिद्ध करने के लिए कि $a$ का अर्थ $b$ है, आपको एक ऐसा फ़ंक्शन लिखना होगा जो $a$ का कोई भी प्रमाण लेता है और $b$ का प्रमाण लौटाता है।

श्रृंखलाबद्ध निहितार्थ (Chained Implication) उदाहरण: यदि आप $c$ को $a$ में बदल सकते हैं, और $b$ को $d$ में बदल सकते हैं, तो आप $a \to b$ वाले फ़ंक्शन को $c \to d$ वाले फ़ंक्शन में बदल सकते हैं।

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. संयोजन / Conjunction (∧) 🔗

तार्किक संयोजन, जिसके लिए $a$ और $b$ दोनों का सत्य होना आवश्यक है, को एक structure के रूप में मॉडल किया जाता है। प्रोग्रामिंग के संदर्भ में, यह एक Product टाइप (एक स्ट्रक्ट या टपल) है जो साक्ष्य के दो अलग-अलग टुकड़ों को रखता है।

परिभाषा:

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

मुख्य प्रमाण पैटर्न:

-- Introduction: Creating an And
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- Symmetry: a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. वियोजन / Disjunction (∨) 🔗

तार्किक वियोजन के लिए कथनों में से कम से कम एक का सत्य होना आवश्यक है। And के विपरीत, Or एक इंडक्टिव Sum टाइप (एक टैग किया गया यूनियन) है, क्योंकि प्रमाण बनाने के दो अलग-अलग, वैकल्पिक तरीके हैं।

परिभाषा:

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

$a \lor b$ को सिद्ध करने के लिए, आप $a$ के प्रमाण को inl (inject-left) कंस्ट्रक्टर में, या $b$ के प्रमाण को inr (inject-right) कंस्ट्रक्टर में लपेटते हैं।

उदाहरण:

-- Symmetry: a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. तार्किक तुल्यता / Logical Equivalence (↔) 🔗

द्वि-निहितार्थ (Bi-implication), या “यदि और केवल यदि” (Iff), दर्शाता है कि दो कथन तार्किक रूप से समतुल्य हैं। इसे दोनों दिशाओं में निहितार्थ रखने वाली एक संरचना के रूप में परिभाषित किया गया है।

परिभाषा:

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

स्वतुल्यता (Reflexivity) उदाहरण:

-- Every proposition is equivalent to itself (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 निष्कर्ष और मुख्य बातें 🔗

Lean 4 में प्रपोज़िशनल लॉजिक को शून्य से फिर से बनाकर, हम औपचारिक प्रणालियों की यांत्रिक सुंदरता को उजागर करते हैं:

1. डिफ़ॉल्ट रूप से रचनात्मक (Constructive by Default): हम केवल यह कहने के बजाय कि कुछ सत्य है, यह परिभाषित करते हैं कि किसी सत्य का साक्ष्य रखने का क्या अर्थ है।
2. टाइप के रूप में कथन (Propositions as Types): करी-हावर्ड मैपिंग के माध्यम से, तार्किक संयोजक सीधे मानक प्रोग्रामिंग संरचनाओं के अनुरूप होते हैं: निहितार्थ एक फ़ंक्शन है, And एक स्ट्रक्ट है, Or एक एनम (enum) है, True एक यूनिट है, और False वॉइड (void) है।
3. प्रोग्राम के रूप में प्रमाण (Proofs as Programs): Lean में एक गणितीय प्रमाण लिखना एक टाइप-सुरक्षित फ़ंक्शन लिखने के समान है जो एक विशिष्ट सिग्नेचर को संतुष्ट करता है।

इन आधारभूत बिल्डिंग ब्लॉक्स में महारत हासिल करना अधिक जटिल गणितीय प्रमेयों, प्रेडिकेट लॉजिक और जटिल सॉफ़्टवेयर प्रणालियों के सत्यापन से निपटने के लिए आवश्यक महत्वपूर्ण आधार प्रदान करता है।