Niezależność założenia

W teorii dowodu i matematyce konstruktywnej zasada niezależności przesłanek mówi, że jeśli φ i ∃ x θ są zdaniami w teorii formalnej i φ → ∃ x θ jest dowodliwe, to ∃ x (φ → θ) jest dowodliwe. Tutaj x nie może być wolną zmienną φ.

Zasada obowiązuje w logice klasycznej. Jego głównym zastosowaniem jest badanie logiki intuicjonistycznej, gdzie zasada nie zawsze jest ważna.

W logice klasycznej

Zasada niezależności przesłanek obowiązuje w logice klasycznej ze względu na prawo wyłączonego środka . Załóżmy, że φ → ∃ x θ jest dowodliwe. Wtedy, jeśli zachodzi φ, istnieje x spełniające φ → θ , ale jeśli φ nie zachodzi, to dowolne x spełnia φ → θ . W obu przypadkach istnieje x , że φ→θ. Zatem ∃ x (φ → θ) jest dowodliwe.

W logice intuicjonistycznej

Zasada niezależności przesłanek nie jest ogólnie obowiązująca w logice intuicjonistycznej (Avigad i Feferman 1999). Można to zilustrować interpretacją BHK , która mówi, że aby intuicyjnie udowodnić φ → ∃ x θ , należy stworzyć funkcję, która pobiera dowód φ i zwraca dowód ∃ x θ . Tutaj sam dowód jest wejściem do funkcji i może być użyty do skonstruowania x . Z drugiej strony dowód ∃ x (φ → θ) musi najpierw wykazać określone x , a następnie podaj funkcję, która konwertuje dowód φ na dowód θ, w którym x ma tę konkretną wartość.

Jako słaby kontrprzykład załóżmy, że θ( x ) jest rozstrzygalnym predykatem liczby naturalnej takiej, że nie wiadomo, czy dowolny x spełnia θ. Na przykład θ może powiedzieć, że x jest formalnym dowodem pewnego matematycznego przypuszczenia, którego możliwość udowodnienia nie jest znana. Niech φ będzie wzorem ∃ z θ( z ) . Wtedy φ → ∃ x θ jest trywialnie dowodliwe. Jednak aby udowodnić ∃ x (φ → θ) , należy wykazać określoną wartość x tak, że jeśli jakakolwiek wartość x spełnia θ, to ta, która została wybrana, spełnia θ. Nie można tego zrobić, nie wiedząc już, czy ∃ x θ , a zatem ∃ x (φ → θ) nie jest intuicyjnie dowodliwe w tej sytuacji.

• Jeremy Avigad i Solomon Feferman (1999). Interpretacja funkcjonalna Gödla („Dialectica”) (PDF) . w S. Buss ed., The Handbook of Proof Theory, North-Holland. s. 337–405.