Logika dla informatyków/Ograniczenia logiki pierwszego rzędu

Linek z wykladu 8 do tw. 4.13. Nazwa linku "Cantoro"

Ograniczenia logiki pierwszego rzędu

Ten rozdział poświęcony jest ograniczeniom, którym podlega język logiki pierwszego rzędu. Okazuje się, że nie każde pojęcie da się w nim wyrazić, a także, że są pojęcia, które dają się wyrazić, ale odpowiednie zdanie lub formuła z konieczności musi być skomplikowane. Rozważania w tym rozdziale będziemy prowadzić przy założeniu, że w sygnaturze występują wyłącznie symbole relacyjne. Wyniki dają się zastosować do sygnatur z symbolami funkcyjnymi, ale wymaga to zakodowania wszystkich funkcji jako relacji.

Zaczniemy od miary skomplikowania formuł, która będzie przydatna w dalszym ciągu.

Definicja

Rangę kwantyfikatorową Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle QR\var(\varphi)} formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} definiujemy jak następuje:

• $QR(\mathrm{\perp })=QR(t_1=t_2)=QR(r(t_1,\dots ,t_k))=0$ dla dowolnych termów $t_1,\dots ,t_k$ oraz $r\in {\mathrm{\Sigma }}_k^R.$
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle QR (\var\varphi\to \psi) =\max (QR (\var\varphi) ,QR (\psi)) } .
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle QR (\forall x\var\varphi) =1+QR (\var\varphi) .}

Intuicyjnie $QR$ to głębokość zagnieżdżenia kwantyfikatorów w formule. Jest to jedna z wielu możliwych miar stopnia komplikacji formuły $\phi .$ Parametr ten ma następujące znaczenie: jeśli struktura Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} ma Parser nie mógł rozpoznać (nieznana funkcja „\vdashl”): {\displaystyle n\Delta\vdashl} elementów, to pesymistyczny czas sprawdzenia, czy dla zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models \var\varphi} jest asymptotycznie proporcjonalny do Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle n^{QR \var\varphi },} gdy użyjemy naturalnego algorytmu do wykonania tego zadania, który dla każdego kwantyfikatora w formule przegląda wszystkie elementy struktury.

Teraz możemy wyjaśnić, dlaczego nie dopuszczamy symboli funkcyjnych w sygnaturze. Otóż ich obecność zakłóca potrzebne nam własności funkcji $QR.$ Tytułem przykładu, formuła $Rx,ffx$ jest atomowa i jej ranga kwantyfikatorowa powinna wynosić $0$. Tymczasem gdy $f$ będziemy reprezentować w strukturze jako dwuargumentową relację </math>FParser nie mógł rozpoznać (błąd składni): {\displaystyle , ta sama formuła przybierze postać } \exists y\exists z F x,y \land F y,z \land R x,z ,</math> której ranga kwantyfikatorowa wynosi 2. Twierdzenia, których dalej dowodzimy, odwołują się do wartości $QR$ zdefiniowanych powyżej dla logiki bez symboli funkcyjnych. To właśnie jest przyczyna, dla której funkcje wykluczamy z rozważań.

Charakteryzacja Fra\"{\i

Definicja

relacyjną oraz $\mathrm{\varnothing }\ne B\subseteq A,$ to struktura Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA_{|B}} tej samej sygnatury $\mathrm{\Sigma }$ co Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} , nazywana \textit{podstrukturą indukowaną przez $B$ w Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,} } ma nośnik $B,$ zaś dla każdego $r\in {\mathrm{\Sigma }}_n^R$

\[r^{\strA_{

=r^\strA\cap B^n.\]

}}

Definicja

strukturami relacyjnymi tej samej sygnatury $\mathrm{\Sigma },$ ponadto niech $A^{\prime }\subseteq A$ i $B^{\prime }\subseteq B$. Jeśli funkcja $h:A^{\prime }\to B^{\prime }$ jest

izomorfizmem podstruktur indukowanych </math>h:\strA_{

\def\blank{\hbox{\sf Bmawiamy się, że

$\mathrm{\varnothing }$

jest częściowym

izomorfizmem z Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} o pustej dziedzinie i pustym obrazie.

Dla dwóch częściowych izomorfizmów $g,h$ z Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} piszemy $g\subseteq h$ gdy $domg\subseteq domh$ oraz $ga=ha$ dla wszystkich $a\in domg,$ to jest wtedy, gdy $g$ jest zawarte jako zbiór w $h.$ }}

Definicja

naturalną. Dwie struktury relacyjne tej samej sygnatury są \textit{$m$-izomorficzne}, co oznaczamy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{m}\strB,} gdy istnieje rodzina Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_n&nbsp;|&nbsp;n\leq m\}} w której każdy $I_n$ jest niepustym zbiorem częściowych izomorfizmów z Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB,} oraz spełniająca następujące dwa warunki:

\begin{description} \item[Tam] Dla każdego $h\in I_{n+1}$ oraz każdego $a\in A$ istnieje takie $g\in I_n$, że $h\subseteq g$ oraz $a\in domg.$ \item[Z powrotem] Dla każdego $h\in I_{n+1}$ oraz każdego $b\in B$ istnieje takie $g\in I_n$, że $h\subseteq g$ oraz $b\in rgg.$ \end{description}

Samą rodzinę Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_n&nbsp;|&nbsp;n\leq m\}} nazywamy wówczas \textit{$m$-izomorfizmem} struktur Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} , co oznaczamy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_n&nbsp;|&nbsp;n\leq m\}:\strA\cong_m\strB.}

Nieformalne wyjaśnienie jest takie: $I_n$ to zbiór częściowych izomorfizmów, które mogą być rozszerzone $n$-krotnie o dowolne elementy w dziedzinie i obrazie, a kolejne rozszerzenia leżą w $I_{n-1},\dots ,I_0.$

Definicja

\rm

Dwie struktury relacyjne tej samej sygnatury są \textit{skończenie izomorficzne}, symbolicznie Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{fin}\strB,} gdy istnieje

rodzina </math>\{I_n 

Fakt

• Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong\strB,} to Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{fin}\strB.}
• Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{fin}\strB} oraz nośnik Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} jest

zbiorem skończonym, to Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong\strB.}

Dowód

{{{3}}}

Definicja

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} tej samej sygnatury są \textit{elementarnie równoważne}, co zapisujemy symbolicznie Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\equiv\strB,} gdy dla każdego zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} logiki pierwszego rzędu nad tą samą sygnaturą, Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\var\varphi} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\models\var\varphi.}

Dwie struktry Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} tej samej sygnatury są \textit{$m$-elementarnie równoważne}, symbolicznie Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\equiv_m\strB,} gdy dla każdego zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} logiki pierwszego rzędu nad tą samą sygnaturą, o randze kwantyfikatorowej nie przekraczającej $m$, zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\var\varphi} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\models\var\varphi.}

Fakt

gdy dla każdego naturalnego $m$ zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_m\strB} .

Dowód

{{{3}}}

Twierdzenie

Niech $\mathrm{\Sigma }$ będzie dowolną sygnaturą relacyjną zawierającą skończenie wiele symboli, oraz niech Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,\strB} będą dowolnymi strukturami nad $\mathrm{\Sigma }.$

• Dla każdego $m\in \mathbb{\mathbb{N}}$ zachodzi równoważność: Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_m\strB}

wtedy i tylko wtedy gdy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\equiv_m\strB} .

• Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{fin}\strB} wtedy i tylko wtedy gdy

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\equiv\strB} .

Dowód

{{{3}}}

\def\blank{\hbox{\sf Bdowodnimy tylko z lewej do prawej strony. Dowód w stronę

przeciwną jest bardziej zawiły technicznie, a w dodatku ta \rightarrowlikacja jest rzadko\boldsymbol{s}}\def\blank{\hbox{\sf Bżywana w praktyce. Wyraża za to istotną z metodologicznego punktu widzenia informację: jeśli dwie struktury są

$m$- elementarnie równoważne, to fakt ten można na pewno\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić 

posługując się metodą Fra\"{\i}ss\'e, choć oczywiście nie ma gwarancji, że będzie to metoda najprostsza.

Ustalmy $m\in \mathbb{\mathbb{N}}$. Dowód tego, że z Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_m\strB} wynika Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\equiv_m\strB} sprowadza się do wykazania następującego faktu za pomocą indukcji ze względu na budowę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} :

\begin{quote} Niech Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_n &nbsp;|&nbsp; n\leq m\''} będzie rodziną o której mowa w definicji Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_m\strB} , niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} będzie formułą o co najwyżej $r$ zmiennych wolnych bez\boldsymbol{s}}\def\blank{\hbox{\sf Btraty ogólności niech będą to $x_1,\dots ,x_r$ i spełniającą Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR \var\varphi \leq n\leq m} oraz niech $g\in I_n.$ Wówczas dla dowolnych $a_1,\dots ,a_r\in domg$ następujące dwa warunki są równoważne:} \[\strA,x_1:a_1,\dots,x_r:a_r\models\var\varphi\] \[\strB,x_1:g a_1 ,\dots,x_r:g a_r \models\var\varphi.\]\end{quote}

Dla formuł atomowych, powyższa teza wynika wprost z faktu, że $g$ jest częściowym izomorfizmem przypomnijmy że w sygnaturze nie ma symboli funkcyjnych i co za tym idzie jedynymi termami są zmienne .

Gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ma postać $\psi \to \xi ,$ to mamy następujący ciąg równoważnych warunków:

• Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:a_1,\dots,x_r:a_r\models\psi\to\xi}

• Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:a_1,\dots,x_r:a_r\not\models\psi} lub

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:a_1,\dots,x_r:a_r\models\xi}

• Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:g a_1 ,\dots,x_r:g a_r \not\models\psi} lub

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:g a_1 ,\dots,x_r:g a_r \models\xi}

• Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:g a_1 ,\dots,x_r:g a_r \models\psi\to\xi,}

przy czym druga równoważność wynika z założenia indukcyjnego, a pierwsza i trzecia z definicji semantyki.

Gdy </math>\var\varphiParser nie mógł rozpoznać (błąd składni): {\displaystyle ma postać } \forall x \psi,Parser nie mógł rozpoznać (błąd składni): {\displaystyle to, jako że } x_{r+1}\notin FV \var\varphi $icozatymidzie$\models \forall x\psi

\leftrightarrow \forall x_{r+1} \psi x_{r+1}/x </math>  patrz Fakt 

#alfa-konw , możemy bez\boldsymbol{s}}\def\blank{\hbox{\sf Btraty ogólności założyć, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ma postać $\mathrm{\forall }{x}_{r+1}\psi .$ Z założenia Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR \var\varphi \leq n} wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR \psi \leq n-1} . Mamy teraz następujący ciąg równoważnych warunków:

• Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:a_1,\dots,x_r:a_r \models\var\varphi}

• Dla każdego $a\in A$ zachodzi

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:a_1,\dots,x_r:a_r,x_{r+1}:a \models\psi}

• Dla każdego $a\in A$ istnieje takie $h\in I_{n-1}$, że $g\subseteq h,$

$a\in domh$ oraz

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:a_1,\dots,x_r:a_r,x_{r+1}:a \models\psi}

• Dla każdego $a\in A$ istnieje takie $h\in I_{n-1}$, że $g\subseteq h,$

$a\in domh$ oraz

Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB,x_1:g a_1 ,\dots,x_r:g a_r ,x_{r+1}:h a \models\psi}

• Dla każdego $b\in B$ istnieje takie $h\in I_{n-1}$, że

$g\subseteq h,$ $b\in rgh$ oraz

Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB,x_1:g a_1 ,\dots,x_r:g a_r ,x_{r+1}:b \models\psi}

• Dla każdego $b\in B$ zachodzi

Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB,x_1:g a_1 ,\dots,x_r:g a_r ,x_{r+1}:b \models\psi}

• Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB,x_1:g a_1 ,\dots,x_r:g a_r \models\var\varphi.}

Równoważności druga i czwarta zachodzą na mocy warunków Tam i Z powrotem, trzecia na mocy założenia indukcyjnego, a pozostałe na mocy definicji spełniania. }}

Pokażemy teraz pierwszy przykład inherentnego ograniczenia logiki pierwszego rzędu.

Fakt

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,\strB} są dwoma skończonymi liniowymi porządkami o mocach większych niż $2^m,$ to Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\equiv_m\strB.}

Dowód

&\text{jeśli $|b-a|<2^k$}\\

\infty&\text{wpp.} \end{cases} \]

Niech $I_k$ dla $k\le m$ będzie zbiorem wszystkich częściowych izomorfizmów </math>g$z$\strA$w$\strBParser nie mógł rozpoznać (błąd składni): {\displaystyle takich, że } \{\langle 0,0\rangle,\langle N,M\rangle\}\subseteq g</math> oraz $d_{k}a,b=d_{k}ga,gb$ dla wszystkich $a,b\in domg.$ Oczywiście </math>I_k\neq \emptyset$bo$\{\langle 0,0\rangle,\langle N,M\rangle\}\in I_k.</math>

Pokazujemy własność Tam} dla rodziny Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_k&nbsp;|&nbsp;k\leq m\'''} . Niech $g\in I_{k+1}.$ Niech $a\in \{0,\dots ,N\}.$ Mamy wskazać w $I_k$ częściowy izomorfizm $h\supseteq g$ taki, że $a\in domh.$

Rozróżniamy dwa przypadki:

i  Jeśli istnieje takie $b\in domg$, że $d_{k}a,b<\mathrm{\infty }$, to w 

$B$ jest dokładnie jeden\Delta\vdashlement $a^{\prime }$, który jest tak samo położony względem $gb$ jak $a$ względem $b,$ oraz spełnia $d_j{a}^{\prime },gb=d_{j}a,b.$ Kładziemy wówczas $ha:=a^{\prime }$ i $h$ jest wtedy częściowym izomorfizmem zachowującym odległości $d_j.$

ii  Jeśli natomiast takiego $b$ nie ma, to niech $a^{\prime }<a<a^{″},$ gdzie 

$a^{\prime },a^{″}$ są najbliższymi $b$\Delta\vdashlementami po lewej i po prawej, które należą do $domg.$ Wówczas $d_j{a}^{\prime },a=d_{j}a,a^{″}=\mathrm{\infty },$ co w myśl definicji $d_j$ oznacza, że $d_{j+1}{a}^{\prime },a^{″}=\mathrm{\infty }.$ Zatem na mocy założenia indukcyjnego także $d_{j+1}g{a}^{\prime },g{a}^{″}=\mathrm{\infty }.$ Istnieje więc $g{a}^{\prime }<b<g{a}^{″}$ takie, że \mbox{$d_{j}g{a}^{\prime },b=d_{j}b,g{a}^{″}=\mathrm{\infty }$},

i wówczas kładąc $ha:=b$\boldsymbol{s

\def\blank{\hbox{\sf Bzyskujemy żądane rozszerzenie.

}}

Przykład powyższy wskazuje na kilka istotnych ograniczeń logiki pierwszego rzędu. Po pierwsze, nie da się żadnym zdaniem zdefiniować nawet tak prostego pojęcia jak ,,porządek liniowy o parzystej liczbie elementów, i to bez względu na to, jak byśmy je rozumieli dla modeli nieskończonych. Istotnie, zdanie które miałoby definiować taką własność musiałoby mieć jakąś rangę kwantyfikatorową, powiedzmy $q$. Jednak w myśl poprzedniego twierdzenia, porządki o mocach $2^q+1$ i $2^q+2$ są $q$-elementarnie równoważne i nasze hipotetyczne zdanie jest albo prawdziwe w obu, albo fałszywe w obu, podczas gdy powinno być w jednym fałszywe, a w drugim prawdziwe.

Drugim ograniczeniem jest fakt, że każda specyfikacja porządku liniowego o mocy $n$ w logice pierwszego rzędu musi z konieczności mieć rangę kwantyfikatorową co najmniej ${\log }_{2}n,$ a więc sugeruje algorytm sprawdzenia, czy dany obiekt mocy $m$ istotnie spełnia tę specyfikację, którego czas działania ma rząd wielkości $m^{{\log }_{2}n},$ co jest wynikiem fatalnym.\footnote{Na szczęście znamy lepsze algorytmy wykonujące to zadanie.} Bierze się to stąd, że prawdziwość zdania o randze kwantyfikatorowej $q$ sprawdza się w danej skończonej strukturze za pomocą $q$ zagnieżdżonych pętli, z których każda przegląda cały nośnik struktury i odpowiada jednemu kwantyfikatorowi.

Gra Ehrenfeuchta

Charakteryzacja Fra\"{\i}ss\'e jest dość skomplikowana i odpychająca w bezpośrednim\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciu. W praktyce jej popularność ogromnie zwiększyło podanie przez Andrzeja Ehrenfeuchta jej równoważnego opisu w terminach dwuosobowej gry, którą teraz zdefiniujemy. Gra ta doskonale sprawdza się w rozumowaniach intuicyjnych. Praktyczne doświadczenie wskazuje, że próby napisania bardzo formalnego dowodu przy\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciu gry kończą się zwykle wskazaniem rodziny zbiorów częściowych izomorfizmów w duchu Fra\"{\i}ss\'e.

Niech $\mathrm{\Sigma }$ będzie sygnaturą relacyjną i niech Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,\strB} będą strukturami sygnatury $\mathrm{\Sigma }.$

Dla\boldsymbol{s}}\def\blank{\hbox{\sf Bproszczenia zakładamy, że $A\cap B=\mathrm{\varnothing }.$ \bigbreak

Definicja

{{{3}}}

Definicja powyższa dopuszcza powtarzanie ruchów przez obu graczy, czyli wybieranie\Delta\vdashlementów, które poprzednio były już wybrane. Jest to dogodne, gdyż\boldsymbol{s}}\def\blank{\hbox{\sf Bpraszcza definicję. Gdybyśmy bowiem zakazali tego, to albo niemożliwe byłoby rozegranie gry Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle G_m \strA,\strB } gdy choć jedna ze struktur ma moc mniejszą niż $m,$ albo trzeba by było wprowadzić w definicji specjalny warunek służący do rozstrzygania zwycięstwa w sytuacjach, gdy brak możliwości dalszych ruchów.

W praktyce jednak w dowodach prawie nigdy nie rozpatruje się takich ruchów, gdyż jest oczywiste, że wykonanie takiego posunięcia przez gracza I nie przybliża go do zwycięstwa, zaś gdy wykona je gracz II mimo że nie zrobił tego gracz I, powoduje to jego natychmiastową przegraną.

Twierdzenie

• Gracz II ma strategię wygrywającą w grze Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle G_m \strA,\strB } wtedy i tylko

wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{m}\strB.}

• Gracz II ma dla każdego $m$ strategię wygrywającą w grze

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle G_m \strA,\strB } wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{fin}\strB.}

Dowód

{{{3}}}

Poniższe twierdzenie ilustruje, w jaki sposób gra może zostać wykorzystana dla wskazania ograniczeń możliwości logiki pierwszego rzędu.

Twierdzenie

{{{3}}}

<span id="

W myśl Twierdzenia #ehrenfeucht należy pokazać, że dla każdego $m$ gracz II ma strategię wygrywającą w grze Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle G_m \strA,\strB .} Opiszemy teraz tę strategię. Jej postać nie zależy od liczby rund do rozegrania. Pokażemy też, że jeśli po zakończeniu poprzedniej rundy warunek wygrywający dla gracza II był spełniony, to po wykonaniu ruchu zgodnie ze wskazaną strategią pozostanie on nadal spełniony. Wówczas na mocy zasady indukcji po rozegraniu dowolnej ilości rund, w których gracz II będzie się stosował do tej strategii, pozostanie on zwycięzcą.

Zauważmy, że warunek o częściowym izomorfizmie w naszej sytuacji oznacza tyle, że zbiory $\{a_1,\dots ,a_k\}$ i $\{b_1,\dots ,b_k\}$ elementów wybranych w każdej ze struktur, po posortowaniu rosnąco zgodnie z porządkiem odpowiednio Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \leq^\strA} oraz Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \leq^\strB} prowadzą do identycznych ciągów indeksów swoich oznaczeń. Dokładnie, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle a_{i_1}<^\strA a_{i_2}<^\strA \dots<^\strA a_{i_k}} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle b_{j_1}<^\strB b_{j_2}<^\strB \dots<^\strB b_{j_k}} , to zachodzą równości $i_{\ell }=j_{\ell }$ dla $\ell =1,\dots ,k.$

• Na pierwszy ruch gracza I gracz II odpowiada w dowolny sposób.

Przed tą rundą nie było wybranych\Delta\vdashlementów, czyli przekształcenie opisane w definicji gry było przekształceniem pustym, które na mocy konwencji jest częściowym izomorfizmem. Po wykonaniu ruchu zgodnie ze strategią ciągi indeksów w obu strukturach są oczywiście identyczne.

• We wszystkich kolejnych rundach gracz II określa swój ruch

następująco. Niech </math>a_{i_1}<^\strA a_{i_2}<^\strA \dots<^\strA a_{i_k}</math> i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle b_{i_1}<^\strB b_{i_2}<^\strB \dots<^\strB b_{i_k}} będą

identycznymi na mocy założenia indukcyjnego  ciągami indeksów przed 

wykonaniem tego ruchu. Ze względu na symetrię sytuacji, możemy bez \boldsymbol{s" style="font-variant:small-caps">Dowód

{{{3}}}

\def\blank{\hbox{\sf Btraty ogólności założyć, że gracz I wybiera strukturę Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} . Może

symbolem $a_{k+1}$ oznaczyć:

• • Element mniejszy od $a_{i_1}.$ Wówczas gracz II

wybiera\Delta\vdashlement mniejszy od $b_{i_1}$ w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} , który istnieje na mocy założenia, że w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} nie ma\Delta\vdashlementu najmniejszego. Widać, że nowe ciągi indeksów pozostaną równe.

• • Element większy od $a_{i_k}.$ Wówczas gracz II wybiera\Delta\vdashlement

większy od $b_{i_k}$ w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} , który istnieje na mocy założenia, że w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} nie ma\Delta\vdashlementu ostatniego. Widać, że także teraz nowe ciągi indeksów pozostaną równe.

• • Element </math>aParser nie mógł rozpoznać (błąd składni): {\displaystyle spełniający } a_{i_{\ell}}<^\strA a<^\strA

a_{i_{\ell+1}}</math> dla pewnego $\ell .$ W Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} istnieje\Delta\vdashlement $b$ spełniający Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle b_{i_{\ell}}<^\strB b<^\strB b_{i_{\ell+1}}} , gdyż Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} jest porządkiem gęstym. Gracz II wybiera taki\Delta\vdashlement i również w tym wypadku widać, że nowe ciągi indeksów pozostaną równe.

Na tym dowód istnienia strategii wygrywającej dla gracza II jest zakończony. }}

Z powyższego wynika między innymi, że </math>\langle \mathbb{R},\leq\rangle\equiv\langle \mathbb{Q},\leq\rangle.</math> Zatem nie ma zdania logiki pierwszego rzędu, które definiuje pojęcie porządku ciągłego tzn. takiego, w którym wszystkie niepuste ograniczone podzbiory mają kres górny i kres dolny , bo musiałoby ono być prawdziwe w pierwszej ze struktur, a fałszywe w drugiej.

Definicja

\ \strA\models\var\varphi,\ \mbox{dla każdego\

\strA\in\K\}</math>

teoria klasy struktur Parser nie mógł rozpoznać (nieznana funkcja „\K”): {\displaystyle \K}
  albo  

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle '''Th} \strA = \{\var\varphi\ |\ \strA\models\var\varphi\'''}

teoria modelu Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA}
 . Teorię  

$\mathrm{\Delta }$ nazywamy \textit{zupełną}, gdy dla każdego zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,} dokładnie jedno ze zdań Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \lnot\var\varphi} należy do

$\mathrm{\Delta }.$ Zbiór zdań prawdziwych w\boldsymbol{s

\def\blank{\hbox{\sf Bstalonym modelu jest oczywiście zawsze

teorią zupełną. }}

Wniosek

Teoria klasy ${𝒜}$ wszystkich porządków liniowych, gęstych, bez\Delta\vdashlementu pierwszego i ostatniego jest zupełna.

Dowód

{{{3}}}

\subsection*{Ćwiczenia}\begin{small}

Wykazać, że dla dostatecznie dużych $q$ istnieje zdanie o randze kwantyfikatorowej $q$ definiujące porządek liniowy o mocy $2^q.$

Adaptując dowód Faktu #qq\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić, że struktury Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\{1-1/n&nbsp;|&nbsp;n=1,2,\dots\},\leq\>} oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<\bigcup_{n=1}^\infty\{1-1/n,1+1/n,3-1/n\},\leq\>} , gdzie $\le$ jest w obu wypadkach standardowym porządkiem liczb wymiernych, są elementarnie równoważne.

Wywnioskować stąd, że pojęcie dobrego porządku nie jest wyrażalne w logice pierwszego rzędu. Zupełnie inny dowód tego faktu poznamy w Rozdziale #zwarciig\leftrightarrowwi.

1. Niech $R$ będzie jednoargumentowym symbolem relacyjnym.

Udowodnić, że klasa wszystkich takich struktur </math>\strA=\langle A,R\rangle</math>, że $|R|=|A-R|$, nie jest aksjomatyzowalna żadnym zbiorem zdań pierwszego rzędu.

1. Udowodnić, że klasa wszystkich skończonych lub nieskończonych grafów

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA=\langle A,E\rangle,} w których istnieją dwa wierzchołki o równych sobie, skończonych stopniach, nie jest aksjomatyzowalna żadnym zdaniem pierwszego rzędu.

1. Udowodnić, że klasa wszystkich skończonych lub nieskończonych grafów

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA=\langle A,E\rangle,} których każdy skończony podgraf jest planarny, nie jest aksjomatyzowalna żadnym zdaniem pierwszego rzędu.

1. Pokazać, że klasa wszystkich relacji równoważności, których

wszystkie skończone klasy abstrakcji mają parzystą moc, nie jest aksjomatyzowalna żadnym zdaniem pierwszego rzędu.

Dane są dwie struktury relacyjne </math>\strA=\langle U,R^\strA\rangle</math> i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB=\langle U,R^\strB\rangle} nad sygnaturą złożoną z jednego dwuargumentowego symbolu relacyjnego. Ich nośnikiem jest $U=\{1,2,\dots ,15\}$, relacja Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle R^\strA x,y } zachodzi \wtw, gdy $x|y$, a relacja Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle R^\strB x,y } \wtw, gdy $x\equiv y(\mathrm{mod}2).$

Ustalić, jaką minimalną rangę kwantyfikatorową ma zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} takie, że Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\var\varphi} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\not\models\var\varphi.}

1. Dane są dwie sześcioelementowe

struktury relacyjne Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} nad sygnaturą złożoną z jednego dwuargumentowego symbolu relacyjnego. Struktury są narysowane poniżej jako grafy skierowane:

Parser nie mógł rozpoznać (nieznana funkcja „\begi”): {\displaystyle \begi\prooftree array \justifies c|c \using \textrm{ W }\endprooftree \xymatrix { *{\ast} \ar@{<->}[r] \ar@{<->}[d] \ar@{<->}[dr] & *{\ast} \ar@{<->}[d] \ar@{<->}[l] \ar@{<->}[dl] & *{\ast} & \\ *{\ast} \ar@{<->}[r] & *{\ast} & *{\ast} & *{\relax} }&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; \xymatrix { *{\ast} \ar@{<->}[d] \ar@{<->}[dr] & *{\ast} & *{\ast} & \\ *{\ast} \ar@{<->}[r] & *{\ast} & *{\ast} & *{\relax} } \end{array} }

Ustalić, jaką minimalną rangę kwantyfikatorową ma zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} takie, że Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\var\varphi} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\not\models\var\varphi.}

\end{small}