Rozhodnutelnost (logika) - Decidability (logic)
V logice , pravda / nepravda rozhodnutí problémem je rozhodnutelný jestli existuje účinný způsob pro odvozování správnou odpověď. Logické systémy, jako je propoziční logika, jsou rozhodnutelné, pokud lze účinně určit členství v jejich sadě logicky platných vzorců (nebo vět). Teorie (sada vět uzavřených za logický důsledek ) v pevné logického systému rozhodnutelný v případě, že je efektivní metoda pro určení, zda se libovolná vzorce zahrnuty v teorii. Mnoho důležitých problémů je nerozhodnutelných , to znamená, že bylo prokázáno, že pro ně nemůže existovat žádná účinná metoda pro určení členství (vrácení správné odpovědi po konečném, i když ve všech případech možná velmi dlouhém čase).
Rozhodnutelnost logického systému
Každý logický systém je dodáván jak se syntaktickou složkou , která mimo jiné určuje pojem prokazatelnosti , tak se sémantickou složkou , která určuje pojem logické platnosti . Logicky platné vzorce systému se někdy nazývají věty systému, zvláště v kontextu logiky prvního řádu, kde Gödelova věta o úplnosti stanoví ekvivalenci sémantického a syntaktického důsledku. V jiných nastaveních, jako je lineární logika , lze k definování vět systému použít vztah syntaktických důsledků (prokazatelnosti).
Logický systém je rozhodnutelný, pokud existuje účinná metoda pro určení, zda libovolné vzorce jsou věty logického systému. Například je možné rozhodnout o výrokové logice , protože pomocí metody tabulky pravdivosti lze určit, zda je libovolný výrokový vzorec logicky platný.
Logika prvního řádu není obecně rozhodnutelná; zejména soubor logických validit v každém podpisu, který zahrnuje rovnost a alespoň jeden další predikát se dvěma nebo více argumenty, není rozhodnutelný. Logické systémy rozšiřující logiku prvního řádu, jako je logika druhého řádu a teorie typů , jsou také nerozhodnutelné.
O validitě monadického predikátového počtu s identitou je však možné rozhodnout. Tento systém je logikou prvního řádu omezenou na ty podpisy, které nemají žádné funkční symboly a jejichž vztahové symboly jiné než rovnost nikdy neberou více než jeden argument.
Některé logické systémy nejsou dostatečně reprezentovány pouze sadou vět. (Například Kleeneova logika nemá vůbec žádné věty.) V takových případech se často používají alternativní definice rozhodnutelnosti logického systému, které požadují efektivní metodu pro určení něčeho obecnějšího, než je pouhá platnost vzorců; například platnost sekvencí nebo vztah důsledků {(Г, A ) | Г A of logiky.
Rozhodnutelnost teorie
Teorie je množina formulí, často předpokládá, že bude uzavřen za logický důsledek . Rozhodnutelnost pro teorii se týká toho, zda existuje účinný postup, který rozhoduje o tom, zda je vzorec členem teorie nebo ne, vzhledem k libovolnému vzorci v podpisu teorie. Problém rozhodnutelnosti vzniká přirozeně, když je teorie definována jako soubor logických důsledků pevné sady axiomů.
O rozhodovatelnosti teorií existuje několik základních výsledků. Každá ( neparakonzistentní ) nekonzistentní teorie je rozhodnutelná, protože každá formule v podpisu teorie bude logickým důsledkem teorie, a tedy jejím členem. Každá úplná rekurzivně vyčíslitelná teorie prvního řádu je rozhodnutelná. Rozšíření teorie s rozhodováním nemusí být rozhodnutelné. Například v propoziční logice existují nerozhodnutelné teorie, i když o souboru validit (nejmenší teorie) lze rozhodnout.
Konzistentní teorie, která má tu vlastnost, že každé konzistentní rozšíření je nerozhodnutelné, je údajně v podstatě nerozhodnutelná . Ve skutečnosti bude každé konzistentní rozšíření v podstatě nerozhodnutelné. Teorie polí je nerozhodnutelná, ale není v podstatě nerozhodnutelná. O Robinsonově aritmetice je známo, že je v podstatě nerozhodnutelná, a tudíž každá konzistentní teorie, která zahrnuje nebo interpretuje Robinsonovu aritmetiku, je také (v podstatě) nerozhodnutelná.
Mezi příklady rozhodovatelných teorií prvního řádu patří teorie reálných uzavřených polí a Presburgerova aritmetika , zatímco teorie skupin a Robinsonova aritmetika jsou příklady nerozhodnutelných teorií.
Některé rozhodovatelné teorie
Mezi některé rozhodnutelné teorie patří (Monk 1976, s. 234):
- Soubor logických validit prvního řádu v podpisu s jedinou rovností, vytvořený Leopoldem Löwenheimem v roce 1915.
- Soubor logických validit prvního řádu v podpisu s rovností a jednou unární funkcí, zavedený Ehrenfeuchtem v roce 1959.
- Teorie prvního řádu přirozených čísel v podpisu s rovností a sčítáním, nazývaná také Presburgerova aritmetika . Úplnost stanovil Mojżesz Presburger v roce 1929.
- Teorie prvního řádu přirozených čísel v podpisu s rovností a násobením, nazývaná také Skolemova aritmetika .
- Teorie prvního řádu booleovských algeber , kterou založil Alfred Tarski v roce 1940 (nalezena v roce 1940, ale vyhlášena v roce 1949).
- Teorie prvního řádu algebraicky uzavřených polí dané charakteristiky, kterou vytvořil Tarski v roce 1949.
- Teorie prvního řádu v reálném uzavřených objednaných polí , zřízený Tarski v roce 1949 (viz též exponenciální funkce problém Tarski ).
- Teorie prvního řádu euklidovské geometrie , kterou založil Tarski v roce 1949.
- Teorie prvního řádu abelianských skupin , kterou založil Szmielew v roce 1955.
- Teorie prvního řádu hyperbolické geometrie , kterou vytvořil Schwabhäuser v roce 1959.
- Specifické rozhodnutelné podjazyky teorie množin zkoumané v 80. letech minulého století až dodnes. (Cantone et al. , 2001)
Mezi metody používané k stanovení rozhodnutelnosti patří eliminace kvantifikátoru , úplnost modelu a test Łoś-Vaught .
Některé nerozhodnutelné teorie
Mezi některé nerozhodnutelné teorie patří (Monk 1976, s. 279):
- Soubor logických validit v libovolném podpisu prvního řádu s rovností a buď: vztahovým symbolem arity ne méně než 2, nebo dvěma unárními funkčními symboly, nebo jedním funkčním symbolem arity ne méně než 2, zavedeným Trakhtenbrotem v roce 1953.
- Teorie prvního řádu přirozených čísel s přidáním, násobením a rovností, kterou založili Tarski a Andrzej Mostowski v roce 1949.
- Teorie prvního řádu racionálních čísel sčítáním, násobením a rovností, kterou založila Julia Robinson v roce 1949.
- Teorie prvního řádu skupin, kterou vytvořil Alfred Tarski v roce 1953. Pozoruhodné je, že nerozhodnutelná je nejen obecná teorie skupin, ale také několik konkrétnějších teorií, například (podle Mal'ceva 1961) teorie konečných skupin . Mal'cev také prokázal, že teorie poloskupin a teorie prstenů jsou nerozhodnutelné. Robinson v roce 1949 zjistil, že teorie polí je nerozhodnutelná.
- Robinsonova aritmetika (a tedy jakékoli konzistentní rozšíření, jako je Peanoova aritmetika ) je v podstatě nerozhodnutelná, jak ji stanovil Raphael Robinson v roce 1950.
- Teorie prvního řádu s rovností a dvěma funkčními symboly
Metoda interpretovatelnosti se často používá ke stanovení nerozhodnutelnosti teorií. Pokud je v podstatě nerozhodnutelná teorie T interpretovatelná v konzistentní teorii S , pak S je také v podstatě nerozhodnutelná. To úzce souvisí s konceptem mnohočetného snížení teorie vypočítatelnosti.
Semidecidability
Vlastností teorie nebo logického systému slabší než rozhodovatelnost je semidecidability . Teorie je semidecidable, pokud existuje účinná metoda, která, daná libovolným vzorcem, vždy správně řekne, kdy je vzorec v teorii, ale může dát buď zápornou odpověď, nebo žádnou odpověď, když vzorec není v teorii. Logický systém je semidecidable, pokud existuje účinná metoda pro generování vět (a pouze vět) tak, že každá věta bude nakonec generována. To se liší od rozhodnutelnosti, protože v semidecidable systému nemusí existovat účinný postup pro kontrolu, že vzorec není věta.
Každá rozhodnutelná teorie nebo logický systém je semidecidable, ale obecně platí, že opak není pravdivý; teorie je rozhodnutelná tehdy a jen tehdy, pokud jsou jak ona, tak její doplněk polorozhodnutelné. Například sada logických validit V logiky prvního řádu je polorozhodnutelná, ale nerozhodnutelná. V tomto případě, je to proto, že neexistuje žádná účinná metoda pro určení pro libovolný vzorce A , zda není v V . Podobně je řada logických důsledků jakékoli rekurzivně vyčíslitelné množiny axiomů prvního řádu polorozhodnutelná. Mnoho z výše uvedených příkladů nerozhodnutelných teorií prvního řádu má tuto formu.
Vztah s úplností
Rozhodnutelnost by neměla být zaměňována s úplností . Například teorie algebraicky uzavřených polí je rozhodnutelná, ale neúplná, zatímco množina všech pravdivých tvrzení prvního řádu o nezáporných celých číslech v jazyce s + a × je úplná, ale nerozhodnutelná. Bohužel, jako terminologická nejednoznačnost je někdy termín „nerozhodnutelné tvrzení“ používán jako synonymum pro nezávislé prohlášení .
Vztah k vyčíslitelnosti
Stejně jako u konceptu rozhodovatelné množiny lze definici rozhodovatelné teorie nebo logického systému podat buď z hlediska efektivních metod, nebo z hlediska vyčíslitelných funkcí . Ty jsou obecně považovány za ekvivalentní podle církevních tezí . Skutečně, důkaz, že logický systém nebo teorie je nerozhodnutelná, použije formální definici vyčíslitelnosti k prokázání, že vhodná množina není množina, o níž lze rozhodnout, a poté vyvolá Churchovu tezi, aby ukázala, že teorii nebo logický systém nelze rozhodnout žádným efektivním metoda (Enderton 2001, s. 206 a násl. ).
V kontextu her
Některé hry byly klasifikovány podle jejich rozhodnutelnosti:
- Šachy jsou rozhodnutelné. Totéž platí pro všechny ostatní konečné hry pro dva hráče s dokonalými informacemi.
- Mate in n v nekonečném šachu (s omezeními pravidel a her) je rozhodnutelné. Existují však pozice (s konečným počtem kusů), které jsou vynucené výhry, ale nejsou spojeny v n pro žádné konečné n .
- Některé týmové hry s nedokonalými informacemi na konečné desce (ale s neomezeným časem) jsou nerozhodnutelné.
- Conwayova hra o život je nerozhodnutelná.
Viz také
Reference
Poznámky
Bibliografie
- Barwise, Jon (1982), „Úvod do logiky prvního řádu“, in Barwise, Jon (ed.), Handbook of Mathematical Logic , Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
- Cantone, D., EG Omodeo a A. Policriti, "Set Theory for Computing. From decision Procedures to Logic Programming with Sets", Monographs in Computer Science, Springer, 2001.
- Chagrov, Alexander; Zakharyaschev, Michael (1997), Modal logic , Oxford Logic Guides, 35 , The Clarendon Press Oxford University Press, ISBN 978-0-19-853779-3, MR 1464942
- Davis, Martin (1958), Vypočitatelnost a neřešitelnost , McGraw-Hill Book Company, Inc, New York
- Enderton, Herbert (2001), Matematický úvod do logiky (2. vydání), Boston, MA: Academic Press , ISBN 978-0-12-238452-3
- Keisler, HJ (1982), „Základy teorie modelů“, in Barwise, Jon (ed.), Handbook of Mathematical Logic , Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
- Monk, J. Donald (1976), Mathematical Logic , Berlin, New York: Springer-Verlag