7738996307

A,*y *«*€*<-***>

Xi są rozłączne

VxViX £ XiAa,i(x)

Xi pokrywają słowo, a tranzycje są zgodne z etykietami

V*V(x, y) -»_{; pi=5i} xeXiAye Xj) kolejne tranzycje są zgodne

pierwsza tranzycja zaczyna się w stanie inicjalnym

V.3tó,V_Bw»6^

ostatnia tranzycja kończy się w stanie akceptującym

Dowód („=*•”)

Chcemy pokazać, że dla każdej formuły MSO <p(Xi... X_n, y\ ■ ■ ■ y_n) istnieje równoważny automat. Udowodnimy to przez indukcję po budowie <p.

Krok 1. Zacznijmy od uproszczenia formuł MSO - eliminacji zmiennych indywiduowych. Pokażemy przez indukcję ze względu na budowę formuły, że każda formuła MSO ®mso(^x1i ■ ■ ■ ,x„, Yj,..., Y_m) posiada równoważną formułę logiki MSOo - '&mso₀(Xi, • • •, X_n,Y\,..., Y_m), w której posługujemy się tylko zmiennymi drugiego rzędu, oraz dysponujemy predykatem C (X, Y) oraz S(X, Y) o następującej semantyce:

S(X,Y) MSOo •*=*■ mso 3_xex3y£Ys{x,y)

Skrót notacyjny ip l_i <=>■ [_J2ip będzie oznaczać „formułę logiki L\ przepisujemy na równoważną - prawdziwą w tych samych słowach (a w przypadku formuł otwartych: w tych samych słowach i dla analogicznych wartościowań zmiennych wolnych) - formułę ip logiki L-i'. Przez „analogiczne” wartościowania rozumiemy takie wartościowania, w których dopuszczamy zmianę wartości zmiennej indywiduowej na singleton zawierający tę wartość. Kwantyfikację po elementach będziemy symulować kwantyfikacją po singletonach, chcemy też w jakiś sposób zastąpić predykaty s(x,y) i €X(y) nowymi predykatami S(X,Y) i C (X, V).

Zdefiniujmy w MSOo pomocniczy predykat sing(X), który jest prawdziwy wtw. gdy zbiór X jest jedno-elementowy:

sing(X) <=* 3yęx(Y ± X) A V_Zcx{Z = XVZ = Y)

(konieczną i wystarczającą własnością singletonów jest fakt posiadania dokładnie jednego podzbioru właściwego).

Możemy teraz przepisać atomowe formuły MSO w języku MSOo-

mso •*=> MSO₀3xsing(X) AtpMSO₀(^x) s(x,y) MSO MSOo S(X,Y) A sing(X) A sing(Y) xeY MSO    MSOo x QY A sing(X)

Zauważmy, że każda formuła MSOo daje się zapisać formułą MSO: wystarczy, że zapiszemy C (X, Y) jako formułę MSO:

Q(X,Y)mso₀ •*=*• msoVxcxY(x).

S(X,Y) już zapisaliśmy w ten sposób. Przejście do MSOo nie zwiększa więc siły wyrazu.

7