Zákon dvojí negace

Zákon dvojité negace  je principem klasické logiky , podle kterého „pokud není pravda , že A není pravdivé, pak A je pravdivé“. Existují 3 formulace zákona dvojí negace. Ve formalizovaném jazyce výrokové logiky jsou vyjádřeny vzorci:

V intuicionistické logice se vyvozuje pouze zákon zavedení dvojité negace, zatímco zákon odčítání se neodvozuje.

V tradiční smysluplné matematice slouží zákon dvojí negace jako logický základ pro provádění tzv. protichůdných důkazů podle následujícího schématu: z předpokladu, že tvrzení A dané matematické teorie je nepravdivé, je v tomto vyvozen rozpor. teorie, pak se na základě konzistence teorie usuzuje , že je nepravdivá „ne A“, a pak se podle zákona o odstranění dvojité negace dochází k závěru, že A je pravdivé. V úvahu připadá, že při uplatnění požadavku algoritmické realizovatelnosti zdůvodnění matematických úsudků se zákon o odstranění dvojité negace ukazuje obecně řečeno jako nepřijatelný.

Typickým příkladem toho je jakýkoli důkaz z opačného výroku A, který má tvar „pro každé x je y takové, že B(x, y)“ je pravdivý, když poslední krok, který spočívá v aplikaci zákona odstranění dvojité negace, se ukazuje jako nemožné kvůli skutečnosti, že konstruktivní chápání úsudku vyžaduje, aby ho ospravedlnilo, konstrukci algoritmu, který by pro každé x dal konstrukci y takovou, že B(x , y) je pravda. Mezitím uvažování pomocí zákona odstranění dvojité negace nevede ke konstrukci žádného algoritmu; navíc hledaný algoritmus v tomto případě nemusí vůbec existovat (viz také princip konstruktivního výběru ).

Jiné znění

Se zákonem vyloučeného středu úzce souvisí zákon dvojí negace a také tzv. Pierceův zákon . V určitém smyslu jsou všechny tři zákony rovnocenné. V intuicionistickém výrokovém počtu, kde tyto zákony nejsou tautologiemi , je tedy každý z těchto dvou zákonů odvoditelný z druhého a přidání jednoho z nich k axiomatice okamžitě vede ke klasické logice . Existují však logiky, ve kterých všechny tři zákony nejsou ekvivalentní [1] .

Pro intuicionistickou logiku existuje slabší forma zákona odčítání - zákon odstranění trojné negace :

.

Poznámky

  1. Zena M. Ariola a Hugo Herbelin. Minimální klasické logické a řídicí operátory. V Třicátém mezinárodním kolokviu o automatech, jazycích a programování, ICALP'03, Eindhoven, Nizozemsko, 30. června - 4. července 2003, svazek 2719 z Lecture Notes in Computer Science, strany 871-885. Springer-Verlag, 2003. [1] Archivováno 18. července 2008 na Wayback Machine