Eliminacja kwantyfikatora

Eliminacja kwantyfikatorów to koncepcja uproszczenia stosowana w logice matematycznej , teorii modeli i informatyce teoretycznej . Nieformalnie, skwantyfikowane stwierdzenie „ $…$ , że $”$ może być postrzegane jako pytanie „Kiedy istnieje takie, $}$ { $}$$\ ldots$ ?”, a stwierdzenie bez kwantyfikatorów można uznać za odpowiedź na to pytanie.

Jednym ze sposobów klasyfikowania formuł jest ilość kwantyfikacji . Formuły o mniejszej głębokości przemienności kwantyfikatora są uważane za prostsze, a formuły bez kwantyfikatorów są najprostsze. Teoria $,$ jeśli dla każdego wzoru $mu$ inny wzór kwantyfikatorów, który jest równoważny ( moduł tej teorii )

Przykłady

wielomian kwadratowy z pojedynczą zmienną ma pierwiastek rzeczywisty wtedy i tylko wtedy, gdy jego wyróżnik jest nieujemny:

${\ Displaystyle \ istnieje x \ in \ mathbb {R}. (a \ neq 0 \ ax klina ^ {2 }+bx+c=0)\ \ \Longleftrightarrow \ \ a\neq 0\klin b^{2}-4ac\geq 0}$

$równoważne$ lewej stronie zawiera kwantyfikator zdanie po prawej nie.

Przykładami teorii, które okazały się rozstrzygalne za pomocą eliminacji kwantyfikatorów, są arytmetyka Presburgera , ciała algebraicznie domknięte , ciała domknięte , bezatomowe algebry Boole'a , algebry terminów , gęste rzędy liniowe , grupy abelowe , grafy losowe , a także wiele ich kombinacji, takich jak Boolean algebra z arytmetyką Presburgera i algebry terminów z kolejkami .

Eliminatorem kwantyfikatorów dla teorii liczb rzeczywistych jako uporządkowanej grupy dodatków jest eliminacja Fouriera-Motzkina ; dla teorii pola liczb rzeczywistych jest to twierdzenie Tarskiego-Seidenberga .

Eliminację kwantyfikatorów można również wykorzystać do pokazania, że ​​„łączenie” rozstrzygalnych teorii prowadzi do nowych rozstrzygalnych teorii (patrz twierdzenie Fefermana-Vaughta ).

Algorytmy i rozstrzygalność

$Jeśli teoria$$eliminację kwantyfikatorów,$ pytanie: Czy istnieje metoda określania dla każdego ? Jeśli istnieje taka metoda, nazywamy ją algorytmem eliminacji kwantyfikatorów . Jeśli taki algorytm istnieje, to rozstrzygalność dla teorii sprowadza się do decydowania o prawdziwości zdań wolnych od kwantyfikatora . Zdania bez kwantyfikatorów nie mają zmiennych, więc często można obliczyć ich ważność w danej teorii, co umożliwia zastosowanie algorytmów eliminacji kwantyfikatorów do decydowania o ważności zdań.

Pojęcia pokrewne

Z eliminacją kwantyfikatorów związane są różne koncepcje teorii modeli i istnieją różne równoważne warunki.

Każda teoria pierwszego rzędu z eliminacją kwantyfikatorów jest modelem kompletnym . I odwrotnie, teoria zupełnego modelu, której teoria uniwersalnych konsekwencji ma właściwość amalgamacji , ma eliminację kwantyfikatora.

${\ displaystyle T$ teorii uniwersalnych konsekwencji teorii są właśnie podstrukturami modeli $}$ . Teoria rzędów liniowych nie ma eliminacji kwantyfikatorów. Jednak teoria jej uniwersalnych konsekwencji ma właściwość amalgamacji.

Podstawowe pomysły

Aby konstruktywnie pokazać, że teoria ma eliminację kwantyfikatora, wystarczy pokazać, że możemy wyeliminować kwantyfikator egzystencjalny zastosowany do koniunkcji literałów , czyli pokazać, że każda formuła postaci:

${\ Displaystyle \ istnieje x. \ bigwedge _ {i = 1} ^ {n} L_ {i}}$

gdzie każdy $,$ jest równoważny formule wolnej od kwantyfikatorów. Rzeczywiście, załóżmy, że wiemy, jak wyeliminować kwantyfikatory ze spójników literałów, to jeśli jest formułą wolną od kwantyfikatorów, możemy zapisać ją w rozłącznej postaci normalnej ${\ displaystyle F}$

${\ Displaystyle \ bigvee _ {j = 1} ^ {m} \ bigwedge _ {i = 1} ^ {n} L_ {ij}}$

i wykorzystać fakt, że

${\ Displaystyle \ istnieje x \ bigvee _ {j = 1} ^ {m} \ bigwedge _ {i = 1} ^ {n} L_ {ij}}$

jest równa

${\ Displaystyle \ bigvee _ {j = 1} ^ {m} \ istnieje x. \ bigwedge _ {i = 1} ^ {n} L_ {ij}.}$

Wreszcie, aby wyeliminować uniwersalny kwantyfikator

${\ displaystyle \ forall xF}$

gdzie jest wolny $normalną$$kwantyfikatorów$ , przekształcamy w dysjunkcyjną ${\ displaystyle \ forall xF}$ i wykorzystujemy fakt, jest równoważne ${\ Displaystyle \ l nie \ istnieje x. \ l nie F.}$

Związek z rozstrzygalnością

We wczesnej teorii modeli eliminacja kwantyfikatorów była używana do wykazania, że ​​różne teorie posiadają takie właściwości, jak rozstrzygalność i kompletność . Powszechną techniką było pokazanie najpierw, że teoria dopuszcza eliminację kwantyfikatorów, a następnie udowodnienie rozstrzygalności lub kompletności, biorąc pod uwagę tylko formuły wolne od kwantyfikatorów. Ta technika może być wykorzystana do wykazania, że ​​arytmetyka Presburgera jest rozstrzygalna.

Teorie mogą być rozstrzygalne, ale nie pozwalają na eliminację kwantyfikatora. Ściśle mówiąc, teoria addytywnych liczb naturalnych nie pozwalała na eliminację kwantyfikatora, ale wykazano, że jest to rozwinięcie addytywnych liczb naturalnych, które są rozstrzygalne. Ilekroć teoria jest rozstrzygalna, a język jej ważnych formuł jest policzalny , można rozszerzyć teorię o przeliczalnie wiele relacji , aby wyeliminować kwantyfikator (na przykład można wprowadzić dla każdej formuły teorii symbol relacji, który wiąże zmienne wolne wzoru).

Przykład: Nullstellensatz dla ciał algebraicznie domkniętych i ciał różniczkowo domkniętych .

Zobacz też

• Cylindryczny rozkład algebraiczny
• Teoria eliminacji
• Eliminacja koniunkcji

Notatki

• Brown, Christopher W. (31 lipca 2002). „Co to jest eliminacja kwantyfikatora” . Źródło 30 sierpnia 2018 r .

•   Enderton, Herbert (2001). Matematyczne wprowadzenie do logiki (wyd. 2). Boston, MA: Prasa akademicka . ISBN 978-0-12-238452-3 .

•   Smażone, Michael D .; Jarden, Mosze (2008). Arytmetyka pola . Ergebnisse der Mathematik und ihrer Grenzgebiete. 3. Folge. Tom. 11 (3. poprawione wydanie). Springer-Verlag . ISBN 978-3-540-77269-9 . Zbl   1145.12001 .

•    Gradel, Erich; Kolaitis, Phokion G. ; Libkin, Leonid ; Maarten, Marks; Spencer, Joel ; Vardi, Mosze Y .; Venema, Yde; Weinstein, Scott (2007). Teoria modeli skończonych i jej zastosowania . Teksty z informatyki teoretycznej . Seria EATCS. Berlin: Springer-Verlag . ISBN 978-3-540-00428-8 . Zbl 1133.03001 .

• Hodges, Wilfrid (1993). Teoria modeli   . Encyklopedia matematyki i jej zastosowań . Tom. 42. Cambridge University Press . doi : 10.1017/CBO9780511551574 . ISBN 9780521304429 .

•   Kuncak, Wiktor; Rinard, Martin (2003). „Podtypowanie strukturalne typów nierekurencyjnych jest rozstrzygalne” (PDF) . 18. doroczne sympozjum IEEE na temat logiki w informatyce, 2003. Obrady . doi : 10.1109/LICS.2003.1210049 . ISBN 0-7695-1884-2 .

• Mnich, J. Donald Monk (2012).   Mathematical Logic (podyplomowe teksty z matematyki (37)) (przedruk w miękkiej oprawie oryginalnego pierwszego wydania z 1976 r.). Skoczek. ISBN 9781468494549 .

•   Nipkow, T (2010). „Eliminacja kwantyfikatora liniowego” (PDF) . Dziennik automatycznego rozumowania . 45 (2): 189–212. doi : 10.1007/s10817-010-9183-0 . S2CID 14279141 . Źródło 2022-11-12 .

• Presburger, Mojżesz (1929). „Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem ​​die Addition als einzige Operation hervortritt”. Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, Warszawa : 92–101. , patrz Stansifer (1984) dla angielskiego tłumaczenia

• Szmielew, Wanda (1955). „Elementarne właściwości grup abelowych” . Fundamenta Mathematicae . 41 (2): 203–271. doi :   10.4064/fm-41-2-203-271 . MR 0072131 .

• Jeannerod, Nicolas; Trenin, Ralf. Decydowanie o teorii pierwszego rzędu algebry drzew cech z aktualizacjami . Międzynarodowa wspólna konferencja na temat automatycznego rozumowania (IJCAR). doi : 10.1007/978-3-319-94205-6_29 .

• Sturm, Thomas (2017). „Przegląd niektórych metod eliminacji, decyzji i spełnialności rzeczywistych kwantyfikatorów oraz ich zastosowań” . Matematyka w informatyce . 11 : 483–502. doi : 10.1007/s11786-017-0319-z .