Eliminarea cuantificatorilor

Eliminarea cuantificatorilor - obținerea, după o formulă logică dată , echivalentă cu aceasta, neconținând cuantificatori . Teoriile care permit eliminarea cuantificatorilor pentru orice formulă prezintă un interes deosebit, deoarece prezența unui algoritm de eliminare permite obținerea unui număr de rezultate semnificative despre această teorie.

Procesele de găsire a algoritmilor de eliminare a cuantificatorilor pentru diverse teorii au trăsături comune, ceea ce ne permite să vorbim despre ei ca pe o singură metodă. Denumirea de metodă de eliminare a cuantificatorului a fost introdusă de Tarski în 1935 , deși considerente de acest fel au fost folosite pentru prima dată de Langford în 1927 . Metoda eliminării cuantificatorilor este aplicabilă numai teoriilor de un tip cu totul special și, în plus, de fiecare dată când această metodă este aplicată unei teorii noi, trebuie efectuate toate dovezile încă de la început, deoarece arsenalul de rezultate generale este foarte sărac. Cu toate acestea, dacă poate fi aplicată, această metodă se dovedește a fi extrem de utilă, deoarece oferă informații cuprinzătoare despre o anumită teorie. De obicei, conduce, de asemenea, la o modalitate obișnuită de a decide dacă o afirmație aparține sau nu unei anumite teorii - cu alte cuvinte, oferă o dovadă a decidabilității teoriei .

Teorii de ordinul întâi

O teorie de ordinul întâi admite eliminarea cuantificatorilor dacă pentru orice formulă (nu neapărat închisă ) a acestei teorii există o formulă care nu conține cuantificatori astfel încât , adică ambele formule sunt echivalente pe toate modelele teoriei . $\mathcal{T}$ $\varphi$ $\psi$ $\mathcal{T}\modeles\varphi\leftrightarrow\psi$ $\mathcal{T}$

Cele mai importante teorii de ordinul întâi care permit eliminarea cuantificatorilor sunt aritmetica Presburger , câmpurile închise algebric , câmpurile reale închise ( teorema Seidenberg-Tarski ), algebrele booleene fără atom , algebra termenului , ordinea liniară densă , teoria grupurilor abeliene , teoria cozilor . În acest caz, de exemplu, în aritmetica întregului , formula este echivalentă cu formula , dar pentru formulă nu există o formulă echivalentă care să nu conțină cuantificatori, adică aritmetica întregului nu permite eliminarea cuantificatorilor. $\exists x(x\geqslant 0\land a+x=b)$ $b\geqslant a$ $\exist x (a = x\cdot b)$

Abordarea dovezii

Pentru a demonstra că eliminarea cuantificatorilor este fezabilă în această teorie, este suficient să arătăm că este posibil să se elimine cuantificatorul existențial aplicat conjuncției literalelor , adică o formulă de forma:

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

Cuantificatorul universal poate fi înlocuit cu cuantificatorul existențial, deoarece este echivalent cu . În plus, formula poate fi scrisă în formă normală disjunctivă și să profite de faptul că: $\forall xF$ $\lnu \există x\lnu F$

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

echivalentă cu

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

Literatură

Keisler G., Chen Ch . Teoria modelelor. — M .: Mir, 1977.
N. K. Vereshchagin, A. Shen . 2. Limbi și calcul // Prelegeri despre logica matematică și teoria algoritmilor. — M .: MTsNMO, 2012.