على كوك:لماذا يكتمل البرهان بعد البرهان لاستقراء واحد فقط عندما يكون لدينا أكثر من متغير واحد؟

Question

لذلك أنا أتعلم كوك.ولقد عثرت على دليل على الترابط بالإضافة إلى ذلك forall (a b c : nat)

على ما يبدو عندما نفعل induction a. بعد intros a b c., ، فإنه يخلق هدفين فرعيين

وبعد ذلك نحتاج ببساطة إلى إثبات أن الطرفين في كلا الهدفين الفرعيين متساويان، واكتمل البرهان.

لذلك أنا فقط أتساءل لماذا لا يتعين علينا القيام بذلك induction b. و induction c. لاستكمال الاثبات؟لماذا فقط أداء الحث على a قادر على استكمال الإثبات؟

أو بمعنى آخر، كيف نحصل على الدالة التي تُرجع الدليل؟ b و c مجانا"؟من الناحية البناءة، ألا نحتاج إلى شيء مثل الحث المزدوج المطبق مرتين؟

Answer 1

أنت لا يملك لإثبات الأشياء عن طريق الاستقراء.على سبيل المثال، يمكنك إثبات $\للجميع ن :\mathbb{N} \,.\, n = n$ بدون الحث عن طريق تطبيق الانعكاسية.في برهانك، نستخدم الحث على $أ$, ولكن بعد ذلك نحن لسنا بحاجة لاستخدام الحث على $ب$ و $ج$ لأنه يمكننا إنهاء البرهان ببساطة باستخدام طرق أخرى.نحن قد يكون له تستخدم الحث على $ب$ و $ج$, ويجب أن تحاول القيام بذلك لترى كيف أن التطبيقات غير الضرورية للاستقراء تجعل برهانك أطول وأقل وضوحًا.

ملاحظة.وهذا لا علاقة له على الإطلاق بالبناء.