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 4.1

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=QRr(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 Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi.} Parametr ten ma następujące znaczenie: jeśli struktura $\mathfrak{𝔄}$ ma $n$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 „\var”): {\displaystyle \mathfrak A\models \var\varphi} jest asymptotycznie proporcjonalny do Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle n^{QR(\var\varphi )},} gdyuż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 $R(x,f(f(x)))$ jest atomowa i jej ranga kwantyfikatorowa powinna wynosić $0$. Tymczasem gdy $f$ będziemy reprezentować w strukturze jako dwuargumentową relację $F$, ta sama formuła przybierze postać $\mathrm{\exists }y\mathrm{\exists }zF(x,y)\wedge F(y,z)\wedge R(x,z)),$ 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ïssé

Definicja 4.2

Jeśli $\mathfrak{𝔄}$ jest strukturą relacyjną oraz $\mathrm{\varnothing }\ne B\subseteq A,$ to struktura ${\mathfrak{𝔄}}_{|B}$ tej samej sygnatury $\mathrm{\Sigma }$ co $\mathfrak{𝔄}$, nazywana podstrukturą indukowaną przez $B$ w $\mathfrak{𝔄},$ ma nośnik $B,$ zaś dla każdego $r\in {\mathrm{\Sigma }}_n^R$

$r^{{\mathfrak{𝔄}}_{|B}}=r^{\mathfrak{𝔄}}\cap B^n.$

Definicja 4.3

Niech $\mathfrak{𝔄},B$ będą 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 $h:{\mathfrak{𝔄}}_{|A^{\prime }}\cong {\mathfrak{𝔅}}_{|B^{\prime }},$ to mówimy, że $h$ jest częściowym izomorfizmem z $\mathfrak{𝔄}$ w $\mathfrak{𝔅}$. Jego dziedzina to $dom(h)=A^{\prime }$, a obraz to $rg(h)=B^{\prime }.$

Na zasadzie konwencjiumawiamy się, że $\mathrm{\varnothing }$ jest częściowym izomorfizmem z $\mathfrak{𝔄}$ w $\mathfrak{𝔅}$ o pustej dziedzinie i pustym obrazie.

Dla dwóch częściowych izomorfizmów $g,h$ z $\mathfrak{𝔄}$ w $\mathfrak{𝔅}$ piszemy $g\subseteq h$ gdy $dom(g)\subseteq dom(h)$ oraz $g(a)=h(a)$ dla wszystkich $a\in dom(g),$ to jest wtedy, gdy $g$ jest zawarte jako zbiór w $h.$

Definicja 4.4

Niech $m$ będzie dodatnią liczbą naturalną. Dwie struktury relacyjne tej samej sygnatury są $m$-izomorficzne, co oznaczamy $\mathfrak{𝔄}{\cong }_m\mathfrak{𝔅},$ gdy istnieje rodzina $\{I_n|n\le m\}$ w której każdy $I_n$ jest niepustym zbiorem częściowych izomorfizmów z $\mathfrak{𝔄}$ w $\mathfrak{𝔅},$ oraz spełniająca następujące dwa warunki:

• Tam Dla każdego $h\in I_{n+1}$ oraz każdego $a\in$ istnieje takie $g\in I_n$, że $h\subseteq g$ oraz $a\in dom(g).$
• 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 rg(g).$

Samą rodzinę $\{I_n|n\le m\}$ nazywamy wówczas $m$-izomorfizmem struktur $\mathfrak{𝔄}$ i $\mathfrak{𝔅}$, co oznaczamy $\{I_n|n\le m\}:\mathfrak{𝔄}{\cong }_m\mathfrak{𝔅}.$

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 4.5

Dwie struktury relacyjne tej samej sygnatury są skończenie izomorficzne, symbolicznie $\mathfrak{𝔄}{\cong }_{fin}\mathfrak{𝔅},$ gdy istnieje rodzina $\{I_n|n\in \omega \}$, taka, że każda podrodzina $\{I_n|n\le m\}$ jest $m$-izomorfizmem.

Jeśli $\{I_n|n\le m\}$ ma powyższe własności, to piszemy $\{I_n|n\le m\}:\mathfrak{𝔄}{\cong }_{fin}\mathfrak{𝔅}$, a samą rodzinę nazywamy skończonym izomorfizmem.

Fakt 4.6

• Jeśli $\mathfrak{𝔄}\cong \mathfrak{𝔅},$ to $\mathfrak{𝔄}{\cong }_{fin}\mathfrak{𝔅}.$
• Jeśli $\mathfrak{𝔄}{\cong }_{fin}\mathfrak{𝔅}$ oraz nośnik math>\mathfrak A</math> jest zbiorem skończonym, to $\mathfrak{𝔄}\cong \mathfrak{𝔅}.$

Dowód

Definicja 4.7

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

Dwie struktry $\mathfrak{𝔄}$ i $\mathfrak{𝔅}$ tej samej sygnatury są $m$-elementarnie równoważne, symbolicznie $\mathfrak{𝔄}{\equiv }_m\mathfrak{𝔅},$ 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 „\var”): {\displaystyle \mathfrak A\models\var\varphi} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak B\models\var\varphi.}

Fakt 4.8

$\mathfrak{𝔄}{\cong }_{f}in\mathfrak{𝔅}$ wtedy i tylko wtedy,gdy dla każdego naturalnego $m$ zachodzi $\mathfrak{𝔄}{\cong }_m\mathfrak{𝔅}$.

Dowód

Wynikanie z lewej do prawej jest oczywiste. Załóżmy teraz, że dla każdego $m$ istnieje rodzina $\{I_n^m|n\le m\}$ spełniająca warunki z definicji relacji ${\cong }_m.$ Rozważmy rodzinę Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{J_n&nbsp;|&nbsp;n\in\omega\},} gdzie $J_n=\bigcup _{m\in \omega }{I}_n^m.$ Bezpośrednie sprawdzenie pokazuje natychmiast, że spełnia ona warunki definicji relacji ${\cong }_{fin}.$

Twierdzenie 4.9

Niech $\mathrm{\Sigma }$ będzie dowolną sygnaturą relacyjną zawierającą skończenie wiele symboli, oraz niech $\mathfrak{𝔄},\mathfrak{𝔅}$ będą dowolnymi strukturami nad $\mathrm{\Sigma }.$

• Dla każdego $m\in \mathbb{\mathbb{N}}$ zachodzi równoważność: $\mathfrak{𝔄}{\cong }_m\mathfrak{𝔅}$ wtedy i tylko wtedy gdy $\mathfrak{𝔄}{\equiv }_m\mathfrak{𝔅}$.
• $\mathfrak{𝔄}{\cong }_{fin}\mathfrak{𝔅}$ wtedy i tylko wtedy gdy $\mathfrak{𝔄}\equiv \mathfrak{𝔅}$.

Dowód

Jest oczywiste, że druga równoważnośc wynika z pierwszej. Pierwszą z kolei udowodnimy tylko z lewej do prawej strony. Dowód w stronę przeciwną jest bardziej zawiły technicznie, a w dodatku ta \rightarrowlikacja jest rzadkouż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 pewnoudowodnić posługując się metodą Fraïssé, choć oczywiście nie ma gwarancji, że będzie to metoda najprostsza.

Ustalmy $m\in \mathbb{\mathbb{N}}$. Dowód tego, że z $\mathfrak{𝔄}{\cong }_m\mathfrak{𝔅}$ wynika $\mathfrak{𝔄}{\equiv }_m\mathfrak{𝔅}$ 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 | n\leq m\''} będzie rodziną o której mowa w definicji $\mathfrak{𝔄}{\cong }_m\mathfrak{𝔅}$, niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} będzie formułą o co najwyżej $r$ zmiennych wolnych (bezutraty ogólności niech będą to $x_1,\dots ,x_r$ ) i spełniającą Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle QR(\var\varphi )\leq n\leq m} oraz niech $g\in I_n.$ Wówczas dla dowolnych $a_1,\dots ,a_r\in dom(g)$ następujące dwa warunki są równoważne:

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A,x_1:a_1,\dots,x_r:a_r\models\var\varphi} Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak B,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:

• $\mathfrak{𝔄},x_1:a_1,\dots ,x_r:a_r\models \psi \to \xi$

• $\mathfrak{𝔄},x_1:a_1,\dots ,x_r:a_r\models ̸\psi$ lub

$\mathfrak{𝔄},x_1:a_1,\dots ,x_r:a_r\models \xi$

• $\mathfrak{𝔄},x_1:g(a_1),\dots ,x_r:g(a_r)\models ̸\psi$ lub

$\mathfrak{𝔄},x_1:g(a_1),\dots ,x_r:g(a_r)\models \xi$

• $\mathfrak{𝔄},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 bezutraty 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 „\var”): {\displaystyle QR(\var\varphi )\leq n} wynika, że $QR(\psi )\le n-1$. Mamy teraz następujący ciąg równoważnych warunków:

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

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

$(\mathfrak{𝔄},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 $gsbseteqh,$

$a\in dom(h)$ oraz

$(\mathfrak{𝔄},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 $gsbseteqh,$

$a\in dom(h)$ oraz

$(\mathfrak{𝔅},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

$gsbseteqh,$ $b\in rg(h)$ oraz

$(\mathfrak{𝔅},x_1:g(a_1),\dots ,x_r:g(a_r),x_{r+1}:b)\models \psi$

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

$(\mathfrak{𝔅},x_1:g(a_1),\dots ,x_r:g(a_r),x_{r+1}:b)\models \psi$

• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak B,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 $\mathfrak{𝔄},\mathfrak{𝔅}$ są dwoma skończonymi liniowymi porządkami o mocach większych niż $2^m,$ to $\mathfrak{𝔄}{\equiv }_m\mathfrak{𝔅}.$

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$\mathfrak A$w$\mathfrak BParser nie mógł rozpoznać (błąd składni): {\displaystyle takich, że } \{\langle 0,0\rangle,\langle N,M\rangle\}sbseteq g</math> oraz $d_k(a,b)=d_k(g(a),g(b))$ dla wszystkich $a,b\in dom(g).$ 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 $hspseteqg$ taki, że $a\in dom(h).$

Rozróżniamy dwa przypadki:

(i ) Jeśli istnieje takie $b\in dom(g)$, że $d_k(a,b)<\mathrm{\infty }$, to w $B$ jest dokładnie jedenelement $a^{\prime }$, który jest tak samo położony względem $g(b)$ jak $a$ względem $b,$ oraz spełnia $d_j(a^{\prime },g(b))=d_j(a,b).$ Kładziemy wówczas $h(a):=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$elementami po lewej i po prawej, które należą do $dom(g).$ 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 $h(a):=b$uzyskujemy żą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średnimuż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 przyuż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 $\mathfrak{𝔄},\mathfrak{𝔅}$ będą strukturami sygnatury $\mathrm{\Sigma }.$

Dlauproszczenia zakładamy, że $A\cap B=\mathrm{\varnothing }.$ \bigbreak

Definicja

{{{3}}}

Definicja powyższa dopuszcza powtarzanie ruchów przez obu graczy, czyli wybieranieelementów, które poprzednio były już wybrane. Jest to dogodne, gdyżupraszcza definicję. Gdybyśmy bowiem zakazali tego, to albo niemożliwe byłoby rozegranie gry $G_m(\mathfrak{𝔄},\mathfrak{𝔅})$ 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 $G_m(\mathfrak{𝔄},\mathfrak{𝔅})$ wtedy i tylko

wtedy, gdy $\mathfrak{𝔄}{\cong }_m\mathfrak{𝔅}.$

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

$G_m(\mathfrak{𝔄},\mathfrak{𝔅})$ wtedy i tylko wtedy, gdy $\mathfrak{𝔄}{\cong }_{fin}\mathfrak{𝔅}.$

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 $G_m(\mathfrak{𝔄},\mathfrak{𝔅}).$ 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 ${\le }^{\mathfrak{𝔄}}$ oraz ${\le }^{\mathfrak{𝔅}}$ prowadzą do identycznych ciągów indeksów swoich oznaczeń. Dokładnie, jeśli $a_{i_1}{<}^{\mathfrak{𝔄}}{a}_{i_2}{<}^{\mathfrak{𝔄}}\dots {<}^{\mathfrak{𝔄}}{a}_{i_k}$ i $b_{j_1}{<}^{\mathfrak{𝔅}}{b}_{j_2}{<}^{\mathfrak{𝔅}}\dots {<}^{\mathfrak{𝔅}}{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 wybranychelementó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}<^\mathfrak A a_{i_2}<^\mathfrak A \dots<^\mathfrak A a_{i_k}</math> i $b_{i_1}{<}^{\mathfrak{𝔅}}{b}_{i_2}{<}^{\mathfrak{𝔅}}\dots {<}^{\mathfrak{𝔅}}{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 utraty ogólności założyć, że gracz I wybiera strukturę $\mathfrak{𝔄}$. Może symbolem $a_{k+1}$ oznaczyć:

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

wybieraelement mniejszy od $b_{i_1}$ w $\mathfrak{𝔅}$, który istnieje na mocy założenia, że w $\mathfrak{𝔅}$ nie maelementu najmniejszego. Widać, że nowe ciągi indeksów pozostaną równe.

• • Element większy od $a_{i_k}.$ Wówczas gracz II wybieraelement

większy od $b_{i_k}$ w $\mathfrak{𝔅}$, który istnieje na mocy założenia, że w $\mathfrak{𝔅}$ nie maelementu 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" style="font-variant:small-caps">Dowód

{{{3}}}

<^\mathfrak A a<^\mathfrak A

a_{i_{\ell+1}}</math> dla pewnego $\ell .$ W $\mathfrak{𝔅}$ istniejeelement $b$ spełniający $b_{i_{\ell }}{<}^{\mathfrak{𝔅}}b{<}^{\mathfrak{𝔅}}{b}_{i_{\ell +1}}$, gdyż $\mathfrak{𝔅}$ jest porządkiem gęstym. Gracz II wybiera takielement 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

\ \mathfrak A\models\var\varphi,\ \mbox{dla każdego\

\mathfrak A\in\K\}</math> (teoria klasy struktur Parser nie mógł rozpoznać (nieznana funkcja „\K”): {\displaystyle \K} ) albo Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle '''Th}(\mathfrak A )= \{\var\varphi\ |\ \mathfrak A\models\var\varphi\'''} (teoria modelu $\mathfrak{𝔄}$ ). 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 wustalonym modelu jest oczywiście zawsze teorią zupełną.

Wniosek

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

Dowód

{{{3}}}

sbsection*{Ć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 #qqudowodnić, ż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>\mathfrak A=\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

$\mathfrak{𝔄}=⟨A,E⟩,$ 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

$\mathfrak{𝔄}=⟨A,E⟩,$ 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>\mathfrak A=\langle U,R^\mathfrak A\rangle</math> i $\mathfrak{𝔅}=⟨U,R^{\mathfrak{𝔅}}⟩$ nad sygnaturą złożoną z jednego dwuargumentowego symbolu relacyjnego. Ich nośnikiem jest $U=\{1,2,\dots ,15\}$, relacja $R^{\mathfrak{𝔄}}(x,y)$ zachodzi \wtw, gdy $x|y$, a relacja $R^{\mathfrak{𝔅}}(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 „\var”): {\displaystyle \mathfrak A\models\var\varphi} i Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak B\not\models\var\varphi.}

1. Dane są dwie sześcioelementowe

struktury relacyjne $\mathfrak{𝔄}$ i $\mathfrak{𝔅}$ 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 „\var”): {\displaystyle \mathfrak A\models\var\varphi} i Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak B\not\models\var\varphi.}

\end{small}