केवल Peano arithmetic ही क्यों पर्याप्त है: PA गणना को encode कर सकता है

 (math.stackexchange.com)
1 पॉइंट द्वारा GN⁺ 2025-06-15 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • PA पूरे Goodstein प्रमेय ∀n G(n) को सिद्ध नहीं कर सकता, लेकिन प्रत्येक standard natural number n के लिए PA में G(n) का proof मौजूद है यह PA के भीतर दिखाया जा सकता है
  • मुख्य विचार यह है कि n के लिए जितनी सीमित ऊँचाई वाला ω exponentiation tower चाहिए, केवल उतने तक ही काम किया जाए, और उस दायरे के लिए transfinite induction proof को यांत्रिक रूप से बनाया जाए
  • आवश्यक ऊँचाई m, n की hereditary base notation की ऊँचाई के अनुरूप होती है और O(log*(n)) है; संक्षिप्त notation ω^[m] का उपयोग करने पर proof की लंबाई O(m log m) तक घट जाती है
  • इस परिणाम का अर्थ केवल यह है कि “हर individual case का proof बनाया जा सकता है”, यह नहीं कि PA पूरा Goodstein प्रमेय सिद्ध करता है
  • PA एक ही natural number के भीतर संख्या, pair, list, program state, और formal logic proof—सब encode कर सकता है, इसलिए PA के भीतर यह verify करना भी संभव है कि बनाया गया proof वास्तव में PA proof है

प्रश्न का गणितीय रूप

  • रुचि का विषय यह कथन G(n) है कि Goodstein sequence अंततः 0 तक पहुँचती है

  • ज्ञात भेद इस प्रकार है

    • PA standard natural numbers के प्रत्येक ठोस case, जैसे G(15), G(268), को सिद्ध कर सकता है
    • PA पूरे कथन ∀n ∈ N: G(n) को सिद्ध नहीं कर सकता

  • प्रश्न यह है कि क्या PA निम्न रूप के कथन को सिद्ध कर सकता है

    ∀n ∈ N: ∃p ∈ N: P_PA(p, ⌜G(n)⌝)

  • P_PA(p, ⌜φ⌝) का अर्थ है कि p, PA में φ का proof code है

  • निष्कर्ष यह है कि इस स्तर पर केवल PA ही पर्याप्त है

PA को क्या सिद्ध करना है

  • प्रत्येक n के लिए PA को निम्न तीन बातें दिखानी होती हैं
    • G(n) को सिद्ध करने के लिए आवश्यक proof length की गणना की जा सकती है
    • proof बनाने की प्रक्रिया terminate करती है
    • बने हुए proof का अंतिम वाक्य G(n) की termination बताता है
  • प्रत्येक G(n) के लिए लंबाई O(log*(n) log(log*(n))) वाला PA proof बनाया जा सकता है
  • log* iterated logarithm है, जो बहुत धीरे बढ़ने वाला function है
  • n बढ़ने पर आवश्यक proof भी लंबा होता जाता है, इसलिए केवल इससे PA पूरे Goodstein प्रमेय को सिद्ध नहीं कर सकता

Goodstein sequence और ordinal notation

  • Goodstein sequence में hereditary base notation का उपयोग होता है, और इसका संबंध Cantor normal form में लिखी ordinal अभिव्यक्तियों से है

  • John von Neumann की शैली की construction में ordinals को sets के रूप में बनाया जाता है

    • 0 empty set है
    • यदि कोई ordinal ord है, तो ord ∪ {ord} भी ordinal है
    • यदि ordinals का कोई set X है, तो X का union भी ordinal है

  • Cantor normal form ordinals को निम्न रूप में व्यक्त करता है

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • प्रत्येक ni एक positive natural number है
    • प्रत्येक ordi एक ordinal है
    • ord1 > ord2 > ... > ordk

  • यह notation निम्न ordinal को दर्शाती है

    n1·ω^ord1 + n2·ω^ord2 + ... + nk·ω^ordk

  • तुलना को ord1, n1, ord2, n2 क्रम की lexicographic comparison से किया जाता है, और यदि एक पक्ष पहले समाप्त हो जाए तो छोटा वाला कम माना जाता है

induction से transfinite induction तक

  • PA का पाँचवाँ axiom natural numbers पर induction देता है
    • S(0) सत्य है
    • यदि S(n) है, तो S(s n) भी सत्य है
    • तब सभी natural numbers के लिए S सत्य है
  • PA इससे < को recursively define कर सकता है, और strong induction भी सिद्ध कर सकता है
    • यदि हर n के लिए यह दिखा दिया जाए कि n से छोटे सभी मानों पर S सत्य होने से S(n) सत्य होता है, तो सभी natural numbers पर S सत्य है
  • ZFC में सभी ordinals पर strong induction का रूप transfinite induction सिद्ध किया जा सकता है
  • Cantor normal form में लिखी वस्तुओं के लिए दो गुण उपयोग में आते हैं
    • Cantor normal form में लिखी descending sequences अनिवार्य रूप से finite होती हैं
    • Cantor normal form की वस्तुओं पर transfinite induction लागू किया जा सकता है

PA के भीतर transfinite induction की सीमा

  • PA सभी ordinals पर transfinite induction सिद्ध नहीं कर सकता
  • लेकिन ordinal की कुछ सीमित ऊँचाई वाली ranges को PA के भीतर संभाला जा सकता है
    • PA strong induction सिद्ध कर सकता है, इसलिए ω तक का transfinite induction संभाला जा सकता है
    • इसी तर्क से ω^ω पर transfinite induction भी सिद्ध किया जा सकता है
    • फिर उसी तरीके से ω^(ω^ω), ω^(ω^(ω^ω)) जैसी सीमित ऊँचाई वाली towers पर इसे दोहराया जा सकता है
  • हर चरण का proof केवल tower की ऊँचाई बदलने के साथ यांत्रिक रूप से generated होता है
  • यदि m-वीं tower को सीधे लिखा जाए, तो कुल proof length O(m^2) होती है
  • ω^[m] जैसी shorthand notation के उपयोग से m लिखने में केवल O(log m) लंबाई लगती है, इसलिए कुल proof O(m log m) हो जाता है
  • ε₀ से नीचे के प्रत्येक ordinal के लिए PA के भीतर transfinite induction proof मौजूद है, लेकिन इन्हें एक साथ जोड़ने के लिए infinite length का proof चाहिए होगा
  • यदि PA ε₀ पर transfinite induction सिद्ध कर सके, तो वह PA की consistency सिद्ध कर सकेगा, जो Gödel के second incompleteness theorem से टकराता है

प्रत्येक G(n) के लिए proof generation procedure

  • किसी निश्चित n के लिए hereditary base notation की tower height तक ही आवश्यकता होती है
  • यह ऊँचाई O(log*(n)) है और PA इसे आसानी से computable function के रूप में ले सकता है
  • program input n पर निम्न आउटपुट दे सकता है
    • PA के बारे में सामान्य तथ्यों के proofs
    • यह proof कि G(n) किसी m के लिए ω^[m] के भीतर एक descending sequence को track करता है
    • m की गणना की प्रक्रिया और m के मान का proof
    • ω^[0] पर transfinite induction proof
    • यह proof कि ω^[i] पर transfinite induction, ω^[i+1] पर transfinite induction को imply करता है
    • i = 0 से m-2 तक प्रत्येक चरण के transfinite induction proofs
    • यह proof कि ω^[m-1] पर transfinite induction, ω^[m] के भीतर हर descending sequence के finite होने को imply करता है
    • निष्कर्ष कि G(n) terminate करती है
  • इस procedure के बारे में PA निम्न बातें सिद्ध कर सकता है
    • procedure terminate करती है
    • procedure वाक्यों की एक list generate करती है
    • list की शुरुआत Peano axioms से होती है
    • प्रत्येक वाक्य, उससे पहले के वाक्यों से तर्कसंगत रूप से निकलता है
    • induction से सभी वाक्य सिद्ध हो जाते हैं
    • अंतिम वाक्य “G(n) terminate करती है” है
  • इसलिए PA किसी भी natural number n के लिए यह सिद्ध करता है कि PA, G(n) की termination सिद्ध करता है

PA गणना को कैसे encode करता है

  • “encoding” का अर्थ है यह तय करना कि कोई natural number किसी विशेष संरचना का प्रतिनिधित्व करे
  • PA की बुनियादी सामग्री निम्न है
    • 0
    • successor function (s n)
    • equality
    • nonzero संख्या के लिए predecessor (p n)
    • induction से उचित ठहराई गई recursive definitions
    • 0 या 1 के आधार पर branch करने वाले conditional expressions
  • PA के भीतर निम्न बुनियादी arithmetic functions को recursively define किया जा सकता है
    • <
    • min, max
    • +
    • *
    • exponentiation
    • remainder %
    • integer division //
  • इन functions के बुनियादी गुण PA के भीतर induction से सिद्ध किए जा सकते हैं

एक natural number से data structures बनाना

  • दो natural numbers को एक natural number में encode करने के लिए binary bits को interleave करने की विधि अपनाई जा सकती है
    • odd positions के bits head हैं
    • even positions के bits tail हैं
  • इस तरह बने pair से फिर head और tail निकाले जा सकते हैं
  • pair बना लेने पर linked list भी व्यक्त की जा सकती है
    • 0 को nil के रूप में उपयोग करना
    • empty list
    • आगे element जोड़ना
    • head और tail पढ़ना
    • length निकालना
    • किसी भी position पर access करना
    • insertion और deletion
  • संख्या, pair, और list होने पर stack, queue, tree, text document, virtual machine जैसी संरचनाएँ भी एक ही natural number से व्यक्त की जा सकती हैं

Lisp और computational procedure का encoding

  • Lisp को उसकी parenthesized structure और command and arguments शैली के कारण parsing और interpretation समझाने के लिए सुविधाजनक भाषा के रूप में लिया जाता है
  • PA के भीतर natural numbers को (type, value) pair के रूप में पढ़ा जा सकता है
    • number
    • boolean
    • pair
    • list
    • text आदि
  • कुछ natural numbers किसी खास type के valid values नहीं होंगे, लेकिन valid values uniquely किसी संरचना का प्रतिनिधित्व कर सकते हैं
  • इस encoding के ऊपर Lisp data structures, Lisp virtual machine, और Lisp interpreter बनाए जा सकते हैं
  • Lisp Turing complete है, इसलिए इस रास्ते से किसी भी computable procedure और उसकी state को PA के भीतर encode किया जा सकता है
  • किसी निश्चित step count के बाद की computational state को भी PA के भीतर व्यक्त और track किया जा सकता है

PA, PA के proofs को भी encode करता है

  • first-order logic का proof वाक्यों की एक list के रूप में देखा जा सकता है
    • प्रत्येक वाक्य एक inference step है
    • गलत वाक्य या गलत inference भी लिखे जा सकते हैं, लेकिन verification procedure उन्हें छाँट सकती है
  • PA के भीतर type-proof जैसा type बनाकर proof को वाक्यों की list के रूप में encode किया जा सकता है
  • निम्न verification procedures को भी PA के भीतर encode किया जा सकता है
    • proof सही ढंग से बना है या नहीं, यह जाँचना
    • हर proof step valid है या नहीं, यह जाँचना
    • कौन-से axioms assume किए गए हैं, यह जाँचना
    • अंतिम निष्कर्ष वांछित वाक्य है या नहीं, यह जाँचना
  • यदि किसी axioms के सेट से किसी वाक्य का proof मौजूद है, तो उस proof को दर्शाने वाला कोई विशिष्ट PA natural number भी मौजूद होगा
  • PA उस संख्या के वास्तव में proof code होने की जाँच करने वाली computation को व्यक्त कर सकता है, इसलिए “PA के भीतर proof” को भी PA के भीतर संभाला जा सकता है
  • Gödel ने पूरी computation को encode किए बिना भी PA के भीतर logic को encode किया था, लेकिन programmer के दृष्टिकोण से computation encoding के रास्ते इसे समझना अधिक स्वाभाविक लगता है

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2025-06-15
Hacker News टिप्पणियाँ

  • यह Stack Overflow के एक सवाल को ब्लॉग पोस्ट के रूप में विस्तार देने वाला लेख है
    इसमें Peano axioms से क्या-क्या साबित किया जा सकता है, उसकी सीमाएँ, और उसी के भीतर Lisp को bootstrap करना कैसे शुरू किया जाए—यह शामिल है
    सारे खराब मज़ाक दूसरे सेक्शन में हैं, और सुधार या follow-up सवालों का स्वागत है

    • पूरा लेख पढ़ने पर "Why Lisp?" सेक्शन के (defun not (x) ...) उदाहरण में parentheses matching की एक गड़बड़ी दिखी
      बाद में लिखी गई बात “कंप्यूटर से balanced parentheses ढूँढवाना सचमुच आसान है” से यह जुड़कर काफी मज़ेदार लगा, और "Basic Number Theory" सेक्शन की “closing parentheses का ढेर दिखना बंद हो जाता है” वाली टिप्पणी भी मज़ेदार थी
      मैंने लंबे समय से Lisp नहीं किया है, फिर भी दोबारा साथ-साथ चलते हुए मुख्य बात समझ पाया, इसलिए लेख अच्छा लगा
    • अभी introduction के बाद बहुत ज़्यादा नहीं पढ़ा है, लेकिन यह premise दिलचस्प है कि Goodstein sequences के हर ठोस instance का 0 पर समाप्त होना PA के भीतर साबित किया जा सकता है, पर यह proposition कि सभी sequences समाप्त होती हैं, साबित नहीं किया जा सकता
      Peano axioms भर से computation को encode किया जा सकता है, यह भी अजीब तरह से कमाल का लगता है, जैसे self-reference की एक और layer बन गई हो
      हाल में set theory और पढ़ना शुरू किया और Goodstein sequences तक पहुँचा हूँ; अगली level की advanced set theory textbook या Peano arithmetic को गहराई से कवर करने वाली किताबों की recommendations जानना चाहूँगा
    • boot sector Lisp भी खुद को bootstrap करता है: https://justine.lol/sectorlisp2/
      https://t3x.org के कई Lisp भी cons cells और apply/eval से numbers और बाकी चीज़ें implement करते हैं
      John McCarthy का metacircular evaluator वह code है जिसे Alan Kay ने “software की Maxwell equations” कहा था, और SectorLISP में यह ASSOC EVAL EVCON APPLY EVLIS PAIRLIS जैसे रूप में implement होता है
      कुछ Forth भी मिलते-जुलते हैं, और T3X का Zenlisp eval/apply के एक-दूसरे को recursively call करने के तरीके पर केंद्रित होकर समझाता है: http://t3x.org/zsp/index.html
    • दो जगह “omega” लिखा है, शायद \omega लिखना चाहिए

  • गणित और programming दोनों कर चुके व्यक्ति के रूप में, computation encoding से ज़्यादा मुझे यह बात दिलचस्प लगती है कि Goodstein theorem की independence को इस तरह की self-reference से bypass किया जा सकता है
    लगता है इसका मतलब है कि PA + “PA ω-consistent है” Goodstein theorem को prove कर सकता है, और शायद ε₀ तक transfinite induction भी सामान्य तौर पर संभव हो सकती है
    सुधार: शायद PA + “PA consistent है” ही पर्याप्त हो

    • मूल SO सवाल लिखने वाले के रूप में, मैंने सवाल में कुछ संबंधित answers के links जोड़ दिए हैं
      मूल बात यह है कि “PA consistent है” अकेले पर्याप्त नहीं है; अगर uniform reflection principle हो—“PA जो कुछ prove करता है, वह true है”—तो पर्याप्त है
      यह principle ω-consistency के equivalent है या नहीं, इस पर मैं 100% पक्का नहीं हूँ, लेकिन नीचे की सामग्री देखकर ऐसा ही पढ़ा जाता है: https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      Wikipedia T के ω-consistent होने को “T + RFN_T + सभी true sentences का set consistent है” के रूप में समझाता है, जो “T + RFN_T true है” जैसा ही अर्थ लगता है
    • मुझे यह recursive structure पसंद है
      मूल रूप से आप PA क्या prove करता है, इस पर एक meta-proof बनाते हैं, और अगर आप PA पर भरोसा करते हैं तो उस meta-proof पर भी भरोसा करने लगते हैं
      हालांकि PA + “PA consistent है” कैसे पर्याप्त होगा, यह मुझे साफ़ नहीं है
      वह system standard natural numbers में Goodstein theorem को true रखता है, लेकिन शायद ऐसे models allow करता है जहाँ किसी nonstandard integer N पर Goodstein theorem false हो, और लगता है ठीक उसी case को मजबूत ω-consistency exclude करती है
    • दुर्भाग्य से ऐसा नहीं है, और pure universal formulas भर से दूसरी चीज़ें भी नहीं हो पातीं
      यानी यह Con(PA) के लिए specific समस्या नहीं, बल्कि ज़्यादा general phenomenon है: https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      पहले सवाल के संबंध में, मैं जानना चाहूँगा कि ω-consistency को PA के formula के रूप में कैसे encode किया जाता है
    • Math Exchange पोस्ट में कहा गया है कि PA + ε₀ पर transfinite induction PA की consistency prove करता है
      इसलिए ऐसा लगता है कि PA + “PA consistent है” ε₀ पर transfinite induction prove कर सकता होगा
    • अब इतने confidence से बोलने के लिए details मेरे क्षेत्र से थोड़ा बाहर हैं
      ChatGPT ने कहा कि PA + “PA consistent है” अकेले पर्याप्त नहीं है, और उसने logic textbooks काफी हद तक absorb की होंगी, इसलिए उस दावे पर भरोसा किया जा सकता है

  • पहली बार Peano arithmetic इस्तेमाल करते समय इसकी expressiveness ने काफी चौंकाया था
    शुरुआत में यह basic system जैसा लगता है, लेकिन जब समझ आता है कि computation खुद PA के भीतर encode किया जा सकता है और कई तरह के computations की नकल की जा सकती है, तो जटिल लगने वाली चीज़ें आपस में फिट होने लगती हैं
    ऐसी encoding techniques को beginners के लिए friendly तरीके से समझाने वाले resources की recommendations जानना चाहूँगा

  • यह Boyer-Moore theory से बहुत मिलती-जुलती है। यह theory भी Peano axioms के स्तर से गणित को बनाती है।
    Boyer और Moore ने इस theory के लिए एक automated theorem prover भी बनाया था, और GNU Common Lisp पर चलने वाली उसकी एक कॉपी https://github.com/John-Nagle/nqthm/tree/master पर रखी है।
    उनके समझाने के मुताबिक, program को एक काफ़ी अच्छे math student की तरह सोचना आसान है। सिर्फ़ Peano axioms दे देने पर उससे prime factorization theorem को prove या discover करने की उम्मीद करना मुश्किल है, लेकिन अगर Peano axioms के साथ “addition की commutative law prove करो”, “prove करो कि multiplication, addition पर distribute होता है”, “prove करो कि GCD function का result दोनों arguments को divide करता है” जैसी theorems की list दी जाए, तो वह इसे अच्छी तरह handle कर सकता है।
    पेपर: https://www.cs.utexas.edu/~boyer/acl.pdf

  • Math StackExchange पर JoJoModding को किया गया comment गलत है।
    “PA यह prove कर सकता है कि वह proof बनाता है, लेकिन शायद यह prove न कर पाए कि वह proof finite length का है” वाली explanation असली मुद्दे को गलत पकड़ती है।
    अगर PA “PA X को prove करता है” prove करता है, तो PA X को prove कर सकता है।
    अहम बात यह नहीं है कि nonstandard models हैं, बल्कि यह है कि standard natural numbers model PA का model है।
    इसलिए अगर PA “PA X को prove करता है” prove करता है, तो वास्तव में “PA X को prove करता है” के encoded proof के बराबर एक standard finite natural number होता है, और उस natural number से PA के अंदर X का proof construct किया जा सकता है।

    • दिए गए natural-language version में ambiguity है, इसलिए distinction ज़रूरी है।
      जो दिखाया गया है वह “PA Provable(forall n, G(n)) prove करता है” नहीं, बल्कि “PA forall n, Provable(G(n)) prove करता है” वाला मामला है।
      पहले वाले में सच में “PA forall n, G(n) prove करता है” follow करेगा, लेकिन दूसरा अलग है।
      Goodstein sequence का reference लिए बिना, मैं यह argument देखना चाहूँगा कि किसी general proposition P के लिए forall n, Provable(P(n)) prove करने से Provable(forall n, P(n)) prove नहीं किया जा सकता।
    • “अगर PA ‘PA X को prove करता है’ prove करता है, तो PA X को prove करता है” यह बात सही नहीं है।
      PA के अंदर एक ऐसा function construct किया जा सकता है जो PA द्वारा बनाए जा सकने वाले सभी proofs को search करता है, और इसी आधार पर कोई function और input return करेगा या नहीं, इसका analysis करने वाला will-return function बनाया जा सकता है।
      यह halting problem को solve करने की कोशिश जैसा है, इसलिए हमेशा काम नहीं करता, लेकिन कई cases में काम करता है।
      यहाँ opposite-return बनाया जाए, तो इसे ऐसा construct किया जा सकता है कि given function और input जब return न करें तो return करने की कोशिश करे, और जब return करें तो return न करे।
      standard halting problem proof की तरह (opposite-return opposite-return opposite-return) पर विचार करें, तो PA prove कर सकता है: “अगर PA prove कर सकता है कि opposite-return return करता है, तो वास्तव में वह return नहीं करता”, “अगर PA prove कर सकता है कि वह return नहीं करता, तो वास्तव में वह return करता है”, “अगर PA वह सब कुछ वास्तव में prove कर सकता है जिसे वह खुद prove करने का proof देता है, तो उसे पिछले दो propositions में से किसी एक का proof मिलना चाहिए”, “इसलिए ऐसे case में PA inconsistent है”।
      यह Gödel’s second incompleteness theorem का एक रूप है, और इसलिए “PA prove करता है” और “PA prove करता है कि वह खुद prove करता है” में distinction रखना ज़रूरी है।
    • standard model का PA का model होना तभी सही है जब PA consistent हो, और PA यह prove नहीं कर सकता कि वह consistent है। जब तक वह inconsistent न हो, Gödel theorem की वजह से यह impossible है।
      इसलिए प्रस्तावित proof PA के अंदर काम नहीं करता, और उस comment का main point भी शायद यही हिस्सा है।

  • https://math.stackexchange.com/questions/4408124/what-does-the-kirby-paris-theorem-mean

  • किसी के साथ inductive data types पर बात करते हुए मैंने Lean या Rocq के Nat जैसी zero/succ definition दिखाई।
    सामने वाले ने पूछा, “बस इतना ही? Peano axioms कहाँ हैं? क्या inductive data type से भी ज़्यादा primitive कुछ है?” यह दिलचस्प था।
    इससे याद आया कि Peano axioms को obvious built-in मानने के बजाय कई possible designs में से एक के रूप में देखना बेहतर है।

    • मेरे हिसाब से natural numbers, inductive data types से ज़्यादा primitive हैं।
      क्योंकि सभी inductive data types natural numbers और कुछ primitive type formers, जैसे Π, Σ, =, Ω आदि को साथ इस्तेमाल करके बनाए जा सकते हैं।

  • सिर्फ़ pure lambda calculus भी काफ़ी है। क्योंकि lambda calculus computation को encode करता है।

  • PA की consistency के बारे में, इसे PA के अंदर prove किया जा सकता है: https://youtu.be/6pjLmmkZnIA

    • जो लोग logician नहीं हैं, उनके लिए context बहुत ज़रूरी है।
      Gödel’s second incompleteness theorem दिखाता है कि अगर PA अपनी खुद की consistency prove कर सके, तो PA inconsistent है, और इसलिए false statements समेत कुछ भी prove कर सकता है।
      linked work ने PA की inconsistency नहीं दिखाई है; उसने “अपनी consistency prove करता है” कहने का एक नया, कमजोर meaning define किया और फिर दिखाया कि PA वह कमजोर काम कर सकता है।
      यह interesting work है, लेकिन इसका मतलब समझने के लिए पहले से काफी logic जानना पड़ता है।

  • इस post को 123 points मिले हैं, लेकिन linked SO post पर सिर्फ़ 11 upvotes हैं।

    • Stack Overflow पर upvote करने के लिए 15 reputation points चाहिए होते हैं।
      वहाँ post डालने पर आसानी से delete हो जाने की reputation वाली समस्या में 15-point restriction भी जुड़ जाता है, इसलिए लगता है कि बहुत से लोग upvote नहीं कर पाते।