यदि दो चीजें बराबर नहीं हैं, तो क्या वे बराबर हैं?

Question

अगर आगाडा, या कुछ अन्य निर्भर रूप से टाइप की गई भाषा में दो मान हैं, तो आप साबित कर सकते हैं कि v₁v₂ के बराबर नहीं है, क्या आप v₁v₂ के बराबर साबित कर सकते हैं?

जैसे, ((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂ के प्रकार का कोई फ़ंक्शन है?

ऐसा लगता है कि यह एक्साइम के रूप में जोड़ने के लिए सुरक्षित है अगर इसे साबित नहीं किया जा सकता है, क्योंकि v₁ ≡ v₂ का अधिकतम मूल्य हो सकता है।

एक कारण यह दिलचस्प है कि डबल अस्वीकरण ((a → ⊥) → ⊥) monad बनाता है। आम तौर पर आप इससे मूल्य निकालने नहीं कर सकते हैं, लेकिन आप कुछ मूल्यों को ⊥ से कर सकते हैं (यदि आप शास्त्रीय तर्क मोनैड में विरोधाभास प्राप्त करते हैं, तो आपके पास एक विरोधाभास है)। मैं सोच रहा था कि समानता एक चीज थी जिसे निकाला जा सकता था।

Answer 1

मुझे लगता है कि कानून आगाडा या कोक में साबित नहीं है।

मोटे तौर पर, हम केवल एक परिकल्पना

(v1 = v2 -> False) -> False 

है और हम थीसिस v1 = v2 साबित करने के लिए की जरूरत है।

अनुक्रम-आधारित प्रमाण प्रणाली में इसका एक कट-मुक्त सबूत पर विचार करें। आखिरी नियम क्या होगा?

यह v1 = v2 का परिचय नहीं हो सकता है, क्योंकि Refl उस प्रकार का नहीं है (v1,v2 विशिष्ट चर हैं)।

इसलिए, यह परिकल्पना की एक उन्मूलन होना चाहिए, यानी

H1: (v1 = v2 -> False) -> False |- v1 = v2 -> False 
H2: (v1 = v2 -> False) -> False , False |- v1 = v2 
--------------------------------------------------- (->E) 
(v1 = v2 -> False) -> False |- v1 = v2 

हालांकि, अगर H1 वास्तव में साध्य है, हम भी

(v1 = v2 -> False) -> False |- False 

होना आवश्यक है जिससे हम प्राप्त

|- ((v1 = v2 -> False) -> False) -> False 

जो

के बराबर है

|- v1 = v2 -> False 

जो v1,v2 पर किसी भी अन्य धारणा के बिना स्पष्ट रूप से साबित नहीं है। दरअसल, अन्यथा हम इसे

|- forall v1 v2, v1 = v2 -> False 

जो सामान्य रूप से गलत है, को सामान्यीकृत कर सकते हैं।

दूसरी तरफ, मेरा मानना ​​है कि आगादा/कोक/... बहिष्कृत मध्य के कानून के अनुरूप हैं, जो प्रस्तावित कानून का तात्पर्य है। इसलिए, कानून स्थिरता का उल्लंघन नहीं कर सकता है।

Answer 2

डबल अस्वीकृति उन्मूलन अंतर्ज्ञानवादी सिद्धांत सिद्धांत में अयोग्य है, जैसा कि यहां प्रस्तुत किया गया है, लेकिन इसकी अस्वीकृति भी अयोग्य है, इसलिए इसे लगातार माना जा सकता है।

हालांकि, शास्त्रीय सिद्धांत सभी प्रकार के लिए साबित नहीं होते हैं, वे निर्णायक प्रकार के लिए साबित होते हैं।डिसाइडेबल प्रकार उन जो provably बसे हुए हैं या निर्जन हैं:

Decidable : Type -> Type 
Decidable A = Either A (A -> False) 

को देखते हुए Decidable A, एक A पर डबल निषेध उन्मूलन को लागू कर सकते हैं: Either A (A -> False) पर सिर्फ पैटर्न मैच, और अगर हम एक A मिलता है, तो हम पूरा कर लें, अगर हमें A -> False मिलते हैं, फिर हम (A -> False) -> False लागू करते हैं और पूर्व falso का उपयोग करते हैं।

एक विशेष मामले के रूप में , i साबित होता है। ई। A में निर्णायक समानता है।

(A -> False) -> False निरंतरता इकाई के रूप में, जब हम इस इकाई हम, शास्त्रीय तर्क के कुछ फार्म प्राप्त monadic यहाँ में शामिल होने के बाद से अंदर काम "चौगुनी" निषेध उन्मूलन, तो not (not (not (not A))) -> not (not A)) से मेल खाती है। हम callCC का भी उपयोग कर सकते हैं, जो Peirce's law, एक और शास्त्रीय बयान के अनुरूप है।

इस बारे में एक दिलचस्प अवलोकन है: हम किसी भी शास्त्रीय सबूत ले सकते हैं, सभी प्रस्तावों को Cont False (दूसरे शब्दों में, उन्हें दोहराएं) को उठाएं, और हमें एक समान रचनात्मक प्रमाण मिलता है जो मूल प्रस्ताव की दोहरी अस्वीकृति साबित करता है। इसका मतलब है कि रचनात्मक तर्क सब कुछ शास्त्रीय तर्क कर सकते हैं, मॉड्यूल शास्त्रीय तार्किक समकक्ष, प्रस्ताव के बाद और इसकी डबल अस्वीकृति शास्त्रीय समकक्ष हैं।