Eliminace kvantifikátorů

Eliminace kvantifikátorů - získání, podle daného logického vzorce, jemu ekvivalentní, neobsahující kvantifikátory . Teorie , které umožňují eliminaci kvantifikátorů pro jakýkoli vzorec, jsou zvláště zajímavé, protože přítomnost eliminačního algoritmu umožňuje získat řadu smysluplných výsledků o této teorii.

Procesy hledání kvantifikátorových eliminačních algoritmů pro různé teorie mají společné rysy, což nám umožňuje hovořit o nich jako o jediné metodě. Metodu eliminace kvantifikátoru zavedl Tarski v roce 1935 , ačkoli úvahy tohoto druhu poprvé použil Langford v roce 1927 . Metoda eliminace kvantifikátoru je použitelná pouze na teorie velmi speciálního druhu a kromě toho pokaždé, když je tato metoda aplikována na novou teorii, je třeba provést všechny důkazy od samého začátku, protože arzenál obecných výsledků je velmi chudý. Pokud se ji však podaří aplikovat, ukazuje se tato metoda jako mimořádně užitečná, neboť poskytuje komplexní informace o dané teorii. Obvykle také vede k regulérnímu způsobu rozhodování, zda nějaké tvrzení k dané teorii patří či nikoliv – jinými slovy, dává důkaz o rozhodnutelnosti teorie .

Teorie prvního řádu

Teorie prvního řádu připouští eliminaci kvantifikátorů, pokud pro libovolnou (ne nutně uzavřenou ) formuli této teorie existuje formule , která neobsahuje kvantifikátory takové, že , to znamená, že obě formule jsou ekvivalentní na všech modelech teorie . $\mathcal{T}$ $\varphi$ $\psi$ $\mathcal{T}\models\varphi\leftrightarrow\psi$ $\mathcal{T}$

Nejdůležitější teorie prvního řádu, které umožňují eliminaci kvantifikátorů, jsou Presburgerova aritmetika , algebraicky uzavřená pole , uzavřená reálná pole ( Seidenbergova-Tarského věta ), bezatomové Booleovy algebry , termínová algebra , hustý lineární řád , Abelovská teorie grup , teorie fronty . V tomto případě je například v celočíselné aritmetice vzorec ekvivalentní vzorci , ale pro vzorec neexistuje žádný ekvivalentní vzorec, který by neobsahoval kvantifikátory, to znamená, že celočíselná aritmetika neumožňuje eliminaci kvantifikátorů. $\exists x(x\geqslant 0\land a+x=b)$ $b\geqslant a$ $\existovat x (a = x\cdot b)$

Přístup k důkazu

Abychom dokázali, že eliminace kvantifikátorů je v této teorii proveditelná, stačí ukázat, že je možné eliminovat existenciální kvantifikátor aplikovaný na konjunkci literálů , tedy formuli ve tvaru:

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

Univerzální kvantifikátor lze nahradit existenčním kvantifikátorem, protože je ekvivalentní . Dále lze vzorec napsat v disjunktivní normální formě a využít toho, že: $\forall xF$ $\lnot \exists x\lnot F$

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

ekvivalentní

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

Literatura

Keisler G., Chen Ch . Teorie modelů. — M .: Mir, 1977.
N. K. Vereščagin, A. Šen . 2. Jazyky a počet // Přednášky o matematické logice a teorii algoritmů. — M. : MTsNMO, 2012.