Logika dla informatyków/Ograniczenia logiki pierwszego rzędu: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
Linia 9: | Linia 9: | ||
{{definicja||| | {{definicja||| | ||
Rangę kwantyfikatorową | |||
<math>\QR\begin{eqnarray*}\var\varphi\end{eqnarray*}</math> formuły <math>\var\varphi</math>definiujemy jak następuje: | |||
Wersja z 10:15, 22 wrz 2006
Linek z wykladu 8 do tw. 4.13. Nazwa linku "Cantoro"
Ten rozdział poświęcony jest ograniczeniom, którym podlega języklogiki pierwszego rzędu. Okazuje się, że nie każde pojęcie da się wnim wyrazić, a także, że są pojęcia, które dają się wyrazić, aleodpowiednie zdanie lub formuła z konieczności musi byćskomplikowane. Rozważania w tym rozdziale będziemy prowadzić przyzałożeniu, że w sygnaturze występują wyłącznie symbole relacyjne.Wyniki dają się zastosować do sygnatur z symbolami funkcyjnymi, alewymaga to zakodowania wszystkich funkcji jako relacji.
Zaczniemy od miary skomplikowania formuł, która będzie przydatna wdalszym ciągu.
Definicja
Rangę kwantyfikatorową Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR\begin{eqnarray*}\var\varphi\end{eqnarray*}} formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} definiujemy jak następuje:
- Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR\begin{eqnarray*}\bot\end{eqnarray*}=\QR\begin{eqnarray*}t_1=t_2\end{eqnarray*}=\QR\begin{eqnarray*}r\begin{eqnarray*}t_1,\dots,t_k\end{eqnarray*}\end{eqnarray*}=0} dla dowolnychtermów oraz
- Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR\begin{eqnarray*}\var\varphi\to \psi\end{eqnarray*}=\max\begin{eqnarray*}\QR\begin{eqnarray*}\var\varphi\end{eqnarray*},\QR\begin{eqnarray*}\psi\end{eqnarray*}\end{eqnarray*}} .
- Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR\begin{eqnarray*}\forall x\var\varphi\end{eqnarray*}=1+\QR\begin{eqnarray*}\var\varphi\end{eqnarray*}.}
Intuicyjnie Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR} to głębokość zagnieżdżenia kwantyfikatorów wformule. Jest to jedna z wielu możliwych miar stopnia komplikacjiformuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi.} Parametr ten ma następujące znaczenie: jeślistruktura Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} ma \Delta\vdashlementó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} jestasymptotycznie proporcjonalny do Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle n^{\QR\begin{eqnarray*}\var\varphi\end{eqnarray*}},} gdy\boldsymbol{s}}\def\blank{\hbox{\sf Bżyjemynaturalnego algorytmu do wykonania tego zadania, który dla każdegokwantyfikatora w formule przegląda wszystkie\Delta\vdashlementy struktury.
Teraz możemy wyjaśnić, dlaczego nie dopuszczamy symboli funkcyjnych wsygnaturze. Otóż ich obecność zakłóca potrzebne nam własności funkcji Tytułem przykładu, formuła Parser nie mógł rozpoznać (błąd składni): {\displaystyle R\begin{eqnarray*}x,f\begin{eqnarray*}f\begin{eqnarray*}x\end{eqnarray*}\end{eqnarray*}\end{eqnarray*}} jest atomowa ijej ranga kwantyfikatorowa powinna wynosić . Tymczasemgdy 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\begin{eqnarray*}F\begin{eqnarray*}x,y\end{eqnarray*}\land F\begin{eqnarray*}y,z\end{eqnarray*}\land R\begin{eqnarray*}x,z\end{eqnarray*}\end{eqnarray*},</math> której ranga kwantyfikatorowawynosi 2. Twierdzenia, których dalej dowodzimy, odwołują się dowartości zdefiniowanych powyżej dla logiki bez symbolifunkcyjnych. \Rightarrow właśnie jest przyczyna, dla której funkcje wykluczamyz rozważań.
Definicja
=r^\strA\cap B^n.\]}}
Definicja
\def\blank{\hbox{\sf Bmawiamy się, że
jest częściowymizomorfizmem 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 z Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} piszemy gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle dom\begin{eqnarray*}g\end{eqnarray*}\subseteq dom\begin{eqnarray*}h\end{eqnarray*}} oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle g\begin{eqnarray*}a\end{eqnarray*}=h\begin{eqnarray*}a\end{eqnarray*}} dlawszystkich Parser nie mógł rozpoznać (błąd składni): {\displaystyle a\in dom\begin{eqnarray*}g\end{eqnarray*},} to jest wtedy, gdy jest zawarte jakozbiór w }}
Definicja
naturalną. Dwie struktury relacyjne tej samej sygnatury są\textit{-izomorficzne}, co oznaczamy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{m}\strB,} gdy istniejerodzina Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_n | n\leq m\}} w której każdy jest niepustym zbioremczęś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ącanastępujące dwa warunki:
\begin{description}\item[Tam] Dla każdego oraz każdego istnieje takie, że oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle a\in dom\begin{eqnarray*}g\end{eqnarray*}.} \item[Z powrotem] Dla każdego oraz każdego istnieje takie , że oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle b\in rg\begin{eqnarray*}g\end{eqnarray*}.} \end{description}
Samą rodzinę Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_n | n\leq m\}} nazywamy wówczas\textit{-izomorfizmem} struktur Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} , co oznaczamyParser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_n | n\leq m\}:\strA\cong_m\strB.}
Nieformalne wyjaśnienie jest takie: to zbiór częściowychizomorfizmów, które mogą być rozszerzone -krotnie o dowolneelementy w dziedzinie i obrazie, a kolejne rozszerzenia leżą w
Definicja
\rm
Dwie struktury relacyjne tej samej sygnatury są \textit{skończenieizomorficzne}, symbolicznie Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{fin}\strB,} gdy istniejerodzina </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} jestzbiorem skończonym, to Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong\strB.}
Dowód
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{elementarnierównoważne}, co zapisujemy symbolicznie Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\equiv\strB,} gdy dlakaż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{-elementarnie równoważne}, symbolicznieParser 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} logikipierwszego rzędu nad tą samą sygnaturą, o randze kwantyfikatorowej nieprzekraczającej , zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\var\varphi} wtedy i tylkowtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\models\var\varphi.}Fakt
Dowód
Twierdzenie
Niech 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ą dowolnymistrukturami nad
- Dla każdego 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 gdyParser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\equiv\strB} .
Dowód
\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 \rightarrowlikacjajest rzadko\boldsymbol{s}}\def\blank{\hbox{\sf Bżywana w praktyce. Wyraża za to istotną zmetodologicznego punktu widzenia informację: jeśli dwie struktury są\begin{eqnarray*}
-\end{eqnarray*}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 magwarancji, że będzie to metoda najprostsza.
Ustalmy . Dowód tego, że z Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_m\strB} wynikaParser 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 | n\leq m\''} będzie rodziną o której mowa w definicjiParser 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 zmiennych wolnych \begin{eqnarray*}bez\boldsymbol{s}}\def\blank{\hbox{\sf Btraty ogólności niech będą to \end{eqnarray*}i spełniającą Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR\begin{eqnarray*}\var\varphi\end{eqnarray*}\leq n\leq m} oraz niech Wówczas dla dowolnych Parser nie mógł rozpoznać (błąd składni): {\displaystyle a_1,\dots,a_r\in dom\begin{eqnarray*}g\end{eqnarray*}} następujące dwawarunki są równoważne:}\[\strA,x_1:a_1,\dots,x_r:a_r\models\var\varphi\]\[\strB,x_1:g\begin{eqnarray*}a_1\end{eqnarray*},\dots,x_r:g\begin{eqnarray*}a_r\end{eqnarray*}\models\var\varphi.\]\end{quote}
Dla formuł atomowych, powyższa teza wynika wprost z faktu, że jestczęściowym izomorfizmem \begin{eqnarray*}przypomnijmy że w sygnaturze nie ma symbolifunkcyjnych i co za tym idzie jedynymi termami są zmienne\end{eqnarray*}.
Gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ma postać to mamy następujący ciągró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} lubParser 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\begin{eqnarray*}a_1\end{eqnarray*},\dots,x_r:g\begin{eqnarray*}a_r\end{eqnarray*}\not\models\psi} lub Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:g\begin{eqnarray*}a_1\end{eqnarray*},\dots,x_r:g\begin{eqnarray*}a_r\end{eqnarray*}\models\xi}
- Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,x_1:g\begin{eqnarray*}a_1\end{eqnarray*},\dots,x_r:g\begin{eqnarray*}a_r\end{eqnarray*}\models\psi\to\xi,}
przy czym druga równoważność wynika z założenia indukcyjnego, apierwsza 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}\notinFV\begin{eqnarray*}\var\varphi\end{eqnarray*}\models \begin{eqnarray*}\forall x\psi\end{eqnarray*}\leftrightarrow \forall x_{r+1} \psi\begin{eqnarray*}x_{r+1}/x\end{eqnarray*}</math> \begin{eqnarray*}patrz Fakt#alfa-konw\end{eqnarray*}, 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} mapostać Z założenia Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR\begin{eqnarray*}\var\varphi\end{eqnarray*}\leq n} wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\QR”): {\displaystyle \QR\begin{eqnarray*}\psi\end{eqnarray*}\leq n-1} . Mamy teraz następujący ciągrównoważnych warunków:
- Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\strA,x_1:a_1,\dots,x_r:a_r\end{eqnarray*}\models\var\varphi}
- Dla każdego zachodziParser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\strA,x_1:a_1,\dots,x_r:a_r,x_{r+1}:a\end{eqnarray*}\models\psi}
- Dla każdego istnieje takie , że Parser nie mógł rozpoznać (błąd składni): {\displaystyle a\in dom\begin{eqnarray*}h\end{eqnarray*}} oraz
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\strA,x_1:a_1,\dots,x_r:a_r,x_{r+1}:a\end{eqnarray*}\models\psi}
- Dla każdego istnieje takie , że Parser nie mógł rozpoznać (błąd składni): {\displaystyle a\in dom\begin{eqnarray*}h\end{eqnarray*}} oraz
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\strB,x_1:g\begin{eqnarray*}a_1\end{eqnarray*},\dots,x_r:g\begin{eqnarray*}a_r\end{eqnarray*},x_{r+1}:h\begin{eqnarray*}a\end{eqnarray*}\end{eqnarray*}\models\psi}
- Dla każdego istnieje takie , że Parser nie mógł rozpoznać (błąd składni): {\displaystyle b\in rg\begin{eqnarray*}h\end{eqnarray*}} oraz
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\strB,x_1:g\begin{eqnarray*}a_1\end{eqnarray*},\dots,x_r:g\begin{eqnarray*}a_r\end{eqnarray*},x_{r+1}:b\end{eqnarray*}\models\psi}
- Dla każdego zachodzi Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\strB,x_1:g\begin{eqnarray*}a_1\end{eqnarray*},\dots,x_r:g\begin{eqnarray*}a_r\end{eqnarray*},x_{r+1}:b\end{eqnarray*}\models\psi}
- Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\strB,x_1:g\begin{eqnarray*}a_1\end{eqnarray*},\dots,x_r:g\begin{eqnarray*}a_r\end{eqnarray*}\end{eqnarray*}\models\var\varphi.}
Równoważności druga i czwarta zachodzą na mocy warunków Tam iZ powrotem, trzecia na mocy założenia indukcyjnego, a pozostałena mocy definicji spełniania.}}
Pokażemy teraz pierwszy przykład inherentnego ograniczenia logikipierwszego rzędu.
Fakt
Dowód
Niech dla będzie zbiorem wszystkich częściowychizomorfizmów </math>g\strA\strBParser nie mógł rozpoznać (błąd składni): {\displaystyle takich, że } \{\langle0,0\rangle,\langle N,M\rangle\}\subseteq g</math> orazParser nie mógł rozpoznać (błąd składni): {\displaystyle d_k\begin{eqnarray*}a,b\end{eqnarray*}=d_k\begin{eqnarray*}g\begin{eqnarray*}a\end{eqnarray*},g\begin{eqnarray*}b\end{eqnarray*}\end{eqnarray*}} dla wszystkich Parser nie mógł rozpoznać (błąd składni): {\displaystyle a,b\in dom\begin{eqnarray*}g\end{eqnarray*}.} Oczywiście</math>I_k\neq \emptyset\{\langle 0,0\rangle,\langleN,M\rangle\}\in I_k.</math>
Pokazujemy własność Tam} dla rodziny Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{I_k | k\leq m\'''} . Niech Niech Mamy wskazać w częściowy izomorfizm taki, że Parser nie mógł rozpoznać (błąd składni): {\displaystyle a\in dom\begin{eqnarray*}h\end{eqnarray*}.}
Rozróżniamy dwa przypadki:
\begin{eqnarray*}i\end{eqnarray*} Jeśli istnieje takie Parser nie mógł rozpoznać (błąd składni): {\displaystyle b\in dom\begin{eqnarray*}g\end{eqnarray*}} , że Parser nie mógł rozpoznać (błąd składni): {\displaystyle d_{k}\begin{eqnarray*}a,b\end{eqnarray*}<\infty} , to w jest dokładnie jeden\Delta\vdashlement , który jest tak samo położonywzględem Parser nie mógł rozpoznać (błąd składni): {\displaystyle g\begin{eqnarray*}b\end{eqnarray*}} jak względem oraz spełniaParser nie mógł rozpoznać (błąd składni): {\displaystyle d_j\begin{eqnarray*}a',g\begin{eqnarray*}b\end{eqnarray*}\end{eqnarray*}=d_{j}\begin{eqnarray*}a,b\end{eqnarray*}.} Kładziemy wówczas Parser nie mógł rozpoznać (błąd składni): {\displaystyle h\begin{eqnarray*}a\end{eqnarray*}:=a'} i jestwtedy częściowym izomorfizmem zachowującym odległości
\begin{eqnarray*}ii\end{eqnarray*} Jeśli natomiast takiego nie ma, to niech gdzie są najbliższymi \Delta\vdashlementami po lewej i po prawej, którenależą do Parser nie mógł rozpoznać (błąd składni): {\displaystyle dom\begin{eqnarray*}g\end{eqnarray*}.} Wówczas Parser nie mógł rozpoznać (błąd składni): {\displaystyle d_j\begin{eqnarray*}a',a\end{eqnarray*}=d_j\begin{eqnarray*}a,a''\end{eqnarray*}=\infty,} co w myśldefinicji oznacza, że Parser nie mógł rozpoznać (błąd składni): {\displaystyle d_{j+1}\begin{eqnarray*}a',a''\end{eqnarray*}=\infty.} Zatem na mocyzałożenia indukcyjnego także Parser nie mógł rozpoznać (błąd składni): {\displaystyle d_{j+1}\begin{eqnarray*}g\begin{eqnarray*}a'\end{eqnarray*},g\begin{eqnarray*}a''\end{eqnarray*}\end{eqnarray*}=\infty.} Istniejewięc Parser nie mógł rozpoznać (błąd składni): {\displaystyle g\begin{eqnarray*}a'\end{eqnarray*}<b<g\begin{eqnarray*}a''\end{eqnarray*}} takie, że \mbox{Parser nie mógł rozpoznać (błąd składni): {\displaystyle d_j\begin{eqnarray*}g\begin{eqnarray*}a'\end{eqnarray*},b\end{eqnarray*}=d_j\begin{eqnarray*}b,g\begin{eqnarray*}a''\end{eqnarray*}\end{eqnarray*}=\infty} }, i wówczas kładąc Parser nie mógł rozpoznać (błąd składni): {\displaystyle h\begin{eqnarray*}a\end{eqnarray*}:=b} \boldsymbol{s
\def\blank{\hbox{\sf Bzyskujemy żądane rozszerzenie.}}
Przykład powyższy wskazuje na kilka istotnych ograniczeń logikipierwszego rzędu. Po pierwsze, nie da się żadnym zdaniem zdefiniowaćnawet tak prostego pojęcia jak ,,porządek liniowy o parzystej liczbieelementów, i to bez względu na to, jak byśmy je rozumieli dla modelinieskończonych. Istotnie, zdanie które miałoby definiować takąwłasność musiałoby mieć jakąś rangę kwantyfikatorową, powiedzmy. Jednak w myśl poprzedniego twierdzenia, porządki o mocach i są -elementarnie równoważne i nasze hipotetyczne zdaniejest albo prawdziwe w obu, albo fałszywe w obu, podczas gdy powinnobyć w jednym fałszywe, a w drugim prawdziwe.
Drugim ograniczeniem jest fakt, że każda specyfikacja porządkuliniowego o mocy w logice pierwszego rzędu musi z koniecznościmieć rangę kwantyfikatorową co najmniej a więc sugerujealgorytm sprawdzenia, czy dany obiekt mocy istotnie spełnia tęspecyfikację, którego czas działania ma rząd wielkości co jest wynikiem fatalnym.\footnote{Na szczęście znamy lepszealgorytmy wykonujące to zadanie.} Bierze się to stąd, że prawdziwośćzdania o randze kwantyfikatorowej sprawdza się w danej skończonejstrukturze za pomocą zagnieżdżonych pętli, z których każdaprzegląda cały nośnik struktury i odpowiada jednemukwantyfikatorowi.
Charakteryzacja Fra\"{\i}ss\'e jest dość skomplikowana i odpychająca wbezpośrednim\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciu. W praktyce jej popularność ogromnie zwiększyłopodanie przez Andrzeja Ehrenfeuchta jej równoważnego opisu w terminachdwuosobowej gry, którą teraz zdefiniujemy. Gra ta doskonale sprawdzasię 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 duchuFra\"{\i}ss\'e.
Niech będzie sygnaturą relacyjną i niech Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA,\strB} będąstrukturami sygnatury
Dla\boldsymbol{s}}\def\blank{\hbox{\sf Bproszczenia zakładamy, że \bigbreak
Definicja
Definicja powyższa dopuszcza powtarzanie ruchów przez obu graczy, czyliwybieranie\Delta\vdashlementów, które poprzednio były już wybrane. Jest todogodne, 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ć (błąd składni): {\displaystyle G_m\begin{eqnarray*}\strA,\strB\end{eqnarray*}} gdy choćjedna ze struktur ma moc mniejszą niż albo trzeba by byłowprowadzić w definicji specjalny warunek służący do rozstrzyganiazwycięstwa w sytuacjach, gdy brak możliwości dalszych ruchów.
W praktyce jednak w dowodach prawie nigdy nie rozpatruje się takichruchów, gdyż jest oczywiste, że wykonanie takiego posunięcia przezgracza I nie przybliża go do zwycięstwa, zaś gdy wykona je gracz IImimo ż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ć (błąd składni): {\displaystyle G_m\begin{eqnarray*}\strA,\strB\end{eqnarray*}} wtedy i tylkowtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{m}\strB.}
- Gracz II ma dla każdego strategię wygrywającą w grzeParser nie mógł rozpoznać (błąd składni): {\displaystyle G_m\begin{eqnarray*}\strA,\strB\end{eqnarray*}} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\cong_{fin}\strB.}
Dowód
Poniższe twierdzenie ilustruje, w jaki sposób gra może zostaćwykorzystana dla wskazania ograniczeń możliwości logiki pierwszegorzędu.
Twierdzenie
<span id="
W myśl Twierdzenia #ehrenfeucht należy pokazać, że dla każdego gracz II ma strategię wygrywającą w grze Parser nie mógł rozpoznać (błąd składni): {\displaystyle G_m\begin{eqnarray*}\strA,\strB\end{eqnarray*}.} Opiszemy teraz tę strategię. Jej postać nie zależy od liczby rund dorozegrania. Pokażemy też, że jeśli po zakończeniu poprzedniej rundywarunek wygrywający dla gracza II był spełniony, to po wykonaniu ruchuzgodnie ze wskazaną strategią pozostanie on nadal spełniony. Wówczasna mocy zasady indukcji po rozegraniu dowolnej ilości rund, w którychgracz II będzie się stosował do tej strategii, pozostanie onzwycięzcą.
Zauważmy, że warunek o częściowym izomorfizmie w naszej sytuacjioznacza tyle, że zbiory i elementów wybranych w każdej ze struktur, po posortowaniu rosnącozgodnie 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}} iParser 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 dla
- Na pierwszy ruch gracza I gracz II odpowiada w dowolny sposób.
Przed tą rundą nie było wybranych\Delta\vdashlementów, czyli przekształcenieopisane w definicji gry było przekształceniem pustym, które na mocykonwencji jest częściowym izomorfizmem. Po wykonaniu ruchu zgodnie zestrategią ciągi indeksów w obu strukturach są oczywiście identyczne.
- We wszystkich kolejnych rundach gracz II określa swój ruchnastępująco. Niech </math>a_{i_1}<^\strA a_{i_2}<^\strA \dots<^\strAa_{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ą\begin{eqnarray*}identycznymi na mocy założenia indukcyjnego\end{eqnarray*} ciągami indeksów przedwykonaniem tego ruchu. Ze względu na symetrię sytuacji, możemy bezutraty ogólności założyć, że gracz I wybiera strukturę Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA}
. Możesymbolem oznaczyć:
- Element mniejszy od Wówczas gracz IIwybiera\Delta\vdashlement mniejszy od w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} , który istnieje na mocyzałożenia, że w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} nie ma\Delta\vdashlementu najmniejszego. Widać, że noweciągi indeksów pozostaną równe.
- Element większy od Wówczas gracz II wybiera\Delta\vdashlementwiększy od w Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} , który istnieje na mocy założenia, że wParser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} nie ma\Delta\vdashlementu ostatniego. Widać, że także teraz nowe ciągiindeksó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
<^\strA a<^\strAa_{i_{\ell+1}}</math> dla pewnego
W Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} istnieje\Delta\vdashlement
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 iró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 jestzakończony.}}
Z powyższego wynika między innymi, że </math>\langle\mathbb{R},\leq\rangle\equiv\langle \mathbb{Q},\leq\rangle.</math> Zatem niema zdania logiki pierwszego rzędu, które definiuje pojęcie porządkuciągłego \begin{eqnarray*}tzn. takiego, w którym wszystkie niepuste ograniczonepodzbiory mają kres górny i kres dolny\end{eqnarray*}, bo musiałoby ono być prawdziwew pierwszej ze struktur, a fałszywe w drugiej.
Definicja
\def\blank{\hbox{\sf Bstalonym modelu jest oczywiście zawsze teorią zupełną.}}
Wniosek
Dowód
\subsection*{Ćwiczenia}\begin{small}
- Wykazać, że dla dostatecznie dużych istnieje zdanie o randzekwantyfikatorowej definiujące porządek liniowy o mocy
- Adaptując dowód Faktu #qq\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić, że strukturyParser nie mógł rozpoznać (błąd składni): {\displaystyle \<\{1-1/n | n=1,2,\dots\},\leq\>} orazParser nie mógł rozpoznać (błąd składni): {\displaystyle \<\bigcup_{n=1}^\infty\{1-1/n,1+1/n,3-1/n\},\leq\>} , gdzie jestw 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. \begin{eqnarray*}Zupełnie inny dowód tego faktu poznamy w Rozdziale #zwarciig\leftrightarrowwi.\end{eqnarray*}
- Niech będzie jednoargumentowym symbolem relacyjnym.Udowodnić, że klasa wszystkich takich struktur </math>\strA=\langleA,R\rangle</math>, że , nie jest aksjomatyzowalna żadnym zbioremzdań pierwszego rzędu.
- Udowodnić, że klasa wszystkich \begin{eqnarray*}skończonych lub nieskończonych\end{eqnarray*} grafów Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA=\langle A,E\rangle,} w których istnieją dwawierzchołki o równych sobie, skończonych stopniach, nie jestaksjomatyzowalna żadnym zdaniem pierwszego rzędu.
- Udowodnić, że klasa wszystkich \begin{eqnarray*}skończonych lub nieskończonych\end{eqnarray*} grafówParser 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.
- Pokazać, że klasa wszystkich relacji równoważności, którychwszystkie skończone klasy abstrakcji mają parzystą moc, nie jestaksjomatyzowalna żadnym zdaniem pierwszego rzędu.
- Dane są dwie struktury relacyjne </math>\strA=\langleU,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 symbolurelacyjnego. Ich nośnikiem jest, relacja Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle R^\strA\begin{eqnarray*}x,y\end{eqnarray*}} zachodzi \wtw, gdy, a relacja Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle R^\strB\begin{eqnarray*}x,y\end{eqnarray*}} \wtw, gdy
Ustalić, jaką minimalną rangę kwantyfikatorową ma zdanieParser 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.}
- Dane są dwie sześcioelementowestruktury 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{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree \xymatrix{*{\ast}\ar@{<->}[r]\ar@{<->}[d]\ar@{<->}[dr]&*{\ast}\ar@{<->}[d]\ar@{<->}[l]\ar@{<->}[dl]&*{\ast}&\\*{\ast}\ar@{<->}[r]&*{\ast}&*{\ast}&*{\relax}} & \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}