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:

• Parser nie mógł rozpoznać (nieznana funkcja „\QRt”): {\displaystyle QR\bot=\QRt_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 „\QR”): {\displaystyle \QR(\var\varphi\to \psi )=\max(\QR(\var\varphi ),\QR(\psi ) )} .
• Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR(\forall x\var\varphi )=1+\QR(\var\varphi ).}

Intuicyjnie Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \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 „\QR”): {\displaystyle n^{\QR(\var\varphi )},} gdyużyjemy naturalnego algorytmu do wykonania tego zadania, który dla każdego kwantyfikatora w formule przegląda wszystkieelementy 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ę </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. \Rightarrow właśnie jest przyczyna, dla której funkcje wykluczamy z rozważań.

Charakteryzacja Fra\"{\i

Definicja

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

\[r^{\mathfrak A_{

=r^\mathfrak A\cap B^n.\]

}}

Definicja

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

izomorfizmem podstruktur indukowanych </math>h:\mathfrak A_{

Definicja

naturalną. Dwie struktury relacyjne tej samej sygnatury są \textit{$m$-izomorficzne}, co oznaczamy Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \mathfrak A\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 $\mathfrak{𝔄}$ 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 $hsbseteqg$ oraz $a\in dom(g).$ \item[Z powrotem] Dla każdego $h\in I_{n+1}$ oraz każdego $b\in B$ istnieje takie $g\in I_n$, że $hsbseteqg$ oraz $b\in rg(g).$ \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 $\mathfrak{𝔄}$ 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\}:\mathfrak A\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 „\strB”): {\displaystyle \mathfrak A\cong_{fin}\strB,} gdy istnieje

rodzina </math>\{I_n 

Fakt

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

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

Dowód

{{{3}}}

Definicja

$\mathfrak{𝔄}$ 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 „\strB”): {\displaystyle \mathfrak A\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 „\var”): {\displaystyle \mathfrak A\models\var\varphi} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\models\var\varphi.}

Dwie struktry $\mathfrak{𝔄}$ 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 „\strB”): {\displaystyle \mathfrak A\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 „\var”): {\displaystyle \mathfrak A\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 „\strB”): {\displaystyle \mathfrak A\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 „\strB”): {\displaystyle \mathfrak A,\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 „\strB”): {\displaystyle \mathfrak A\cong_m\strB}

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

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

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

<span id="

Jest oczywiste, że druga równoważnośc wynika z pierwszej. Pierwszą z koleiudowodnimy 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\"{\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 „\strB”): {\displaystyle \mathfrak A\cong_m\strB} wynika Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \mathfrak A\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 „\strB”): {\displaystyle \mathfrak A\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 (bezutraty 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 dom(g)$ następujące dwa warunki są równoważne:} \[\mathfrak A,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:

• $\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 „\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 „\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

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

$gsbseteqh,$ $b\in rg(h)$ 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. " style="font-variant:small-caps">Dowód

{{{3}}}

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

Fakt

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \mathfrak A,\strB} są dwoma skończonymi liniowymi porządkami o mocach większych niż $2^m,$ to Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \mathfrak A\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$\mathfrak A$w$\strBParser 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 Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \mathfrak A,\strB} 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 Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle G_m(\mathfrak A,\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 „\strB”): {\displaystyle G_m(\mathfrak A,\strB )} wtedy i tylko

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

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

Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle G_m(\mathfrak A,\strB )} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \mathfrak A\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 „\strB”): {\displaystyle G_m(\mathfrak A,\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 ${\le }^{\mathfrak{𝔄}}$ 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 $a_{i_1}{<}^{\mathfrak{𝔄}}{a}_{i_2}{<}^{\mathfrak{𝔄}}\dots {<}^{\mathfrak{𝔄}}{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 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 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 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 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 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 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 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 Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} istniejeelement $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 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 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 $R^{\mathfrak{𝔄}}(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 „\var”): {\displaystyle \mathfrak A\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 $\mathfrak{𝔄}$ 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 „\var”): {\displaystyle \mathfrak A\models\var\varphi} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\not\models\var\varphi.}

\end{small}