Eliminering av kvantifierare

Eliminering av kvantifierare - erhåller, enligt en given logisk formel, likvärdig med den, som inte innehåller kvantifierare . Teorier som tillåter eliminering av kvantifierare för vilken formel som helst är av särskilt intresse, eftersom närvaron av en elimineringsalgoritm tillåter en att få ett antal meningsfulla resultat om denna teori.

Processerna för att hitta kvantifieringselimineringsalgoritmer för olika teorier har gemensamma drag, vilket gör att vi kan tala om dem som en enda metod. Namnet kvantifierare elimineringsmetoden introducerades av Tarski 1935 , även om överväganden av detta slag först användes av Langford 1927 . Kvantifieringselimineringsmetoden är endast tillämplig på teorier av ett mycket speciellt slag, och dessutom, varje gång denna metod tillämpas på en ny teori, måste man utföra alla bevis från första början, eftersom arsenalen av generella resultat är mycket fattig. Men om den kan tillämpas visar sig denna metod vara extremt användbar, eftersom den ger omfattande information om en given teori. Det leder vanligtvis också till ett regelbundet sätt att avgöra om något påstående tillhör en given teori eller inte - det ger med andra ord ett bevis på teorins avgörbarhet .

Första ordningens teorier

En teori av första ordningen medger eliminering av kvantifierare om det för någon (inte nödvändigtvis sluten ) formel i denna teori finns en formel som inte innehåller kvantifierare så att , det vill säga båda formlerna är likvärdiga på alla modeller av teorin . $\mathcal{T}$ $\varphi$ $\psi$ $\mathcal{T}\models\varphi\leftrightarrow\psi$ $\mathcal{T}$

De viktigaste första ordningens teorier som tillåter eliminering av kvantifierare är Presburger-arithmetik , algebraiskt slutna fält , slutna reella fält ( Seidenberg-Tarski-satsen ), atomlösa booleska algebror , termalgebra , tät linjär ordning , Abelsk gruppteori , köteori . I det här fallet, till exempel, i heltalsaritmetik är formeln ekvivalent med formeln , men för formeln finns det ingen ekvivalent formel som inte innehåller kvantifierare, det vill säga heltalsaritmetik tillåter inte eliminering av kvantifierare. $\exists x(x\geqslant 0\land a+x=b)$ $b\geqslant a$ $\exist x (a = x\cdot b)$

Tillvägagångssätt till beviset

För att bevisa att eliminering av kvantifierare är genomförbart i denna teori, räcker det att visa att det är möjligt att eliminera den existentiella kvantifierare som tillämpas på konjunktionen av bokstaver , det vill säga en formel av formen:

\exists x\bigwedge _{i=1}^{n}L_{i}

Den universella kvantifieraren kan ersättas med den existentiella kvantifieraren, eftersom den motsvarar . Vidare kan formeln skrivas i disjunktiv normal form och dra fördel av det faktum att: $\förallt xF$ $\lnot \exists x\lnot F$

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

ekvivalent med

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

Litteratur

Keisler G., Chen Ch . Theory of Models. — M .: Mir, 1977.
N.K. Vereshchagin, A. Shen . 2. Språk och analys // Föreläsningar om matematisk logik och teori om algoritmer. — M. : MTsNMO, 2012.