A kvantorok kiiktatása

Kvantifikátorok kiiktatása - adott logikai képlet szerint, azzal ekvivalens, kvantorokat nem tartalmazó kinyerése . Különösen érdekesek azok az elméletek , amelyek lehetővé teszik bármely képlet kvantorainak kiküszöbölését, mivel az eliminációs algoritmus jelenléte lehetővé teszi, hogy számos értelmes eredményt kapjunk erről az elméletről.

A különböző elméletekhez tartozó kvantor-eltávolító algoritmusok keresési folyamatai közös vonásokkal rendelkeznek, ami lehetővé teszi, hogy egyetlen módszerként beszéljünk róluk. A kvantor eliminációs módszer elnevezést Tarski vezette be 1935 -ben , bár az ilyen jellegű megfontolásokat először Langford használta 1927 -ben . A kvantor eliminációs módszer csak nagyon speciális elméletekre alkalmazható, ráadásul minden alkalommal, amikor ezt a módszert egy új elméletre alkalmazzák, a kezdetektől fogva minden bizonyítást el kell végezni, mivel az általános eredmények arzenálja nagyon nagy. szegény. Ha azonban alkalmazható, akkor ez a módszer rendkívül hasznosnak bizonyul, hiszen átfogó információt ad egy adott elméletről. Ez rendszerint arra is vezet, hogy egy állítás egy adott elmélethez tartozik-e vagy sem – más szóval bizonyítja az elmélet eldönthetőségét .

Elsőrendű elméletek

Egy elsőrendű elmélet megengedi a kvantorok kiküszöbölését, ha ennek az elméletnek bármelyik (nem feltétlenül zárt ) formulájára létezik olyan képlet , amely nem tartalmaz kvantorokat úgy, hogy , azaz mindkét formula ekvivalens az elmélet összes modelljén . $\mathcal{T}$ $\varphi$ $\psi$ $\mathcal{T}\models\varphi\leftrightarrow\psi$ $\mathcal{T}$

A kvantorok eliminálását lehetővé tevő legfontosabb elsőrendű elméletek a Presburger aritmetika , algebrailag zárt mezők , zárt valós mezők ( Seidenberg-Tarski-tétel ), atom nélküli Boole-algebrák , termalgebra , sűrű lineáris rend , Abeli -csoportelmélet , sorban állás elmélet . Ebben az esetben például az integer aritmetikában a képlet ekvivalens a képlettel , de a képlethez nincs olyan ekvivalens képlet, amely ne tartalmazna kvantorokat, vagyis az egész számaritmetika nem teszi lehetővé a kvantorok eltávolítását. $\exists x(x\geqslant 0\land a+x=b)$ $b\geqslant a$ $\exist x (a = x\cdot b)$

A bizonyítás megközelítése

Annak bizonyítására, hogy ebben az elméletben a kvantorok kiküszöbölése megvalósítható, elegendő megmutatni, hogy lehetséges a literálok kötőszóra alkalmazott egzisztenciális kvantor megszüntetése , vagyis egy olyan képlet, amelynek alakja:

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

Az univerzális kvantor helyettesíthető az egzisztenciális kvantorral, mivel az ekvivalens -val . Továbbá a képlet felírható diszjunktív normál formában , és kihasználhatja azt a tényt, hogy: $\forall xF$ $\lnot \exists x\lnot F$

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

egyenértékű

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

Irodalom

Keisler G., Chen Ch . Modellelmélet. - M .: Mir, 1977.
N. K. Verescsagin, A. Shen . 2. Nyelvek és kalkulus // Előadások a matematikai logikáról és az algoritmusok elméletéről. — M. : MTsNMO, 2012.