Entscheidungsverfahren (Ansatz)

Def.: Menge M⊂$\mathbb {N}$^k mathend000# heißt P-definierbar

$\iff$ mathend000# es gibt eine P-Formel F mathend000# so daß M = Mod(F) mathend000#

wobei Mod(F) : = {m∈$\mathbb {N}$^k | {x₁ $\mapsto$ m₁,…, x_k $\mapsto$ m_k} $\models$ F} mathend000#

für F mathend000# mit freien Var. x₁,…, x_k mathend000#,

Satz: jede solche Modellmenge Mod(F) mathend000# ist effektiv regulär:

• es gibt einen Algorithmus, der zu jeder P-Formel F mathend000# ...
• ...einen endl. Automaten A mathend000# konstruiert mit Lang(A) = Kodierung vonMod(F) mathend000#

Folgerung: Allgemeingültigkeit ist entscheidbar:

Lang(A) = ∅ mathend000# gdw. Mod(F) = ∅ mathend000# gdw. F mathend000# ist widersprüchlich gdw. ¬F mathend000# ist allgemeingültig.