استقلال از فرضیه
در نظریه اثبات و ریاضیات سازنده، اصل استقلال از فرضیه بیان میکند که اگر φ و ∃x θ جملههایی در یک نظریه صوری باشند و φ → ∃x θ قابل اثبات باشد، آنگاه ∃x (φ → θ) نیز قابل اثبات است. در اینجا x نمیتواند یک متغیر آزاد در φ باشد، در حالی که θ میتواند یک گزارهای باشد که به x بستگی دارد.
کاربرد اصلی این اصل در مطالعه منطق شهودی است، جایی که این اصل به طور کلی معتبر نیست. اما در منطق کلاسیک، این اصل معتبر است.
بحث
همانطور که معمول است، حوزه گفتمان فرض میشود که مسکونی است. یعنی، بخشی از نظریه حداقل یک جمله است. برای بحث، یکی از این جملهها را به عنوان a در نظر میگیریم. در نظریه اعداد طبیعی، این نقش ممکن است توسط عدد 7 ایفا شود.
به راحتی میتوان ثابت کرد که:
- اگر φ ثابت شود که درست است، آنگاه اگر فرض شود که ∃x θ قابل اثبات است، x ای وجود دارد که φ → θ را برآورده میکند.
- اگر φ ثابت شود که نادرست است، آنگاه به دلیل انفجار، هر گزارهای از شکل φ → ψ درست است. بنابراین، هر x به طور صوری φ → θ را برآورده میکند.
در سناریوی اول، x ای که در فرضیه محدود شده است در نتیجه دوباره استفاده میشود، و به طور کلی a ای که آن را معتبر میکند، نیست. در سناریوی دوم، مقدار a به طور خاص نتیجه اصل را معتبر میکند.
در منطق شهودی
مثال حسابی فوق آنچه که به عنوان یک ضد مثال ضعیف شناخته میشود را ارائه میدهد. ادعای وجود ∃x (φ → θ) نمیتواند با روشهای شهودی اثبات شود.
مثلاً، در نظر بگیرید که حدس گلدباخ یا اثبات دارد یا ندارد. اگر اثبات ندارد، فرض اینکه اثبات دارد، مضحک است و هر چیز دیگری نتیجه میدهد.
مسئله همچنین میتواند با استفاده از تفسیر BHK برای اثباتهای شهودی مورد بررسی قرار گیرد.